mathlib3

c1d28601 - feat(measure_theory/probability_mass_function): Measures of sets under `pmf` monad operations (#11613)

feat(measure_theory/probability_mass_function): Measures of sets under `pmf` monad operations (#11613) This PR adds explicit formulas for the measures of sets under `pmf.pure`, `pmf.bind`, and `pmf.bind_on_support`.