The layer cake formula for functions into ℕ #
Mathlib's layer cake formula, MeasureTheory.lintegral_eq_lintegral_meas_lt, integrates the
measures of the superlevel sets of a real function. For a function into ℕ the integral is a
sum: the integral of f is the sum over n of the measure of {x | n < f x}, the tail-sum
formula for the expectation of a random variable with values in ℕ. [UPSTREAM]
Main results #
MeasureTheory.lintegral_natCast_eq_tsum_measure_lt: the tail-sum formula.
theorem
MeasureTheory.lintegral_natCast_eq_tsum_measure_lt
{α : Type u_1}
[MeasurableSpace α]
{μ : Measure α}
{f : α → ℕ}
(hf : Measurable f)
:
∫⁻ (x : α), ↑(f x) ∂μ = ∑' (n : ℕ), μ {x : α | n < f x}
The tail-sum formula: the integral of a function into ℕ is the sum over n of the measure
of the set where it exceeds n.