Ball's lemma for K_p(f) is 1D Borell–Brascamp–Lieb at exponent -1/(p+1)

If you have one-dimensional BBL for negative exponents (h((a+b)/2) ≥ M_{p'}(F a, G b) ⇒ ∫h ≥ M_{p'/(p'+1)}(∫F, ∫G), p' ∈ (-1,0)), Ball's lemma for weighted ray integrals I(φ)=∫₀^∞ r^{p-1}φ(r)dr needs no separate level-set proof: substitute a = 1/r, F(a) = f(1/a)·a^{-(p+1)} (then ∫F = I(f) via the existing r ↦ 1/r change of variables plus a⁻¹^(p-1)·a⁻¹^2 = a^{-(p+1)}), and weighted AM–GM with weights a/(a+b), b/(a+b) shows H((a+b)/2) ≥ M_{-1/(p+1)}^{1/2}(F a, G b). The conclusion exponent (-1/(p+1))/(-1/(p+1)+1) = -1/p is exactly Ball's. In Lean, handle X,Y ∈ {0, ⊤} in ℝ≥0∞ first (top_rpow_of_pos, rpow_ne_zero_of_pos), then pull to reals with powerMean_ofReal. Homogeneity of the gauge: setLIntegral_congr_fun on Ioi (to use r > 0 for Real.mul_rpow), then lintegral_const_mul' and the dilation lemma.