isProbabilityMeasureSMul — Mathlib

English

If μ is finite and nonzero, the normalized measure (μ univ)⁻¹ • μ is a probability measure.

Русский

Если μ конечна и не нулевая, нормализованная мера (μ унив)⁻¹ • μ является вероятностной мерой.

LaTeX

$$$\text{IsProbabilityMeasure}\left(((\mu\ univ)^{-1}) \cdot \mu\right)$$$

Lean4

instance isProbabilityMeasureSMul [IsFiniteMeasure μ] [NeZero μ] : IsProbabilityMeasure ((μ univ)⁻¹ • μ) :=
  ⟨ENNReal.inv_mul_cancel (NeZero.ne (μ univ)) (measure_ne_top _ _)⟩

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