toFiniteMeasure_normalize_eq_self

English

Let μ be a probability measure on Ω. The finite measure associated to μ, when normalized, equals μ itself.

Русский

Пусть μ — вероятностная мера на Ω. Связанная с μ конечная мера, при нормировке, равна самой μ.

LaTeX

$$$\\operatorname{normalize}(\\mu_{\\mathrm{fin}}) = \\mu$$$

Lean4

@[simp]
theorem _root_.ProbabilityMeasure.toFiniteMeasure_normalize_eq_self {m0 : MeasurableSpace Ω}
    (μ : ProbabilityMeasure Ω) : μ.toFiniteMeasure.normalize = μ :=
  by
  apply ProbabilityMeasure.eq_of_forall_apply_eq
  intro s _s_mble
  rw [μ.toFiniteMeasure.normalize_eq_of_nonzero μ.toFiniteMeasure_nonzero s]
  simp only [ProbabilityMeasure.mass_toFiniteMeasure, inv_one, one_mul, μ.coeFn_toFiniteMeasure]

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