Revision #3341 → #3885 · back to history
modifiedLyapunov CLT02c1d31e2d6f
| Field | From #3341 | To #3885 |
|---|
| note | Verified: no `Lyapunov`-named declaration in Mathlib and no Lyapunov CLT. | Verified: loogle finds no `Lyapunov`-named declaration in Mathlib and no Lyapunov CLT. |
modifiedLyapunov implies Lindeberg048e79bb5b82
| Field | From #3341 | To #3885 |
|---|
| note | Neither the Lyapunov nor the Lindeberg condition is defined in Mathlib. | Neither the Lyapunov nor the Lindeberg condition is defined in Mathlib (loogle finds no such declarations). |
modifiedLindeberg condition709fe4ba5121
| Field | From #3341 | To #3885 |
|---|
| note | Verified: no declaration containing `Lindeberg` in Mathlib. | Verified: loogle finds no declaration containing `Lindeberg` in Mathlib. |
modifiedBerry–Esseen type bound for multivariate CLT4fa6b3b85b61
| Field | From #3341 | To #3885 |
|---|
| note | Verified: no `BerryEsseen`/`Berry_Esseen` declaration in Mathlib. | Verified: no `BerryEsseen` declaration in Mathlib. |
modifiedCramér–Wold theoremf6162240a4da
| Field | From #3341 | To #3885 |
|---|
| note | Verified: no `CramerWold`/`Cramer_Wold` declaration in Mathlib. | Verified: no `CramerWold` declaration in Mathlib. |
modifiedLaw of the iterated logarithmb7cf937424f2
| Field | From #3341 | To #3885 |
|---|
| note | Verified: no `IteratedLog` or `iteratedLogarithm` declaration in Mathlib. | Verified: no `iteratedLog` declaration in Mathlib. |
modifiedMultiplicative CLT (Gibrat's law)223932743036
| Field | From #3341 | To #3885 |
|---|
| note | Verified: no log-normal distribution or multiplicative CLT in Mathlib. | Verified: no `logNormal` distribution or multiplicative CLT in Mathlib. |
modifiedAlmost sure convergence44a79d66a563
| Field | From #3341 | To #3885 |
|---|
| note | Almost-sure convergence is `∀ᵐ x ∂μ, Tendsto (fun n => X n x) atTop (𝓝 L)` using the `MeasureTheory.ae μ` filter (module corrected from `MeasurableSpace.Basic`). | Almost-sure convergence is `∀ᵐ x ∂μ, Tendsto (fun n => X n x) atTop (𝓝 L)` using the `MeasureTheory.ae μ` filter. |
modifiedTotal variation distance of measures7540447518a1
| Field | From #3341 | To #3885 |
|---|
| mathlib.match_kind | partial | special_case |
| note | Verified: `SignedMeasure.totalVariation` gives the TV of a signed measure (corrected module path from `SignedHahn`); usable to compare log-concave marginals with the Gaussian. | Verified: `SignedMeasure.totalVariation` gives the TV of a signed measure; usable to compare log-concave marginals with the Gaussian. |
modifiedHaar measure on the orthogonal groupb3fd5eb76914
| Field | From #3341 | To #3885 |
|---|
| mathlib.match_kind | partial | generalization |
| note | Mathlib has Haar measure on locally compact groups; the specific normalized Haar measure on O(n,ℝ) is an instance. | Mathlib has Haar measure on locally compact groups; the specific normalized Haar measure on O(n,ℝ) is an instance not stated separately. |
| status | formalized | partial |
addedGlivenko–Cantelli theoremf455b156ad3b
addedCauchy distributionad5e52db1e9c
addedWeak law of large numbers08bb63f4cbc7
addedSample mean72f1136c78ed