Probability mass functions #
This file is about probability mass functions or discrete probability measures:
a function α → ℝ≥0∞
such that the values have (infinite) sum 1
.
Construction of monadic pure
and bind
is found in ProbabilityMassFunction/Monad.lean
,
other constructions of Pmf
s are found in ProbabilityMassFunction/Constructions.lean
.
Given p : Pmf α
, Pmf.toOuterMeasure
constructs an OuterMeasure
on α
,
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 Measure
on α
, see Pmf.toMeasure
.
Pmf.toMeasure.isProbabilityMeasure
shows this associated measure is a probability measure.
Conversely, given a probability measure μ
on a measurable space α
with all singleton sets
measurable, μ.toPmf
constructs a Pmf
on α
, setting the probability mass of a point x
to be the measure of the singleton set {x}
.
Tags #
probability mass function, discrete probability measure
Slightly stronger than OuterMeasure.mono
having an intersection with p.support
.
Since every set is Carathéodory-measurable under Pmf.toOuterMeasure
,
we can further extend this OuterMeasure
to a Measure
on α
.
Instances For
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.
Instances For
The measure associated to a Pmf
by toMeasure
is a probability measure.