toMeasure_normalize_eq_of_nonzero

English

The normalized finite measure equals the scalar multiple of μ when viewed as a measure.

Русский

Нормализованная мера совпадает с константным масштабированием μ, если рассматривать как меру.

LaTeX

$$$(\\mu.normalize : \\text{Measure } \\Omega) = \\mu.mass^{-1} \\cdot \\mu$$$

Lean4

theorem toMeasure_normalize_eq_of_nonzero (nonzero : μ ≠ 0) : (μ.normalize : Measure Ω) = μ.mass⁻¹ • μ :=
  by
  ext1 s _s_mble
  rw [← μ.normalize.ennreal_coeFn_eq_coeFn_toMeasure s, μ.normalize_eq_of_nonzero nonzero s, ENNReal.coe_mul,
    ennreal_coeFn_eq_coeFn_toMeasure]
  exact Measure.coe_nnreal_smul_apply _ _ _

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