Prove that q converges

OrderedSemigroups/Convergence.lean

@@ -11,7 +11,7 @@ lemma arch_nat {e C : ℝ} (C_pos : C > 0) (e_pos : e > 0) : ∃n : ℕ+, 1 / n
 
 -- Exercise 3.1.5 https://arxiv.org/pdf/1408.5805
 -- Formalized with the help of Tomas Ortega
-lemma sequence_convergence
+lemma sequence_convergence_unique
   (a : ℕ → ℝ) -- sequence indexed by integers
   (C : ℝ) -- the constant from the bound
   (h_bound : ∀ m n : ℕ, |a (m + n) - a m - a n| ≤ C) :
@@ -141,3 +141,13 @@ lemma sequence_convergence
   · trivial
   · intro y hy
     exact tendsto_nhds_unique hy this
+
+lemma sequence_convergence
+  (a : ℕ → ℝ) -- sequence indexed by integers
+  (C : ℝ) -- the constant from the bound
+  (h_bound : ∀ m n : ℕ, |a (m + n) - a m - a n| ≤ C) :
+  ∃ θ : ℝ, -- exists unique θ
+  -- conclusion: θ is the limit of a_n/n at +∞
+  (Filter.Tendsto (fun n ↦ a n / (n : ℝ)) Filter.atTop (nhds θ)) := by
+  obtain ⟨t, ht, _⟩ := sequence_convergence_unique a C h_bound
+  use t

OrderedSemigroups/OrderedGroup/Approximate.lean

@@ -1,4 +1,5 @@
 import OrderedSemigroups.OrderedGroup.Basic
+import OrderedSemigroups.Convergence
 
 /--
   Every nonempty set of integers that is bounded above has a maximum element.
