Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-08 17:16 8ab1b3b4

View on Github →

feat(measure_theory/probability_mass_function): Calculate supports of pmf constructions (#10371) This PR gives explicit descriptions for the support of the various pmf constructions in mathlib. This also tries to clean up the variable declarations in the different sections, so that all the lemmas don't need to specify them explicitly.

Estimated changes

modified theorem pmf.apply_eq_zero_iff
modified theorem pmf.bind_apply
modified theorem pmf.mem_support_iff
deleted theorem pmf.mem_support_pure_iff
modified theorem pmf.pure_apply
added theorem pmf.support_bind
added theorem pmf.support_pure
added theorem pmf.bernoulli_apply
deleted theorem pmf.bernuolli_apply
modified def pmf.bind_on_support
modified theorem pmf.bind_on_support_apply
modified theorem pmf.bind_pure_comp
modified def pmf.filter
modified theorem pmf.filter_apply
added theorem pmf.map_apply
modified theorem pmf.map_comp
modified theorem pmf.map_id
modified theorem pmf.normalize_apply
modified def pmf.of_finset
modified theorem pmf.of_finset_apply
modified def pmf.of_fintype
modified theorem pmf.of_fintype_apply
modified theorem pmf.of_multiset_apply
modified theorem pmf.pure_bind_on_support
modified theorem pmf.pure_map
modified def pmf.seq
added theorem pmf.seq_apply
added theorem pmf.support_bernoulli
added theorem pmf.support_filter
added theorem pmf.support_map
added theorem pmf.support_normalize
added theorem pmf.support_of_finset
added theorem pmf.support_of_fintype
added theorem pmf.support_seq
modified theorem pmf.uniform_of_finset_apply