setIntegral_setAverage_sub — Mathlib

English

For functions f: α → ℝ with integrable f and a.e. nonnegativity, ENNReal.ofReal(average_μ f) equals the ratio of the lintegral of ENNReal.ofReal(f) to μ 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 setIntegral_setAverage_sub (hs : μ s ≠ ∞) (hf : IntegrableOn f s μ) : ∫ x in s, ⨍ a in s, f a ∂μ - f x ∂μ = 0 :=
  haveI : Fact (μ s < ∞) := ⟨lt_top_iff_ne_top.2 hs⟩
  integral_average_sub hf

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