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