mathlib3

dba3dcef - feat(measure_theory/function/conditional_expectation): monotonicity of the conditional expectation (#15024)

feat(measure_theory/function/conditional_expectation): monotonicity of the conditional expectation (#15024) Co-authored-by: RemyDegenne <Remydegenne@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>