Theorems · Theorem · measure theory

MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul

∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → ℝ},
  0 ≤ᵐ[μ] f →
    AEMeasurable f μ →
      ∀ {p : ℝ},
        0 < p →
          ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
            ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a} * ENNReal.ofReal (t ^ (p - 1))

An application of the layer cake formula / Cavalieri's principle / tail probability formula: For a nonnegative function f on a measure space, the Lebesgue integral of f can be written (roughly speaking) as: ∫⁻ f^p ∂μ = p * ∫⁻ t in 0..∞, t^(p-1) * μ {ω | f(ω) > t}. See MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul for a version with sets of the form {ω | f(ω) ≥ t} instead.

Defined in

Mathlib.Analysis.SpecialFunctions.Pow.Integral

Cited by

0 results in Mathlib

Foundations

Depth 271 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpace