mathlib3

47a3cd26 - feat(probability/integration): Bochner integral of the product of independent functions (#13140)

feat(probability/integration): Bochner integral of the product of independent functions (#13140) This is limited to real-valued functions, which is not very satisfactory but it is not clear (to me) what the most general version of each of those lemmas would be.