Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.eLpNorm_pow_eq_distribution

Carleson.ToMathlib.WeakType · Carleson/ToMathlib/WeakType.lean:864 to 870

Source documentation

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

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eLpNorm_pow_eq_distribution {f : α → ε} (hf : AEStronglyMeasurable f μ) {p : ℝ≥0} (hp : 0 < p) :    eLpNorm f p μ ^ (p : ℝ) =    ∫⁻ t in Ioi (0 : ℝ), p * ENNReal.ofReal (t ^ ((p : ℝ) - 1)) * distribution f (.ofReal t) μ := by  have h2p : 0 < (p : ℝ) := hp  simp_rw [eLpNorm_nnreal_eq_eLpNorm' hp.ne', eLpNorm', one_div, ← ENNReal.rpow_mul,    inv_mul_cancel₀ h2p.ne', ENNReal.rpow_one, lintegral_norm_pow_eq_distribution hf h2p,    ENNReal.ofReal_mul zero_le_coe, ofReal_coe_nnreal]