Theorems · Theorem · measure theory

MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul

∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ} {g : ℝ → ℝ} (μ : MeasureTheory.Measure α),
  0 ≤ᵐ[μ] f →
    AEMeasurable f μ →
      (∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t) →
        (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), 0 ≤ g t) →
          ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
            ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

The layer cake formula / Cavalieri's principle / tail probability formula: Let f be a non-negative measurable function on a measure space. Let G be an increasing absolutely continuous function on the positive real line, vanishing at the origin, with derivative G' = g. Then the integral of the composition G ∘ f can be written as the integral over the positive real line of the "tail measures" μ {ω | f(ω) ≥ t} of f weighted by g. Roughly speaking, the statement is: ∫⁻ (G ∘ f) ∂μ = ∫⁻ t in 0..∞, g(t) * μ {ω | f(ω) ≥ t}. See MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul for a version with sets of the form {ω | f(ω) > t} instead.

Defined in

Mathlib.MeasureTheory.Integral.Layercake

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpace