Commit 2021-09-01 07:45 5b04a896

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 α.