Revision #2226 → #2878 · back to history
modifiedCentral limit theorem (informal)538b179931e6
| Field | From #2226 | To #2878 |
|---|
| note | The informal statement matches Mathlib's 1D i.i.d. CLT giving convergence in distribution of the standardized sum to a Gaussian. | Verified: `tendstoInDistribution_inv_sqrt_mul_sum_sub` in `Mathlib/Probability/CentralLimitTheorem.lean` is Mathlib's 1D i.i.d. CLT giving convergence in distribution of the normalized sum to a Gaussian. |
modifiedCLT statistical statement88a3f8f9a89a
| Field | From #2226 | To #2878 |
|---|
| note | The standard CLT statement is formalized via `tendstoInDistribution_inv_sqrt_mul_sum_sub` to `gaussianReal`. | Verified: the standard CLT statement is `tendstoInDistribution_inv_sqrt_mul_sum_sub` with target `gaussianReal`. |
modifiedLaw of large numbers (sample average)8c17ce194a4b
| Field | From #2226 | To #2878 |
|---|
| note | Almost-sure convergence of the sample average is Mathlib's strong law of large numbers. | Verified: `strong_law_ae_real` in `Mathlib/Probability/StrongLaw.lean` gives a.s. convergence of the sample average. |
modifiedLyapunov CLT02c1d31e2d6f
| Field | From #2226 | To #2878 |
|---|
| note | No Lyapunov condition or Lyapunov CLT appears in Mathlib (loogle returns 0 hits for `Lyapunov`). | Verified: no `Lyapunov`-named declaration in Mathlib and no Lyapunov CLT. |
modifiedLindeberg condition709fe4ba5121
| Field | From #2226 | To #2878 |
|---|
| note | Loogle finds no declaration whose name contains `Lindeberg`. | Verified: no declaration containing `Lindeberg` in Mathlib. |
modifiedBerry–Esseen type bound for multivariate CLT4fa6b3b85b61
| Field | From #2226 | To #2878 |
|---|
| note | No Berry–Esseen bound (univariate or multivariate) is in Mathlib. | Verified: no `BerryEsseen`/`Berry_Esseen` declaration in Mathlib. |
modifiedCramér–Wold theoremf6162240a4da
| Field | From #2226 | To #2878 |
|---|
| note | The Cramér–Wold device is not formalized (loogle returns 0 hits for `CramerWold`). | Verified: no `CramerWold`/`Cramer_Wold` declaration in Mathlib. |
modifiedMartingale difference CLTc708422267a1
| Field | From #2226 | To #2878 |
|---|
| note | Mathlib has martingale theory but no martingale CLT (loogle finds no `centralLimit`/martingale match). | Mathlib has martingale theory but no martingale CLT is present. |
modifiedProof of classical CLT via characteristic functions85733343d51f
| Field | From #2226 | To #2878 |
|---|
| note | Mathlib's proof goes via characteristic functions with this key pointwise limit and Lévy's continuity theorem. | Verified: this is the pointwise limit of characteristic functions used with Lévy's continuity theorem in Mathlib's CLT proof. |
modifiedLévy's continuity theorem4e9c12f10bd3
| Field | From #2226 | To #2878 |
|---|
| note | Lévy's continuity theorem is formalized as the equivalence between weak convergence and pointwise convergence of characteristic functions. | Verified: `ProbabilityMeasure.tendsto_iff_tendsto_charFun` is Lévy's continuity theorem. |
modifiedLaw of the iterated logarithmb7cf937424f2
| Field | From #2226 | To #2878 |
|---|
| note | The law of the iterated logarithm is not formalized in Mathlib. | Verified: no `IteratedLog` or `iteratedLogarithm` declaration in Mathlib. |
modifiedStable distribution7c8cefaeb3f4
| Field | From #2226 | To #2878 |
|---|
| note | Stable distributions are not defined in Mathlib (only Cauchy and Gaussian are present). | Verified: no stable distribution defined in Mathlib. |
modifiedCLT restated via characteristic functions9ad4f88c98f4
| Field | From #2226 | To #2878 |
|---|
| note | Mathlib expresses the characteristic function of the normalized sum as a power and shows it converges to the Gaussian char function. | Verified: `charFun_inv_sqrt_mul_sum` expresses the char function of the normalized sum as a power, converging to the Gaussian char function. |
modifiedMultiplicative CLT (Gibrat's law)223932743036
| Field | From #2226 | To #2878 |
|---|
| note | No log-normal distribution or multiplicative CLT is in Mathlib. | Verified: no log-normal distribution or multiplicative CLT in Mathlib. |
modifiedConvergence in distribution612e2878f4e5
| Field | From #2226 | To #2878 |
|---|
| note | Weak convergence of probability measures (convergence in distribution) is formalized via the topology on `ProbabilityMeasure`. | Verified: weak convergence of probability measures characterized via bounded continuous integrals. |
modifiedMultivariate normal (Gaussian) distributionec4d86cabbdd
| Field | From #2226 | To #2878 |
|---|
| note | Multivariate Gaussian distributions are defined in Mathlib though no multidimensional CLT targets them. | Verified: `multivariateGaussian μ S` defined on `EuclideanSpace ℝ ι`. |
modifiedCharacteristic function of a random variable222fb5847931
| Field | From #2226 | To #2878 |
|---|
| note | The characteristic function E[e^{itX}] is formalized as `MeasureTheory.charFun` (module corrected to `…CharacteristicFunction.Basic`). | Verified: `charFun μ t = ∫ x, exp (⟪x, t⟫ * I) ∂μ`. |
addedNormal (Gaussian) distribution on ℝ303e3f8b81df
addedIndependent and identically distributed random variablesb6d00e78d305
addedAlmost sure convergence44a79d66a563
addedConvolution of probability densities0a7d801f63a8
addedTotal variation distance of measures7540447518a1