Specific Constructions of Probability Mass Functions #
This file gives a number of different
pmf constructions for common probability distributions.
of_fintype simplify the construction of a
pmf α from a function
f : α → ℝ≥0,
by allowing the "sum equals 1" constraint to be in terms of
finset.sum instead of
uniform_of_fintype construct probability mass functions
from the corresponding object, with proportional weighting for each element of the object.
bind to allow binding to a partial function,
so that the second argument only needs to be defined on the support of the first argument.
Generalized version of
f to only be defined on the support of
p.bind f is equivalent to
p.bind_on_support (λ a _, f a), see