Lemma 3.14: Approximation error bound for truncated Fourier series

of Sobolev functions (book lines 2429–2461).

The book works with infinite sequences θ ∈ ℓ₂(ℕ) belonging to the Sobolev ellipsoid Θ(β, Q) = {θ ∈ ℓ₂(ℕ) : Σ_{j≥1} a_j² θ_j² ≤ Q}, where a_j are the Sobolev coefficients from eq. (3.9): a_j = j^β for j even, (j-1)^β for j odd.

The coefficients satisfy a_j = (2⌊j/2⌋)^β for j ≥ 2, reflecting that the cosine/sine pair with frequency ⌊j/2⌋ share the same Sobolev weight. In particular, a₁ = 0 (constant term unconstrained).

We use 0-based indexing: our j = 0, 1, 2, ... corresponds to the book's j = 1, 2, 3, ... The weight for index j is a_{j+1}² = (sobolevCoeff β (j+1))².

Part (i) (eq. 3.10): For θ ∈ Θ(β, Q) with β > 1/2 and M ≥ 1, ‖φ_{θ*}^M − f‖{L₂}² = Σ{j>M} |θ_j*|² ≤ Q·M^{−2β}. The first equality is Parseval's theorem (orthonormality of the basis). The inequality uses the key algebraic step: Σ_{j>M} θ_j² ≤ (1/a_{M+1}²) Σ_{j>M} a_j² θ_j² ≤ Q/M^{2β}.

Part (ii) (eq. 3.11): For M = n−1, |φ_{θ*}^{n-1} − f|₂² ≤ 2n(Σ_{j≥n} |θ_j*|)² ≲ Q·n^{2−2β}. The proof uses Cauchy-Schwarz (book line 2460): Σ |θ_j| = Σ a_j|θ_j| · (1/a_j) ≤ √(Σ a_j²θ_j²) · √(Σ 1/a_j²) ≤ √Q · √(Σ 1/a_j²). The empirical norm bound |φ_{θ*}^{n-1} − f|₂ ≤ 2√(2n) Σ_{j>n} |θ_j*| uses |φ_j|₂ ≤ √(2n) for the trigonometric basis (book line 2456–2458).

noncomputable def SobolevEllipsoidInf (β Q : ℝ) : Set (ℕ → ℝ)

The Sobolev ellipsoid Θ(β, Q) for infinite sequences in ℓ₂(ℕ) (book eq. 3.9, Thm 3.11). A sequence θ : ℕ → ℝ belongs to the ellipsoid if Σ_{j=0}^∞ a_{j+1}² · θ_j² ≤ Q, where a_j are the Sobolev coefficients from eq. (3.9): a_j = j^β for j even, (j-1)^β for j odd. Equivalently, a_j = (2⌊j/2⌋)^β for j ≥ 2 (cosine/sine pairs share weight). We use 0-based indexing: j = 0, 1, 2, ... corresponds to the book's j = 1, 2, 3, ... Note: a₁ = 0 (since 1 is odd, a₁ = (1-1)^β = 0), so the constant term is unconstrained.

theorem sobolevCoeff_eq_floor_form (β : ℝ) (j : ℕ) (hj : 2 ≤ j) : Chapter3.sobolevCoeff β j = (2 * ↑(j / 2)) ^ β

The Sobolev weight a_j equals (2⌊j/2⌋)^β for j ≥ 2 (eq. 3.9). For even j, a_j = j^β = (2·(j/2))^β. For odd j ≥ 3, a_j = (j-1)^β = (2·⌊j/2⌋)^β.

theorem summable_mul_of_summable_sq {ι : Type u_1} {f g : ι → ℝ} (hf : Summable fun (j : ι) => f j ^ 2) (hg : Summable fun (j : ι) => g j ^ 2) : Summable fun (j : ι) => f j * g j

Summable product of two functions given summability of their squares. By AM-GM: |f·g| ≤ (f² + g²)/2, so the product is dominated by a summable function.

theorem tsum_inner_mul_le {ι : Type u_1} {f g : ι → ℝ} (hf : Summable fun (j : ι) => f j ^ 2) (hg : Summable fun (j : ι) => g j ^ 2) (hfg : Summable fun (j : ι) => f j * g j) : (∑' (j : ι), f j * g j) ^ 2 ≤ (∑' (j : ι), f j ^ 2) * ∑' (j : ι), g j ^ 2

