Commit 2021-08-23 16:45 608faf0a

feat(measure_theory/function/conditional_expectation): uniqueness of the conditional expectation (#8802) The main part of the PR is the new file ae_eq_of_integral, in which many different lemmas prove variants of the statement "if two functions have same integral on all sets, then they are equal almost everywhere". In the file conditional_expectation, a similar lemma is written for functions which have same integral on all sets in a sub-sigma-algebra and are measurable with respect to that sigma-algebra. This proves the uniqueness of the conditional expectation.