Revision #3389 → #3911 · back to history
addedGalton board pellet distribution1ca269ac1abd
modifiedRegression toward the mean criterion on correlationa35a70eafc05
| Field | From #3389 | To #3911 |
|---|
| note | Criterion 0 < β < 1 for regression toward the mean is not stated in Mathlib. | Criterion -1 < r_xy < 1 for regression toward the mean is not stated in Mathlib. |
| provenance | ai | ai-moderated |
addedConditional mean is within |r| standard deviations4c6662dcd843
modifiedLaw of large numbers (referenced contrast)bed6506c6a92
| Field | From #3389 | To #3911 |
|---|
| note | The article contrasts regression to the mean with the law of large numbers; the (strong) LLN is formalized in Mathlib as `ProbabilityTheory.strong_law_ae` (confirmed via decl_exists). | The strong law of large numbers is formalized in Mathlib as `ProbabilityTheory.strong_law_ae` (confirmed via decl_exists). |
addedGambler's fallacy (contrast)4f23fef58bec