mathlib3

5c92eb0b - feat(measure_theory/function/conditional_expectation): conditional expectation on real functions equal Radon-Nikodym derivative (#9378)

feat(measure_theory/function/conditional_expectation): conditional expectation on real functions equal Radon-Nikodym derivative (#9378) Co-authored-by: RemyDegenne <Remydegenne@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>