English
A variant of the standard layer cake formula using strict inequality: ∫ f dμ = ∫_{0}^{∞} μ{a : f(a) > t} dt for nonnegative measurable f.
Русский
вариант стандартной формулы слоя с использованием строгого неравенства: ∫ f dμ = ∫_{0}^{∞} μ{a : f(a) > t} dt.
LaTeX
$$$$ \\int f \\, d\\mu = \\int_{0}^{\\infty} \\mu\\{a : f(a) > t\\} \\, dt. $$$$
Lean4
/-- The layer cake formula / Cavalieri's principle / tail probability formula:
Let `f` be a non-negative measurable function on a measure space. Let `G` be an
increasing absolutely continuous function on the positive real line, vanishing at the origin,
with derivative `G' = g`. Then the integral of the composition `G ∘ f` can be written as
the integral over the positive real line of the "tail measures" `μ {ω | f(ω) > t}` of `f`
weighted by `g`.
Roughly speaking, the statement is: `∫⁻ (G ∘ f) ∂μ = ∫⁻ t in 0..∞, g(t) * μ {ω | f(ω) > t}`.
See `lintegral_comp_eq_lintegral_meas_le_mul` for a version with sets of the form `{ω | f(ω) ≥ t}`
instead. -/
theorem lintegral_comp_eq_lintegral_meas_lt_mul (μ : Measure α) (f_nn : 0 ≤ᵐ[μ] f) (f_mble : AEMeasurable f μ)
(g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t) (g_nn : ∀ᵐ t ∂volume.restrict (Ioi 0), 0 ≤ g t) :
∫⁻ ω, ENNReal.ofReal (∫ t in 0..f ω, g t) ∂μ = ∫⁻ t in Ioi 0, μ {a : α | t < f a} * ENNReal.ofReal (g t) :=
by
rw [lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble g_intble g_nn]
apply lintegral_congr_ae
filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f] with t ht
rw [ht]
