Bump mathlib

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -5,6 +5,7 @@ import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Expect.Complex
+import LeanAPAP.Prereqs.Inner.Discrete.Basic
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 
 /-!

LeanAPAP/Physics/Unbalancing.lean

@@ -1,7 +1,7 @@
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
-import LeanAPAP.Prereqs.Inner.Discrete.Basic
+import LeanAPAP.Prereqs.Inner.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Weighted
 
 /-!

LeanAPAP/Prereqs/AddChar/Basic.lean

@@ -1,6 +1,6 @@
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Prereqs.Expect.Basic
-import LeanAPAP.Prereqs.Inner.Discrete.Basic
+import LeanAPAP.Prereqs.Inner.Discrete.Defs
 
 open Finset hiding card
 open Fintype (card)

LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean

@@ -1,3 +1,4 @@
+import Mathlib.Algebra.Star.Conjneg
 import Mathlib.Analysis.Complex.Basic
 import LeanAPAP.Prereqs.Function.Translate
 

LeanAPAP/Prereqs/Convolution/Norm.lean

@@ -1,7 +1,8 @@
+import Mathlib.Algebra.Order.Star.Conjneg
 import Mathlib.Data.Real.StarOrdered
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
-import LeanAPAP.Prereqs.Inner.Discrete.Basic
+import LeanAPAP.Prereqs.Inner.Discrete.Defs
 
 /-!
 # Norm of a convolution

LeanAPAP/Prereqs/Convolution/Order.lean

@@ -1,3 +1,4 @@
+import Mathlib.Algebra.Order.Star.Conjneg
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 

LeanAPAP/Prereqs/Convolution/ThreeAP.lean

@@ -2,7 +2,7 @@ import Mathlib.Combinatorics.Additive.AP.Three.Defs
 import Mathlib.Data.Real.StarOrdered
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Defs
-import LeanAPAP.Prereqs.Inner.Discrete.Basic
+import LeanAPAP.Prereqs.Inner.Discrete.Defs
 
 /-!
 # The convolution characterisation of 3AP-free sets

LeanAPAP/Prereqs/Expect/Basic.lean

@@ -4,9 +4,9 @@ import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Algebra.CharP.Defs
 import Mathlib.Algebra.Module.Rat
 import Mathlib.Algebra.Order.Module.Rat
-import Mathlib.Data.Finset.Density
 import Mathlib.Data.Finset.Pointwise.Basic
 import Mathlib.Data.Fintype.BigOperators
+import Mathlib.Data.NNRat.Order
 
 /-!
 # Average over a finset

LeanAPAP/Prereqs/Function/Indicator/Basic.lean

@@ -1,8 +1,9 @@
+import Mathlib.Algebra.AddTorsor
+import Mathlib.Algebra.Star.Conjneg
 import Mathlib.Data.Fintype.Lattice
 import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Function.Indicator.Defs
-import Mathlib.Algebra.AddTorsor
 
 open Finset Function
 open Fintype (card)

LeanAPAP/Prereqs/Function/Translate.lean

@@ -1,6 +1,5 @@
 import Mathlib.Algebra.BigOperators.Pi
-import Mathlib.Algebra.Order.Pi
-import Mathlib.Algebra.Star.Order
+import Mathlib.Algebra.Star.SelfAdjoint
 import Mathlib.Data.ZMod.Basic
 
 /-!
@@ -71,88 +70,6 @@ lemma translate_prod_right (a : α) (f : ι → α → β) (s : Finset ι) :
 
 end translate
 
