mathlib3

4ace3b73 - feat(measure_theory/conditional_expectation): define the Lp subspace of functions measurable wrt a sigma-algebra, prove completeness (#7945)

feat(measure_theory/conditional_expectation): define the Lp subspace of functions measurable wrt a sigma-algebra, prove completeness (#7945) This is the first step towards defining the conditional expectation: - in this PR a subspace of L^p is shown to be complete, which is necessary to define an orthogonal projection on that subspace; - the conditional expectation of functions in L^2 will be the orthogonal projection; - the definition will be extended to L^1 through simple functions (as is done for the integral definition).