Commit 2021-09-10 13:08 5ce9280f

feat(measure_theory/integral/bochner): generalize the Bochner integral construction (#8939) The construction of the Bochner integral is generalized to a process extending a set function T : set α → (E →L[ℝ] F) from sets to functions in L1. The integral corresponds to T s equal to the linear map E →L[ℝ] E with value λ x, (μ s).to_real • x. The conditional expectation from L1 to L1 will be defined by taking for T the function condexp_ind : set α → (E →L[ℝ] α →₁[μ] E) defined in #8920 .