Binomial

📁 Source: Mathlib/Probability/ProbabilityMassFunction/Binomial.lean

Statistics

Metric	Count
Definitions binomial	1
Theorems binomial_apply, binomial_apply_last, binomial_apply_of_le, binomial_apply_self, binomial_apply_zero, binomial_one_eq_bernoulli	6
Total	7

PMF

Definitions

Name	Category	Theorems
binomial 📖	CompOp	7 math math: binomial_apply_zero, binomial_apply_of_le, binomial_apply, binomial_apply_self, binomial_one_eq_bernoulli, ProbabilityTheory.binomial_tendsto_poissonPMFReal_atTop, binomial_apply_last

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
binomial_apply 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instOne	DFunLike.coe PMF ENNReal instFunLike binomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ENNReal.ofNNReal ENNReal.instSub AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddMonoidWithOne.toNatCast Nat.choose	—	ENNReal.coe_sub ofFintype.congr_simp
binomial_apply_last 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instOne	DFunLike.coe PMF ENNReal instFunLike binomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal	—	binomial_apply tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero mul_one Nat.choose_self Nat.cast_one
binomial_apply_of_le 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instOne	ENNReal.ofReal Real Real.instMul Real.instNatCast Nat.choose Monoid.toPow Real.instMonoid NNReal.toReal Real.instSub Real.instOne DFunLike.coe PMF ENNReal instFunLike binomial	—	Nat.instNoMaxOrder Order.lt_add_one_iff Nat.cast_one covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Fin.ofNat_eq_cast binomial_apply Fin.val_natCast ENNReal.coe_nnreal_eq mul_rotate ENNReal.ofReal_mul mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing pow_nonneg IsOrderedRing.toZeroLEOneClass NNReal.coe_nonneg ENNReal.ofReal_pow ENNReal.ofReal_natCast
binomial_apply_self 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instOne	DFunLike.coe PMF ENNReal instFunLike binomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal	—	binomial_apply_last
binomial_apply_zero 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instOne	DFunLike.coe PMF ENNReal instFunLike binomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instSub AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal ENNReal.ofNNReal	—	binomial_apply pow_zero tsub_zero Nat.instOrderedSub one_mul Nat.choose_zero_right Nat.cast_one mul_one
binomial_one_eq_bernoulli 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instOne	binomial map bernoulli	—	ext Fintype.complete binomial_apply pow_zero tsub_zero Nat.instOrderedSub pow_one one_mul Nat.choose_succ_self_right zero_add Nat.cast_one mul_one map_apply bernoulli_apply tsum_fintype SummationFilter.instLeAtTopUnconditional Finset.sum_insert Fin.instNeZeroHAddNatOfNat_mathlib_1 Finset.sum_singleton ENNReal.coe_sub tsub_self Nat.instCanonicallyOrderedAdd Nat.choose_self add_zero

---

← Back to Index