English
For a nonnegative measurable function f on a measure space, the integral of f equals the tail integral over t > 0 of the measure of the superlevel set {a : f(a) ≥ t}: ∫ f dμ = ∫_{0}^{∞} μ{a : f(a) ≥ t} dt.
Русский
Для неотрицимой измеримой функции f на мере μ верна формула слоя: ∫ f dμ = ∫_{0}^{∞} μ{a : f(a) ≥ t} dt.
LaTeX
$$$$ \\int f \\; d\\mu = \\int_{0}^{\\infty} \\mu\\{a : f(a) \\ge t\\} \, dt. $$$$
Lean4
/-- 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 `MeasureTheory.lintegral_eq_lintegral_meas_lt` for a version with sets of the form
`{ω | f(ω) > t}` instead. -/
theorem lintegral_eq_lintegral_meas_le (μ : Measure α) (f_nn : 0 ≤ᵐ[μ] f) (f_mble : AEMeasurable f μ) :
∫⁻ ω, ENNReal.ofReal (f ω) ∂μ = ∫⁻ t in Ioi 0, μ {a : α | t ≤ f a} :=
by
set cst := fun _ : ℝ => (1 : ℝ)
have cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t := fun _ _ => intervalIntegrable_const
have key :=
lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble cst_intble (Eventually.of_forall fun _ => zero_le_one)
simp_rw [cst, ENNReal.ofReal_one, mul_one] at key
rw [← key]
congr with ω
simp only [intervalIntegral.integral_const, sub_zero, Algebra.id.smul_eq_mul, mul_one]
