Revision #2326 → #3981 · back to history
modifiedKy Fan metric for convergence in probabilitybfec9aabbb37
| Field | From #2326 | To #3981 |
|---|
| anchors | [{"section":"Properties (2)","snippet":"This topology is metrizable by the Ky Fan metric"},{"type":"math_alttext","value":"{\\displaystyle d(X,Y)=\\inf \\!{\\big \\{}\\varepsilon >0:\\ \\mathbb {P} {\\big (}|X-Y|>\\varepsilon {\\big )}\\leq \\varepsilon {\\big \\}}}"},{"type":"math_alttext","value":"{\\displaystyle d(X,Y)=\\mathbb {E} \\left[\\min(|X-Y|,1)\\right].}"}] | — |
modifiedConvergence in distribution without convergence in probability924be299f32f
| Field | From #2326 | To #3981 |
|---|
| anchors | [{"section":"Counterexamples","snippet":"consider a sequence of standard normal random variables"},{"type":"math_alttext","value":"{\\displaystyle P(|X_{n}-Y_{n}|\\geq \\epsilon )=P(|X_{n}|\\cdot |(1-(-1)^{n})|\\geq \\epsilon )}"}] | — |
modifiedAlmost sure convergencea6d1679405e2
| Field | From #2326 | To #3981 |
|---|
| anchors | [{"section":"Definition (3)","snippet":"converges almost surely"},{"type":"math_alttext","value":"{\\displaystyle \\mathbb {P} \\!\\left(\\lim _{n\\to \\infty }\\!X_{n}=X\\right)=1.}"}] | — |
| mathlib.module | Mathlib.Order.Filter.Basic | Mathlib.Order.Filter.Defs |
modifiedAlmost sure convergence via limit superior of sets7e1f4fe2c9e9
| Field | From #2326 | To #3981 |
|---|
| anchors | [{"section":"Definition (3)","snippet":"Using the notion of the limit superior of a sequence of sets"},{"type":"math_alttext","value":"{\\displaystyle \\mathbb {P} {\\Bigl (}\\limsup _{n\\to \\infty }{\\bigl \\{}\\omega \\in \\Omega :|X_{n}(\\omega )-X(\\omega )|>\\varepsilon {\\bigr \\}}{\\Bigr )}=0\\quad {\\text{for all}}\\quad \\varepsilon >0.}"}] | — |
modifiedAlmost sure convergence on metric spaces6b128f2a61b6
| Field | From #2326 | To #3981 |
|---|
| anchors | [{"section":"Definition (3)","snippet":"For generic random elements"},{"type":"math_alttext","value":"{\\displaystyle \\mathbb {P} {\\Bigl (}\\omega \\in \\Omega \\colon \\,d{\\big (}X_{n}(\\omega ),X(\\omega ){\\big )}\\,{\\underset {n\\to \\infty }{\\longrightarrow }}\\,0{\\Bigr )}=1}"}] | — |
| mathlib.module | Mathlib.Order.Filter.Basic | Mathlib.Order.Filter.Defs |
modifiedSure (pointwise) convergencee3c406c01497
| Field | From #2326 | To #3981 |
|---|
| mathlib.module | Mathlib.Order.Filter.Basic | Mathlib.Order.Filter.Defs |
modifiedConvergence in r-th meand70a45bd11d9
| Field | From #2326 | To #3981 |
|---|
| mathlib.module | Mathlib.MeasureTheory.Function.LpSeminorm.Basic | Mathlib.MeasureTheory.Function.LpSeminorm.Defs |
modifiedConvergence in mean and mean square960e31bd2cee
| Field | From #2326 | To #3981 |
|---|
| mathlib.module | Mathlib.MeasureTheory.Function.LpSeminorm.Basic | Mathlib.MeasureTheory.Function.LpSeminorm.Defs |
addedCentral limit theorem202660968292
addedConvergence in distribution (cdf pointwise at continuity points)483de72f7314
deletedAlmost sure convergence implies convergence in probability11962d06981c
deletedConvergence in probability implies convergence in distributiond457c74a27c3
deletedr-th order mean implies convergence in probabilityc1ca5de4386a
deletedHigher order mean implies lower order mean9cdced105dbb
deletedConvergence in distribution to constant implies in probability0040d68ba809