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

.