Theorems · Theorem · probability
ProbabilityTheory.binomial_singleton
∀ (n k : ℕ) (p : ↑unitInterval),
(ProbabilityTheory.binomial n p) {k} = ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k))- Cited by
- 2 results in Mathlib
- Foundations
- Depth 291 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- MeasureTheory.Measurestatement · cited by 10,939
- ENNRealstatement and proof · cited by 9,879
- Set.Elemstatement and proof · cited by 7,166
- ENNReal.ofRealstatement and proof · cited by 863
- unitIntervalstatement and proof · cited by 607
- Nat.choosestatement and proof · cited by 494
- MeasureTheory.measureReal_defproof · cited by 68
- ENNReal.ofReal_toRealproof · cited by 65
- ProbabilityTheory.binomialstatement and proof · cited by 20
Cited by2
Results whose statement or proof uses this declaration.
- ProbabilityTheory.binomial_eq_sum_diracproof · cited by 2
- ProbabilityTheory.binomial_tendsto_poissonPMFReal_atTopproof · cited by 0