Definitions and basic properties #
a_{2k} = (2k)^β (even Sobolev coefficient).
a_{2k+1} = (2k)^β (odd Sobolev coefficient).
Step 1: Integration by parts recurrence (Book lines 2317-2326) #
Using integration by parts and the periodic boundary conditions f^(j-1)(0) = f^(j-1)(1), the Fourier coefficients of derivatives satisfy: s_{2k}(j) = (2πk) · s_{2k+1}(j-1) s_{2k+1}(j) = -(2πk) · s_{2k}(j-1)
This requires the full integration by parts machinery on [0,1] with
periodic boundary conditions. The proof uses Mathlib's IBP theorem
(AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul) with
helper lemmas (axiomatized) for standard calculus facts not proved in the book.
Standard analysis fact (not proved in the book): for a Sobolev function f ∈ W(β, L), each iterated derivative iteratedDeriv k f is differentiable on [0,1] when k < β, with derivative equal to iteratedDeriv (k+1) f.
Axiom justification: The Sobolev class W(β, L) requires the (β-1)-th derivative to be
absolutely continuous on [0,1] (Definition 3.10). By the fundamental theorem of calculus
for AC functions, this means the (β-1)-th derivative is differentiable a.e. with derivative
equal to the β-th derivative. The pointwise HasDerivAt statement (rather than a.e.)
for all intermediate derivatives is a standard consequence of the Sobolev embedding theorem
and the recursive structure of absolute continuity. The book does not prove this fact;
it is implicitly used in the integration by parts argument (Book lines 2317–2326).
One-step downward regularity for iterated derivatives: if iteratedDeriv (k+1) f is absolutely continuous on [0,1] and iteratedDeriv k f is differentiable on [0,1] with the correct derivative, then iteratedDeriv k f is also absolutely continuous on [0,1].
Proof: the (k+1)-th derivative being AC implies it is continuous on [0,1] (by
AbsolutelyContinuousOnInterval.continuousOn), hence bounded on the compact interval
(by AbsolutelyContinuousOnInterval.exists_bound). With the differentiability hypothesis,
the k-th derivative has this bounded function as its derivative everywhere on [0,1],
making it Lipschitz (by Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le), hence AC
(by LipschitzOnWith.absolutelyContinuousOnInterval).
For a Sobolev function f ∈ W(β, L) with j < β, iteratedDeriv (j-1) f is AC on [0,1]. This follows by downward regularity: the (β-1)-th derivative is AC (from the Sobolev definition), hence all lower-order derivatives are AC by repeated application of ac_step_iteratedDeriv. The differentiability hypothesis at each step is provided by sobolev_iteratedDeriv_hasDerivAt (a standard analysis fact, not proved in the book).
The proof uses Nat.decreasingInduction from β-1 down to j-1, applying ac_step_iteratedDeriv at each step.
For f ∈ W(β, L) with 1 ≤ j ≤ β, iteratedDeriv (j-1) f is absolutely continuous on [0,1]. The j = β case follows directly from the Sobolev class definition. The j < β case uses downward regularity (standard analysis, not proved in the book).
A function x ↦ √2 * cos(c * x) is absolutely continuous on [0,1], since it is globally Lipschitz.
A function x ↦ √2 * sin(c * x) is absolutely continuous on [0,1], since it is globally Lipschitz.
Trig basis functions are absolutely continuous on [0,1] (they are smooth).
Proved via the Lipschitz → AC route: each branch of trigBasis is either
constant or a composition of Lipschitz functions (scalar multiplication,
cos/sin), hence globally Lipschitz, hence absolutely continuous on any
interval.
Derivative of the even trig basis function: d/dx [√2 cos(2πkx)] = -2πk · √2 sin(2πkx) = -(2πk) · φ_{2k+1}(x). Standard calculus derivative not proved in the book.
Derivative of the odd trig basis function: d/dx [√2 sin(2πkx)] = 2πk · √2 cos(2πkx) = (2πk) · φ_{2k}(x). Standard calculus derivative not proved in the book.
Convert derivFourierCoeff (Icc integral) to interval integral.
Integration by parts for Fourier coefficients: the cos case. ∫₀¹ f^(j)(t) · √2 cos(2πkt) dt = [f^(j-1)(t) · √2 cos(2πkt)]₀¹ + (2πk) ∫₀¹ f^(j-1)(t) · √2 sin(2πkt) dt = 0 + (2πk) · s_{2k+1}(j-1) The boundary term vanishes by cos(2πk) = 1 and periodic BC. This is an application of integration by parts (a standard tool not proved in the book) to the specific integrals defining Fourier coefficients.
Integration by parts for Fourier coefficients: the sin case. ∫₀¹ f^(j)(t) · √2 sin(2πkt) dt = [f^(j-1)(t) · √2 sin(2πkt)]₀¹ - (2πk) ∫₀¹ f^(j-1)(t) · √2 cos(2πkt) dt = 0 - (2πk) · s_{2k}(j-1) The boundary term vanishes by sin(2πk) = sin(0) = 0. This is an application of integration by parts (a standard tool not proved in the book) to the specific integrals defining Fourier coefficients.
Integration by parts recurrence for Fourier coefficients of derivatives (Book lines 2319–2326). For f ∈ W(β, L) and 1 ≤ j ≤ β, k ≥ 1: s_{2k}(j) = (2πk) s_{2k+1}(j-1) and s_{2k+1}(j) = -(2πk) s_{2k}(j-1). Proof: integration by parts using periodic boundary conditions. Proof: integration by parts using periodic boundary conditions (ibp_cos_step and ibp_sin_step).
Step 2: Induction result (Book line 2334) #
From the IBP recurrence, by induction on β: s_{2k}(β)² + s_{2k+1}(β)² = (2πk)^{2β} · (θ_{2k}² + θ_{2k+1}²) where θ_j = s_j(0) are the Fourier coefficients of f.
Induction on the IBP recurrence (Book line 2330): s_{2k}(j)² + s_{2k+1}(j)² = (2πk)² · [s_{2k}(j-1)² + s_{2k+1}(j-1)²]. Follows directly from the IBP recurrence by squaring and adding.
By induction on β (Book line 2334): s_{2k}(β)² + s_{2k+1}(β)² = (2πk)^{2β} · (θ_{2k}² + θ_{2k+1}²) where θ_j = s_j(0) = derivFourierCoeff f 0 j.
Key identity (Theorem 3.11 proof, by IBP induction): s_{2k}(β)² + s_{2k+1}(β)² = (2πk)^{2β}(θ_{2k}² + θ_{2k+1}²) implies the Sobolev coefficient form = π^{2β}(a_{2k}² θ_{2k}² + a_{2k+1}² θ_{2k+1}²).
Step 3: Parseval's identity for derivatives (Book line 2343) #
Parseval's identity applied to f^(β) ∈ L₂([0,1]): ∫₀¹ (f^(β)(t))² dt = Σ_{k=1}^∞ s_k(β)² This is a standard result for orthonormal bases in L₂.
Orthonormality of the trigonometric basis (standard integral computation, not proved in the book). For i, j ≥ 1: ∫₀¹ φ_i(x) φ_j(x) dx = δ_{ij} This is a direct computation using the integrals of products of sin/cos functions on [0,1]. The book assumes this as a known property of the trigonometric system.
trigBasis is continuous for each j.
The partial Fourier sum is continuous.
Continuous functions are integrable on Icc 0 1.
If g² is integrable and g is AEStronglyMeasurable on Icc 0 1, then g is integrable on Icc 0 1 (L² ⊂ L¹ on finite measure spaces).
L² error formula via orthonormality (not proved in the book). For g ∈ L²([0,1]), the L² error of the N-th partial Fourier sum equals the L² norm minus the sum of squared Fourier coefficients: ∫₀¹ (g - Σ_{k=1}^N c_k φ_k)² dx = ∫₀¹ g² dx - Σ_{k=1}^N c_k² where c_k = ∫₀¹ g φ_k dx. This follows by expanding the square and using orthonormality of {φ_k}. Proof by induction on N: the base case is trivial, and the induction step uses the algebraic identity (a - b - c)² = (a-b)² - 2c(a-b) + c² together with orthonormality to evaluate the cross terms.
L² convergence of the trigonometric Fourier series (axiom). For a mean-zero square-integrable function g on [0,1], the partial Fourier sums (over the non-constant trig basis elements φ₁, φ₂, ...) converge to g in L² norm. The mean-zero hypothesis is essential: the sum excludes the constant basis element trigBasis 0 = 1, so the limit captures all of ‖g‖² only when ⟨g, 1⟩ = ∫g = 0.
The book states L² completeness of the full trig system at lines 2297–2299
without proof. Mathlib proves the analogous result for complex Fourier series
on AddCircle T (hasSum_fourier_series_L2), but bridging from that to this
real formulation requires substantial infrastructure.
L₂ completeness of the trigonometric system (ε-δ form)
(not proved in the book).
For any mean-zero square-integrable function g on [0,1] and any ε > 0,
the Fourier partial sum approximation error eventually stays below ε.
The mean-zero hypothesis is needed because the sum excludes trigBasis 0.
Proved from trigBasis_L2_convergence_axiom via Metric.tendsto_atTop.
L₂ completeness of the trigonometric system (not proved in the book).
For any mean-zero square-integrable function g on [0,1], the partial Fourier
sums (excluding the constant term) converge to g in L₂ norm.
The mean-zero hypothesis is needed because the sum excludes trigBasis 0.
Follows from trigBasis_L2_approx via Metric.tendsto_atTop.
Parseval's identity for L₂([0,1]) with the trigonometric ONB. For any square-integrable function g on [0,1]: ∫₀¹ g(x)² dx = ∑_{k≥1} (∫₀¹ g(x) φ_k(x) dx)² The book invokes this identity at line 2343 ("Together with the Parseval identity") without proof.
Proof structure: From orthonormality of {φ_k} (trigBasis_orthonormal), the L² error satisfies ∫(g - S_N)² = ∫g² - Σ_{k≤N} c_k² (trigBasis_L2_error_eq). By completeness (trigBasis_L2_completeness), ∫(g - S_N)² → 0. Therefore Σ c_k² → ∫g², giving the Parseval identity.
Parseval's identity for f^(β): the L₂ norm of the β-th derivative equals the sum of squares of its Fourier coefficients (Book line 2343). This is a standard Hilbert space result for the trigonometric ONB.
Step 4: Combining Parseval + IBP + coefficient identity (Book line 2343) #
The key formula: ∫₀¹ (f^(β))² dt = π^{2β} · Σ_{j≥1} a_j² θ_j²
This combines:
- Parseval: ∫ = Σ s_k(β)²
- IBP induction: s_{2k}(β)² + s_{2k+1}(β)² = (2πk)^{2β}(θ_{2k}² + θ_{2k+1}²)
- Coefficient identity: (2πk)^{2β} = π^{2β}(a_{2k}² + a_{2k+1}² terms)
Parity regrouping: if two summable sequences agree on pair sums (f(2k+1) + f(2k+2) = g(2k+1) + g(2k+2)) and have the same first term, then their total sums agree. This is used to match the IBP-derived pairs.
Companion function for parity regrouping: swaps adjacent odd/even indices. companion(0) = 0, companion(2k+1) = 2(k+1), companion(2(k+1)) = 2k+1.
Instances For
Summability from pair identity: if two nonneg sequences agree on pair sums and at index 0, and one is summable, then so is the other.
Summability of Fourier coefficients squared, extracted from Bessel's inequality. For a square-integrable function g on [0,1], the sequence (∫ g · φ_{k+1})² is summable, bounded by ∫ g².
Series regrouping: the sum of squares of derivative Fourier coefficients ∑{k≥1} s_k(β)² equals π^{2β} ∑{j≥1} a_j² θ_j². This combines:
- s₁(β) = 0 (by periodic BC: ∫₀¹ f^(β)(t) dt = f^(β-1)(1) - f^(β-1)(0) = 0)
- IBP induction: s_{2k}(β)² + s_{2k+1}(β)² = (2πk)^{2β}(θ_{2k}² + θ_{2k+1}²)
- Coefficient identity: (2πk)^{2β} = π^{2β} · a_{2k}² (resp. a_{2k+1}²)
- Regrouping: ∑{j≥1} = a₁²θ₁² + ∑{k≥1}(a_{2k}²θ_{2k}² + a_{2k+1}²θ_{2k+1}²), with a₁=0. The regrouping of an absolutely convergent series by parity is a standard analysis fact not proved in the book.
The combined Parseval–IBP–coefficient identity (Book line 2343): ∫₀¹ (f^(β)(t))² dt = π^{2β} · Σ_{j≥1} a_j² θ_j² where θ_j = s_j(0) are the Fourier coefficients of f.
This is the analytical core of Theorem 3.11, combining:
- Parseval's identity for f^(β),
- the IBP induction s_{2k}(β)² + s_{2k+1}(β)² = (2πk)^{2β}(θ_{2k}² + θ_{2k+1}²),
- the rewriting (2πk)^{2β} = π^{2β} · a_{2k}² (and a_{2k+1}²).
The series regrouping (parity decomposition) is captured in series_parity_regroup.
Part A: Fourier series representation (Book lines 2297-2299) #
f ∈ W(β, L) can be represented as f = Σ θ_j* φ_j (convergence in L₂). This is a consequence of the completeness of the trigonometric system.
L² convergence of the full trigonometric Fourier series (axiom).
For any square-integrable function g on [0,1], the partial sums over the
full trigonometric basis {φ₀, φ₁, φ₂, ...} = {1, √2cos(2πx), √2sin(2πx), ...}
converge to g in L² norm. Unlike trigBasis_L2_convergence_axiom, this
includes the constant basis element trigBasis 0 = 1, so no mean-zero
hypothesis is needed.
The book states this at lines 2297–2299 without proof.
Theorem 3.11, Part A (Fourier series representation). For f ∈ W(β, L), there exists a sequence θ of Fourier coefficients θ_j = ∫₀¹ f(t)φ_j(t)dt such that f = Σ θ_j φ_j in L₂([0,1]), i.e., ∫₀¹ |f(t) - Σ_{j=0}^{N-1} θ_j φ_j(t)|² dt → 0 as N → ∞. Here the sum includes the constant basis element φ₀ = 1.
This is a standard consequence of {φ_j} being an orthonormal basis of L₂([0,1]): every L₂ function can be expanded in the basis. Proof: Follows from the L₂ completeness of the full trigonometric system (trigBasis_L2_full_convergence_axiom), which is not proved in the book.
Part B: Main theorem — ellipsoid bound (Book lines 2345-2349) #
Theorem 3.11, Part B (Sobolev class ⊂ Fourier ellipsoid). If f ∈ W(β, L), then its Fourier coefficients θ_j = ⟨f, φ_j⟩ satisfy Σ_{j≥1} a_j² θ_j² ≤ L²/π^{2β}, i.e., θ ∈ Θ(β, L²/π^{2β}).
Proof: By the Parseval–IBP identity (parseval_sobolev_coeff_identity), ∫₀¹ (f^(β))² = π^{2β} Σ a_j² θ_j². Since f ∈ W(β,L), ∫₀¹ (f^(β))² ≤ L², giving Σ a_j² θ_j² ≤ L²/π^{2β}.
Finite-dimensional corollary: the truncated coefficients lie in the finite Sobolev ellipsoid.
Theorem 3.11 (Sobolev Fourier representation and ellipsoid membership). For f ∈ W(β, L): (A) f can be represented as f = Σ θ_j φ_j (convergence in L²), where θ_j = ∫₀¹ f(t)φ_j(t) dt are the Fourier coefficients; and (B) the sequence θ belongs to the Sobolev ellipsoid Θ(β, L²/π^{2β}), i.e., Σ_{j≥1} a_j² θ_j² ≤ L²/π^{2β}.
This bundles sobolev_fourier_representation (Part A) and
sobolev_fourier_ellipsoid (Part B) into a single combined statement.