Commit 2026-03-18 15:17 b8caa95b

View on Github →

feat: binomial random variables (#28248) Define the binomial distribution and compute the expectation, variance, conditional variance of a binomial random variable. From MiscYD

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/Set.lean

added theorem MeasureTheory.integral_eq_setIntegral

Modified Mathlib/Order/Filter/Germ/Basic.lean

modified theorem Filter.const_eventuallyEq

Modified Mathlib/Probability/CondVar.lean

Created Mathlib/Probability/Distributions/Binomial.lean

added theorem ProbabilityTheory.ae_le_of_hasLaw_binomial

Created Mathlib/Probability/Distributions/TwoValued.lean

added theorem MeasureTheory.integral_of_ae_eq_zero_or_one

added theorem MeasureTheory.integral_one_sub_of_ae_eq_zero_or_one

added theorem ProbabilityTheory.condVar_of_ae_eq_zero_or_one

added theorem ProbabilityTheory.variance_of_ae_eq_zero_or_one