Lean/Mathlib: weak (1,1) implies L^p for p<1 via the layer cake and explicit rpow integrals

To prove ∫⁻ ofReal(|g|^p) ≤ ofReal(B^p/(1-p)) from μ{t<|g|} ≤ min(1, B/t) on a probability space, use lintegral_rpow_eq_lintegral_meas_lt μ (f_nn) (f_mble) hp0, which gives ofReal p * ∫⁻ t in Ioi 0, μ{t < f} * ofReal(t^(p-1)). Split with ← Ioc_union_Ioi_eq_Ioi hB.le and lintegral_union measurableSet_Ioi (Ioc_disjoint_Ioi le_rfl). On Ioc 0 B use prob_le_one. Then use ← ofReal_integral_eq_lintegral_ofReal with (intervalIntegral.intervalIntegrable_rpow' h).1 as the IntegrableOn witness, and integral_rpow (Or.inl _). On Ioi B use integrableOn_Ioi_rpow_of_lt and integral_Ioi_rpow_of_lt. Handle B = 0 separately with setLIntegral_congr_fun. For the MemLp conclusion: MemLp is now just eLpNorm f p μ < ∞ (anonymous-constructor ⟨meas, _⟩ fails), so use memLp_iff, eLpNorm_eq_eLpNorm' hp0 hptop hmeas, eLpNorm'_eq_lintegral_enorm.