mathlib3

6dd5e43c - feat(measure_theory/function/uniform_integrable): conditional expectations form a uniformly integrable class (#15378)

feat(measure_theory/function/uniform_integrable): conditional expectations form a uniformly integrable class (#15378) Useful for the L1 martingale convergence theorem. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>