Bump mathlib

LeanAPAP.lean

@@ -2,34 +2,22 @@ import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
-import LeanAPAP.Mathlib.Algebra.Group.Basic
-import LeanAPAP.Mathlib.Algebra.Group.Pointwise.Finset
-import LeanAPAP.Mathlib.Algebra.Group.Subgroup.Basic
-import LeanAPAP.Mathlib.Algebra.Order.Floor
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
 import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
-import LeanAPAP.Mathlib.Algebra.Order.Module.Rat
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic
-import LeanAPAP.Mathlib.Algebra.Order.Ring.Cast
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Defs
 import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
-import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom
 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.Finset.Density
-import LeanAPAP.Mathlib.Data.Finset.Preimage
 import LeanAPAP.Mathlib.Data.Fintype.Basic
 import LeanAPAP.Mathlib.Data.Real.ConjExponents
 import LeanAPAP.Mathlib.Data.ZMod.Module
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Mathlib.MeasureTheory.Measure.Count
-import LeanAPAP.Mathlib.Order.CompleteLattice
 import LeanAPAP.Mathlib.Order.Hom.Basic
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
@@ -73,6 +61,5 @@ import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Weighted
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 import LeanAPAP.Prereqs.NNLpNorm
-import LeanAPAP.Prereqs.PointwiseDensity
 import LeanAPAP.Prereqs.Randomisation
 import LeanAPAP.Prereqs.Rudin

LeanAPAP/FiniteField.lean

@@ -1,17 +1,12 @@
 import Mathlib.FieldTheory.Finite.Basic
-import LeanAPAP.Mathlib.Algebra.Group.Subgroup.Basic
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic
-import LeanAPAP.Mathlib.Algebra.Order.Ring.Cast
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Defs
-import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom
 import LeanAPAP.Mathlib.Data.Finset.Density
-import LeanAPAP.Mathlib.Data.Finset.Preimage
 import LeanAPAP.Mathlib.Data.ZMod.Module
 import LeanAPAP.Prereqs.Chang
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.FourierTransform.Convolution
 import LeanAPAP.Prereqs.Inner.Function
-import LeanAPAP.Prereqs.PointwiseDensity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing
@@ -22,7 +17,7 @@ import LeanAPAP.Physics.Unbalancing
 
 set_option linter.haveLet 0
 
-attribute [-simp] div_pow Real.log_inv
+attribute [-simp] Real.log_inv
 
 open FiniteDimensional Fintype Function Real MeasureTheory
 open Finset hiding card
@@ -188,10 +183,10 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
         _ ≤ 2 ^ 12 * 𝓛 α * (2 * 𝓛 α) * (2 ^ 3 * 𝓛 (ε * α)) ^ 2 / ε ^ 2 := by
           gcongr
           · exact le_add_of_nonneg_left zero_le_one
-          · exact (Int.ceil_lt_two_mul $ one_le_curlog hα₀.le hα₁).le
+          · exact Int.ceil_le_two_mul <| two_inv_lt_one.le.trans <| one_le_curlog hα₀.le hα₁
           · calc
               k ≤ 2 * 𝓛 (ε * α / 4) :=
-                (Nat.ceil_lt_two_mul $ one_le_curlog (by positivity) sorry).le
+                Nat.ceil_le_two_mul <| two_inv_lt_one.le.trans <| one_le_curlog (by positivity) sorry
               _ ≤ 2 * (4 * 𝓛 (ε * α)) := by
                 gcongr
                 exact curlog_div_le (by positivity) (mul_le_one hε₁ hα₀.le hα₁) (by norm_num)
@@ -211,11 +206,14 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
         · calc
             exp 1 ^ 2 ≤ 2.7182818286 ^ 2 := by gcongr; exact exp_one_lt_d9.le
             _ ≤ 2 ^ 3 := by norm_num
-        · exact (Nat.ceil_lt_two_mul $ one_le_curlog (by positivity) $ mod_cast T.dens_le_one).le
+        · exact Nat.ceil_le_two_mul <| two_inv_lt_one.le.trans <|
+            one_le_curlog (by positivity) <| mod_cast T.dens_le_one
       _ = ⌈2 ^ 11 * 𝓛 T.dens⌉₊ := by ring_nf
