English
Let f: α → ℝ be integrable on s with respect to μ and nonnegative almost everywhere on s. Then ENNReal.ofReal of the average of f over s equals the average of ENNReal.ofReal(f) over s, i.e. ENNReal.ofReal (⨍ x in s, f x ∂μ) = (∫⁻ x in s, ENNReal.ofReal (f x) ∂μ) / μ s.
Русский
Пусть f: α → ℝ интегрируема на s по мере μ и неотрицательна μ-подмножество почти всюду на s. Тогда ENNReal.ofReal от среднего значения f по s равно среднему значению ENNReal.ofReal(f) по μ, то есть ENNReal.ofReal (⨍ x in s, f x ∂μ) = (∫⁻ x in s, ENNReal.ofReal (f x) ∂μ) / μ s.
LaTeX
$$$$ \operatorname{ENNReal}.ofReal\left( ⨍ x \in s, f x \partial \mu \right) = \dfrac{ \int^- x \in s, \operatorname{ENNReal}.ofReal(f x) \partial \mu }{ \mu s } $$$$
Lean4
theorem ofReal_setAverage {f : α → ℝ} (hf : IntegrableOn f s μ) (hf₀ : 0 ≤ᵐ[μ.restrict s] f) :
ENNReal.ofReal (⨍ x in s, f x ∂μ) = (∫⁻ x in s, ENNReal.ofReal (f x) ∂μ) / μ s := by
simpa using ofReal_average hf hf₀
