mathlib
b7e72ea4 - feat(measure_theory/probability_mass_function): Measure calculations for additional pmf constructions (#11858)

Commit

4 years ago

feat(measure_theory/probability_mass_function): Measure calculations for additional pmf constructions (#11858) This PR adds calculations of the measures of sets under various `pmf` constructions.

Author

dtumad

Parents

e9a18930

mathlib b7e72ea4 - feat(measure_theory/probability_mass_function): Measure calculations for additional pmf constructions (#11858)

mathlib
b7e72ea4 - feat(measure_theory/probability_mass_function): Measure calculations for additional pmf constructions (#11858)