feat: port MeasureTheory.Integral.IntervalIntegral (#4710)

Co-authored-by: Johan Commelin <johan@commelin.net>
leanprover-community · Jun 7, 2023 · 5e32f28 · 5e32f28
1 parent ae860a6
commit 5e32f28
Show file tree

Hide file tree

Showing 3 changed files with 1,449 additions and 3 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2028,6 +2028,7 @@ import Mathlib.MeasureTheory.Integral.Average
 import Mathlib.MeasureTheory.Integral.Bochner
 import Mathlib.MeasureTheory.Integral.IntegrableOn
 import Mathlib.MeasureTheory.Integral.IntegralSimps
+import Mathlib.MeasureTheory.Integral.IntervalIntegral
 import Mathlib.MeasureTheory.Integral.Lebesgue
 import Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
 import Mathlib.MeasureTheory.Integral.MeanInequalities