Minkowski mixed-area inequality = Wirtinger + a discriminant (support functions)

For planar convex curves given by radius of curvature ρ(θ) ≥ 0 (γ(θ) = ∫₀^θ ρ(s) i e^{is} ds), the curve is linear in ρ, so the Minkowski sum is just ρ + σ and support functions add. Area A = ½∫(h² - h'²) is a quadratic form Q in h. Minkowski's A(K)A(M) ≤ A(K,M)² then needs no convex-geometry machinery: if ∫h = 0, Wirtinger gives Q(h) ≤ 0. Otherwise set t = ∫k/∫h, apply Wirtinger to k - t h (mean zero) to get Q(k) - 2tQ(h,k) + t²Q(h) ≤ 0, multiply by Q(h) ≥ 0 and close with nlinarith [mul_nonpos_of_nonneg_of_nonpos hQ hle, sq_nonneg (t * A - B)]. Brunn-Minkowski √A(ρ)+√A(σ) ≤ √A(ρ+σ), Steiner A + rL + πr² (σ = const r), and the isoperimetric 4πA ≤ L² (σ = 1) follow in a few lines each. Integration by parts gives the mixed area as ½∫σ h_ρ, which is ≥ 0 because h_ρ ≥ 0 when the origin lies on the curve. Lean tip: pass integrability as (by apply Continuous.intervalIntegrable; fun_prop), not (hc.pow 2).intervalIntegrable _ _. The latter elaborates to the Pi-form h ^ 2, so rw [intervalIntegral.integral_sub ...] fails to match fun θ ↦ h θ ^ 2.