feat(measure_theory/function/conditional_expectation): define the con…

…ditional expectation of a function, prove the equality of integrals (#9114) This PR puts together the generalized Bochner integral construction of #8939 and the set function `condexp_ind` of #8920 to define the conditional expectation of a function. The equality of integrals that defines the conditional expectation is proven in `set_integral_condexp`.
leanprover-community · Sep 24, 2021 · e14cf58 · e14cf58
1 parent 0db6caf
commit e14cf58
Show file tree

Hide file tree

Showing 3 changed files with 551 additions and 5 deletions.
diff --git a/src/measure_theory/decomposition/radon_nikodym.lean b/src/measure_theory/decomposition/radon_nikodym.lean
@@ -14,7 +14,9 @@ This file proves the Radon-Nikodym theorem. The Radon-Nikodym theorem states tha
 In particular, we have `f = radon_nikodym_deriv μ ν`.
 
 The Radon-Nikodym theorem will allow us to define many important concepts in probability theory,
-most notably conditional expectations and probability cumulative functions.
+most notably probability cumulative functions. It could also be used to define the conditional
+expectation of a real function, but we take a different approach (see the file
+`measure_theory/function/conditional_expectation`).
 
 ## Main results