Theorems · Theorem · measure theory

MeasureTheory.lintegral_eq_lintegral_meas_lt

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

The standard case 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 ∂μ = ∫⁻ t in 0..∞, μ {ω | f(ω) > t}. See lintegral_eq_lintegral_meas_le for a version with sets of the form {ω | f(ω) ≥ t} instead.

Defined in

Mathlib.MeasureTheory.Integral.Layercake

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpace