Revision #1383 → #1761 · back to history
2a1ab572e189| Field | From #1383 | To #1761 |
|---|---|---|
| mathlib.decl | ProbabilityTheory.variance_of_hasLaw_binomial | — |
| note | The Bernoulli distribution is defined (PMF.bernoulli) and the binomial variance p(1-p)n is stated, but only as an unproved `proof_wanted`, so Var = p(1-p) is not actually established. | The Bernoulli distribution is defined (PMF.bernoulli) and the binomial variance np(1-p) appears only as a `proof_wanted` placeholder in Mathlib/Probability/Distributions/Binomial.lean, so Var = p(1-p) is not actually established as a real declaration. |