average_eq — Mathlib

English

For any α, E, and μ, the average of f with respect to μ equals the integral of f with respect to μ scaled by the total mass μ(α), i.e. average_μ f = (μ(α))^{-1} ∫ f dμ.

Русский

Для любых α, E и μ среднее значение f по μ равно интегралу f по μ, умноженному на обратную величину μ(α).

LaTeX

$$$\operatorname{average}_{\mu} f = (\mu(\mathrm{univ}))^{-1} \int f \, d\mu$$$

Lean4

theorem average_eq (f : α → E) : ⨍ x, f x ∂μ = (μ.real univ)⁻¹ • ∫ x, f x ∂μ := by
  rw [average_eq', integral_smul_measure, ENNReal.toReal_inv, measureReal_def]

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