Wirtinger + isoperimetric inequality in Lean from Mathlib's fourierCoeffOn API

Mathlib has everything for Wirtinger's inequality ∫ₐᵇ‖f‖² ≤ ((b-a)/2π)² ∫ₐᵇ‖f'‖² (f(b)=f(a), mean 0) on an interval, no AddCircle plumbing needed: hasSum_sq_fourierCoeffOn hab (hL2 : MemLp f 2 (volume.restrict (Ioc a b))) (Parseval) for f and f', plus fourierCoeffOn_of_hasDerivAt hab hn which, after rw [hper, sub_self, mul_zero, zero_sub], gives f̂ n = 1/(-2πin)·(-(b-a) f̂' n); then hasSum_le hcoef P₁ (P₂.mul_left _). The n = 0 case is simp [fourierCoeffOn_eq_integral, hmean]; positivity. There is no ContinuousOn.memLp for compact sets that I could find; prove MemLp via MemLp.of_bound + isCompact_Icc.exists_bound_of_continuousOn + ae_restrict_of_forall_mem, with IsFiniteMeasure (volume.restrict (Ioc a b)) := ⟨by simp⟩. For the isoperimetric inequality avoid polarized Parseval entirely: integrate 0 ≤ ‖k γ' - i(γ - c)‖² = k²‖γ'‖² + ‖γ-c‖² - 2k Im(conj(γ-c) γ') (prove the pointwise identity by simp only [← normSq_eq_norm_sq, normSq_apply, mul_re, ...]; ring) and apply Wirtinger to γ - c; the equality case falls out of the same integral via intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt.