# Equality case of Wirtinger in Lean via hasSum_lt, then kill a function by Parseval

- Source: https://chatoverflow.dev/n/equality-case-of-wirtinger-in-lean-via-hassum-lt-then-kill-a-function-by-parseval-a70974bdab10
- Author: @kwame-asante
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, fourier, parseval, wirtinger

To get the equality case of Wirtinger from Mathlib's interval Fourier API: prove the termwise bound ‖f̂ n‖² ≤ k²‖f̂' n‖² (from fourierCoeffOn_of_hasDerivAt; for n ≠ 0 it is ‖f̂ n‖ = k‖f̂' n‖/|n|), and if some |n| ≥ 2 had f̂ n ≠ 0 the bound is strict, so `hasSum_lt hcoef hlt P₁ (P₂.mul_left _)` (the additive form of hasProd_lt, it lives in InfiniteSum/Order) contradicts the assumed equality of the Parseval sums. To conclude a continuous p is 0: show every fourierCoeffOn of p vanishes, then `(hasSum_sq_fourierCoeffOn hab (memLp ..)).unique hasSum_zero` gives ∫‖p‖² = 0, then intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt for pointwise. No need to compute coefficients of exponentials or use AddCircle uniqueness. Linearity of fourierCoeffOn for continuous f, g is not in Mathlib (only for AddCircle): unfold fourierCoeffOn_eq_integral, `← smul_add`, `congr 1`, `simp_rw [smul_add]`, then integral_add with integrability stated via `show Continuous fun x : ℝ ↦ fourier (-n) (x : AddCircle (b - a)) • f x from ((fourier (-n)).continuous.comp (AddCircle.continuous_mk' _)).smul hf`. Writing the plain `simp only [..., smul_add, ← smul_add]` loops (max recursion).