Bump mathlib

LeanAPAP.lean

@@ -1,16 +1,13 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.Probability.UniformOn
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing
-import LeanAPAP.Prereqs.AddChar.Basic
-import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 import LeanAPAP.Prereqs.Bohr.Arc
 import LeanAPAP.Prereqs.Bohr.Basic
 import LeanAPAP.Prereqs.Bohr.Regular
@@ -25,10 +22,10 @@ import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.FourierTransform.Convolution
 import LeanAPAP.Prereqs.FourierTransform.Discrete
+import LeanAPAP.Prereqs.Function.Dilate
 import LeanAPAP.Prereqs.Function.Indicator.Basic
 import LeanAPAP.Prereqs.Function.Indicator.Complex
 import LeanAPAP.Prereqs.Function.Indicator.Defs
-import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Inner.Function
 import LeanAPAP.Prereqs.Inner.Hoelder.Compact
 import LeanAPAP.Prereqs.Inner.Hoelder.Discrete
@@ -39,5 +36,4 @@ import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Weighted
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 import LeanAPAP.Prereqs.NNLpNorm
-import LeanAPAP.Prereqs.Randomisation
 import LeanAPAP.Prereqs.Rudin

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -1,6 +1,7 @@
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.Data.Complex.ExponentialBounds
+import Mathlib.Tactic.Bound
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Inner.Hoelder.Discrete
@@ -11,7 +12,7 @@ import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 -/
 
 open MeasureTheory
-open scoped Pointwise Combinatorics.Additive
+open scoped Pointwise Combinatorics.Additive translate
 
 namespace Finset
 variable {α : Type*} [DecidableEq α] {s : Finset α} {k : ℕ}
@@ -246,7 +247,7 @@ lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m)
   refine this.trans_eq ?_
   rw [l]
   congr with a : 3
-  refine pow_le_pow_iff_left ?_ ?_ ?_ <;> positivity
+  refine pow_le_pow_iff_left₀ ?_ ?_ ?_ <;> positivity
 
 variable [DiscreteMeasurableSpace G]
 
@@ -374,13 +375,7 @@ lemma T_bound (hK₂ : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ)
   rw [Nat.cast_add_one, ← le_sub_iff_add_le, hk']
   refine (Nat.ceil_lt_add_one ?_).le.trans ?_
   · positivity
-  have : (1 : ℝ) ≤ 128 * (m / ε ^ 2) := by
-    rw [div_eq_mul_one_div]
-    refine one_le_mul_of_one_le_of_one_le (by norm_num1) ?_
-    refine one_le_mul_of_one_le_of_one_le (Nat.one_le_cast.2 hm) ?_
-    refine one_le_one_div (by positivity) ?_
-    rw [sq_le_one_iff hε.le]
-    exact hε'
+  have : (1 : ℝ) ≤ 128 * (m / ε ^ 2) := by rw [div_eq_mul_one_div]; bound
   rw [mul_div_assoc, mul_div_assoc]
   linarith only [this]
 

LeanAPAP/Physics/DRC.lean

@@ -214,9 +214,11 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
       · exact Pi.le_def.1 (dconv_nonneg (R := ℝ) mu_nonneg mu_nonneg) x
       · exact dconv_nonneg indicate_nonneg indicate_nonneg _
       · simpa using hx
-    _ ≤ ∑ x, (μ B₁ ○ μ B₂) x * ((1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂]) ^ p :=
-      sum_le_univ_sum_of_nonneg fun x ↦
-        mul_nonneg (dconv_nonneg (mu_nonneg (β := ℝ)) mu_nonneg _) $ hp.pow_nonneg _
+    _ ≤ ∑ x, (μ B₁ ○ μ B₂) x * ((1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂]) ^ p := by
+      gcongr
+      · intros
+        exact mul_nonneg (dconv_nonneg (mu_nonneg (β := ℝ)) mu_nonneg _) $ hp.pow_nonneg _
+      · exact subset_univ _
     _ = ‖μ_[ℝ] B₁‖_[1] * ‖μ_[ℝ] B₂‖_[1] * ((1 - ε) ^ p * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p)
         := ?_
     _ ≤ _ :=