mathlib

1019dd67 - feat(measure_theory/probability_mass_function): Define a measure assosiated to a pmf (#9966)

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.