Commit 2021-11-02 10:26 fc12ca8d

View on Github →

feat(measure_theory/probability_mass_function): Define uniform pmf on an inhabited fintype (#9920) This PR defines uniform probability mass functions on nonempty finsets and inhabited fintypes.

Estimated changes

Modified src/measure_theory/probability_mass_function.lean

added theorem pmf.bernuolli_apply

added def pmf.of_finset

added theorem pmf.of_finset_apply

added theorem pmf.of_finset_apply_of_not_mem

added theorem pmf.of_fintype_apply

added theorem pmf.of_multiset_apply

added theorem pmf.of_multiset_apply_of_not_mem

added def pmf.uniform_of_finset

added theorem pmf.uniform_of_finset_apply

added theorem pmf.uniform_of_finset_apply_of_mem

added theorem pmf.uniform_of_finset_apply_of_not_mem

added def pmf.uniform_of_fintype

added theorem pmf.uniform_of_fintype_apply