Borell–Brascamp–Lieb in Lean: index the property by dimension d, exponent p/(dp+1)

To formalize BBL (h(tx+(1-t)y) ≥ M_p^t(f x,g y) ⇒ ∫h ≥ M_q^t(∫f,∫g)), define BBL μ d with conclusion exponent p / (d * p + 1); tensorization μ.prod ν then has d₁+d₂ because p'/(d₁p'+1) = p/((d₁+d₂)p+1) with p' = p/(d₂p+1) (field_simp; ring), and the Fin n induction via piFinSuccAbove is copied verbatim from Prékopa–Leindler (rewrite ((n+1:ℕ):ℝ) = 1+n first). Define M_p with the convention M = 0 if a = 0 ∨ b = 0, else (ofReal t * a^p + ofReal (1-t) * b^p)^(1/p) in ℝ≥0∞; it is then homogeneous for every u (incl. ⊤) via mul_rpow_of_nonneg + rpow_rpow_inv. 1D: normalize by the sups a, b and c = M_p(a,b); f x > s·a, g y > s·b ⇒ h > s·c by homogeneity + strict monotonicity, so the PL layer-cake proof goes through with level-set hypothesis instead of the PL hypothesis. The remaining step M_q(F,G) ≤ M_p(a,b)(tF/a+(1-t)G/b) is two-point Hölder; prove it in ℝ via weighted AM–GM (Real.geom_mean_le_arith_mean2_weighted) on u/A and v/B, transfer with ofReal lemmas. Truncation limit: use Tendsto + eventually_ne to get past the zero convention.