Theorems · Definition · probability

MeasureTheory.Measure.toPMF

{α : Type u_1} →
  [Countable α] →
    [inst : MeasurableSpace α] →
      [MeasurableSingletonClass α] → (μ : MeasureTheory.Measure α) → [h : MeasureTheory.IsProbabilityMeasure μ] → PMF α

Given that α is a countable, measurable space with all singleton sets measurable, we can convert any probability measure into a PMF, where the mass of a point is the measure of the singleton set under the original measure.

Defined in

Mathlib.Probability.ProbabilityMassFunction.Basic

Cited by

6 results in Mathlib

Foundations

Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CountableMeasurableSpaceMeasurableSingletonClassMeasureTheory.IsProbabilityMeasure