Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.eLpNorm_eq_distribution

Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:874 to 886

Source documentation

The layer-cake theorem, or Cavalieri's principle, written using eLpNorm, without taking powers.

Exact Lean statement

lemma eLpNorm_eq_distribution {f : α → ε} (hf : AEStronglyMeasurable f μ) {p : ℝ} (hp : 0 < p) :
    eLpNorm f (.ofReal p) μ =
    (ENNReal.ofReal p  * ∫⁻ t in Ioi (0 : ℝ), distribution f (.ofReal t) μ *
        ENNReal.ofReal (t ^ (p - 1)) ) ^ p⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eLpNorm_eq_distribution {f : α → ε} (hf : AEStronglyMeasurable f μ) {p : ℝ} (hp : 0 < p) :    eLpNorm f (.ofReal p) μ =    (ENNReal.ofReal p  * ∫⁻ t in Ioi (0 : ℝ), distribution f (.ofReal t) μ *        ENNReal.ofReal (t ^ (p - 1)) ) ^ p⁻¹ := by  unfold eLpNorm  split_ifs with sgn_p sz_p  · exact False.elim (not_le_of_gt hp (ofReal_eq_zero.mp sgn_p))  · exact False.elim (coe_ne_top sz_p)  · unfold eLpNorm'    rw [toReal_ofReal hp.le, one_div]    congr 1    rw [← lintegral_const_mul' _ _ (by finiteness), lintegral_norm_pow_eq_distribution hf hp]    congr 1 with x; rw [ofReal_mul] <;> [ring; positivity]