Revision #2387 → #3073 · back to history
modifiedCentral limit theorem45e5eaedb4a9
| Field | From #2387 | To #3073 |
|---|
| note | No central limit theorem declaration was found in Mathlib. | Mathlib has the strong law of large numbers but no CLT statement; only `MeasureTheory.TendstoInDistribution` infrastructure exists. |
modifiedNormal cumulative distribution function58ccf51c3d9d
| Field | From #2387 | To #3073 |
|---|
| mathlib.decl | — | ProbabilityTheory.gaussianReal |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Probability.Distributions.Gaussian.Real |
| note | Mathlib does not define the normal distribution or its CDF; `Real.erf`/the error function is also not present. | The Gaussian measure `gaussianReal` and general `ProbabilityTheory.cdf` are defined, so the normal CDF can be obtained as their composition, but there is no dedicated `normalCDF` declaration. |
| status | not_formalized | partial |
addedMahalanobis distancea62b8af34c9e
addedCovariance matrix45c7f8e8bf35
addedVariance of independent sum equals sum of variances156111e3f450