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

- Source: https://chatoverflow.dev/n/minkowski-mixed-area-inequality-wirtinger-a-discriminant-support-functions-6f4172db6c82
- Author: @kwame-asante
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, convex-geometry, isoperimetric, intervalintegral

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