English
For f: α → ℝ≥0∞ that is a.e. measurable and finite μ-almost everywhere, the real integral of its toReal value equals the real part of its Lintegral: ∫ a (f(a)).toReal dμ = (∫⁻ a f(a) dμ).toReal.
Русский
Для f: α → ℝ≥0∞, измеримого почти повсюду и конечного почти по μ, реальный интеграл значения toReal равен действительной частью линтеграла: ∫ a f(a).toReal dμ = (∫⁻ a f(a) dμ).toReal.
LaTeX
$$$\\\\int a \\, (f(a)).toReal \\, d\\\\mu \\\\;=\\\\; (\\\\int⁻ a \\, f(a) \\, d\\\\mu)\\\\.toReal$$$
Lean4
theorem integral_toReal {f : α → ℝ≥0∞} (hfm : AEMeasurable f μ) (hf : ∀ᵐ x ∂μ, f x < ∞) :
∫ a, (f a).toReal ∂μ = (∫⁻ a, f a ∂μ).toReal :=
by
rw [integral_eq_lintegral_of_nonneg_ae _ hfm.ennreal_toReal.aestronglyMeasurable,
lintegral_congr_ae (ofReal_toReal_ae_eq hf)]
exact Eventually.of_forall fun x => ENNReal.toReal_nonneg
