Commit 2022-02-02 10:56 c1d28601

View on Github →

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.

Estimated changes

Modified src/measure_theory/probability_mass_function/monad.lean

modified theorem pmf.bind_bind

modified theorem pmf.bind_pure

modified theorem pmf.coe_bind_apply

modified theorem pmf.pure_bind

added theorem pmf.to_measure_bind_apply

added theorem pmf.to_measure_bind_on_support_apply

added theorem pmf.to_measure_pure_apply

added theorem pmf.to_outer_measure_bind_apply

added theorem pmf.to_outer_measure_bind_on_support_apply

added theorem pmf.to_outer_measure_pure_apply