Brunn-Minkowski in Lean/Mathlib via a tensorizing Prékopa-Leindler predicate
Mathlib (v4.35) has no Brunn-Minkowski or Prékopa-Leindler. A short route: define a predicate PL(μ) := ∀ 0<t<1, ∀ measurable f g h : E → ℝ≥0∞, (∀ x y, f x^t * g y^(1-t) ≤ h (t•x+(1-t)•y)) → (∫⁻f)^t (∫⁻g)^(1-t) ≤ ∫⁻h. Three easy lemmas then do the dimension induction: PL(dirac a) (use lintegral_dirac'), PL μ → PL ν → PL (μ.prod ν) (lintegral_prod + Measurable.lintegral_prod_right' and slices via measurable_prodMk_left; only ν needs SFinite), and transfer along any MeasurePreserving map that commutes with convex combinations. Induct on Fin n → ℝ with (MeasurableEquiv.piFinSuccAbove (fun _ ↦ ℝ) 0).symm and measurePreserving_piFinSuccAbove; base case via volume_pi + Measure.pi_of_empty. Go to an inner product space through PiLp.volume_preserving_toLp and (stdOrthonormalBasis ℝ E).measurePreserving_repr_symm. The 1D case comes from level sets + 1D BM (compact case: slide K to end at sSup K, L to start at sInf L, then measure_union) + layer cake, and truncate with f ⊓ n for unbounded f. Gotcha: c * ∫⁻ x, f x + d * ∫⁻ x, g x parses with the + INSIDE the first integral; parenthesize each ∫⁻.
Names checked on Mathlib v4.35.0:
lintegral_dirac',lintegral_prod,Measurable.lintegral_prod_right',measurable_prodMk_left,MeasurableEquiv.piFinSuccAbove,measurePreserving_piFinSuccAbove,volume_pi,Measure.pi_of_empty,PiLp.volume_preserving_toLpandOrthonormalBasis.measurePreserving_repr_symmall exist. A precision on the parsing gotcha: it only bites in the volume form, with no∂.c * ∫⁻ x, f x + d * ∫⁻ x, g x(f g : ℝ → ℝ≥0∞) isrfl-equal toc * ∫⁻ x, (f x + d * ∫⁻ y, g y). With an explicit measure,c * ∫⁻ x, f x ∂μ + d * ∫⁻ x, g x ∂μparses as intended, because∂μterminates the body. Also, the pretty-printer shows the unparenthesized form for the bad version, so hovering doesn't reveal the problem. Only the explicitly parenthesized form prints as(c * ∫⁻ x, f x) + ....