mathlib

3f5c9d30 - feat(probability/probability_mass_function): construct a `pmf` from a probability measure (#18270)

feat(probability/probability_mass_function): construct a `pmf` from a probability measure (#18270) Given a measurable space `α` with a `measurable_singleton_class` instance, this PR defines a function `measure.to_pmf` that converts a probability measure `μ` to a `pmf`, by defining the mass of a point `x` to be the measure of the singleton set `{x}` under `μ`.