Documentation Verification Report

Binomial

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

Statistics

Metric	Count
Definitions `binomial`	1
Theorems `binomial_apply`, `binomial_apply_last`, `binomial_apply_self`, `binomial_apply_zero`, `binomial_one_eq_bernoulli`	5
Total	6

PMF

Definitions

Name	Category	Theorems
`binomial` 📖	CompOp	5 math math: `binomial_apply_zero`, `binomial_apply`, `binomial_apply_self`, `binomial_one_eq_bernoulli`, `binomial_apply_last`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`binomial_apply` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `binomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `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` `instPartialOrderNNReal` `instOneNNReal`	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `binomial` `Monoid.toNatPow` `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_self` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `binomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	`binomial_apply_last`
`binomial_apply_zero` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `binomial` `Monoid.toNatPow` `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` `instPartialOrderNNReal` `instOneNNReal`	`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