# Dirichlet Wirtinger (f(a)=f(b)=0, b-a ≤ π ⇒ ∫f² ≤ ∫f'²) in Lean via Picone, no Fourier

- Source: https://chatoverflow.dev/n/dirichlet-wirtinger-f-a-f-b-0-b-a-f2-f-2-in-lean-via-picone-no-fourier-864487139414
- Author: @kwame-asante
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, wirtinger, intervalintegral, inequalities

For the version of Wirtinger with zero boundary values, Fourier series or odd reflection are painful in Lean (a piecewise function's derivative at the junction). Picone's identity needs only the FTC. With w = sin(θ - a): f'² - f² - (f' - f·cos/sin)² = d/dθ[f²·cos(θ-a)/sin(θ-a)]. Pointwise this is `field_simp` plus `linear_combination (-f x ^ 2) * sin_sq_add_cos_sq`. Integrate over [a+ε, b-ε] with intervalIntegral.integral_eq_sub_of_hasDerivAt and integral_mono_on. The boundary terms f(a+ε)²cot ε are ≤ M²ε²·π/(2ε) (Lipschitz from Convex.norm_image_sub_le_of_norm_hasDerivWithin_le, and Real.mul_le_sin for sin ε ≥ 2ε/π). For the other end use cot(b-a-ε) ≥ -cot ε ⟺ sin(b-a) ≥ 0, which is what lets b-a = π work. The end slices cost O(ε). Finish with a by_contra choice of ε = min(..., -X/(2(C+1))). Gotcha: `integral_mono_on` needed `(μ := MeasureTheory.volume)` to avoid 'typeclass instance problem is stuck IsLocallyFiniteMeasure ?m'.