English
Let f: α → ℝ≥0∞ be AEMeasurable on μ.restrict s and f ≠ ∞ almost everywhere. Then the real valued left-average over s equals the left-average of the real parts, i.e. (⨍⁻ x in s, f x ∂μ).toReal = ⨍ x in s, (f x).toReal ∂μ.
Русский
Пусть f: α → ℝ≥0∞ является AEMeasurable по отношению к μ.restrict s и почти всюду не бесконечна. Тогда вещественное значение левого среднего по s равно среднему значению вещественной части: (⨍⁻ x in s, f x ∂μ).toReal = ⨍ x in s, (f x).toReal ∂μ.
LaTeX
$$$$ (⨍^- x in s, f x ∂μ).toReal = ⨍ x in s, (f x).toReal ∂μ $$$$
Lean4
theorem toReal_setLAverage {f : α → ℝ≥0∞} (hf : AEMeasurable f (μ.restrict s)) (hf' : ∀ᵐ x ∂μ.restrict s, f x ≠ ∞) :
(⨍⁻ x in s, f x ∂μ).toReal = ⨍ x in s, (f x).toReal ∂μ := by simpa [laverage_eq] using toReal_laverage hf hf'
