Bump mathlib

YaelDillies · Sep 11, 2024 · 63833e4 · 63833e4
1 parent 66453e9
commit 63833e4
Show file tree

Hide file tree

Showing 9 changed files with 5 additions and 149 deletions.
diff --git a/LeanAPAP.lean b/LeanAPAP.lean
@@ -17,7 +17,6 @@ import LeanAPAP.Mathlib.Algebra.Order.Ring.Defs
 import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom
 import LeanAPAP.Mathlib.Data.Complex.Basic
@@ -33,9 +32,7 @@ import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.MeasureTheory.Measure.Count
 import LeanAPAP.Mathlib.Order.CompleteLattice
-import LeanAPAP.Mathlib.Order.Filter.Basic
 import LeanAPAP.Mathlib.Order.Hom.Basic
-import LeanAPAP.Mathlib.Order.LiminfLimsup
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC

diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean
@@ -1,7 +1,6 @@
 import Mathlib.MeasureTheory.Function.EssSup
 import Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.MeasureTheory.Measure.Count
-import LeanAPAP.Mathlib.Order.LiminfLimsup
 
 open Filter MeasureTheory ProbabilityTheory
 open scoped ENNReal

diff --git a/LeanAPAP/Mathlib/Order/Filter/Basic.lean b/LeanAPAP/Mathlib/Order/Filter/Basic.lean
diff --git a/LeanAPAP/Mathlib/Order/LiminfLimsup.lean b/LeanAPAP/Mathlib/Order/LiminfLimsup.lean
diff --git a/LeanAPAP/Prereqs/LpNorm/Compact.lean b/LeanAPAP/Prereqs/LpNorm/Compact.lean
@@ -3,7 +3,6 @@ import Mathlib.Data.Finset.Density
 import Mathlib.Data.Fintype.Order
 import Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
-import LeanAPAP.Mathlib.Order.Filter.Basic
 import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Expect.Order
 import LeanAPAP.Prereqs.Function.Translate

diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
@@ -1,6 +1,5 @@
 import Mathlib.Data.Fintype.Order
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
-import LeanAPAP.Mathlib.Order.Filter.Basic
 import LeanAPAP.Prereqs.NNLpNorm
 
 /-!

diff --git a/LeanAPAP/Prereqs/NNLpNorm.lean b/LeanAPAP/Prereqs/NNLpNorm.lean
@@ -2,7 +2,6 @@ import Mathlib.Analysis.Normed.Group.Constructions
 import Mathlib.MeasureTheory.Integral.Bochner
 import Mathlib.Tactic.Positivity.Finset
 import LeanAPAP.Mathlib.Algebra.Order.Module.Rat
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Prereqs.Expect.Basic
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8feac540abb781cb1349688c816dc02fae66b49c",
+   "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e291aa4de57079b3d2199b9eb7b4b00922b85a7c",
+   "rev": "e5e4f1e9385f5a636cd95f7b5833d9ba7907115c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3e96ea03edd48b932566ca9b201285ae2d57130d",
+   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "57e84d671a0d63a14c1ccd2bcdfe43bccb5fe6ab",
+   "rev": "4b83244f3ea8cf1ebc70f68bc5b94691e826c827",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "09aca1c90e4f75b286d955e1c57b2df75ae51948",
+   "rev": "1b0072fea2aa6a0ef8ef8b506ec5223b184cb4d0",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",