From eab4db88db6540532159863a93f334675c946549 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 28 Sep 2024 11:26:48 +0000 Subject: [PATCH] Bump mathlib --- LeanAPAP.lean | 5 --- LeanAPAP/FiniteField.lean | 29 ++++++++++------- LeanAPAP/Mathlib/Algebra/Group/Basic.lean | 5 --- .../Mathlib/Algebra/Group/Subgroup/Basic.lean | 3 -- LeanAPAP/Mathlib/Algebra/Order/Floor.lean | 32 ------------------- .../Mathlib/Algebra/Order/Module/Rat.lean | 12 ------- LeanAPAP/Mathlib/Algebra/Order/Ring/Cast.lean | 4 --- LeanAPAP/Physics/AlmostPeriodicity.lean | 2 +- LeanAPAP/Physics/DRC.lean | 2 +- LeanAPAP/Physics/Unbalancing.lean | 18 ++++++++--- LeanAPAP/Prereqs/NNLpNorm.lean | 2 +- lake-manifest.json | 6 ++-- 12 files changed, 36 insertions(+), 84 deletions(-) delete mode 100644 LeanAPAP/Mathlib/Algebra/Group/Basic.lean delete mode 100644 LeanAPAP/Mathlib/Algebra/Group/Subgroup/Basic.lean delete mode 100644 LeanAPAP/Mathlib/Algebra/Order/Floor.lean delete mode 100644 LeanAPAP/Mathlib/Algebra/Order/Module/Rat.lean delete mode 100644 LeanAPAP/Mathlib/Algebra/Order/Ring/Cast.lean diff --git a/LeanAPAP.lean b/LeanAPAP.lean index efb7e390b1..330b07b601 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -2,15 +2,10 @@ 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 diff --git a/LeanAPAP/FiniteField.lean b/LeanAPAP/FiniteField.lean index 0e0a9daaf7..b7a3bcf05b 100644 --- a/LeanAPAP/FiniteField.lean +++ b/LeanAPAP/FiniteField.lean @@ -1,7 +1,5 @@ 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 @@ -22,7 +20,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 +186,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 +209,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 +285,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 ∧ diff --git a/LeanAPAP/Mathlib/Algebra/Group/Basic.lean b/LeanAPAP/Mathlib/Algebra/Group/Basic.lean deleted file mode 100644 index e81bd99784..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Group/Basic.lean +++ /dev/null @@ -1,5 +0,0 @@ -/-! -# TODO - -Unsimp `div_pow`/`zsmul_sub` --/ diff --git a/LeanAPAP/Mathlib/Algebra/Group/Subgroup/Basic.lean b/LeanAPAP/Mathlib/Algebra/Group/Subgroup/Basic.lean deleted file mode 100644 index 5b2df3ffd4..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Group/Subgroup/Basic.lean +++ /dev/null @@ -1,3 +0,0 @@ -import Mathlib.Algebra.Group.Subgroup.Basic - -attribute [simp] AddMonoidHom.mem_ker diff --git a/LeanAPAP/Mathlib/Algebra/Order/Floor.lean b/LeanAPAP/Mathlib/Algebra/Order/Floor.lean deleted file mode 100644 index a5017131ad..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Order/Floor.lean +++ /dev/null @@ -1,32 +0,0 @@ -import Mathlib.Algebra.Order.Floor - -namespace Nat -variable {α : Type*} [LinearOrderedField α] [FloorSemiring α] {a b : α} - -lemma ceil_lt_mul (ha : 0 ≤ a) (hb : 1 < b) (h : (b - 1)⁻¹ ≤ a) : ⌈a⌉₊ < b * a := by - rw [← sub_pos] at hb - calc - ⌈a⌉₊ < a + 1 := ceil_lt_add_one ha - _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity - _ ≤ a + (b - 1) * a := by gcongr; positivity - _ = b * a := by rw [sub_one_mul, add_sub_cancel] - -lemma ceil_lt_two_mul (ha : 1 ≤ a) : ⌈a⌉₊ < 2 * a := - ceil_lt_mul (by positivity) one_lt_two (by norm_num; exact ha) - -end Nat - -namespace Int -variable {α : Type*} [LinearOrderedField α] [FloorRing α] {a b : α} - -lemma ceil_lt_mul (hb : 1 < b) (ha : (b - 1)⁻¹ ≤ a) : ⌈a⌉ < b * a := by - rw [← sub_pos] at hb - calc - ⌈a⌉ < a + 1 := ceil_lt_add_one _ - _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity - _ ≤ a + (b - 1) * a := by gcongr; positivity - _ = b * a := by rw [sub_one_mul, add_sub_cancel] - -lemma ceil_lt_two_mul (ha : 1 ≤ a) : ⌈a⌉ < 2 * a := ceil_lt_mul one_lt_two (by norm_num; exact ha) - -end Int diff --git a/LeanAPAP/Mathlib/Algebra/Order/Module/Rat.lean b/LeanAPAP/Mathlib/Algebra/Order/Module/Rat.lean deleted file mode 100644 index 61a408f06f..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Order/Module/Rat.lean +++ /dev/null @@ -1,12 +0,0 @@ -import Mathlib.Algebra.Order.Module.Defs -import Mathlib.Data.Rat.Cast.Order - -variable {α : Type*} - -instance [Preorder α] [MulAction ℚ α] [PosSMulMono ℚ α] : PosSMulMono ℚ≥0 α where - elim a _ _b₁ _b₂ hb := (smul_le_smul_of_nonneg_left hb a.2 :) - -instance LinearOrderedSemifield.toPosSMulStrictMono [LinearOrderedSemifield α] : - PosSMulStrictMono ℚ≥0 α where - elim a ha b₁ b₂ hb := by - simp_rw [NNRat.smul_def]; exact mul_lt_mul_of_pos_left hb (NNRat.cast_pos.2 ha) diff --git a/LeanAPAP/Mathlib/Algebra/Order/Ring/Cast.lean b/LeanAPAP/Mathlib/Algebra/Order/Ring/Cast.lean deleted file mode 100644 index e495c938dd..0000000000 --- a/LeanAPAP/Mathlib/Algebra/Order/Ring/Cast.lean +++ /dev/null @@ -1,4 +0,0 @@ -import Mathlib.Algebra.Order.Ring.Cast - -@[gcongr] protected alias ⟨_, GCongr.intCast_mono⟩ := Int.cast_le -@[gcongr] protected alias ⟨_, GCongr.intCast_strictMono⟩ := Int.cast_lt diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean index b0a33275ed..ece7ce2046 100644 --- a/LeanAPAP/Physics/AlmostPeriodicity.lean +++ b/LeanAPAP/Physics/AlmostPeriodicity.lean @@ -451,7 +451,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) := diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean index 26d73ae868..b21b66d5aa 100644 --- a/LeanAPAP/Physics/DRC.lean +++ b/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 diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean index cf697e5b8b..182217da11 100644 --- a/LeanAPAP/Physics/Unbalancing.lean +++ b/LeanAPAP/Physics/Unbalancing.lean @@ -1,6 +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 @@ -217,10 +216,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 diff --git a/LeanAPAP/Prereqs/NNLpNorm.lean b/LeanAPAP/Prereqs/NNLpNorm.lean index efde1e2939..1f01d80597 100644 --- a/LeanAPAP/Prereqs/NNLpNorm.lean +++ b/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 diff --git a/lake-manifest.json b/lake-manifest.json index a9cc34c679..9c532dc609 100644 --- a/lake-manifest.json +++ b/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": "8d426f12d4550cf82ee62f169425f78684c746d1", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,