Commit 2021-09-11 14:06 6823886c

feat(measure_theory/function/conditional_expectation): conditional expectation of an indicator (#8920) This PR builds condexp_ind (s : set α) : E →L[ℝ] α →₁[μ] E, which takes x : E to the conditional expectation of the indicator of the set s with value x, seen as an element of α →₁[μ] E. This linear map will be used in a next PR to define the conditional expectation from L1 to L1, by using the same extension mechanism as in the Bochner integral construction.