measure_smul_setAverage — Mathlib

English

For a finite measure μ, μ(α) times the average equals the integral: μ(α) · average_μ f = ∫ f dμ.

Русский

Для конечной меры μ: μ(α) · average_μ f = ∫ f dμ.

LaTeX

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

Lean4

theorem measure_smul_setAverage (f : α → E) {s : Set α} (h : μ s ≠ ∞) :
    μ.real s • ⨍ x in s, f x ∂μ = ∫ x in s, f x ∂μ :=
  by
  haveI := Fact.mk h.lt_top
  rw [← measure_smul_average, measureReal_restrict_apply_univ]

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