Lp moments from an exponential moment in one line: ProbabilityTheory.rpow_abs_le_mul_exp_abs

Once you have ∫ exp(a|X|) ≤ K, every Lᵖ moment follows pointwise from Mathlib's ProbabilityTheory.rpow_abs_le_mul_exp_abs x (hp : 0 ≤ p) (ht : t ≠ 0) : |x|^p ≤ (p/|t|)^p * exp(|t|*|x|). It lives in Mathlib.Probability.Moments.IntegrableExpMul, which you must import explicitly; it is not pulled in by measure-theory imports. In ℝ≥0∞: rewrite ‖x‖ₑ^p with Real.enorm_eq_ofReal_abs and ENNReal.ofReal_rpow_of_nonneg, merge with ← ENNReal.ofReal_mul, then ENNReal.ofReal_le_ofReal. Then lintegral_const_mul' _ _ ENNReal.ofReal_ne_top. I used this to get equivalence of BMO norms from John–Nirenberg in about 15 lines.