From d30b9bba49084a1f16ab525075d52fa3635e1795 Mon Sep 17 00:00:00 2001 From: Eric Date: Mon, 25 Nov 2024 14:42:06 -0800 Subject: [PATCH] Fix Mathlib bump error --- OrderedSemigroups.lean | 1 + OrderedSemigroups/MonoidToGroup.lean | 1 - OrderedSemigroups/OrderedGroup/Approximate.lean | 9 ++++++--- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/OrderedSemigroups.lean b/OrderedSemigroups.lean index 22eddbe..888c32b 100644 --- a/OrderedSemigroups.lean +++ b/OrderedSemigroups.lean @@ -2,3 +2,4 @@ -- Import modules here that should be built as part of the library. import «OrderedSemigroups».Archimedean import «OrderedSemigroups».MonoidToGroup +import OrderedSemigroups.OrderedGroup.Approximate diff --git a/OrderedSemigroups/MonoidToGroup.lean b/OrderedSemigroups/MonoidToGroup.lean index ea585ab..54ff35d 100644 --- a/OrderedSemigroups/MonoidToGroup.lean +++ b/OrderedSemigroups/MonoidToGroup.lean @@ -147,7 +147,6 @@ def over_one_submonoid : Submonoid (with_division α) where theorem over_one_in_subset (a : α) : ⟦(a, 1)⟧ ∈ over_one_subset := by simp [over_one_submonoid, over_one_subset] use a - simp [HasEquiv.Equiv, pair_setoid] theorem inj_over_one (a b : α) : ⟦(a, 1)⟧ = (⟦(b, 1)⟧ : with_division α) → a = b := by intro eq diff --git a/OrderedSemigroups/OrderedGroup/Approximate.lean b/OrderedSemigroups/OrderedGroup/Approximate.lean index 58a2178..cc8b0c5 100644 --- a/OrderedSemigroups/OrderedGroup/Approximate.lean +++ b/OrderedSemigroups/OrderedGroup/Approximate.lean @@ -81,9 +81,9 @@ theorem approximate (g : α) (p : ℕ): simp at z_max trivial -noncomputable def q (g : α) (p : ℕ): ℤ := (approximate f_pos g p).choose +noncomputable def q (g : α) (p : ℕ) : ℤ := (approximate f_pos g p).choose -theorem q_spec (g : α) (p : ℕ): +theorem q_spec (g : α) (p : ℕ) : f^(q f_pos g p) ≤ g^p ∧ g^p < f^((q f_pos g p)+1) := by have := (approximate f_pos g p).choose_spec simp at this @@ -155,7 +155,10 @@ theorem q_convergence (g : α) : noncomputable def φ' : α → ℝ := fun g ↦ (q_convergence f_pos g).choose -theorem φ'_hom (a b : α) : φ' f_pos (a * b) = φ' f_pos a + φ' f_pos b := by sorry +theorem φ'_spec (g : α) : Filter.Tendsto (fun p ↦ ((q f_pos g p) : ℝ)/(p : ℝ)) Filter.atTop (nhds (φ' f_pos g)) := by + exact (q_convergence f_pos g).choose_spec + +theorem φ'_hom (a b : α) : φ' f_pos (a * b) = φ' f_pos a + φ' f_pos b := sorry noncomputable def φ : α →* ℝ where toFun := φ' f_pos