mathlib

5b04a896 - feat(measure_theory/conditional_expectation): the integral of the norm of the conditional expectation is lower (#8318)

feat(measure_theory/conditional_expectation): the integral of the norm of the conditional expectation is lower (#8318) Let `m` be a sub-σ-algebra of `m0`, `f` a `m0`-measurable function and `g` a `m`-measurable function, such that their integrals coincide on `m`-measurable sets with finite measure. Then `∫ x in s, ∥g x∥ ∂μ ≤ ∫ x in s, ∥f x∥ ∂μ` on all `m`-measurable sets with finite measure. This PR also defines a notation `measurable[m] f`, to mean that `f : α → β` is measurable with respect to the `measurable_space` `m` on `α`. Co-authored-by: RemyDegenne <remydegenne@gmail.com>