normalize — Mathlib

Lean4
/-- Normalize a finite measure so that it becomes a probability measure, i.e., divide by the
total mass. -/
def normalize : ProbabilityMeasure Ω :=
  if zero : μ.mass = 0 then ⟨Measure.dirac ‹Nonempty Ω›.some, Measure.dirac.isProbabilityMeasure⟩
  else
    { val := μ.mass⁻¹ • (μ : Measure Ω)
      property := by
        refine ⟨?_⟩
        simp only [Measure.coe_smul, Pi.smul_apply, Measure.nnreal_smul_coe_apply, ENNReal.coe_inv zero, ennreal_mass]
        rw [← Ne, ← ENNReal.coe_ne_zero, ennreal_mass] at zero
        exact ENNReal.inv_mul_cancel zero μ.prop.measure_univ_lt_top.ne }
Похожие утверждения