feat(probability_theory/notation): add notations for expected value, conditional expectation (#9469)
feat(probability_theory/notation): add notations for expected value, conditional expectation (#9469)

When working in probability theory, the measure on the space is most often implicit. With our current notations for measure spaces, that means writing `volume` in a lot of places. To avoid that and introduce notations closer to the usual practice, this PR defines
- `𝔼[X]` for the expected value (integral) of a function `X` over the volume measure,
- `P[X]` for the expected value over the measure `P`,
- `𝔼[X | hm]` for the conditional expectation with respect to the volume,
- `X =ₐₛ Y` for `X =ᵐ[volume] Y` and similarly for `X ≤ᵐ[volume] Y`,
- `∂P/∂Q` for `P.rn_deriv Q`

All notations are localized to the `probability_theory` namespace.






leanprover-community/mathlib,leanprover-community/mathlib