Commit 2021-07-04 16:29 4ace3b73

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).