mathlib

15d987a3 - 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.