Bump mathlib

LeanAPAP.lean

@@ -1,19 +1,10 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
-import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
-import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
-import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic
-import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
-import LeanAPAP.Mathlib.Data.Complex.Basic
 import LeanAPAP.Mathlib.Data.ENNReal.Basic
-import LeanAPAP.Mathlib.Data.ENNReal.Operations
-import LeanAPAP.Mathlib.Data.ENNReal.Real
-import LeanAPAP.Mathlib.Data.Real.ConjExponents
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Mathlib.Order.Hom.Basic
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
@@ -22,7 +13,6 @@ import LeanAPAP.Prereqs.AddChar.Basic
 import LeanAPAP.Prereqs.AddChar.MeasurableSpace
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 import LeanAPAP.Prereqs.Balance.Complex
-import LeanAPAP.Prereqs.Balance.Defs
 import LeanAPAP.Prereqs.Bohr.Arc
 import LeanAPAP.Prereqs.Bohr.Basic
 import LeanAPAP.Prereqs.Bohr.Regular
@@ -34,7 +24,6 @@ import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Convolution.Order
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.Energy
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.FourierTransform.Convolution
 import LeanAPAP.Prereqs.FourierTransform.Discrete

LeanAPAP/Extras/BSG.lean

@@ -239,7 +239,7 @@ lemma claim_eight (c : ℝ) (hc : 0 ≤ c) (hA : (0 : ℝ) < card A) (hB : (0 :
 lemma test_case {E A B : ℕ} {K : ℝ} (hK : 0 < K) (hE : K⁻¹ * (A ^ 2 * B) ≤ E)
     (hA : 0 < A) (hB : 0 < B) :
     A / (Real.sqrt 2 * K) ≤ Real.sqrt 2⁻¹ * (E / (A * B)) := by
-  rw [inv_mul_le_iff hK] at hE
+  rw [inv_mul_le_iff₀ hK] at hE
   rw [mul_div_assoc', div_le_div_iff, ← mul_assoc, ← sq]
   rotate_left
   · positivity
@@ -266,7 +266,7 @@ lemma lemma_one {c K : ℝ} (hc : 0 < c) (hK : 0 < K)
       Real.sqrt_sq (by positivity)] at this
     refine this.trans' ?_
     -- I'd like automation to handle the rest of this
-    rw [inv_mul_le_iff hK] at hE
+    rw [inv_mul_le_iff₀ hK] at hE
     rw [mul_div_assoc', div_le_div_iff, ← mul_assoc, ← sq]
     rotate_left
     · positivity

LeanAPAP/FiniteField.lean

@@ -1,5 +1,4 @@
 import Mathlib.FieldTheory.Finite.Basic
-import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic
 import LeanAPAP.Prereqs.Balance.Complex
 import LeanAPAP.Prereqs.Chang
 import LeanAPAP.Prereqs.Convolution.ThreeAP
@@ -193,7 +192,7 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
     calc
       (↑(finrank (ZMod q) G - finrank (ZMod q) V) : ℝ)
         ≤ ↑(finrank (ZMod q) G - finrank (ZMod q) W) := by
-        gcongr; exact Submodule.finrank_le_finrank_of_le hWV
+        gcongr; exact Submodule.finrank_mono hWV
       _ ≤ Δ'.card := sorry
       _ ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖μ T‖_[1] ^ 2 / ‖μ T‖_[2] ^ 2 / card G)⌉₊ / 2⁻¹ ^ 2⌉₊ := by
         gcongr
@@ -289,7 +288,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
           (2⁻¹ : ℝ) ≤ 2 ^ 15 * 1 * 1 := by norm_num
           _ ≤ 2 ^ 15 * ε⁻¹ ^ 3 * 𝓛 γ := ?_
         gcongr
-        exact one_le_pow₀ (one_le_inv hε₀ hε₁.le) _
+        exact one_le_pow₀ (one_le_inv hε₀ hε₁.le)
       _ = 2 ^ 17 * 𝓛 γ / ε ^ 3 := by ring
   obtain ⟨A₁, A₂, hA, hA₁, hA₂⟩ : ∃ (A₁ A₂ : Finset G),
       1 - ε / 32 ≤ ∑ x ∈ s q' (ε / 16) univ univ A, (μ A₁ ○ μ A₂) x ∧
@@ -341,7 +340,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
     ap_in_ff' _ (by positivity)
     (calc
       4⁻¹ * (A.dens : ℝ) ^ (2 * q') ≤ 4⁻¹ * 1 := by
-        gcongr; exact pow_le_one _ (by positivity) $ mod_cast A.dens_le_one
+        gcongr; exact pow_le_one₀ (by positivity) $ mod_cast A.dens_le_one
       _ ≤ 2⁻¹ := by norm_num) (by positivity) (by linarith) hA₁ hA₂
   replace hV :=
     calc
@@ -362,7 +361,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
           𝓛 (ε / 32 * (4⁻¹ * α ^ (2 * q'))) ^ 2 * (ε / 32)⁻¹ ^ 2 := hVdim
       _ ≤ 2 ^ 32 * (8 * q' * 𝓛 α) ^ 2 *
           (2 ^ 8 * q' * 𝓛 α / ε) ^ 2 * (ε / 32)⁻¹ ^ 2 := by
-        have : α ^ (2 * q') ≤ 1 := pow_le_one _ hα₀.le hα₁
+        have : α ^ (2 * q') ≤ 1 := pow_le_one₀ hα₀.le hα₁
         have : 4⁻¹ * α ^ (2 * q') ≤ 1 := mul_le_one (by norm_num) (by positivity) ‹_›
         have : ε / 32 * (4⁻¹ * α ^ (2 * q')) ≤ 1 := mul_le_one (by linarith) (by positivity) ‹_›
         have : 0 ≤ log (ε / 32 * (4⁻¹ * α ^ (2 * q')))⁻¹ :=
@@ -526,7 +525,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
     calc
       _ ≤ (1 : ℝ) := mod_cast dens_le_one
       _ < _ := ?_
-    rw [← inv_pos_lt_iff_one_lt_mul, lt_pow_iff_log_lt, ← div_lt_iff]
+    rw [← inv_pos_lt_iff_one_lt_mul, lt_pow_iff_log_lt, ← div_lt_iff₀]
     calc
       log α⁻¹ / log (65 / 64)
         < ⌊log α⁻¹ / log (65 / 64)⌋₊ + 1 := Nat.lt_floor_add_one _

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -3,7 +3,6 @@ import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Inner.Hoelder.Discrete
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 
@@ -363,7 +362,7 @@ lemma T_bound (hK₂ : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ)
     refine h₂.trans (mul_le_mul_of_nonneg_right hK₂ (Nat.cast_nonneg _))
     exact zero_lt_two
   rw [neg_mul, neg_div, Real.rpow_neg hK.le, mul_left_comm,
-    inv_mul_le_iff (Real.rpow_pos_of_pos hK _)]
+    inv_mul_le_iff₀ (Real.rpow_pos_of_pos hK _)]
   refine (mul_le_mul_of_nonneg_right this (Nat.cast_nonneg _)).trans ?_
   rw [mul_assoc]
   rw [← @Nat.cast_le ℝ, Nat.cast_mul] at h₁

LeanAPAP/Physics/DRC.lean

@@ -87,7 +87,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
   set M : ℝ :=
     2 ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p * (sqrt B₁.card * sqrt B₂.card) / A.card ^ p
       with hM_def
-  have hM : 0 < M := by rw [hM_def]; sorry -- positivity
+  have hM : 0 < M := by rw [hM_def]; positivity
   replace hf : 0 < ∑ x, (μ_[ℝ] B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * f x := by
     have : 0 ≤ μ_[ℝ] B₁ ○ μ B₂ * (𝟭 A ○ 𝟭 A) ^ p * (↑) ∘ f :=
       mul_nonneg (mul_nonneg (dconv_nonneg mu_nonneg mu_nonneg) $ pow_nonneg
@@ -148,7 +148,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     refine (le_or_lt_of_add_le_add ?_).resolve_left h.not_le
     simp_rw [← not_le, ← compl_filter, ← two_mul, ← mul_add, sum_compl_add_sum]
     rfl
-  rw [← lt_div_iff' (zero_lt_two' ℝ), div_eq_inv_mul]
+  rw [← lt_div_iff₀' (zero_lt_two' ℝ), div_eq_inv_mul]
   calc
     ∑ s with g s < M ^ 2, g s = ∑ s with g s < M ^ 2 ∧ g s ≠ 0, sqrt (g s) * sqrt (g s)
           := by simp_rw [mul_self_sqrt (hg _), ← filter_filter, sum_filter_ne_zero]
@@ -189,7 +189,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
         c.Nonempty := by
     simp_rw [nonempty_iff_ne_empty]
     rintro c r h rfl
-    simp [pow_mul', (zero_lt_four' ℝ).not_le, inv_mul_le_iff (zero_lt_four' ℝ), mul_assoc,
+    simp [pow_mul', (zero_lt_four' ℝ).not_le, inv_mul_le_iff₀ (zero_lt_four' ℝ), mul_assoc,
       div_nonpos_iff, mul_nonpos_iff, (pow_pos (dLpNorm_conv_pos hp₀.ne' hB hA) 2).not_le] at h
     norm_cast at h
     simp [hp₀, hp₀.ne', hA.ne_empty] at h
@@ -233,7 +233,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
     (1 - ε) ^ p ≤ exp (-ε) ^ p := pow_le_pow_left (sub_nonneg.2 hε₁) (one_sub_le_exp_neg _) _
     _ = exp (-(ε * p)) := by rw [← neg_mul, exp_mul, rpow_natCast]
     _ ≤ exp (-log (2 / δ)) :=
-      (exp_monotone $ neg_le_neg $ (inv_mul_le_iff $ by positivity).1 hpε)
+      (exp_monotone $ neg_le_neg $ (inv_mul_le_iff₀ $ by positivity).1 hpε)
     _ = δ / 2 := by rw [exp_neg, exp_log, inv_div]; positivity
 
 -- TODO: When `1 < ε`, the result is trivial since `S = univ`.

LeanAPAP/Physics/Unbalancing.lean

@@ -1,6 +1,5 @@
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Data.Complex.ExponentialBounds
-import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Complex
 import LeanAPAP.Prereqs.Inner.Weighted
@@ -105,7 +104,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
   set T := univ.filter fun i ↦ 3 / 4 * ε ≤ f i
   have hTP : T ⊆ P := monotone_filter_right _ fun i ↦ le_trans $ by positivity
   have : 2⁻¹ * ε ^ p ≤ ∑ i in P, ↑(ν i) * (f ^ p) i := by
-    rw [inv_mul_le_iff (zero_lt_two' ℝ), sum_filter]
+    rw [inv_mul_le_iff₀ (zero_lt_two' ℝ), sum_filter]
     convert this using 3
     rw [Pi.posPart_apply, posPart_eq_ite]
     split_ifs <;> simp [pow_sub_one_mul hp₁.pos.ne']

LeanAPAP/Prereqs/Balance/Complex.lean

@@ -1,8 +1,9 @@
-import LeanAPAP.Prereqs.Balance.Defs
-import LeanAPAP.Prereqs.Expect.Complex
+import Mathlib.Algebra.BigOperators.Balance
+import Mathlib.Analysis.RCLike.Basic
+import Mathlib.Data.Complex.BigOperators
 
-open Finset
-open scoped BigOperators NNReal
+open Fintype
+open scoped NNReal
 
 namespace Complex
 variable {ι : Type*}
@@ -28,4 +29,3 @@ lemma coe_balance : (↑(balance f a) : 𝕜) = balance ((↑) ∘ f) a := map_b
   simp [balance]
 
 end RCLike
-