Commit 2026-06-06 16:12 e4794ec4

View on Github →

feat: API for binomial distribution (#37736) Provide basic API regarding the binomial distribution, computing the measure of singletons and writing it as a sum of Dirac masses. Provide basic results regarding integrability. Deprecate PMF.binomial.

Estimated changes

Modified Mathlib/Probability/Distributions/Binomial.lean

added theorem ProbabilityTheory.binomial_eq_sum_dirac

added theorem ProbabilityTheory.binomial_nat

added theorem ProbabilityTheory.binomial_nonneg

added theorem ProbabilityTheory.binomial_one_eq_bernoulliMeasure

added theorem ProbabilityTheory.binomial_real_self

added theorem ProbabilityTheory.binomial_real_singleton

added theorem ProbabilityTheory.binomial_real_zero

added theorem ProbabilityTheory.binomial_singleton

added theorem ProbabilityTheory.binomial_zero

added theorem ProbabilityTheory.integrable_binomial

added theorem ProbabilityTheory.integrable_map_cast_binomial

added theorem ProbabilityTheory.integral_binomial

added theorem ProbabilityTheory.integral_map_cast_binomial

added theorem ProbabilityTheory.map_cast_binomial_eq_sum_dirac

added theorem ProbabilityTheory.map_cast_binomial_real_self

added theorem ProbabilityTheory.map_cast_binomial_real_singleton

added theorem ProbabilityTheory.map_cast_binomial_real_zero

added theorem ProbabilityTheory.map_cast_binomial_singleton

added theorem ProbabilityTheory.map_cast_binomial_zero

Modified Mathlib/Probability/Distributions/Poisson/PoissonLimitThm.lean

modified theorem ProbabilityTheory.binomial_tendsto_poissonPMFReal_atTop

Modified Mathlib/Probability/Distributions/SetBernoulli.lean

added theorem ProbabilityTheory.map_ncard_setBernoulli_apply

added theorem ProbabilityTheory.map_ncard_setBernoulli_real_singleton

added theorem ProbabilityTheory.map_ncard_setBernoulli_singleton

Modified Mathlib/Probability/ProbabilityMassFunction/Binomial.lean