Revision #1494 → #1786 · back to history
modifiedProbability0cf745eb944a
| Field | From #1494 | To #1786 |
|---|
| mathlib.decl | IsProbabilityMeasure | MeasureTheory.IsProbabilityMeasure |
modifiedProbability distribution61c4760f45b1
| Field | From #1494 | To #1786 |
|---|
| mathlib.decl | ProbabilityMeasure | MeasureTheory.ProbabilityMeasure |
modifiedProbability measure38b96a6eecfe
| Field | From #1494 | To #1786 |
|---|
| mathlib.decl | IsProbabilityMeasure | MeasureTheory.IsProbabilityMeasure |
modifiedHierarchy of convergence modes939e1998f203
| Field | From #1494 | To #1786 |
|---|
| note | In-probability⇒in-distribution is TendstoInMeasure.tendstoInDistribution, and a.s.⇒in-probability is tendstoInMeasure_of_tendsto_ae. | In-probability⇒in-distribution is TendstoInMeasure.tendstoInDistribution, and a.s.⇒in-probability is available via the ae→inMeasure lemma in ConvergenceInMeasure. |
addedProbability of entire sample space is 120a28bc6d669
addedProbability of null event is 023e0f570fa09
addedDirac delta function0f8f7a20e523
addedσ-algebraafb34b1491d3
addedBorel σ-algebracebc2c8b8348
addedCounting measure856ca9bc9eab
addedLebesgue measure6d23594dd571
addedBrownian motionb883d9b11286
addedIndependent and identically distributede659f64c01bd
addedExpected valuefd5e59aa1cf7
addedVariance172523f017da
addedNormal distribution262eae6b0b8b