Revision #3318 → #3973 · back to history
fcb1b6c0b822| Field | From #3318 | To #3973 |
|---|---|---|
| note | The expectation of a random variable is captured by the Bochner integral against a probability measure, but Mathlib does not provide a dedicated decision-theoretic `expectedValue` definition. | Expectation of a random variable is captured by the Bochner integral `MeasureTheory.integral` against a probability measure, but there is no dedicated decision-theoretic `expectedValue` definition. |
e2a03be33259683230a5ad359d58de6fbf7d74198ff65ceb