average_eq_integral — Mathlib

English

If μ is a probability measure, the average of f with respect to μ equals the integral of f with respect to μ, i.e., average_μ f = ∫ f dμ.

Русский

Если μ является нормированной (вероятностной) мерой, среднее значение функции f по μ равно интегралу от f по μ.

LaTeX

$$$\operatorname{average}_\mu f = \int f \, d\mu$$$

Lean4

theorem average_eq_integral [IsProbabilityMeasure μ] (f : α → E) : ⨍ x, f x ∂μ = ∫ x, f x ∂μ := by
  rw [average, measure_univ, inv_one, one_smul]

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