feat: port MeasureTheory.Integral.PeakFunction (leanprover-community#…

…4772)
qawbecrdtey · Jun 12, 2023 · 3ab531a · 3ab531a
1 parent 37352ec
commit 3ab531a
Show file tree

Hide file tree

Showing 2 changed files with 329 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2027,6 +2027,7 @@ import Mathlib.MeasureTheory.Integral.IntegralSimps
 import Mathlib.MeasureTheory.Integral.Lebesgue
 import Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
 import Mathlib.MeasureTheory.Integral.MeanInequalities
+import Mathlib.MeasureTheory.Integral.PeakFunction
 import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani
 import Mathlib.MeasureTheory.Integral.SetIntegral
 import Mathlib.MeasureTheory.Integral.SetToL1