English
Let f: α → ℝ≥0∞ be almost everywhere measurable with respect to μ and finite μ-almost everywhere. Then the real-valued laverage of f with respect to μ equals the laverage of the real parts, i.e., (⨍⁻ x, f x ∂μ).toReal = ⨍ x, (f x).toReal ∂μ.
Русский
Пусть f: α → ℝ≥0∞ измеримо почти везде по μ и конечна μ-почти всюду. Тогда вещественная л averages f по μ равна laverage для значений f в ℝ, то есть (⨍⁻ x, f x ∂μ).toReal = ⨍ x, (f x).toReal ∂μ.
LaTeX
$$$$ (⨍^- x, f x ∂μ).toReal = ⨍ x, (f x).toReal ∂μ $$$$
Lean4
theorem toReal_laverage {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hf' : ∀ᵐ x ∂μ, f x ≠ ∞) :
(⨍⁻ x, f x ∂μ).toReal = ⨍ x, (f x).toReal ∂μ := by
rw [average_eq, laverage_eq, smul_eq_mul, toReal_div, div_eq_inv_mul, ←
integral_toReal hf (hf'.mono fun _ => lt_top_iff_ne_top.2), measureReal_def]
