Commit 2021-09-24 12:53 e14cf589

feat(measure_theory/function/conditional_expectation): define the conditional expectation of a function, prove the equality of integrals (#9114) This PR puts together the generalized Bochner integral construction of #8939 and the set function condexp_ind of #8920 to define the conditional expectation of a function. The equality of integrals that defines the conditional expectation is proven in set_integral_condexp.