Cauchy-Schwarz inequality for infinite series (discriminant argument). (∑' j, f j · g j)² ≤ (∑' j, f j²) · (∑' j, g j²). Proved via the non-negativity of ∑' j, (t·f_j − g_j)² for all t ∈ ℝ.

theorem sobolevCoeff_succ_ge (β : ℝ) (hβ : 0 < β) (j : ℕ) : ↑j ^ β ≤ Chapter3.sobolevCoeff β (j + 1)

The Sobolev coefficient a_{j+1} ≥ j^β for all j (0-based indexing). For j+1 even: a_{j+1} = (j+1)^β ≥ j^β. For j+1 odd: a_{j+1} = j^β.

theorem sobolevCoeff_succ_ge_of_le (β : ℝ) (hβ : 0 < β) (M j : ℕ) (hj : M ≤ j) : ↑M ^ β ≤ Chapter3.sobolevCoeff β (j + 1)

For j ≥ M: a_{j+1} ≥ M^β (since a_{j+1} ≥ j^β ≥ M^β).

theorem sobolevCoeff_succ_pos (β : ℝ) (_hβ : 0 < β) (j : ℕ) (hj : 1 ≤ j) : 0 < Chapter3.sobolevCoeff β (j + 1)

The Sobolev coefficient a_{j+1} is positive for j ≥ 1 when β > 0.

theorem sobolevCoeff_succ_ne_zero (β : ℝ) (hβ : 0 < β) (j : ℕ) (hj : 1 ≤ j) : Chapter3.sobolevCoeff β (j + 1) ≠ 0

The Sobolev coefficient a_{j+1} is nonzero for j ≥ 1 when β > 0.

theorem sobolev_weight_ge_one (β : ℝ) (hβ : 0 < β) (j : ℕ) (hj : 1 ≤ j) : 1 ≤ Chapter3.sobolevCoeff β (j + 1) ^ 2

The Sobolev weight a_{j+1}² ≥ 1 for j ≥ 1 when β > 0. Since a_{j+1} ≥ j^β ≥ 1 for j ≥ 1.

theorem sobolev_weight_ge_rpow (β : ℝ) (hβ : 0 < β) (M j : ℕ) (hj : M ≤ j) : ↑M ^ (2 * β) ≤ Chapter3.sobolevCoeff β (j + 1) ^ 2

The Sobolev weight a_{j+1}² ≥ M^{2β} for j ≥ M when β > 0.

theorem summable_sq_of_sobolev {β Q : ℝ} (hβ : 1 / 2 < β) (θ : ℕ → ℝ) (hθ : θ ∈ SobolevEllipsoidInf β Q) : Summable fun (j : ℕ) => θ j ^ 2

Summability of θ_j² when θ belongs to the Sobolev ellipsoid with β > 1/2. For j ≥ 1, we have a_{j+1}² ≥ 1, so θ_j² ≤ a_{j+1}² θ_j². For j = 0, the weight is 0 (since a₁ = 0), so we need θ₀² to be finite, which it is since it's a single term.

theorem trigBasis_L2_orthonormal (j k : ℕ) (hj : 0 < j) (hk : 0 < k) : ∫ (x : ℝ) in Set.Icc 0 1, Chapter3.trigBasis j x * Chapter3.trigBasis k x = if j = k then 1 else 0

Orthonormality of trigBasis in L₂([0,1]) (Problem 3.4, book line 2582): ∫ x in Icc 0 1, φ_j(x) · φ_k(x) = δ_{jk} for j, k ≥ 1.

The proof uses product-to-sum identities and the vanishing of ∫₀¹ cos(2πmx) dx = 0 and ∫₀¹ sin(2πmx) dx = 0 for m ≠ 0. This is stated as Problem 3.4 in the book and invoked at line 2448.

theorem summable_of_sobolev {β Q : ℝ} (hβ : 1 / 2 < β) (θ : ℕ → ℝ) (hθ : θ ∈ SobolevEllipsoidInf β Q) : Summable θ

Absolute summability of θ from Sobolev membership with β > 1/2. For θ ∈ Θ(β, Q) with β > 1/2, we have Σ |θ_j| < ∞. The proof uses Cauchy-Schwarz on the tail j ≥ 1: Σ_{j≥1} |θ_j| = Σ a_{j+1}|θ_j| · (1/a_{j+1}) ≤ √(Σ a_{j+1}² θ_j²) · √(Σ 1/a_{j+1}²) < ∞ since a_{j+1} ≥ j^β ≥ 1 for j ≥ 1 and 2β > 1. (Derivable via Cauchy-Schwarz and the p-series test with p = 2β > 1.)

theorem summable_trigBasis_mul (θ : ℕ → ℝ) (x : ℝ) (h_abs_sum : Summable θ) : Summable fun (j : ℕ) => θ j * Chapter3.trigBasis (j + 1) x

Pointwise summability of θ_j · φ_{j+1}(x) for absolutely summable θ. Since |trigBasis j x| ≤ √2 for all j, x, the product series is dominated by √2 · Σ|θ_j| which converges when θ is absolutely summable.

theorem tsum_sub_sum_range {f : ℕ → ℝ} (hf : Summable f) (M : ℕ) : ∑' (j : ℕ), f j - ∑ j ∈ Finset.range M, f j = ∑' (j : ↑(Set.Ici M)), f ↑j

Splitting identity: ∑' j, f j - ∑{j<M} f j = ∑'{j≥M} f j for summable f.

theorem integrand_tsum_sub_finsum_sq (θ : ℕ → ℝ) (M : ℕ) (h_abs_sum : Summable θ) : ∫ (x : ℝ) in Set.Icc 0 1, (∑' (j : ℕ), θ j * Chapter3.trigBasis (j + 1) x - ∑ j ∈ Finset.range M, θ j * Chapter3.trigBasis (j + 1) x) ^ 2 = ∫ (x : ℝ) in Set.Icc 0 1, (∑' (j : ↑(Set.Ici M)), θ ↑j * Chapter3.trigBasis (↑j + 1) x) ^ 2

Rewriting ∑' j − ∑_{j<M} as a tail tsum under the integral (pointwise rewrite). For absolutely summable θ, the series ∑ θ_j φ_{j+1}(x) converges pointwise, so we can rewrite the difference ∑' j − ∑{j<M} = ∑{j≥M} pointwise and then integrate.

theorem integral_sq_tsum_eq_double_sum (θ : ℕ → ℝ) (M : ℕ) (h_sq_sum : Summable fun (j : ℕ) => θ j ^ 2) (h_sum : Summable θ) : ∫ (x : ℝ) in Set.Icc 0 1, (∑' (j : ↑(Set.Ici M)), θ ↑j * Chapter3.trigBasis (↑j + 1) x) ^ 2 = ∑' (j : ↑(Set.Ici M)) (k : ↑(Set.Ici M)), θ ↑j * θ ↑k * ∫ (x : ℝ) in Set.Icc 0 1, Chapter3.trigBasis (↑j + 1) x * Chapter3.trigBasis (↑k + 1) x

Exchange of Lebesgue integral and squared tail tsum (Parseval's identity for the trigonometric basis — standard result, not proved in the book). For a square-summable sequence θ and bounded basis functions φ_j with |φ_j| ≤ √2, the integral of the squared tail series equals the double sum: ∫ (∑{j≥M} θ_j φ{j+1})² = ∑{j≥M} ∑{k≥M} θ_j θ_k ∫ φ_{j+1} φ_{k+1}.

This requires dominated convergence for L² functions, which holds because |θ_j φ_{j+1}(x)| ≤ √2 |θ_j| and ∑ |θ_j| < ∞ (since ∑ θ_j² < ∞ with bounded basis functions).

theorem parseval_truncation_L2_error (θ : ℕ → ℝ) (M : ℕ) (h_sq_sum : Summable fun (j : ℕ) => θ j ^ 2) (h_abs_sum : Summable θ) : ∫ (x : ℝ) in Set.Icc 0 1, (∑' (j : ℕ), θ j * Chapter3.trigBasis (j + 1) x - ∑ j ∈ Finset.range M, θ j * Chapter3.trigBasis (j + 1) x) ^ 2 = ∑' (j : ↑(Set.Ici M)), θ ↑j ^ 2

Parseval's identity for the trigonometric basis (book line 2448): ‖φ_{θ*}^M − f‖{L₂}² = Σ{j≥M} |θ_j|².

This is Parseval's identity applied to the truncation error of a Fourier series expansion in the trigonometric basis {φ_j}_{j≥1}. The book states this without proof as a well-known consequence of orthonormality: "Since {φ_j}_j forms an orthonormal system in L₂([0,1]), we have..." (line 2448).

The proof proceeds in three steps:

1. Rewrite the difference as a tail tsum: ∑' j − ∑{j<M} = ∑{j≥M}
2. Exchange the integral with the double sum (dominated convergence)
3. Apply orthonormality: cross terms vanish, diagonal terms give θ_j²

Steps 1-2 are formalized via helper lemmas. Step 3 uses trigBasis_L2_orthonormal.

theorem approx_error_sobolev (M : ℕ) (β Q : ℝ) (hβ : 1 / 2 < β) (hM : 0 < M) (θ : ℕ → ℝ) (hθ : θ ∈ SobolevEllipsoidInf β Q) : ∑' (j : ↑(Set.Ici M)), θ ↑j ^ 2 ≤ Q * ↑M ^ (-(2 * β))

Lemma 3.14(i): Tail bound for the Sobolev ellipsoid (eq. 3.10). If θ ∈ Θ(β, Q) with β > 1/2 and M ≥ 1, then Σ_{j≥M} θ_j² ≤ Q·M^{−2β}.

The proof follows the book's key algebraic step (line 2452): Σ_{j>M} θ_j² = Σ_{j>M} a_j² θ_j² / a_j² ≤ (1/a_{M+1}²) Σ_{j>M} a_j² θ_j² [since a_j ≥ a_{M+1} for j > M] ≤ Q / a_{M+1}² [Sobolev condition] ≤ Q / M^{2β} [since a_{M+1} ≥ M^β]

theorem approx_error_sobolev_L2 (M : ℕ) (β Q : ℝ) (hβ : 1 / 2 < β) (hM : 0 < M) (θ : ℕ → ℝ) (hθ : θ ∈ SobolevEllipsoidInf β Q) : ∫ (x : ℝ) in Set.Icc 0 1, (∑' (j : ℕ), θ j * Chapter3.trigBasis (j + 1) x - ∑ j ∈ Finset.range M, θ j * Chapter3.trigBasis (j + 1) x) ^ 2 ≤ Q * ↑M ^ (-(2 * β))

Combined Parseval + tail bound: the L₂ approximation error of the M-term Fourier truncation satisfies ‖φ_{θ*}^M − f‖{L₂}² = Σ{j≥M} θ_j² ≤ Q · M^{−2β}. This is the full content of eq. (3.10) in Lemma 3.14(i).

theorem Q_nonneg_of_sobolev {β Q : ℝ} {θ : ℕ → ℝ} (hθ : θ ∈ SobolevEllipsoidInf β Q) : 0 ≤ Q

Q ≥ 0 when the Sobolev ellipsoid is non-empty, since ∑ a_j²θ_j² ≤ Q and the left side is a sum of nonneg terms.

theorem tail_abs_sum_sq_le (M : ℕ) (β Q : ℝ) (hβ : 1 / 2 < β) (hM : 0 < M) (θ : ℕ → ℝ) (hθ : θ ∈ SobolevEllipsoidInf β Q) (h_inv_sum : Summable fun (j : ℕ) => if Chapter3.sobolevCoeff β (j + 1) = 0 then 0 else Chapter3.sobolevCoeff β (j + 1) ^ (-2)) : (∑' (j : ↑(Set.Ici M)), |θ ↑j|) ^ 2 ≤ Q * ∑' (j : ↑(Set.Ici M)), if Chapter3.sobolevCoeff β (↑j + 1) = 0 then 0 else Chapter3.sobolevCoeff β (↑j + 1) ^ (-2)

Cauchy-Schwarz bound on the tail sum of absolute values (book line 2460). For θ ∈ Θ(β, Q) with M ≥ 1 (so all Sobolev coefficients a_{j+1} > 0): (Σ_{j ∈ Ici M} |θ_j|)² ≤ Q · Σ_{j ∈ Ici M} 1/a_{j+1}².

The proof follows the book: writing |θ_j| = a_{j+1}|θ_j| · (1/a_{j+1}) and applying Cauchy-Schwarz gives (Σ |θ_j|)² ≤ (Σ a_{j+1}² θ_j²)(Σ 1/a_{j+1}²) ≤ Q · Σ 1/a_{j+1}². The condition M ≥ 1 ensures a_{j+1} ≥ j^β ≥ 1 > 0 for all j ≥ M.

theorem approx_error_sobolev_empirical (n : ℕ) (β Q : ℝ) (hβ : 1 / 2 < β) (hn : 0 < n) (θ : ℕ → ℝ) (hθ : θ ∈ SobolevEllipsoidInf β Q) (h_inv_sum : Summable fun (j : ℕ) => if Chapter3.sobolevCoeff β (j + 1) = 0 then 0 else Chapter3.sobolevCoeff β (j + 1) ^ (-2)) : 2 * ↑n * (∑' (j : ↑(Set.Ici n)), |θ ↑j|) ^ 2 ≤ 2 * ↑n * (Q * ∑' (j : ↑(Set.Ici n)), if Chapter3.sobolevCoeff β (↑j + 1) = 0 then 0 else Chapter3.sobolevCoeff β (↑j + 1) ^ (-2))

Lemma 3.14(ii): Empirical approximation bound (equation 3.11). For M = n−1, the empirical approximation error satisfies |φ_{θ*}^{n-1} − f|₂² ≤ 2n · (Σ_{j≥n} |θ_j*|)² ≤ 2n · Q · Σ_{j≥n} 1/a_{j+1}².

The first inequality comes from the bound (book line 2456): |φ_{θ*}^{n-1} − f|₂ = |Σ_{j>n} θ_j* φ_j|₂ ≤ 2√(2n) Σ_{j>n} |θ_j*| where |φ_j|₂ ≤ √(2n) for the trigonometric basis.

theorem trigBasis_empirical_norm_bound (n j : ℕ) (X : Fin n → ℝ) (hn : 0 < n) (_hj : 1 ≤ j) : 1 / ↑n * ∑ i : Fin n, Chapter3.trigBasis j (X i) ^ 2 ≤ 2 * ↑n

Empirical norm connection (book line 2456–2458). For the trigonometric basis, each φ_j satisfies |φ_j|∞ ≤ √2, hence (trigBasis j x)² ≤ 2 for all x. Summing over n terms and dividing by n gives (1/n) Σᵢ (trigBasis j (Xᵢ))² ≤ 2 ≤ 2n.

theorem summable_succ_rpow_neg (p : ℝ) (hp : 1 < p) : Summable fun (j : ℕ) => (↑j + 1) ^ (-p)

Summability of the shifted p-series (j+1)^{-p} for p > 1. Follows from summability of n^{-p} via re-indexing.

noncomputable def iciEquivNat (n : ℕ) : ℕ ≃ ↑(Set.Ici n)

Equivalence between ℕ and the subtype Set.Ici n, mapping k ↦ k + n.

theorem tsum_Ici_eq_tsum_add (f : ℕ → ℝ) (n : ℕ) : ∑' (j : ↑(Set.Ici n)), f ↑j = ∑' (k : ℕ), f (k + n)

Converting a tsum over Set.Ici n to a shifted tsum over ℕ.

theorem finite_sum_le_integral_bound (n N : ℕ) (p : ℝ) (hp : 1 < p) (hn : 1 ≤ n) : ∑ k ∈ Finset.range N, ↑(k + n + 1) ^ (-p) ≤ ↑n ^ (1 - p) / (p - 1)

Finite sum bound via the integral comparison test (AntitoneOn.sum_le_integral). For p > 1 and n ≥ 1: ∑_{k=0}^{N-1} (k+n+1)^{-p} ≤ n^{1-p}/(p-1).

theorem summable_shifted_rpow_neg (n : ℕ) (p : ℝ) (hp : 1 < p) : Summable fun (k : ℕ) => ↑(k + n) ^ (-p)

Summability of the shifted series (k + n)^{-p} for p > 1.

theorem tail_pseries_rpow_bound (n : ℕ) (p : ℝ) (hp : 1 < p) (hn : 0 < n) : ∑' (j : ↑(Set.Ici n)), (↑↑j + 1) ^ (-p) ≤ p / (p - 1) * ↑n ^ (1 - p)

Tail bound for the p-series (integral comparison test). For p > 1 and n ≥ 1: Σ_{j≥n} (j+1)^{-p} ≤ (p/(p-1)) · n^{1-p}. The book uses this implicitly via the ≲ notation in eq. (3.11). Proved via the integral comparison test: for the antitone function x^{-p}, Σ_{m≥n+1} m^{-p} ≤ ∫_n^∞ x^{-p} dx = n^{1-p}/(p-1) ≤ (p/(p-1))·n^{1-p}.

theorem sobolev_inv_weight_tail_bound (n : ℕ) (β : ℝ) (hβ : 1 / 2 < β) (hn : 0 < n) : (∑' (j : ↑(Set.Ici n)), if Chapter3.sobolevCoeff β (↑j + 1) = 0 then 0 else Chapter3.sobolevCoeff β (↑j + 1) ^ (-2)) ≤ 2 * β / (2 * β - 1) * ↑n ^ (1 - 2 * β)

Bound on the tail sum of inverse Sobolev weights. For β > 1/2 and n ≥ 1: Σ_{j≥n} 1/a_{j+1}² ≤ (2β/(2β-1)) · n^{1-2β}. Uses 1/a_{j+1}² ≤ 1/j^{2β} for j ≥ 1, then bounds the resulting p-series tail by the integral comparison test.

theorem approx_error_sobolev_empirical_bound (n : ℕ) (β Q : ℝ) (hβ : 1 / 2 < β) (hn : 0 < n) (θ : ℕ → ℝ) (hθ : θ ∈ SobolevEllipsoidInf β Q) (h_inv_sum : Summable fun (j : ℕ) => if Chapter3.sobolevCoeff β (j + 1) = 0 then 0 else Chapter3.sobolevCoeff β (j + 1) ^ (-2)) : 2 * ↑n * (∑' (j : ↑(Set.Ici n)), |θ ↑j|) ^ 2 ≤ 4 * β / (2 * β - 1) * Q * ↑n ^ (2 - 2 * β)

Lemma 3.14(ii) full asymptotic bound (equation 3.11). For θ ∈ Θ(β, Q) with β > 1/2 and n ≥ 1: 2n · (Σ_{j≥n} |θ_j|)² ≤ (4β/(2β-1)) · Q · n^{2-2β}.

This is the full content of eq. (3.11), formalizing the book's ≲ notation. The proof combines Cauchy-Schwarz (tail_abs_sum_sq_le) with the p-series tail bound (sobolev_inv_weight_tail_bound).

theorem lemma_3_14 (n : ℕ) (β Q : ℝ) (hβ : 1 / 2 < β) (hn : 0 < n) (θ : ℕ → ℝ) (hθ : θ ∈ SobolevEllipsoidInf β Q) (h_inv_sum : Summable fun (j : ℕ) => if Chapter3.sobolevCoeff β (j + 1) = 0 then 0 else Chapter3.sobolevCoeff β (j + 1) ^ (-2)) : ∑' (j : ↑(Set.Ici n)), θ ↑j ^ 2 ≤ Q * ↑n ^ (-(2 * β)) ∧ 2 * ↑n * (∑' (j : ↑(Set.Ici n)), |θ ↑j|) ^ 2 ≤ 4 * β / (2 * β - 1) * Q * ↑n ^ (2 - 2 * β)

Lemma 3.14 (bundled): Approximation error bounds for truncated Fourier series of Sobolev functions. For θ ∈ Θ(β, Q) with β > 1/2 and M ≥ 1:

Part (i) (eq. 3.10): ‖φ_{θ*}^M − f‖{L₂}² = Σ{j≥M} θ_j² ≤ Q · M^{−2β}. Part (ii) (eq. 3.11): 2n · (Σ_{j≥n} |θ_j|)² ≤ (4β/(2β-1)) · Q · n^{2-2β}.