-      _ ≤ 2 * (2 ^ 11 * 𝓛 T.dens) :=
-        (Nat.ceil_lt_two_mul $ one_le_mul_of_one_le_of_one_le (by norm_num) $
-          one_le_curlog (by positivity) $ mod_cast T.dens_le_one).le
+      _ ≤ 2 * (2 ^ 11 * 𝓛 T.dens) := Nat.ceil_le_two_mul <|
+          calc
+            (2⁻¹ : ℝ) ≤ 2 ^ 11 * 1 := by norm_num
+            _ ≤ 2 ^ 11 * 𝓛 T.dens := by
+              gcongr; exact one_le_curlog (by positivity) $ mod_cast T.dens_le_one
       _ = 2 ^ 12 * 𝓛 T.dens := by ring
       _ ≤ 2 ^ 12 * (1 + 2 ^ 19 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2) := by gcongr
       _ ≤ 2 ^ 12 * (2 ^ 19 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 +
@@ -284,12 +282,16 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
         gcongr
         · assumption
         · norm_num
-        · exact (Nat.ceil_lt_two_mul ‹_›).le
+        · exact Nat.ceil_le_two_mul <| two_inv_lt_one.le.trans ‹_›
       _ = 2 * ⌈2 ^ 15 * ε⁻¹ ^ 3 * 𝓛 γ⌉₊ := by ring_nf
       _ ≤ 2 * (2 * (2 ^ 15 * ε⁻¹ ^ 3 * 𝓛 γ)) := by
         gcongr
-        exact (Nat.ceil_lt_two_mul $ one_le_mul_of_one_le_of_one_le (one_le_mul_of_one_le_of_one_le
-          (by norm_num) $ one_le_pow₀ (one_le_inv hε₀ hε₁.le) _) ‹_›).le
+        refine Nat.ceil_le_two_mul ?_
+        calc
+          (2⁻¹ : ℝ) ≤ 2 ^ 15 * 1 * 1 := by norm_num
+          _ ≤ 2 ^ 15 * ε⁻¹ ^ 3 * 𝓛 γ := ?_
+        gcongr
+        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 ∧

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -1,7 +1,6 @@
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.Data.Complex.ExponentialBounds
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Expect.Complex
@@ -451,7 +450,7 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
           calc
             _ ≤ 2.7182818286 ^ 2 := pow_le_pow_left (by positivity) exp_one_lt_d9.le _
             _ ≤ _ := by norm_num
-      _ = _ := by simp [div_div_eq_mul_div, ← mul_div_right_comm, mul_right_comm]
+      _ = _ := by simp [div_div_eq_mul_div, ← mul_div_right_comm, mul_right_comm, div_pow]
       _ ≤ _ := hKT
   set F : G → ℂ := τ t (μ A ∗ 𝟭 B) - μ A ∗ 𝟭 B
   have (x) :=

LeanAPAP/Physics/DRC.lean

@@ -122,7 +122,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     have : (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p)
       ≤ (A₁ s).card / B₁.card * ((A₂ s).card / B₂.card) := by
       rw [div_mul_div_comm, le_div_iff₀]
-      simpa [hg_def, hM_def, mul_pow, pow_mul', show (2 : ℝ) ^ 2 = 4 by norm_num,
+      simpa [hg_def, hM_def, mul_pow, div_pow, pow_mul', show (2 : ℝ) ^ 2 = 4 by norm_num,
         mul_div_right_comm] using h
       positivity
     refine ⟨(lt_of_mul_lt_mul_left (hs.trans_eq' ?_) $ hg s).le, this.trans $ mul_le_of_le_one_right

LeanAPAP/Physics/Unbalancing.lean

@@ -1,7 +1,5 @@
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Data.Complex.ExponentialBounds
-import LeanAPAP.Mathlib.Algebra.Order.Floor
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
 import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Complex
@@ -217,10 +215,19 @@ lemma unbalancing' (p : ℕ) (hp : p ≠ 0) (ε : ℝ) (hε₀ : 0 < ε) (hε₁
   · calc
       (⌈120 / ε * log (3 / ε) * p⌉₊ : ℝ)
         = ⌈120 * ε⁻¹ * log (3 * ε⁻¹) * p⌉₊ := by simp [div_eq_mul_inv]
-      _ ≤ 2 * (120 * ε⁻¹ * log (3 * ε⁻¹) * p) :=
-        (Nat.ceil_lt_two_mul $ one_le_mul_of_one_le_of_one_le
-          (one_le_mul_of_one_le_of_one_le (one_le_mul_of_one_le_of_one_le (by norm_num) $
-            one_le_inv hε₀ hε₁) $ sorry) $ by simpa [Nat.one_le_iff_ne_zero]).le
+      _ ≤ 2 * (120 * ε⁻¹ * log (3 * ε⁻¹) * p) := Nat.ceil_le_two_mul <|
+        calc
+          (2⁻¹ : ℝ) ≤ 120 * 1 * 1 * 1 := by norm_num
+          _ ≤ 120 * ε⁻¹ * log (3 * ε⁻¹) * p := by
+            gcongr
+            · exact one_le_inv hε₀ hε₁
+            · rw [← log_exp 1]
+              gcongr
+              calc
+                exp 1 ≤ 2.7182818286 := exp_one_lt_d9.le
+                _ ≤ 3 * 1 := by norm_num
+                _ ≤ 3 * ε⁻¹ := by gcongr; exact one_le_inv hε₀ hε₁
+            · exact mod_cast hp
       _ ≤ 2 * (120 * ε⁻¹ * (3 * ε⁻¹) * p) := by gcongr; exact Real.log_le_self (by positivity)
       _ ≤ 2 * (2 ^ 7 * ε⁻¹ * (2 ^ 2 * ε⁻¹) * p) := by gcongr <;> norm_num
       _ = 2 ^ 10 * ε⁻¹ ^ 2 * p := by ring

LeanAPAP/Prereqs/Chang.lean

@@ -1,6 +1,5 @@
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Analysis.MeanInequalities
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.LargeSpec

LeanAPAP/Prereqs/NNLpNorm.lean

@@ -1,8 +1,8 @@
 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.Algebra.Order.Module.Rat
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 
 open Filter

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ce0037d487217469a1efeb9ea8196fe15ab9c46",
+   "rev": "e0b13c946e9c3805f1eec785c72955e103a9cbaf",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "61fb4d1a2a6a4fe4be260ca31c58af1234ff298b",
+   "rev": "a895713f7701e295a015b1087f3113fd3d615272",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "09c50fb84c0b5e89b270ff20af6ae7e4bd61511e",
+   "rev": "01252d1a6f839f6087e70a512e98d1f050a9d0a1",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,