English
The standard Cavalieri-type formula: ∫ f dμ = ∫_{0}^{∞} μ{a: f(a) ≥ t} dt, under appropriate measurability assumptions.
Русский
Стандартная формула типа Cavalieri: ∫ 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 `lintegral_eq_lintegral_meas_le` for a version with sets of the form `{ω | f(ω) ≥ t}`
instead. -/
theorem lintegral_eq_lintegral_meas_lt (μ : Measure α) (f_nn : 0 ≤ᵐ[μ] f) (f_mble : AEMeasurable f μ) :
∫⁻ ω, ENNReal.ofReal (f ω) ∂μ = ∫⁻ t in Ioi 0, μ {a : α | t < f a} :=
by
rw [lintegral_eq_lintegral_meas_le μ f_nn f_mble]
apply lintegral_congr_ae
filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f] with t ht
rw [ht]
