AcceptedLemma · Statement with omitted proof

Best approximation by a finite orthonormal system

The finite Fourier expansion minimizes the distance to the span of an orthonormal family.

Larsson & Thomée ↗
Lemma 6.1 · printed p. 82

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

The finite Fourier expansion minimizes the distance to the span of an orthonormal family.

\Bigl\|v-\sum_{j=1}^{N}(v,\varphi_j)\varphi_j\Bigr\|=\min_{c_1,\ldots,c_N}\Bigl\|v-\sum_{j=1}^{N}c_j\varphi_j\Bigr\|.

Assumptions & context

A complete real or complex inner-product space and a finite orthonormal system.

Source

Larsson & Thomée. Partial differential equations with numerical methods.

Lemma 6.1 · printed p. 82

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem lem_6_1 {𝕜 : Type*} [RCLike 𝕜] {H : Type*}
    [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H]
    (φ : ℕ → H) (hφ : Orthonormal 𝕜 (fun j : Set.Ici (1 : ℕ) => φ j))
    (N : ℕ) (v : H) :
    IsBestApproximation (𝕜 := 𝕜) φ N v (partialFourierSum (𝕜 := 𝕜) φ N v) := by
  sorry

Complete Lean file and local definitions

import PDETextbook.Base

open MeasureTheory
open scoped BigOperators ENNReal

noncomputable section

namespace PDETextbook.LarssonThomee.Lem61

/-- The book's partial Fourier sum `v_N = ∑_{j=1}^N (v, φ_j) φ_j`.
The book's scalar product `(v, φ_j)` is linear in its FIRST argument;
in Mathlib's convention (conjugate-linear in the first argument) it is `⟪φ_j, v⟫`. -/
def partialFourierSum {𝕜 : Type*} [RCLike 𝕜] {H : Type*}
    [NormedAddCommGroup H] [InnerProductSpace 𝕜 H]
    (φ : ℕ → H) (N : ℕ) (v : H) : H :=
  ∑ j ∈ Finset.Icc 1 N, (inner 𝕜 (φ j) v) • φ j

/-- A linear combination `∑_{j=1}^N c_j φ_j` of the first `N` functions `φ_j`. -/
def linComb {𝕜 : Type*} [RCLike 𝕜] {H : Type*}
    [NormedAddCommGroup H] [InnerProductSpace 𝕜 H]
    (φ : ℕ → H) (N : ℕ) (c : ℕ → 𝕜) : H :=
  ∑ j ∈ Finset.Icc 1 N, c j • φ j

/-- `w` is the best approximation of `v` among linear combinations of `φ_1, …, φ_N`:
`w` is such a linear combination, it minimizes `‖v - ·‖` over all of them, and it is the
unique minimizer ("the" best approximation). -/
def IsBestApproximation {𝕜 : Type*} [RCLike 𝕜] {H : Type*}
    [NormedAddCommGroup H] [InnerProductSpace 𝕜 H]
    (φ : ℕ → H) (N : ℕ) (v w : H) : Prop :=
  (∃ c : ℕ → 𝕜, w = linComb φ N c) ∧
  (∀ c : ℕ → 𝕜, ‖v - w‖ ≤ ‖v - linComb φ N c‖) ∧
  (∀ c : ℕ → 𝕜, ‖v - linComb φ N c‖ ≤ ‖v - w‖ → linComb φ N c = w)

/-- Lemma 6.1 (Larsson–Thomée). Let `{φ_j}_{j=1}^∞` be an orthonormal set in the Hilbert
space `H`. Then the best approximation of `v ∈ H` by a linear combination of the first `N`
functions `φ_j` is `v_N = ∑_{j=1}^N (v, φ_j) φ_j`. -/
theorem lem_6_1 {𝕜 : Type*} [RCLike 𝕜] {H : Type*}
    [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H]
    (φ : ℕ → H) (hφ : Orthonormal 𝕜 (fun j : Set.Ici (1 : ℕ) => φ j))
    (N : ℕ) (v : H) :
    IsBestApproximation (𝕜 := 𝕜) φ N v (partialFourierSum (𝕜 := 𝕜) φ N v) := by
  sorry

end PDETextbook.LarssonThomee.Lem61

How to read the formalization

The projection coefficients follow the inner-product convention in the complete Lean file.

← Back to all statements