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.to_outer_measure 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.to_measure.is_probability_measure shows this associated measure is a probability measure.
probability mass function, discrete probability measure