Bump mathlib

YaelDillies · Aug 28, 2024 · 471cd18 · 471cd18
1 parent 597ddfa
commit 471cd18
Show file tree

Hide file tree

Showing 19 changed files with 26 additions and 48 deletions.
diff --git a/LeanAPAP.lean b/LeanAPAP.lean
@@ -5,14 +5,12 @@ import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
 import LeanAPAP.Mathlib.Analysis.RCLike.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Mathlib.Data.Fintype.Order
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.MeasureTheory.MeasurableSpace.Defs
 import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpaceDef
-import LeanAPAP.Mathlib.MeasureTheory.Measure.Typeclasses
 import LeanAPAP.Mathlib.Order.Filter.Basic
 import LeanAPAP.Mathlib.Order.LiminfLimsup
 import LeanAPAP.Mathlib.Tactic.Positivity

diff --git a/LeanAPAP/Extras/BSG.lean b/LeanAPAP/Extras/BSG.lean
@@ -1,5 +1,6 @@
 import Mathlib.Combinatorics.Additive.Energy
 import Mathlib.Data.Real.StarOrdered
+import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Order
 
 open BigOperators Finset

diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean
@@ -1,5 +1,5 @@
+import Mathlib.FieldTheory.Finite.Basic
 import LeanAPAP.Prereqs.Convolution.ThreeAP
-import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.Unbalancing

diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean
@@ -1,4 +1,6 @@
-import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
+import Mathlib.Algebra.EuclideanDomain.Basic
+import Mathlib.Algebra.EuclideanDomain.Field
+import Mathlib.Analysis.SpecialFunctions.Complex.Circle
 
 open AddChar Multiplicative Real
 open scoped ComplexConjugate Real

diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@@ -1,5 +1,4 @@
 import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 /-!
 # TODO

diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@@ -1,5 +1,4 @@
 import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Mathlib.Data.ENNReal.Real
 
 noncomputable section
 

diff --git a/LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean b/LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
@@ -1,7 +1,7 @@
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Combinatorics.Additive.DoublingConst
-import Mathlib.Combinatorics.Pigeonhole
 import Mathlib.Data.Complex.ExponentialBounds
+import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Curlog
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund

diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean
@@ -1,4 +1,7 @@
+import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
+import LeanAPAP.Prereqs.Convolution.Order
+import LeanAPAP.Prereqs.Function.Indicator.Basic
 import LeanAPAP.Prereqs.LpNorm.Weighted
 
 /-!

diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean
@@ -1,6 +1,6 @@
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Data.Complex.ExponentialBounds
-import LeanAPAP.Prereqs.Convolution.Discrete.Basic
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Weighted
 
 /-!

diff --git a/LeanAPAP/Prereqs/Convolution/Compact.lean b/LeanAPAP/Prereqs/Convolution/Compact.lean
@@ -1,5 +1,6 @@
-import LeanAPAP.Prereqs.Convolution.Discrete.Basic
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Expect.Complex
+import LeanAPAP.Prereqs.Function.Indicator.Defs
 
 /-!
 # Convolution in the compact normalisation

diff --git a/LeanAPAP/Prereqs/Convolution/Norm.lean b/LeanAPAP/Prereqs/Convolution/Norm.lean
@@ -1,6 +1,6 @@
 import Mathlib.Data.Real.StarOrdered
-import LeanAPAP.Prereqs.Convolution.Order
-import LeanAPAP.Prereqs.LpNorm.Compact
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
+import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
 
 /-!
 # Norm of a convolution

diff --git a/LeanAPAP/Prereqs/Convolution/Order.lean b/LeanAPAP/Prereqs/Convolution/Order.lean
@@ -1,5 +1,5 @@
 import LeanAPAP.Mathlib.Tactic.Positivity
-import LeanAPAP.Prereqs.Convolution.Discrete.Basic
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 
 open Finset Function Real
 open scoped ComplexConjugate NNReal Pointwise

diff --git a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean
@@ -1,5 +1,8 @@
 import Mathlib.Combinatorics.Additive.AP.Three.Defs
-import LeanAPAP.Prereqs.Convolution.Norm
+import Mathlib.Data.Real.StarOrdered
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
+import LeanAPAP.Prereqs.Function.Indicator.Defs
+import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 
 /-!
 # The convolution characterisation of 3AP-free sets

diff --git a/LeanAPAP/Prereqs/Convolution/WithConv.lean b/LeanAPAP/Prereqs/Convolution/WithConv.lean
@@ -1,4 +1,4 @@
-import LeanAPAP.Prereqs.Convolution.Discrete.Basic
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 
 /-!
 # The ring of functions under convolution

diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean
@@ -1,6 +1,7 @@
 import LeanAPAP.Prereqs.AddChar.Basic
-import LeanAPAP.Prereqs.Convolution.Order
-import LeanAPAP.Prereqs.FourierTransform.Compact
+import LeanAPAP.Prereqs.Convolution.Discrete.Basic
+import LeanAPAP.Prereqs.Expect.Complex
+import LeanAPAP.Prereqs.FourierTransform.Discrete
 
 noncomputable section
 

diff --git a/LeanAPAP/Prereqs/FourierTransform/Compact.lean b/LeanAPAP/Prereqs/FourierTransform/Compact.lean
@@ -1,6 +1,7 @@
 import LeanAPAP.Prereqs.Convolution.Compact
-import LeanAPAP.Prereqs.FourierTransform.Discrete
 import LeanAPAP.Prereqs.Expect.Complex
+import LeanAPAP.Prereqs.FourierTransform.Discrete
+import LeanAPAP.Prereqs.Function.Indicator.Basic
 
 /-!
 # Discrete Fourier transform in the compact normalisation

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c8013cf7e8ac16ecaa8d30d18799360769ea5e8b",
+   "rev": "79ef7496100b18304654c1476691e872fa7c491a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,