feat(measure_theory/function/conditional_expectation): conditional ex…

…pectation 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.