Probability mass functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file is about probability mass functions or discrete probability measures:
α → ℝ≥0∞ such that the values have (infinite) sum
Construction of monadic
bind is found in
other constructions of
pmfs are found in
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.
Conversely, given a probability measure
μ on a measurable space
α with all singleton sets
μ.to_pmf 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.