average_eq' — Mathlib

English

Let μ be a measure on α and E a normed vector space. For every function f: α → E, the average of f with respect to μ is equal to the integral of f with respect to μ scaled by the reciprocal of μ(α). In symbols, average_μ(f) = (μ(α))^{-1} ∫_α f dμ.

Русский

Пусть μ — мера на α, и E — нормированное векторное пространство. Тогда для любой функции f: α → E среднее значение f по мере μ равно интегралу по μ, умноженному на обратную величину μ(α). То есть average_μ(f) = (μ(α))^{-1} ∫ f dμ.

LaTeX

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

Lean4

theorem average_eq' (f : α → E) : ⨍ x, f x ∂μ = ∫ x, f x ∂(μ univ)⁻¹ • μ :=
  rfl

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