mathlib3

e50b8c26 - feat(probability/probability_mass_function/*): Define `pmf` in terms of `ennreal` instead of `nnreal` (#17032)

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`.