laverage_mul_measure_univ — Mathlib

English

With a finite μ, laverage times μ(univ) equals the lintegral over μ.

Русский

Для конечной μ лаverage умноженное на μ(univ) равно линтегралу по μ.

LaTeX

$$$(\\laverage_{μ} f) \\cdot μ(\\mathrm{univ}) = ∫⁻ x, f x ∂μ$$$

Lean4

@[simp]
theorem laverage_mul_measure_univ (μ : Measure α) [IsFiniteMeasure μ] (f : α → ℝ≥0∞) :
    (⨍⁻ (a : α), f a ∂μ) * μ univ = ∫⁻ x, f x ∂μ :=
  by
  obtain rfl | hμ := eq_or_ne μ 0
  · simp
  · rw [laverage_eq, ENNReal.div_mul_cancel (measure_univ_ne_zero.2 hμ) (measure_ne_top _ _)]

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