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.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: RemyDegenne

src/analysis/normed_space/hahn_banach.lean

@@ -157,4 +157,18 @@ begin
   { exact exists_dual_vector 𝕜 x hx }
 end
 
+/-- Variant of Hahn-Banach, eliminating the hypothesis that `x` be nonzero, but only ensuring that
+    the dual element has norm at most `1` (this can not be improved for the trivial
+    vector space). -/
+theorem exists_dual_vector'' (x : E) :
+  ∃ g : E →L[𝕜] 𝕜, ∥g∥ ≤ 1 ∧ g x = norm' 𝕜 x :=
+begin
+  by_cases hx : x = 0,
+  { refine ⟨0, by simp, _⟩,
+    symmetry,
+    simp [hx], },
+  { rcases exists_dual_vector 𝕜 x hx with ⟨g, g_norm, g_eq⟩,
+    exact ⟨g, g_norm.le, g_eq⟩ }
+end
+
 end dual_vector