Probability mass functions #
This file is about probability mass functions or discrete probability measures:
α → ℝ≥0∞ such that the values have (infinite) sum
p : Pmf α,
Pmf.toOuterMeasure constructs an
by assigning each set the sum of the probabilities of each of its elements.
Under this outer measure, every set is Carathéodory-measurable,
so we can further extend this to a
Pmf.toMeasure.isProbabilityMeasure shows this associated measure is a probability measure.
Conversely, given a probability measure
μ on a measurable space
α with all singleton sets
μ.toPmf constructs a
α, setting the probability mass of a point
to be the measure of the singleton set
probability mass function, discrete probability measure
α 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.