Bump mathlib

YaelDillies · Aug 28, 2024 · e156025 · e156025
1 parent 9214356
commit e156025
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 200 deletions.
diff --git a/LeanAPAP.lean b/LeanAPAP.lean
@@ -4,7 +4,6 @@ import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
 import LeanAPAP.Mathlib.Analysis.RCLike.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Mathlib.Data.ENNReal.Real

diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean
@@ -1,4 +1,3 @@
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.LargeSpec
@@ -228,9 +227,8 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
           gcongr
           rw [inv_le ‹_› (by positivity)]
           calc
-            65⁻¹ = (1 + 64)⁻¹ := by norm_num
-            _ ≤ log (1 + 64⁻¹) := le_log_one_add_inv (by norm_num)
-            _ = log (65 / 64) := by norm_num
+            65⁻¹ = 1 - (65 / 64)⁻¹ := by norm_num
+            _ ≤ log (65 / 64) := one_sub_inv_le_log_of_pos (by positivity)
     _ = ↑(card V) := by simp [card_eq_pow_finrank (K := ZMod q) (V := V)]
     _ ≤ 2 * β⁻¹ ^ 2 := by
       rw [← natCast_card_mul_nnratCast_dens, mul_pow, mul_inv, ← mul_assoc,

diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
+   "rev": "adaeb6b4d4bf02f60ba3ff6717486a7e895eba77",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fa7fd3cbb00526761d472e04e481259557e55c53",
+   "rev": "c8013cf7e8ac16ecaa8d30d18799360769ea5e8b",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b5c59823650e1e36145625411c896de0088947cb",
+   "rev": "83f718b9055972dce4f92f5b3917426b91a0d2fe",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",