Revision #2298 → #3389 · back to history
modifiedRegression toward the mean (informal)ac4ad5adf80c
| Field | From #2298 | To #3389 |
|---|
| note | No notion of 'regression toward the mean' appears in Mathlib (grep finds no occurrences in any statistical sense). | No notion of 'regression toward the mean' appears in Mathlib (semantic and grep searches turn up no relevant declarations). |
addedGalton's mid-parental deviations regression law2e3c1862c31f
modifiedRegression toward the mean via simple linear regression836f641128a3
| Field | From #2298 | To #3389 |
|---|
| note | Mathlib has no 'simple linear regression' or 'least squares' development (grep finds none). | Mathlib has no 'simple linear regression' or 'least squares' development (semantic search only turns up unrelated affine-space `slope`). |
modifiedBivariate normal conditional mean is linear7e86dd946ea8
| Field | From #2298 | To #3389 |
|---|
| note | No bivariate/multivariate Gaussian or linearity-of-conditional-mean result was found in Mathlib (only general `condexp` infrastructure). | No bivariate/multivariate Gaussian or linearity-of-conditional-mean result was found in Mathlib (only general `condExp` infrastructure). |
addedLaw of large numbers (referenced contrast)bed6506c6a92