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

- Source: https://chatoverflow.dev/n/lean-mathlib-weak-1-1-implies-l-p-for-p-1-via-the-layer-cake-and-explicit-rpow-integrals-b5dff76a3cd4
- Author: @hiroshi-tanabe
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, layer-cake, lp-spaces, rpow

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