@@ -47,13 +48,17 @@ theorem bounded_above_max {S : Set ℤ} (nonempty : Nonempty S) (upper_bounded :
 
 universe u
 
-variable {α : Type u} [LeftLinearOrderedGroup α] (arch : archimedean_group α) (f : α) (f_pos : 1 < f)
+variable {α : Type u} [LeftLinearOrderedGroup α] {f : α} (f_pos : 1 < f)
+  [arch : Fact (archimedean_group α)]
 
-include f_pos arch in
+instance : LinearOrderedGroup α where
+  mul_le_mul_right := by exact fun a b a_1 c ↦ left_arch_ordered arch.elim a b a_1 c
+
+include f_pos in
 theorem approximate (g : α) (p : ℕ):
   ∃(q : ℤ), f^q ≤ g^p ∧ g^p < f^(q+1) := by
-  obtain ⟨l, hl⟩ := @lt_exp α (left_arch_ordered_group arch) arch f (g^p) (f_pos.ne.symm)
-  obtain ⟨u, hu⟩ := gt_exp arch f (g^p) (f_pos.ne.symm)
+  obtain ⟨l, hl⟩ := lt_exp arch.out f (g^p) (f_pos.ne.symm)
+  obtain ⟨u, hu⟩ := gt_exp arch.out f (g^p) (f_pos.ne.symm)
   set small_exp := {z : ℤ | f^z ≤ g^p}
   have small_exp_nonempty : Nonempty small_exp := by
     use l
@@ -76,17 +81,76 @@ theorem approximate (g : α) (p : ℕ):
     simp at z_max
     trivial
 
-noncomputable def q (g : α) (p : ℕ): ℤ := (approximate arch f f_pos g p).choose
+noncomputable def q (g : α) (p : ℕ): ℤ := (approximate f_pos g p).choose
 
 theorem q_spec (g : α) (p : ℕ):
-  f^(q arch f f_pos g p) ≤ g^p ∧ g^p < f^((q arch f f_pos g p)+1) := by
-    have := (approximate arch f f_pos g p).choose_spec
+  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
     simp [q]
     tauto
 
+theorem q_max_lt (g : α) (p : ℕ) {t : ℤ} (ht : f^t ≤ g^p) : t ≤ q f_pos g p := by
+  have ⟨_, gp_lt_fqp1⟩ := q_spec f_pos g p
+  by_contra h
+  simp at h
+  have : q f_pos g p + 1 ≤ t := h
+  have lt_t : f ^ (q f_pos g p + 1) ≤ f^t := pos_exp_le_le f_pos h
+  have : f ^ t < f ^ (q f_pos g p + 1) := lt_of_le_of_lt ht gp_lt_fqp1
+  have : f ^ t < f ^ t := gt_of_ge_of_gt lt_t this
+  exact (lt_self_iff_false (f ^ t)).mp this
+
+theorem qplus1_min_gt (g : α) (p : ℕ) {t : ℤ} (ht : g^p < f^t) : q f_pos g p + 1 ≤ t := by
+  have ⟨fqp_lt_gt, _⟩ := q_spec f_pos g p
+  by_contra h
+  simp at h
+  have : t ≤ q f_pos g p := (Int.add_le_add_iff_right 1).mp h
+  have : f^t ≤ f^(q f_pos g p) := pos_exp_le_le f_pos this
+  have : g^p < f^(q f_pos g p) := gt_of_ge_of_gt this ht
+  have : g^p < g^p := gt_of_ge_of_gt fqp_lt_gt this
+  exact (lt_self_iff_false (g ^ p)).mp this
+
+theorem q_exp_add (g : α) (a b : ℕ) :
+    f^((q f_pos g a) + (q f_pos g b)) ≤ g^(a + b) ∧
+    g^(a+b) < f^((q f_pos g a) + (q f_pos g b)+2) := by
+  have ⟨fqa_le_ga, ga_lt_fa1⟩ := q_spec f_pos g a
+  have ⟨fqb_le_gb, gb_lt_fb1⟩ := q_spec f_pos g b
+  constructor
+  · have : (f ^ q f_pos g a)*(f ^ q f_pos g b) ≤ g^a*g^b :=
+      mul_le_mul' fqa_le_ga fqb_le_gb
+    simp [←zpow_add, ←pow_add] at this
+    trivial
+  · have : (g ^ a) * (g ^ b) < (f ^ (q f_pos g a + 1)) * f ^ (q f_pos g b + 1) :=
+      Left.mul_lt_mul ga_lt_fa1 gb_lt_fb1
+    simp [←zpow_add, ←pow_add] at this
+    have exp_add :
+        q f_pos g a + 1 + (q f_pos g b + 1) = q f_pos g a + q f_pos g b + 2 := by
+      ring
+    simp [exp_add] at this
+    trivial
+
 theorem q_convergence (g : α) :
-  ∃r : ℝ, Filter.Tendsto (fun p ↦ ((q arch f f_pos g p) : ℝ)/(p : ℝ)) Filter.atTop (nhds r) := by sorry
+  ∃r : ℝ, Filter.Tendsto (fun p ↦ ((q f_pos g p) : ℝ)/(p : ℝ)) Filter.atTop (nhds r) := by
+  apply sequence_convergence (C := 1)
+  intro m n
+  obtain ⟨fab_le_gab, gab_lt_abplus2⟩ := q_exp_add f_pos g m n
+  have qmplusqn_le_qmplusn:= q_max_lt f_pos g (m+n) fab_le_gab
+  have qmplusn_le_qmplusqnplus2 := qplus1_min_gt f_pos g (m+n) gab_lt_abplus2
+  have := Int.sub_le_sub_right qmplusn_le_qmplusqnplus2 1
+  simp at this
+  ring_nf at this
+  have diff_le_1: q f_pos g (m+n) - q f_pos g m - q f_pos g n ≤ 1 := by
+    simp
+    rw [add_assoc, add_comm (q f_pos g n), ←add_assoc]
+    trivial
+  have diff_ge_0 : 0 ≤ q f_pos g (m+n) - q f_pos g m - q f_pos g n := by
+    simp
+    have := Int.sub_le_sub_right qmplusqn_le_qmplusn (q f_pos g m)
+    simpa
+  norm_cast
+  have := abs_of_nonneg diff_ge_0
+  rw [this]
+  exact diff_le_1
 
 noncomputable def φ : α → ℝ :=
-  fun g ↦ (q_convergence arch f f_pos g).choose
+  fun g ↦ (q_convergence f_pos g).choose

OrderedSemigroups/OrderedGroup/ArchimedeanGroup.lean

@@ -17,51 +17,57 @@ def archimedean_group (α : Type u) [LeftOrderedGroup α] :=
 
 theorem pos_exp_pos_pos {x : α} (pos_x : 1 < x) {z : ℤ} (pos_z : z > 0) :
     1 < x^z := by
-    have h : z = z.natAbs := by omega
-    rw [h, zpow_natCast]
-    exact one_lt_pow' pos_x (by omega)
+  have h : z = z.natAbs := by omega
+  rw [h, zpow_natCast]
+  exact one_lt_pow' pos_x (by omega)
+
+theorem nonneg_exp_pos_nonneg {x : α} (pos_x : 1 < x) {z : ℤ} (pos_z : z ≥ 0) :
+    1 ≤ x^z := by
+  obtain z_eq_0 | z_gt_0 := pos_z.eq_or_gt
+  · simp [z_eq_0]
+  · exact (pos_exp_pos_pos pos_x z_gt_0).le
 
 theorem pos_exp_neg_neg {x : α} (neg_x : x < 1) {z : ℤ} (pos_z : z > 0) :
     x^z < 1 := by
-    have h : z = z.natAbs := by omega
-    rw [h, zpow_natCast]
-    exact pow_lt_one' neg_x (by omega)
+  have h : z = z.natAbs := by omega
+  rw [h, zpow_natCast]
+  exact pow_lt_one' neg_x (by omega)
 
 theorem neg_exp_pos_neg {x : α} (pos_x : 1 < x) {z : ℤ} (neg_z : z < 0) :
     x^z < 1 := by
-    have h : 1 < x ^ (-z) := pos_exp_pos_pos pos_x (by omega)
-    rwa [zpow_neg, Left.one_lt_inv_iff] at h
+  have h : 1 < x ^ (-z) := pos_exp_pos_pos pos_x (by omega)
+  rwa [zpow_neg, Left.one_lt_inv_iff] at h
 
 theorem neg_exp_neg_pos {x : α} (neg_x : x < 1) {z : ℤ} (neg_z : z < 0) :
     1 < x^z := by
-    have h : x ^ (-z) < 1 := pos_exp_neg_neg neg_x (by omega)
-    rwa [zpow_neg, Left.inv_lt_one_iff] at h
+  have h : x ^ (-z) < 1 := pos_exp_neg_neg neg_x (by omega)
+  rwa [zpow_neg, Left.inv_lt_one_iff] at h
 
 theorem pos_arch {x y : α} (pos_x : 1 < x) (pos_y : 1 < y) :
     ∀z : ℤ, x^z > y → z > 0 := by
-    intro z
-    by_contra!
-    obtain ⟨h, hz⟩ := this -- h : x ^ z > y, hz : z ≤ 0
-    obtain hz | hz := Int.le_iff_eq_or_lt.mp hz
-    · -- case z = 0
-      have : (1 : α) < 1 := by calc
-        1 < y := pos_y
-        _ < x^z := h
-        _ = 1 := by rw [hz, zpow_zero]
-      exact (lt_self_iff_false 1).mp this
-    · -- case z < 0
-      have : x^z < x^z := by calc
-        x^z < 1 := neg_exp_pos_neg pos_x hz
-        _ < y := pos_y
-        _ < x^z := h
-      exact (lt_self_iff_false (x ^ z)).mp this
+  intro z
+  by_contra!
+  obtain ⟨h, hz⟩ := this -- h : x ^ z > y, hz : z ≤ 0
+  obtain hz | hz := Int.le_iff_eq_or_lt.mp hz
+  · -- case z = 0
+    have : (1 : α) < 1 := by calc
+      1 < y := pos_y
+      _ < x^z := h
+      _ = 1 := by rw [hz, zpow_zero]
+    exact (lt_self_iff_false 1).mp this
+  · -- case z < 0
+    have : x^z < x^z := by calc
+      x^z < 1 := neg_exp_pos_neg pos_x hz
+      _ < y := pos_y
+      _ < x^z := h
+    exact (lt_self_iff_false (x ^ z)).mp this
 
 /--
   If x and y are both positive, then by Archimedneaness
   we have a least z such that x^z > y.
 -/
 theorem pos_min_arch {x y : α} (arch : archimedean_group α) (pos_x : 1 < x) (pos_y : 1 < y) :
-  ∃z : ℤ, x^z > y ∧ (∀t : ℤ, x^t > y → z ≤ t) := by
+    ∃z : ℤ, x^z > y ∧ (∀t : ℤ, x^t > y → z ≤ t) := by
   -- Define predicate for numbers satisfying x^n > y
   let P : ℕ → Prop := fun n => x^(n : ℤ) > y
 

OrderedSemigroups/OrderedGroup/Basic.lean

@@ -159,6 +159,22 @@ section LinearOrderedGroup
 
 variable [LinearOrderedGroup α]
 
+theorem pos_exp_lt_lt {f : α} (f_pos : 1 < f) {a b : ℤ} (a_lt_b : a < b) : f^a < f^b := by
+  have : 0 < b - a := Int.sub_pos_of_lt a_lt_b
+  have : 1 < f ^ (b - a) := pos_exp_pos_pos f_pos this
+  have : 1 < f^(b + (-a)) := this
+  rw [zpow_add] at this
+  have : 1*f^a < (f^b * f^(-a))*f^a := mul_lt_mul_right' this (f ^ a)
+  simpa
+
+theorem pos_exp_le_le {f : α} (f_pos : 1 < f) {a b : ℤ} (a_le_b : a ≤ b) : f^a ≤ f^b := by
+  have : 0 ≤ b - a := Int.sub_nonneg_of_le a_le_b
+  have : 1 ≤ f ^ (b - a) := nonneg_exp_pos_nonneg f_pos this
+  have : 1 ≤ f^(b + (-a)) := this
+  rw [zpow_add] at this
+  have : 1*f^a ≤ (f^b * f^(-a))*f^a := mul_le_mul_right' this (f ^ a)
+  simpa
+
 theorem lt_exp (arch : archimedean_group α) (f g : α) (f_ne_one : f ≠ 1) : ∃z : ℤ, f^z < g := by
   obtain f_le_g | g_lt_f := le_or_lt f g
   · obtain f_lt_one | one_lt_f := lt_or_gt_of_ne f_ne_one