ofReal_average — Mathlib

English

For real-valued f integrable and a.e. nonnegative, ENNReal.ofReal(average_μ f) equals lintegral of ENNReal.ofReal(f) divided by μ univ.

Русский

Для действительностной f интегрируемой и неотрицательной почти повсюду, ENNReal.ofReal(average_μ f) равен линегралу ENNReal.ofReal(f) делённому на μ univ.

LaTeX

$$$\text{ENNReal.ofReal}(\operatorname{average}_\mu f) = \dfrac{\int ENNReal.ofReal(f) \, d\mu}{\mu(\mathrm{univ})}$$$

Lean4

theorem ofReal_average {f : α → ℝ} (hf : Integrable f μ) (hf₀ : 0 ≤ᵐ[μ] f) :
    ENNReal.ofReal (⨍ x, f x ∂μ) = (∫⁻ x, ENNReal.ofReal (f x) ∂μ) / μ univ :=
  by
  obtain rfl | hμ := eq_or_ne μ 0
  · simp
  ·
    rw [average_eq, smul_eq_mul, measureReal_def, ← toReal_inv, ofReal_mul toReal_nonneg,
      ofReal_toReal (inv_ne_top.2 <| measure_univ_ne_zero.2 hμ), ofReal_integral_eq_lintegral_ofReal hf hf₀,
      ENNReal.div_eq_inv_mul]

Похожие утверждения