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

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'.