Commit 2026-05-21 09:29 fca9f6f5

feat: drop completeness assumption in the definition of setToFun, expand API (#39615) The definition of the Bochner integral and the vector measure integral handle the non-completeness of the space in a completely parallel way. To avoid duplication and streamline proofs, we move this handling of non-completeness one step higher, to the definition of setToFun. We also expand its API -- this is cherry-picked from a work on vector measure integrals that has highlighted the need for the lemmas I am adding here. To minimize the size of the PR, I went for minimal fixes in the files on Bochner integrals and on conditional expectations. Further cleanup will be done in subsequent PRs.