Revision #1523 → #1845 · back to history
modifiedDiscrete random variabled4e7d36f5303
| Field | From #1523 | To #1845 |
|---|
| note | Discrete distributions are captured by `PMF`, but `Mathlib` has no class `IsDiscreteRandomVariable`. | Discrete distributions are captured by `PMF`, but Mathlib has no class `IsDiscreteRandomVariable`. |
modifiedProbability distribution of a random variablef90672f5ec1d
| Field | From #1523 | To #1845 |
|---|
| note | The law of `X` is `Measure.map X ℙ`, and `ProbabilityTheory.HasLaw` packages this. | The law of `X` is `Measure.map X ℙ`, packaged also via `ProbabilityTheory.HasLaw`. |
modifiedDensity transformation under invertible differentiable g6cdf72fd63f4
| Field | From #1523 | To #1845 |
|---|
| mathlib.module | Mathlib.MeasureTheory.Function.Jacobian | Mathlib.MeasureTheory.Function.JacobianOneDim |
modifiedExample 2: exponential distribution via transformation88dec761ac15
| Field | From #1523 | To #1845 |
|---|
| mathlib.decl | MeasureTheory.pdf.IsExponential | ProbabilityTheory.exponentialPDF |
| note | Exponential distribution is defined, but this specific transformation example is not formalized. | Exponential distribution is defined via `exponentialPDF`, but this specific transformation example is not formalized. |
modifiedAlmost sure equality5e7e3e383ad5
| Field | From #1523 | To #1845 |
|---|
| mathlib.module | Mathlib.Order.Filter.Basic | Mathlib.Order.Filter.Defs |
addedProbability mass function95b81011c855
addedPushforward measure (law of a random variable)4ce82714ac89
addedProbability density functionf97dfd83102a
addedRadon–Nikodym derivative75f4d8492557
addedVariance and standard deviation0b7647e4f6a1
addedMoment generating function7aa2c811fe33
addedLaw of large numbersb9d24d9c6484
addedCentral limit theorem0a0bd7f2f441
addedConvergence of random variables9877706534a8