feat: port MeasureTheory.Function.ConditionalExpectation.CondexpL1 (#…

…5174)
leanprover-community · Jun 25, 2023 · f23969a · f23969a
1 parent 6629bd2
commit f23969a
Show file tree

Hide file tree

Showing 2 changed files with 607 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2134,6 +2134,7 @@ import Mathlib.MeasureTheory.Function.AEEqOfIntegral
 import Mathlib.MeasureTheory.Function.AEMeasurableOrder
 import Mathlib.MeasureTheory.Function.AEMeasurableSequence
 import Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
+import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
 import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
 import Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
 import Mathlib.MeasureTheory.Function.ContinuousMapDense