setAverage_eq — Mathlib

English

For a set s, the average with respect to the restricted measure μ|s equals the integral over s divided by μ(s): average_{μ|s} f = (μ(s))^{-1} ∫_s f dμ.

Русский

Среднее по мере, ограниченной множеством s, равно интегралу по s, делённому на μ(s).

LaTeX

$$$\operatorname{average}_{\mu|_s} f = (\mu(s))^{-1} \int_{s} f \, d\mu$$$

Lean4

theorem setAverage_eq (f : α → E) (s : Set α) : ⨍ x in s, f x ∂μ = (μ.real s)⁻¹ • ∫ x in s, f x ∂μ := by
  rw [average_eq, measureReal_restrict_apply_univ]

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