Tail Layer-Cake Formula

A real-valued specialization of the layer-cake formula for nonnegative random variables.

Main definitions

This module introduces no new definitions.

Main results

• lintegral_eq_lintegral_tail: a nonnegative function is the integral of its upper tails.

theorem LeanPool.lintegral_eq_lintegral_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX_meas : AEMeasurable X μ) (hX_nonneg : 0 ≤ᵐ[μ] X) : ∫⁻ (ω : Ω), ENNReal.ofReal (X ω) ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, μ {ω : Ω | t ≤ X ω}

The expected value of a non-negative random variable equals the integral of its tail probabilities. This is the layer-cake formula.