Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-23 00:20 e50b8c26

View on Github →

feat(probability/probability_mass_function/*): Define pmf in terms of ennreal instead of nnreal (#17032) This PR modifies the definition of a pmf from {f : α → ℝ≥0 // has_sum f 1} to {f : α → ℝ≥0∞ // has_sum f 1}. This makes it much easier to work with the infinite sums as there is no longer any need to prove summability. It also aligns more closely with the definition of measure and outer_measure which are in terms of ennreal.

Estimated changes

modified theorem pmf.apply_eq_one_iff
added theorem pmf.apply_lt_top
added theorem pmf.apply_ne_top
added theorem pmf.apply_pos_iff
deleted theorem pmf.summable_coe
deleted theorem pmf.to_measure_apply'
modified theorem pmf.to_measure_apply
modified theorem pmf.to_measure_apply_finset
modified theorem pmf.to_outer_measure_apply
added theorem pmf.tsum_coe_ne_top
modified def {u}
modified def pmf.bernoulli
modified def pmf.normalize
modified theorem pmf.normalize_apply
modified def pmf.of_finset
modified def pmf.of_fintype
modified theorem pmf.support_normalize
deleted theorem pmf.coe_bind_apply
added theorem ennreal.has_sum_lt
added theorem ennreal.tsum_lt_tsum