English
For an integrable a.e.-nonnegative function f, the Bochner integral ∫ f equals ∫_0^∞ μ{a: t < f(a)} dt.
Русский
Для интегрируемой по а.е. неотрицательной функции f справедлива формула Лебега: ∫ f dμ = ∫_0^∞ μ{a: t < f(a)} dt.
LaTeX
$$$$ \\int f \\, d\\mu = \\int_{0}^{\\infty} \\mu\\{a : t < f(a)\\} \\, dt. $$$$
Lean4
/-- The standard case of the layer cake formula / Cavalieri's principle / tail probability formula:
For an integrable a.e.-nonnegative real-valued function `f`, the Bochner 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 Lebesgue integral `∫⁻`
instead. -/
theorem integral_eq_integral_meas_lt (f_intble : Integrable f μ) (f_nn : 0 ≤ᵐ[μ] f) :
∫ ω, f ω ∂μ = ∫ t in Set.Ioi 0, μ.real {a : α | t < f a} :=
by
have key := lintegral_eq_lintegral_meas_lt μ f_nn f_intble.aemeasurable
have lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞ := Integrable.lintegral_lt_top f_intble
have rhs_finite : ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a} < ∞ := by simp only [← key, lhs_finite]
have rhs_integrand_finite : ∀ (t : ℝ), t > 0 → μ {a | t < f a} < ∞ := fun t ht ↦ measure_gt_lt_top f_intble ht
convert (ENNReal.toReal_eq_toReal lhs_finite.ne rhs_finite.ne).mpr key
· exact integral_eq_lintegral_of_nonneg_ae f_nn f_intble.aestronglyMeasurable
· have aux :=
@integral_eq_lintegral_of_nonneg_ae _ _ ((volume : Measure ℝ).restrict (Set.Ioi 0))
(fun t ↦ μ.real {a : α | t < f a}) ?_ ?_
· rw [aux]
congr 1
apply setLIntegral_congr_fun measurableSet_Ioi
exact fun t t_pos ↦ ENNReal.ofReal_toReal (rhs_integrand_finite t t_pos).ne
· exact Eventually.of_forall (fun x ↦ by positivity)
· apply Measurable.aestronglyMeasurable
refine Measurable.ennreal_toReal ?_
exact Antitone.measurable (fun _ _ hst ↦ measure_mono (fun _ h ↦ lt_of_le_of_lt hst h))
