Revision #1478 → #2627 · back to history
modifiedPoisson distributiond89351327fa3
| Field | From #1478 | To #2627 |
|---|
| mathlib.decl | poissonMeasure | ProbabilityTheory.poissonMeasure |
| provenance | ai | ai-moderated |
modifiedProbability of k events1a50a2d66589
| Field | From #1478 | To #2627 |
|---|
| mathlib.decl | poissonMeasure_singleton | ProbabilityTheory.poissonMeasure_singleton |
| provenance | ai | ai-moderated |
modifiedProbability mass function985768669bb4
| Field | From #1478 | To #2627 |
|---|
| mathlib.decl | poissonMeasure_singleton | ProbabilityTheory.poissonMeasure_singleton |
| provenance | ai | ai-moderated |
modifiedMean equals variance equals λe0cbd34ed010
| Field | From #1478 | To #2627 |
|---|
| mathlib.decl | integral_poissonMeasure | ProbabilityTheory.integral_poissonMeasure |
| provenance | ai | ai-moderated |
modifiedLimit of a binomial distributiond619d65dd557
| Field | From #1478 | To #2627 |
|---|
| mathlib.decl | tendsto_choose_mul_pow_of_tendsto_mul_atTop | ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop |
| provenance | ai | ai-moderated |
modifiedExpected value4512ffbffe8f
| Field | From #1478 | To #2627 |
|---|
| mathlib.decl | integral_poissonMeasure | ProbabilityTheory.integral_poissonMeasure |
| provenance | ai | ai-moderated |
modifiedVariancef11efb9be248
| Field | From #1478 | To #2627 |
|---|
| mathlib.decl | integral_poissonMeasure | ProbabilityTheory.integral_poissonMeasure |
| provenance | ai | ai-moderated |
modifiedLimiting case of binomialbf5dbe4cb5b8
| Field | From #1478 | To #2627 |
|---|
| mathlib.decl | tendsto_choose_mul_pow_of_tendsto_mul_atTop | ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop |
| provenance | ai | ai-moderated |
modifiedPoisson limit theoremb86db90f8822
| Field | From #1478 | To #2627 |
|---|
| mathlib.decl | tendsto_choose_mul_pow_of_tendsto_mul_atTop | ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTop |
| provenance | ai | ai-moderated |