Completeness of the Fourier sine system on an interval

On an interval [a, b] with a < b, the functions x ↦ sin (k π (x - a) / (b - a)), k = 1, 2, …, are the eigenfunctions of -d²/dx² with zero boundary values at both ends. This file proves that they form a complete system in L²(a, b): a square integrable function orthogonal to all of them vanishes almost everywhere (TauCeti.ae_eq_zero_of_forall_integral_mul_sin_eq_zero). The theorem does not assume a < b: when b ≤ a the interval (a, b] is empty, so the restricted measure is zero and the conclusion holds trivially.

For a < b, the proof reduces to Mathlib's completeness of the exponentials on a circle. Extend g oddly about a to [2a - b, b]. On this interval of length 2(b - a), the n-th Fourier coefficient of the odd extension is a nonzero multiple of ∫ g(x) sin (n π (x - a) / (b - a)) dx, so all of them vanish, and Parseval's identity (hasSum_sq_fourierCoeffOn) forces the extension, hence g, to vanish almost everywhere. The first step is recorded separately: a square integrable function on (a, b] whose Fourier coefficients on [a, b] all vanish is zero almost everywhere (TauCeti.ae_eq_zero_of_forall_fourierCoeffOn_eq_zero).

Main results

• TauCeti.ae_eq_zero_of_forall_fourierCoeffOn_eq_zero: uniqueness of Fourier coefficients of square integrable functions on an interval.
• TauCeti.ae_eq_zero_of_forall_integral_mul_sin_eq_zero: completeness of the sine system sin (k π (x - a) / (b - a)), k ≥ 1, in L²(a, b).

References

• G. B. Folland, Fourier Analysis and its Applications, Section 2.4 (odd extensions and Fourier sine series) and Section 3.4 (completeness of the trigonometric system).

theorem TauCeti.ae_eq_zero_of_forall_fourierCoeffOn_eq_zero {a b : ℝ} (hab : a < b) {f : ℝ → ℂ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) (h : ∀ (n : ℤ), fourierCoeffOn hab f n = 0) : f =ᵐ[MeasureTheory.volume.restrict (Set.Ioc a b)] 0

A square integrable function with vanishing Fourier coefficients is zero. If f is square integrable on (a, b] and every Fourier coefficient of f on [a, b] vanishes, then f = 0 almost everywhere on (a, b]. This is Parseval's identity hasSum_sq_fourierCoeffOn.

Completeness of the sine system

theorem TauCeti.ae_eq_zero_of_forall_integral_mul_sin_eq_zero {a b : ℝ} {g : ℝ → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) (h : ∀ (k : ℕ), 0 < k → ∫ (x : ℝ) in a..b, g x * Real.sin (↑k * Real.pi * (x - a) / (b - a)) = 0) : g =ᵐ[MeasureTheory.volume.restrict (Set.Ioc a b)] 0

Completeness of the Fourier sine system. A function g square integrable on (a, b] with

∫ x in a..b, g x * sin (k π (x - a) / (b - a)) = 0 for every k ≥ 1

vanishes almost everywhere on (a, b]. For a < b these sines are the Dirichlet eigenfunctions of -d²/dx² on (a, b), so this is the completeness half of the Fourier sine expansion. For b ≤ a the interval (a, b] is empty, the restricted measure is zero, and the conclusion holds trivially.