Commit 2022-02-10 08:34 b7e72ea4

View on Github →

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.

Estimated changes

Modified src/measure_theory/probability_mass_function/constructions.lean

added theorem pmf.mem_support_uniform_of_fintype

deleted theorem pmf.mem_support_uniform_of_fintype_iff

modified theorem pmf.support_uniform_of_fintype

added theorem pmf.to_measure_map_apply

added theorem pmf.to_measure_of_finset_apply

added theorem pmf.to_measure_of_fintype_apply

added theorem pmf.to_measure_of_multiset_apply

added theorem pmf.to_measure_uniform_of_finset_apply

added theorem pmf.to_measure_uniform_of_fintype_apply

added theorem pmf.to_outer_measure_map_apply

added theorem pmf.to_outer_measure_of_finset_apply

added theorem pmf.to_outer_measure_of_fintype_apply

added theorem pmf.to_outer_measure_of_multiset_apply

added theorem pmf.to_outer_measure_uniform_of_finset_apply

added theorem pmf.to_outer_measure_uniform_of_fintype_apply

Modified src/measure_theory/probability_mass_function/monad.lean

modified theorem pmf.to_measure_bind_apply

modified theorem pmf.to_measure_bind_on_support_apply

modified theorem pmf.to_measure_pure_apply

modified theorem pmf.to_outer_measure_bind_apply

modified theorem pmf.to_outer_measure_bind_on_support_apply

modified theorem pmf.to_outer_measure_pure_apply