instIsProbabilityMeasureToMeasure

English

The underlying measure of a probability measure is a probability measure when viewed as a measure; i.e., the corresponding Measure obtained from a ProbabilityMeasure has total mass 1 on the whole space.

Русский

При восприятии распределения как меры получаем меру, обладающую общей массой 1 на всём пространстве.

LaTeX

$$$(\\mu.toMeasure)(\\mathrm{univ}) = 1$$$

Lean4

instance (μ : ProbabilityMeasure Ω) : IsProbabilityMeasure (μ : Measure Ω) :=
  μ.prop

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