Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-08 19:30 4e9fbb94

View on Github →

feat(measure_theory/probability_mass_function): Add definitions for filtering pmfs on a predicate (#6033)

Estimated changes

added def pmf.filter
added theorem pmf.filter_apply
added theorem pmf.mem_support_iff
added def pmf.normalize
added theorem pmf.normalize_apply