Bump mathlib

YaelDillies · Nov 26, 2024 · 0db79d9 · 0db79d9
1 parent b66e535
commit 0db79d9
Show file tree

Hide file tree

Showing 10 changed files with 6 additions and 106 deletions.
diff --git a/LeanAPAP.lean b/LeanAPAP.lean
@@ -1,10 +1,6 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
-import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
-import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Mathlib.Probability.UniformOn
-import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing
@@ -18,6 +14,7 @@ import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Convolution.Order
 import LeanAPAP.Prereqs.Convolution.ThreeAP
+import LeanAPAP.Prereqs.DummyPositivity
 import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.FourierTransform.Convolution

diff --git a/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean b/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
diff --git a/LeanAPAP/Mathlib/Probability/UniformOn.lean b/LeanAPAP/Mathlib/Probability/UniformOn.lean
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
@@ -2,7 +2,6 @@ import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.Data.Complex.ExponentialBounds
 import Mathlib.Tactic.Bound
-import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Inner.Hoelder.Discrete

diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean
@@ -1,7 +1,6 @@
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Analysis.MeanInequalities
 import Mathlib.Tactic.Bound
-import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Prereqs.Rudin

diff --git a/LeanAPAP/Prereqs/Convolution/Order.lean b/LeanAPAP/Prereqs/Convolution/Order.lean
@@ -1,5 +1,5 @@
 import Mathlib.Algebra.Order.Star.Conjneg
-import LeanAPAP.Mathlib.Tactic.Positivity
+import LeanAPAP.Prereqs.DummyPositivity
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 
 open Finset Function Real

diff --git a/LeanAPAP/Mathlib/Tactic/Positivity.lean → LeanAPAP/Prereqs/DummyPositivity.lean b/LeanAPAP/Mathlib/Tactic/Positivity.lean → LeanAPAP/Prereqs/DummyPositivity.lean
diff --git a/LeanAPAP/Prereqs/NNLpNorm.lean b/LeanAPAP/Prereqs/NNLpNorm.lean
@@ -1,9 +1,5 @@
-import Mathlib.Algebra.BigOperators.Expect
-import Mathlib.Algebra.Order.Module.Rat
-import Mathlib.Analysis.Normed.Group.Constructions
 import Mathlib.MeasureTheory.Integral.Bochner
 import Mathlib.Tactic.Positivity.Finset
-import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 
 open Filter
 open scoped BigOperators ComplexConjugate ENNReal NNReal
@@ -184,11 +180,11 @@ lemma nnLpNorm_mono_real {g : α → ℝ} (hg : Memℒp g p μ) (h : ∀ x, ‖f
 
 lemma nnLpNorm_smul_measure_of_ne_zero {f : α → E} {c : ℝ≥0} (hc : c ≠ 0) :
     nnLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • nnLpNorm f p μ := by
-  simp [nnLpNorm, eLpNorm_smul_measure_of_ne_zero'' hc f p μ]
+  simp [nnLpNorm, eLpNorm_smul_measure_of_ne_zero' hc f p μ]
 
 lemma nnLpNorm_smul_measure_of_ne_top (hp : p ≠ ∞) {f : α → E} (c : ℝ≥0) :
     nnLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • nnLpNorm f p μ := by
-  simp [nnLpNorm, eLpNorm_smul_measure_of_ne_top'' hp]
+  simp [nnLpNorm, eLpNorm_smul_measure_of_ne_top' hp]
 
 @[simp] lemma nnLpNorm_conj {K : Type*} [RCLike K] (f : α → K) (p : ℝ≥0∞) (μ : Measure α) :
     nnLpNorm (conj f) p μ = nnLpNorm f p μ := by simp [← nnLpNorm_norm]

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "485efbc439ee0ebdeae8afb0acd24a5e82e2f771",
+   "rev": "7488499a8aad6ffada87ab6db73673d88dc04c97",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fb23240e8b4409f2f23bcd07aa73c7451f216413",
+   "rev": "5ad34c033417c6e6efd3fcd9062fa1764d240209",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,