Revision #1727 → #2226 · back to history
modifiedCentral limit theorem (informal)538b179931e6
| Field | From #1727 | To #2226 |
|---|
| kind | definition | theorem |
| note | The informal statement is captured by Mathlib's 1D CLT for i.i.d. variables with mean μ and variance v. | The informal statement matches Mathlib's 1D i.i.d. CLT giving convergence in distribution of the standardized sum to a Gaussian. |
| provenance | ai | ai-moderated |
modifiedCLT statistical statement88a3f8f9a89a
| Field | From #1727 | To #2226 |
|---|
| note | The standard CLT statement is formalized via convergence in distribution to gaussianReal. | The standard CLT statement is formalized via `tendstoInDistribution_inv_sqrt_mul_sum_sub` to `gaussianReal`. |
modifiedde Moivre–Laplace theoremc0761c854448
| Field | From #1727 | To #2226 |
|---|
| note | Binomial distribution is defined in Mathlib but the de Moivre–Laplace special case is not separately stated; it follows from the general CLT. | The binomial special case is not stated separately; it is subsumed by the general i.i.d. CLT. |
modifiedLaw of large numbers (sample average)8c17ce194a4b
| Field | From #1727 | To #2226 |
|---|
| note | The almost-sure convergence of the sample average is given by the strong law of large numbers in Mathlib. | Almost-sure convergence of the sample average is Mathlib's strong law of large numbers. |
modifiedClassical CLT (uniform convergence of cdfs)a7e1604fa1b1
| Field | From #1727 | To #2226 |
|---|
| note | Convergence in distribution (which is equivalent to pointwise convergence of CDFs at continuity points) is the form used in the Mathlib statement. | Mathlib's CLT is stated in the equivalent form of convergence in distribution (weak convergence of laws). |
modifiedLindeberg–Lévy CLTb4ab40cc40ea
| Field | From #1727 | To #2226 |
|---|
| note | The Lindeberg–Lévy (i.i.d.) CLT is exactly what Mathlib's `tendstoInDistribution_inv_sqrt_mul_sum_sub` states. | Lindeberg–Lévy is exactly what `tendstoInDistribution_inv_sqrt_mul_sum_sub` states. |
modifiedLyapunov CLT02c1d31e2d6f
| Field | From #1727 | To #2226 |
|---|
| note | No Lyapunov condition or non-i.i.d. CLT is present in Mathlib. | No Lyapunov condition or Lyapunov CLT appears in Mathlib (loogle returns 0 hits for `Lyapunov`). |
modifiedLyapunov implies Lindeberg048e79bb5b82
| Field | From #1727 | To #2226 |
|---|
| note | Neither the Lyapunov nor Lindeberg condition is defined in Mathlib. | Neither the Lyapunov nor the Lindeberg condition is defined in Mathlib. |
modifiedLindeberg condition709fe4ba5121
| Field | From #1727 | To #2226 |
|---|
| note | The Lindeberg condition itself is not defined in Mathlib. | Loogle finds no declaration whose name contains `Lindeberg`. |
modifiedLindeberg–Feller CLT7f12a8e832f1
| Field | From #1727 | To #2226 |
|---|
| note | The Lindeberg–Feller CLT is not formalized in Mathlib. | The Lindeberg–Feller CLT for non-i.i.d. arrays is not formalized in Mathlib. |
modifiedRobbins CLT04cfcce381c9
| Field | From #1727 | To #2226 |
|---|
| note | Robbins' CLT for random sums is not formalized in Mathlib. | Robbins' CLT for random sums is not formalized. |
modifiedMultidimensional CLT2dcc3abb6692
| Field | From #1727 | To #2226 |
|---|
| note | Mathlib's CLT is stated only in dimension 1; multivariate Gaussian is defined but no multidimensional CLT is proven. | Mathlib's CLT is one-dimensional only; no multidimensional CLT is proven though `multivariateGaussian` is defined. |
modifiedBerry–Esseen type bound for multivariate CLT4fa6b3b85b61
| Field | From #1727 | To #2226 |
|---|
| note | No Berry–Esseen bound is present in Mathlib. | No Berry–Esseen bound (univariate or multivariate) is in Mathlib. |
modifiedCramér–Wold theoremf6162240a4da
| Field | From #1727 | To #2226 |
|---|
| note | The Cramér–Wold device (reducing multivariate convergence in distribution to one-dimensional projections) is not formalized in Mathlib. | The Cramér–Wold device is not formalized (loogle returns 0 hits for `CramerWold`). |
modifiedGeneralized central limit theorem24429ed7c66f
| Field | From #1727 | To #2226 |
|---|
| note | The generalized CLT with stable laws is not formalized; stable distributions are absent from Mathlib. | Stable distributions and the generalized CLT are not in Mathlib. |
modifiedStrong mixing (α-mixing)5a0f355bad40
| Field | From #1727 | To #2226 |
|---|
| note | No α-mixing coefficient or related mixing definitions are present in Mathlib. | No α-mixing coefficient is defined in Mathlib. |
modifiedMartingale difference CLTc708422267a1
| Field | From #1727 | To #2226 |
|---|
| note | Martingale theory exists in Mathlib but no martingale CLT is proven. | Mathlib has martingale theory but no martingale CLT (loogle finds no `centralLimit`/martingale match). |
modifiedProof of classical CLT via characteristic functions85733343d51f
| Field | From #1727 | To #2226 |
|---|
| note | Mathlib's CLT proof uses characteristic functions, with the key limit `tendsto_charFun_inv_sqrt_mul_pow` and Lévy continuity theorem in `LevyConvergence`. | Mathlib's proof goes via characteristic functions with this key pointwise limit and Lévy's continuity theorem. |
modifiedLévy's continuity theorem4e9c12f10bd3
| Field | From #1727 | To #2226 |
|---|
| note | Lévy's continuity theorem (pointwise convergence of characteristic functions implies weak convergence) is formalized in Mathlib. | Lévy's continuity theorem is formalized as the equivalence between weak convergence and pointwise convergence of characteristic functions. |
modifiedBerry–Esseen rate of convergencee24fe4deb8f8
| Field | From #1727 | To #2226 |
|---|
| note | The Berry–Esseen rate-of-convergence bound is not in Mathlib. | Berry–Esseen rate bounds are not in Mathlib. |
modifiedCLT restated via characteristic functions9ad4f88c98f4
| Field | From #1727 | To #2226 |
|---|
| note | Mathlib computes the characteristic function of the normalized sum as a power and shows it converges to the Gaussian char function. | Mathlib expresses the characteristic function of the normalized sum as a power and shows it converges to the Gaussian char function. |
modifiedMultiplicative CLT (Gibrat's law)223932743036
| Field | From #1727 | To #2226 |
|---|
| note | No log-normal distribution or multiplicative CLT is present in Mathlib. | No log-normal distribution or multiplicative CLT is in Mathlib. |
modifiedCLT for linear functions of orthogonal matrices0724c69f513c
| Field | From #1727 | To #2226 |
|---|
| note | No CLT for entries/linear functionals of Haar-random orthogonal matrices is formalized. | No CLT for linear functionals of Haar-random orthogonal matrices is formalized. |
modifiedCLT on a crystal lattice2d46c9a00256
| Field | From #1727 | To #2226 |
|---|
| note | Crystal lattices and random walks on them are not formalized. | Crystal lattices and CLTs for random walks on them are not formalized. |
modifiedRegression error termsc3b03b361131
| Field | From #1727 | To #2226 |
|---|
| note | Applications of CLT to regression error terms are not formalized in Mathlib. | The CLT-for-regression-errors application is not formalized. |
addedConvergence in distribution612e2878f4e5
addedMultivariate normal (Gaussian) distributionec4d86cabbdd
addedCharacteristic function of a random variable222fb5847931