Commit 2025-07-12 23:16 a4ebcd79

View on Github →

refactor(Probability/ProbabilityMassFunction): Make constructions use NNReal (#26596) This refactor makes the functions for Bernoulli/Binomial random variables take an NNReal parameter, rather than an ENNReal. This is convenient, since we have to prove p \le 1 anyway, and this can now be done with field_simp for explicit p.

Estimated changes

modified def PMF.binomial
modified theorem PMF.binomial_apply
modified theorem PMF.binomial_apply_last
modified theorem PMF.binomial_apply_self
modified theorem PMF.binomial_apply_zero
modified def PMF.bernoulli
modified theorem PMF.bernoulli_apply
modified theorem PMF.bernoulli_expectation