Commit 2021-11-12 07:59 1019dd67

feat(measure_theory/probability_mass_function): Define a measure assosiated to a pmf (#9966) This PR defines pmf.to_outer_measure and pmf.to_measure, where the measure of a set is given by the total probability of elements of the set, and shows that this is a probability measure.