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

…5174)
leanprover-community · Jun 17, 2023 · dd44571 · dd44571
1 parent 48f6a19
commit dd44571
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