Bump mathlib

YaelDillies · Aug 25, 2024 · 0e6c20d · 0e6c20d
1 parent fd9430b
commit 0e6c20d
Show file tree

Hide file tree

Showing 18 changed files with 9 additions and 158 deletions.
diff --git a/LeanAPAP.lean b/LeanAPAP.lean
@@ -11,18 +11,12 @@ import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Mathlib.Data.ENNReal.Operations
 import LeanAPAP.Mathlib.Data.ENNReal.Real
-import LeanAPAP.Mathlib.Data.Finset.Density
 import LeanAPAP.Mathlib.Data.Fintype.Order
 import LeanAPAP.Mathlib.Data.NNReal.Basic
-import LeanAPAP.Mathlib.Data.Nat.Cast.Order.Basic
 import LeanAPAP.Mathlib.Data.Rat.Cast.Order
-import LeanAPAP.Mathlib.Data.Real.Sqrt
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.MeasureTheory.MeasurableSpace.Defs
-import LeanAPAP.Mathlib.MeasureTheory.Measure.Count
-import LeanAPAP.Mathlib.MeasureTheory.Measure.Dirac
-import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpace
 import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpaceDef
 import LeanAPAP.Mathlib.MeasureTheory.Measure.Typeclasses
 import LeanAPAP.Mathlib.Order.Filter.Basic
@@ -32,7 +26,6 @@ import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing
 import LeanAPAP.Prereqs.AddChar.Basic
-import LeanAPAP.Prereqs.AddChar.Defs
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 import LeanAPAP.Prereqs.Bohr.Basic
 import LeanAPAP.Prereqs.Bohr.Regular

diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean
@@ -1,8 +1,6 @@
 import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
-import LeanAPAP.Mathlib.Data.Finset.Density
-import LeanAPAP.Mathlib.Data.Nat.Cast.Order.Basic
 import LeanAPAP.Mathlib.Data.Rat.Cast.Order
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.FourierTransform.Compact

diff --git a/LeanAPAP/Mathlib/Data/Finset/Density.lean b/LeanAPAP/Mathlib/Data/Finset/Density.lean
diff --git a/LeanAPAP/Mathlib/Data/Nat/Cast/Order/Basic.lean b/LeanAPAP/Mathlib/Data/Nat/Cast/Order/Basic.lean
diff --git a/LeanAPAP/Mathlib/Data/Real/Sqrt.lean b/LeanAPAP/Mathlib/Data/Real/Sqrt.lean
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean
@@ -1,5 +1,5 @@
 import Mathlib.MeasureTheory.Function.EssSup
-import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpace
+import Mathlib.MeasureTheory.Measure.MeasureSpace
 import LeanAPAP.Mathlib.Order.LiminfLimsup
 
 open Filter MeasureTheory

diff --git a/LeanAPAP/Mathlib/MeasureTheory/Measure/Count.lean b/LeanAPAP/Mathlib/MeasureTheory/Measure/Count.lean
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Measure/Dirac.lean b/LeanAPAP/Mathlib/MeasureTheory/Measure/Dirac.lean
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/LeanAPAP/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
diff --git a/LeanAPAP/Prereqs/AddChar/Basic.lean b/LeanAPAP/Prereqs/AddChar/Basic.lean
@@ -1,5 +1,4 @@
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
-import LeanAPAP.Prereqs.AddChar.Defs
 import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 

diff --git a/LeanAPAP/Prereqs/AddChar/Defs.lean b/LeanAPAP/Prereqs/AddChar/Defs.lean
diff --git a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean
@@ -1,3 +1,4 @@
+import Mathlib.Algebra.DirectSum.AddChar
 import Mathlib.GroupTheory.FiniteAbelian
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Prereqs.AddChar.Basic

diff --git a/LeanAPAP/Prereqs/Bohr/Basic.lean b/LeanAPAP/Prereqs/Bohr/Basic.lean
@@ -1,5 +1,4 @@
 import Mathlib.Analysis.Complex.Basic
-import LeanAPAP.Prereqs.AddChar.Defs
 
 open AddChar Complex Function
 open scoped NNReal

diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean
@@ -63,6 +63,6 @@ lemma nlpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) :
       Complex.coe_iterConv, Complex.ofReal_comp_indicate]
 
 lemma nl2Norm_dft_indicate (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[2] = sqrt s.card := by
-  rw [eq_comm, sqrt_eq_iff_sq_eq]
-  simpa using nlpNorm_dft_indicate_pow 1 s
+  rw [eq_comm, sqrt_eq_iff_eq_sq]
+  simpa [eq_comm] using nlpNorm_dft_indicate_pow 1 s
   all_goals positivity
diff --git a/LeanAPAP/Prereqs/LpNorm/Compact.lean b/LeanAPAP/Prereqs/LpNorm/Compact.lean
@@ -507,7 +507,7 @@ lemma nl2Norm_sq_indicate (s : Finset α) : ‖𝟭_[β] s‖ₙ_[2] ^ 2 = s.den
   simpa using nlpNorm_pow_indicate two_ne_zero s
 
 lemma nl2Norm_indicate (s : Finset α) : ‖𝟭_[β] s‖ₙ_[2] = Real.sqrt s.dens := by
-  rw [eq_comm, sqrt_eq_iff_sq_eq, nl2Norm_sq_indicate] <;> positivity
+  rw [eq_comm, sqrt_eq_iff_eq_sq, nl2Norm_sq_indicate] <;> positivity
 
 @[simp] lemma nl1Norm_indicate (s : Finset α) : ‖𝟭_[β] s‖ₙ_[1] = s.dens := by
   simpa using nlpNorm_pow_indicate one_ne_zero s

diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean
@@ -98,7 +98,7 @@ lemma l2Norm_sq_indicate (s : Finset α) : ‖𝟭_[β] s‖_[2] ^ 2 = s.card :=
   simpa using lpNorm_pow_indicate two_ne_zero s
 
 lemma l2Norm_indicate (s : Finset α) : ‖𝟭_[β] s‖_[2] = Real.sqrt s.card := by
-  rw [eq_comm, sqrt_eq_iff_sq_eq, l2Norm_sq_indicate] <;> positivity
+  rw [eq_comm, sqrt_eq_iff_eq_sq, l2Norm_sq_indicate] <;> positivity
 
 @[simp] lemma l1Norm_indicate (s : Finset α) : ‖𝟭_[β] s‖_[1] = s.card := by
   simpa using lpNorm_pow_indicate one_ne_zero s

diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
@@ -127,7 +127,7 @@ private lemma step_four {k : Fin n → ℕ} :
   · norm_num
   split_ifs with h
   · rw [h.neg_one_pow, one_add_one_eq_two]
-  rw [← Nat.odd_iff_not_even] at h
+  rw [Nat.not_even_iff_odd] at h
   simp [h.neg_one_pow]
 
 -- double_multinomial

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9339d48cc3b7431b6353af47f303691e9d4da229",
+   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7ed205ef984ad7571fa0d6f21e444be1731d200b",
+   "rev": "9b07fb6d08b58de5b55813b29f5ac9aa6fa0b1ad",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,