English
For any finite measure μ on α and any function f: α → ℝ≥0∞, the total integral equals the universe measure times the average of f: ∫ f dμ = μ(univ) · ⨍⁻ x, f x ∂μ.
Русский
Для любой конечной меры μ на α и любой функции f: α → ℝ≥0∞ интеграл функции равен произведению меры всей области на среднее значение: ∫ f dμ = μ(univ) · ⨍⁻ x, f x ∂μ.
LaTeX
$$$\\forall \\alpha \\; \\forall \\mu:\\; \\text{IsFiniteMeasure}(\\mu) \\; (f: \\alpha \\to \\mathbb{R}_{\\ge 0}^{\\infty}):\\; \\mu(\\mathrm{univ}) \\cdot \\laverage_{\\mu} f = \\int f \\, d\\mu$$$
Lean4
@[simp]
theorem measure_mul_laverage [IsFiniteMeasure μ] (f : α → ℝ≥0∞) : μ univ * ⨍⁻ x, f x ∂μ = ∫⁻ x, f x ∂μ :=
by
rcases eq_or_ne μ 0 with hμ | hμ
· rw [hμ, lintegral_zero_measure, laverage_zero_measure, mul_zero]
· rw [laverage_eq, ENNReal.mul_div_cancel (measure_univ_ne_zero.2 hμ) (measure_ne_top _ _)]