-/-! ### Conjugation negation operator -/
-
-section conjneg
-variable {ι α β γ : Type*} [AddGroup α]
-
-section CommSemiring
-variable [CommSemiring β] [StarRing β] {f g : α → β}
-
-def conjneg (f : α → β) : α → β := conj fun x ↦ f (-x)
-
-@[simp] lemma conjneg_apply (f : α → β) (x : α) : conjneg f x = conj (f (-x)) := rfl
-@[simp] lemma conjneg_conjneg (f : α → β) : conjneg (conjneg f) = f := by ext; simp
-
-lemma conjneg_injective : Injective (conjneg : (α → β) → α → β) :=
-  Involutive.injective conjneg_conjneg
-
-@[simp] lemma conjneg_inj : conjneg f = conjneg g ↔ f = g := conjneg_injective.eq_iff
-lemma conjneg_ne_conjneg : conjneg f ≠ conjneg g ↔ f ≠ g := conjneg_injective.ne_iff
-
-@[simp] lemma conjneg_conj (f : α → β) : conjneg (conj f) = conj (conjneg f) := rfl
-
-@[simp] lemma conjneg_zero : conjneg (0 : α → β) = 0 := by ext; simp
-@[simp] lemma conjneg_one : conjneg (1 : α → β) = 1 := by ext; simp
-@[simp] lemma conjneg_add (f g : α → β) : conjneg (f + g) = conjneg f + conjneg g := by ext; simp
-
-@[simp] lemma conjneg_sum (s : Finset ι) (f : ι → α → β) :
-    conjneg (∑ i in s, f i) = ∑ i in s, conjneg (f i) := by
-  ext; simp only [map_sum, conjneg_apply, Finset.sum_apply]
-
-@[simp] lemma conjneg_prod (s : Finset ι) (f : ι → α → β) :
-    conjneg (∏ i in s, f i) = ∏ i in s, conjneg (f i) := by
-  ext; simp only [map_prod, conjneg_apply, Finset.prod_apply]
-
-@[simp] lemma conjneg_eq_zero : conjneg f = 0 ↔ f = 0 := by
-  rw [← conjneg_inj, conjneg_conjneg, conjneg_zero]
-
-@[simp]
-lemma conjneg_eq_one : conjneg f = 1 ↔ f = 1 := by rw [← conjneg_inj, conjneg_conjneg, conjneg_one]
-
-lemma conjneg_ne_zero : conjneg f ≠ 0 ↔ f ≠ 0 := conjneg_eq_zero.not
-lemma conjneg_ne_one : conjneg f ≠ 1 ↔ f ≠ 1 := conjneg_eq_one.not
-
-lemma sum_conjneg [Fintype α] (f : α → β) : ∑ a, conjneg f a = ∑ a, conj (f a) :=
-  Fintype.sum_equiv (Equiv.neg _) _ _ fun _ ↦ rfl
-
-@[simp] lemma support_conjneg (f : α → β) : support (conjneg f) = -support f := by
-  ext; simp [starRingEnd_apply]
-
-end CommSemiring
-
-section CommRing
-variable [CommRing β] [StarRing β]
-
-@[simp] lemma conjneg_sub (f g : α → β) : conjneg (f - g) = conjneg f - conjneg g := by ext; simp
-@[simp] lemma conjneg_neg (f : α → β) : conjneg (-f) = -conjneg f := by ext; simp
-
-end CommRing
-
-section OrderedCommSemiring
-variable [OrderedCommSemiring β] [StarRing β] [StarOrderedRing β] {f : α → β}
-
-@[simp] lemma conjneg_nonneg : 0 ≤ conjneg f ↔ 0 ≤ f :=
-  (Equiv.neg _).forall_congr' $ by simp [starRingEnd_apply]
-
-@[simp] lemma conjneg_pos : 0 < conjneg f ↔ 0 < f := by
-  simp_rw [lt_iff_le_and_ne, @ne_comm (α → β) 0, conjneg_nonneg, conjneg_ne_zero]
-
-end OrderedCommSemiring
-
-section OrderedCommRing
-variable [OrderedCommRing β] [StarRing β] [StarOrderedRing β] {f : α → β}
-
-@[simp] lemma conjneg_nonpos : conjneg f ≤ 0 ↔ f ≤ 0 := by
-  simp_rw [← neg_nonneg, ← conjneg_neg, conjneg_nonneg]
-
-@[simp]
-lemma conjneg_neg' : conjneg f < 0 ↔ f < 0 := by simp_rw [← neg_pos, ← conjneg_neg, conjneg_pos]
-
-end OrderedCommRing
-
-end conjneg
-
 open Fintype
 
 variable {α β G 𝕜 : Type*} [AddCommGroup G]

LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean

@@ -1,6 +1,7 @@
 import Mathlib.Data.Finset.Density
 import Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Prereqs.Expect.Complex
+import LeanAPAP.Prereqs.Expect.Order
 import LeanAPAP.Prereqs.NNLpNorm
 
 /-!

LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean

@@ -1,3 +1,4 @@
+import Mathlib.Algebra.Star.Conjneg
 import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.Function.Translate

LeanAPAP/Prereqs/LpNorm/Weighted.lean

@@ -1,3 +1,4 @@
+import Mathlib.Algebra.Star.Conjneg
 import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 

LeanAPAP/Prereqs/NNLpNorm.lean

@@ -3,7 +3,7 @@ import Mathlib.MeasureTheory.Integral.Bochner
 import Mathlib.Tactic.Positivity.Finset
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Prereqs.Expect.Order
+import LeanAPAP.Prereqs.Expect.Basic
 
 open Filter
 open scoped BigOperators ComplexConjugate ENNReal NNReal

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa571ea02a804b52a59e58012b1e21fe4f0514f2",
+   "rev": "8feac540abb781cb1349688c816dc02fae66b49c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ad85095b6112bb3a7ad6c068fd0844d1e35706f2",
+   "rev": "e291aa4de57079b3d2199b9eb7b4b00922b85a7c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6f9a1b99e76899a578a6ca0fd1d435f00428014b",
+   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.42-pre2",
+   "inputRev": "v0.0.42",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b191738f9875e429b3680fecf251652a03f77cee",
+   "rev": "57e84d671a0d63a14c1ccd2bcdfe43bccb5fe6ab",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "929690af200efb291babee737b087d244a70c3c3",
+   "rev": "7afce91e4fcee25c1ed06dca8d71b82bed396776",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c138ab5c566c4268798b24bfcbea2f4c42413cdd",
+   "rev": "0a294fe9bf23b396c5cc955054c50b9b652ec5ad",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e490631b72a43a6a82b4ddd3a2d020b2029491d0",
+   "rev": "09aca1c90e4f75b286d955e1c57b2df75ae51948",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",