The sharp spectral gap on the circle

For a mean-zero complex L² function on the circle, its squared norm is at most the sum of n² times its squared Fourier coefficients, provided this spectral energy is summable. Equality holds exactly on the span of the two first harmonics. The Haar measure in these statements has total mass one.

This is the spectral comparison underlying the sharp periodic Wirtinger inequality and its equality case. It does not assume differentiability: identifying the spectral energy with a derivative integral is a separate integration-by-parts step. In particular, the equality conclusion remains available when that step uses only a weak or an almost-everywhere derivative.

The proofs use Mathlib's Fourier Hilbert basis and Parseval identity.

The interval versions below identify first harmonics by their Fourier support. They provide the bridge between the abstract circle equality case and cosine--sine formulas on a real interval.

References

• G. H. Hardy, J. E. Littlewood and G. Pólya, Inequalities, Theorem 258.

theorem TauCeti.fourierCoeffOn_cos_smul_add_sin_smul {a b : ℝ} (hab : a < b) (u v : ℂ) {n : ℤ} (hn₁ : n ≠ 1) (hn₂ : n ≠ -1) : fourierCoeffOn hab (fun (t : ℝ) => Real.cos (2 * Real.pi * t / (b - a)) • u + Real.sin (2 * Real.pi * t / (b - a)) • v) n = 0

A first harmonic on [a, b] has no Fourier coefficients outside the frequencies ±1.

theorem TauCeti.exists_cos_smul_add_sin_smul {a b : ℝ} (hab : a < b) {g : ℝ → ℂ} (hg : ContinuousOn g (Set.Icc a b)) (hgab : g a = g b) (h : ∀ (n : ℤ), n ≠ 1 → n ≠ -1 → fourierCoeffOn hab g n = 0) : ∃ (u : ℂ) (v : ℂ), ∀ t ∈ Set.Icc a b, g t = Real.cos (2 * Real.pi * t / (b - a)) • u + Real.sin (2 * Real.pi * t / (b - a)) • v

A continuous closed curve on [a, b] whose Fourier coefficients vanish outside the frequencies ±1 is a first harmonic at every point of [a, b].

theorem TauCeti.integral_norm_sq_le_tsum_frequency_sq_fourierCoeff {T : ℝ} [Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (hzero : fourierCoeff (↑↑f) 0 = 0) (henergy : Summable fun (n : ℤ) => ↑n ^ 2 * ‖fourierCoeff (↑↑f) n‖ ^ 2) : ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂AddCircle.haarAddCircle ≤ ∑' (n : ℤ), ↑n ^ 2 * ‖fourierCoeff (↑↑f) n‖ ^ 2

The sharp spectral-gap inequality for a mean-zero L² function on the circle. Summability is essential: an unsummable real tsum would otherwise be zero.

theorem TauCeti.integral_norm_sq_eq_tsum_frequency_sq_fourierCoeff_iff {T : ℝ} [Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (hzero : fourierCoeff (↑↑f) 0 = 0) (henergy : Summable fun (n : ℤ) => ↑n ^ 2 * ‖fourierCoeff (↑↑f) n‖ ^ 2) : ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂AddCircle.haarAddCircle = ∑' (n : ℤ), ↑n ^ 2 * ‖fourierCoeff (↑↑f) n‖ ^ 2 ↔ ∃ (a : ℂ) (b : ℂ), f = a • fourierLp 2 1 + b • fourierLp 2 (-1)

Equality in the circle spectral gap holds exactly for linear combinations of its positive and negative first harmonics. Equality is in L², hence is independent of the choice of almost-everywhere representative.

theorem MeasureTheory.Lp.fourierCoeff_eq_zero_of_integral_norm_sq_eq_tsum_frequency_sq {T : ℝ} [Fact (0 < T)] (f : ↥(Lp ℂ 2 AddCircle.haarAddCircle)) (hzero : fourierCoeff (↑↑f) 0 = 0) (henergy : Summable fun (n : ℤ) => ↑n ^ 2 * ‖fourierCoeff (↑↑f) n‖ ^ 2) (heq : ∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂AddCircle.haarAddCircle = ∑' (n : ℤ), ↑n ^ 2 * ‖fourierCoeff (↑↑f) n‖ ^ 2) {n : ℤ} (hn₁ : n ≠ 1) (hn₂ : n ≠ -1) : fourierCoeff (↑↑f) n = 0

If an L² class on the circle has vanishing zeroth Fourier coefficient, summable n² ‖ĝ n‖², and squared norm equal to ∑ n² ‖ĝ n‖², then every Fourier coefficient of frequency other than ±1 vanishes.