feat: port MeasureTheory.Function.ConvergenceInMeasure (#4484)

Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
leanprover-community · Jun 1, 2023 · dc28581 · dc28581
1 parent 0165a5b
commit dc28581
Show file tree

Hide file tree

Showing 2 changed files with 370 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1862,6 +1862,7 @@ import Mathlib.MeasureTheory.Decomposition.UnsignedHahn
 import Mathlib.MeasureTheory.Function.AEEqFun
 import Mathlib.MeasureTheory.Function.AEMeasurableOrder
 import Mathlib.MeasureTheory.Function.AEMeasurableSequence
+import Mathlib.MeasureTheory.Function.ConvergenceInMeasure
 import Mathlib.MeasureTheory.Function.Egorov
 import Mathlib.MeasureTheory.Function.EssSup
 import Mathlib.MeasureTheory.Function.Floor