Wirtinger's inequality for periodic functions

Let f : ℝ → V be an absolutely continuous function on [a, b] with f a = f b, valued in a finite-dimensional real inner product space, whose almost-everywhere derivative f' is square integrable. Wirtinger's inequality bounds the L² distance of f from its mean by its derivative, with the sharp constant:

∫ x in a..b, ‖f x - ⨍ y in a..b, f y‖ ^ 2 ≤ ((b - a) / (2π)) ^ 2 * ∫ x in a..b, ‖f' x‖ ^ 2 (TauCeti.integral_norm_sub_average_sq_le).

Equality holds exactly when f is its mean plus a first harmonic, that is, when there are u v : V with f t = ⨍ y in a..b, f y + cos (2π t / (b - a)) • u + sin (2π t / (b - a)) • v for every t ∈ [a, b] (TauCeti.integral_norm_sub_average_sq_eq_iff). Taking V = ℂ gives the complex-valued statements.

The proof is Fourier-analytic: for an absolutely continuous closed curve the n-th Fourier coefficient of f' on [a, b] is that of f multiplied by 2πin / (b - a) (TauCeti.hasSum_sq_frequency_mul_sq_fourierCoeffOn), the zeroth coefficient of f minus its mean vanishes, and Parseval's identity (hasSum_sq_fourierCoeffOn) turns the coefficientwise comparison into the inequality. Equality forces every coefficient of frequency |n| ≥ 2 to vanish, and a continuous closed curve with finitely many nonzero coefficients is the sum of its Fourier series at every point. Vector values reduce to complex scalars coordinatewise in an orthonormal basis. No smoothness beyond absolute continuity is assumed.

Together with the Cauchy--Schwarz inequality it bounds the integral of any continuous bilinear form along a loop: since ∫ B(m, f') = B(m, f b - f a) = 0 for the mean m,

‖∫ x in a..b, B (f x) (f' x)‖ ≤ ‖B‖ * ((b - a) / (2π)) * ∫ x in a..b, ‖f' x‖ ^ 2 (ContinuousLinearMap.norm_integral_apply_apply_le).

For B a symplectic form this is the isoperimetric inequality for the symplectic area of a loop, the estimate behind removal of singularities and energy quantization for holomorphic curves.

Main results

• TauCeti.integral_norm_sub_average_sq_le: Wirtinger's inequality.
• TauCeti.integral_norm_sub_average_sq_eq_iff: its equality case.
• ContinuousLinearMap.norm_integral_apply_apply_le: the bound on the integral of a bilinear form along a loop.

References

• G. H. Hardy, J. E. Littlewood and G. Pólya, Inequalities, Cambridge University Press, 1934, Theorem 258 (Wirtinger's inequality).
• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Section 4.4 (the isoperimetric inequality, proved by the same Fourier argument).

theorem TauCeti.integral_norm_sub_average_sq_le {a b : ℝ} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {f f' : ℝ → V} (hab : a < b) (hf : AbsolutelyContinuousOnInterval f a b) (hff' : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt f (f' t) t) (hfab : f a = f b) (hf' : MeasureTheory.MemLp f' 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) : ∫ (x : ℝ) in a..b, ‖f x - ⨍ (y : ℝ) in a..b, f y‖ ^ 2 ≤ ((b - a) / (2 * Real.pi)) ^ 2 * ∫ (x : ℝ) in a..b, ‖f' x‖ ^ 2

Wirtinger's inequality. An absolutely continuous function on [a, b] with f a = f b, valued in a finite-dimensional real inner product space and with square-integrable almost-everywhere derivative, deviates from its mean in L² by at most (b - a) / (2π) times the L² norm of its derivative.

theorem TauCeti.integral_norm_sub_average_sq_eq_iff {a b : ℝ} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {f f' : ℝ → V} (hab : a < b) (hf : AbsolutelyContinuousOnInterval f a b) (hff' : ∀ᵐ (t : ℝ), t ∈ Set.uIoc a b → HasDerivAt f (f' t) t) (hfab : f a = f b) (hf' : MeasureTheory.MemLp f' 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) : ∫ (x : ℝ) in a..b, ‖f x - ⨍ (y : ℝ) in a..b, f y‖ ^ 2 = ((b - a) / (2 * Real.pi)) ^ 2 * ∫ (x : ℝ) in a..b, ‖f' x‖ ^ 2 ↔ ∃ (u : V) (v : V), ∀ t ∈ Set.Icc a b, f t - ⨍ (y : ℝ) in a..b, f y = Real.cos (2 * Real.pi * t / (b - a)) • u + Real.sin (2 * Real.pi * t / (b - a)) • v

Equality in Wirtinger's inequality. Equality holds exactly when, on [a, b], the function is its mean plus a first harmonic cos (2π t / (b - a)) • u + sin (2π t / (b - a)) • v.

theorem ContinuousLinearMap.norm_integral_apply_apply_le {a b : ℝ} {V : Type u_1} {G : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : V →L[ℝ] V →L[ℝ] G) (hab : a < b) {f f' : ℝ → V} (hf : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (hfab : f a = f b) (hf' : MeasureTheory.MemLp f' 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) : ‖∫ (x : ℝ) in a..b, (B (f x)) (f' x)‖ ≤ ‖B‖ * ((b - a) / (2 * Real.pi)) * ∫ (x : ℝ) in a..b, ‖f' x‖ ^ 2

Along a loop f on [a, b] with square-integrable derivative, the integral of a continuous bilinear form B (f x) (f' x) is bounded by ‖B‖ (b - a) / (2π) times the L² energy of the loop. For a symplectic form B the left side is twice the symplectic area enclosed by the loop, and this is the isoperimetric inequality.