measure_smul_average — Mathlib

English

If μ is finite, then multiplying the average of f by the total mass μ(α) recovers the integral of f: μ(α) · average_μ f = ∫ f dμ.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem measure_smul_average [IsFiniteMeasure μ] (f : α → E) : μ.real univ • ⨍ x, f x ∂μ = ∫ x, f x ∂μ :=
  by
  rcases eq_or_ne μ 0 with hμ | hμ
  · rw [hμ, integral_zero_measure, average_zero_measure, smul_zero]
  · rw [average_eq, smul_inv_smul₀]
    refine (ENNReal.toReal_pos ?_ <| measure_ne_top _ _).ne'
    rwa [Ne, measure_univ_eq_zero]

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