From d9e00cbeb8c2aba0cf9601cdc5340e58f7d6fea5 Mon Sep 17 00:00:00 2001 From: Eric Date: Tue, 3 Dec 2024 12:07:37 -0800 Subject: [PATCH] Show that phi is order preserving and injective --- .../OrderedGroup/Approximate.lean | 235 +++++++++++------- 1 file changed, 148 insertions(+), 87 deletions(-) diff --git a/OrderedSemigroups/OrderedGroup/Approximate.lean b/OrderedSemigroups/OrderedGroup/Approximate.lean index e921476..88f5b5f 100644 --- a/OrderedSemigroups/OrderedGroup/Approximate.lean +++ b/OrderedSemigroups/OrderedGroup/Approximate.lean @@ -49,17 +49,16 @@ theorem bounded_above_max {S : Set ℤ} (nonempty : Nonempty S) (upper_bounded : universe u -variable {α : Type u} [LeftLinearOrderedGroup α] {f : α} (f_pos : 1 < f) - [arch : Fact (archimedean_group α)] +variable {α : Type u} [LeftLinearOrderedGroup α] (f : α) + [arch : Fact (archimedean_group α)] [f_pos : Fact (1 < f)] 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 arch.out f (g^p) (f_pos.ne.symm) - obtain ⟨u, hu⟩ := gt_exp arch.out f (g^p) (f_pos.ne.symm) + obtain ⟨l, hl⟩ := lt_exp arch.out f (g^p) (f_pos.out.ne.symm) + obtain ⟨u, hu⟩ := gt_exp arch.out f (g^p) (f_pos.out.ne.symm) set small_exp := {z : ℤ | f^z ≤ g^p} have small_exp_nonempty : Nonempty small_exp := by use l @@ -71,7 +70,7 @@ theorem approximate (g : α) (p : ℕ): intro a ha simp [small_exp] at ha have : f^a < f^u := by exact lt_of_le_of_lt ha hu - exact (pos_lt_exp_lt f_pos this).le + exact (pos_lt_exp_lt f_pos.out this).le obtain ⟨z, z_small, z_max⟩ := bounded_above_max small_exp_nonempty small_exp_bddabove use z simp [small_exp, upperBounds] at z_small z_max @@ -82,71 +81,71 @@ 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 g p).choose 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 + f^(q f g p) ≤ g^p ∧ g^p < f^((q f g p)+1) := by + have := (approximate f 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 +theorem q_max_lt (g : α) (p : ℕ) {t : ℤ} (ht : f^t ≤ g^p) : t ≤ q f g p := by + have ⟨_, gp_lt_fqp1⟩ := q_spec f 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 : q f g p + 1 ≤ t := h + have lt_t : f ^ (q f g p + 1) ≤ f^t := pos_exp_le_le f h + have : f ^ t < f ^ (q f 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 +theorem qplus1_min_gt (g : α) (p : ℕ) {t : ℤ} (ht : g^p < f^t) : q f g p + 1 ≤ t := by + have ⟨fqp_lt_gt, _⟩ := q_spec f 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 : t ≤ q f g p := (Int.add_le_add_iff_right 1).mp h + have : f^t ≤ f^(q f g p) := pos_exp_le_le f_pos.out this + have : g^p < f^(q f 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 + f^((q f g a) + (q f g b)) ≤ g^(a + b) ∧ + g^(a+b) < f^((q f g a) + (q f g b)+2) := by + have ⟨fqa_le_ga, ga_lt_fa1⟩ := q_spec f g a + have ⟨fqb_le_gb, gb_lt_fb1⟩ := q_spec f g b constructor - · have : (f ^ q f_pos g a)*(f ^ q f_pos g b) ≤ g^a*g^b := + · have : (f ^ q f g a)*(f ^ q f 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) := + · have : (g ^ a) * (g ^ b) < (f ^ (q f g a + 1)) * f ^ (q f 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 + q f g a + 1 + (q f g b + 1) = q f g a + q f g b + 2 := by ring simp [exp_add] at this trivial theorem q_convergence (g : α) : - ∃r : ℝ, Filter.Tendsto (fun p ↦ ((q f_pos g p) : ℝ)/(p : ℝ)) Filter.atTop (nhds r) := by + ∃r : ℝ, Filter.Tendsto (fun p ↦ ((q f 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 + obtain ⟨fab_le_gab, gab_lt_abplus2⟩ := q_exp_add f g m n + have qmplusqn_le_qmplusn:= q_max_lt f g (m+n) fab_le_gab + have qmplusn_le_qmplusqnplus2 := qplus1_min_gt f 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 + have diff_le_1: q f g (m+n) - q f g m - q f g n ≤ 1 := by simp - rw [add_assoc, add_comm (q f_pos g n), ←add_assoc] + rw [add_assoc, add_comm (q f 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 + have diff_ge_0 : 0 ≤ q f g (m+n) - q f g m - q f g n := by simp - have := Int.sub_le_sub_right qmplusqn_le_qmplusn (q f_pos g m) + have := Int.sub_le_sub_right qmplusqn_le_qmplusn (q f g m) simpa norm_cast have := abs_of_nonneg diff_ge_0 @@ -154,42 +153,42 @@ theorem q_convergence (g : α) : exact diff_le_1 noncomputable def φ' : α → ℝ := - fun g ↦ (q_convergence f_pos g).choose + fun g ↦ (q_convergence f g).choose -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 φ'_spec (g : α) : Filter.Tendsto (fun p ↦ ((q f g p) : ℝ)/(p : ℝ)) Filter.atTop (nhds (φ' f g)) := by + exact (q_convergence f g).choose_spec -theorem φ'_def (g : α) {s : ℝ} (s_lim : Filter.Tendsto (fun p ↦ ((q f_pos g p) : ℝ)/(p : ℝ)) Filter.atTop (nhds s)) : - φ' f_pos g = s := by - have := φ'_spec f_pos g +theorem φ'_def (g : α) {s : ℝ} (s_lim : Filter.Tendsto (fun p ↦ ((q f g p) : ℝ)/(p : ℝ)) Filter.atTop (nhds s)) : + φ' f g = s := by + have := φ'_spec f g exact tendsto_nhds_unique this s_lim theorem φ'_hom_case (a b : α) : - ∀p : ℕ, q f_pos a p + q f_pos b p ≤ q f_pos (a*b) p ∧ - q f_pos (a*b) p ≤ q f_pos a p + q f_pos b p + 1 := by + ∀p : ℕ, q f a p + q f b p ≤ q f (a*b) p ∧ + q f (a*b) p ≤ q f a p + q f b p + 1 := by intro p - obtain ⟨a_spec1, a_spec2⟩ := q_spec f_pos a p - obtain ⟨b_spec1, b_spec2⟩ := q_spec f_pos b p + obtain ⟨a_spec1, a_spec2⟩ := q_spec f a p + obtain ⟨b_spec1, b_spec2⟩ := q_spec f b p obtain ab_le_ba | ba_le_ab := LinearOrder.le_total (a * b) (b * a) · constructor · have factor_le : a^p*b^p ≤ (a*b)^p := comm_factor_le_group ab_le_ba p - have : f^(q f_pos a p) * f^(q f_pos b p) ≤ a^p * b^p := mul_le_mul' a_spec1 b_spec1 - have : f^(q f_pos a p) * f^(q f_pos b p) ≤ (a*b)^p := Preorder.le_trans _ _ _ this factor_le + have : f^(q f a p) * f^(q f b p) ≤ a^p * b^p := mul_le_mul' a_spec1 b_spec1 + have : f^(q f a p) * f^(q f b p) ≤ (a*b)^p := Preorder.le_trans _ _ _ this factor_le simp [←zpow_add] at this - exact q_max_lt f_pos (a * b) p this + exact q_max_lt f (a * b) p this · have dist_le : (b*a)^p ≤ b^p*a^p := by exact comm_dist_le_group ab_le_ba p have : (a*b)^p ≤ (b*a)^p := by exact comm_swap_le_group ab_le_ba p have prod_le : (a*b)^p ≤ b^p*a^p := by exact Preorder.le_trans _ _ _ this dist_le - have : b^p*a^p < f ^ (q f_pos b p + 1) * f ^ (q f_pos a p + 1) := + have : b^p*a^p < f ^ (q f b p + 1) * f ^ (q f a p + 1) := Left.mul_lt_mul b_spec2 a_spec2 simp [←zpow_add] at this - have exp_rw : (q f_pos b p + 1) + (q f_pos a p + 1) = q f_pos a p + q f_pos b p + 2 := by + have exp_rw : (q f b p + 1) + (q f a p + 1) = q f a p + q f b p + 2 := by ring simp [exp_rw] at this - have : (a * b)^p < f^(q f_pos a p + q f_pos b p + 2) := lt_of_le_of_lt prod_le this - have : q f_pos (a*b) p + 1 ≤ q f_pos a p + q f_pos b p + 2 := - qplus1_min_gt f_pos (a * b) p this - have : q f_pos (a*b) p + 1 - 1 ≤ q f_pos a p + q f_pos b p + 2 - 1 := + have : (a * b)^p < f^(q f a p + q f b p + 2) := lt_of_le_of_lt prod_le this + have : q f (a*b) p + 1 ≤ q f a p + q f b p + 2 := + qplus1_min_gt f (a * b) p this + have : q f (a*b) p + 1 - 1 ≤ q f a p + q f b p + 2 - 1 := Int.sub_le_sub_right this 1 ring_nf at this ring_nf @@ -198,102 +197,102 @@ theorem φ'_hom_case (a b : α) : · have factor_le : b^p*a^p ≤ (b*a)^p := comm_factor_le_group ba_le_ab p have : (b*a)^p ≤ (a*b)^p := by exact comm_swap_le_group ba_le_ab p have factor_le' : b^p*a^p ≤ (a*b)^p := Preorder.le_trans _ _ _ factor_le this - have : f^(q f_pos b p) * f^(q f_pos a p) ≤ b^p * a^p := mul_le_mul' b_spec1 a_spec1 - have : f^(q f_pos b p) * f^(q f_pos a p) ≤ (a*b)^p := Preorder.le_trans _ _ _ this factor_le' + have : f^(q f b p) * f^(q f a p) ≤ b^p * a^p := mul_le_mul' b_spec1 a_spec1 + have : f^(q f b p) * f^(q f a p) ≤ (a*b)^p := Preorder.le_trans _ _ _ this factor_le' simp [←zpow_add] at this - have := q_max_lt f_pos (a * b) p this + have := q_max_lt f (a * b) p this rw [←add_comm] trivial - · have : a^p*b^p < f ^ (q f_pos a p + 1)*f ^ (q f_pos b p + 1) := Left.mul_lt_mul a_spec2 b_spec2 + · have : a^p*b^p < f ^ (q f a p + 1)*f ^ (q f b p + 1) := Left.mul_lt_mul a_spec2 b_spec2 have dist_le : (a*b)^p ≤ a^p*b^p := comm_dist_le_group ba_le_ab p - have : (a*b)^p < f ^ (q f_pos a p + 1)*f ^ (q f_pos b p + 1) := lt_of_le_of_lt dist_le this + have : (a*b)^p < f ^ (q f a p + 1)*f ^ (q f b p + 1) := lt_of_le_of_lt dist_le this simp [←zpow_add] at this - have := qplus1_min_gt f_pos (a*b) p this - have exp_rw : (q f_pos a p + 1) + (q f_pos b p + 1) = q f_pos a p + q f_pos b p + 2 := by + have := qplus1_min_gt f (a*b) p this + have exp_rw : (q f a p + 1) + (q f b p + 1) = q f a p + q f b p + 2 := by ring rw [exp_rw] at this - have : q f_pos (a*b) p + 1 - 1 ≤ q f_pos a p + q f_pos b p + 2 - 1 := Int.sub_le_sub_right this 1 + have : q f (a*b) p + 1 - 1 ≤ q f a p + q f b p + 2 - 1 := Int.sub_le_sub_right this 1 ring_nf at this ring_nf trivial -theorem φ'_hom (a b : α) : φ' f_pos (a * b) = φ' f_pos a + φ' f_pos b := by - have sequence_le := φ'_hom_case f_pos a b - have a_spec := φ'_spec f_pos a - have b_spec := φ'_spec f_pos b - have ab_spec := φ'_spec f_pos (a*b) +theorem φ'_hom (a b : α) : φ' f (a * b) = φ' f a + φ' f b := by + have sequence_le := φ'_hom_case f a b + have a_spec := φ'_spec f a + have b_spec := φ'_spec f b + have ab_spec := φ'_spec f (a*b) - have sequence_sum : Filter.Tendsto (fun p ↦ (q f_pos a p : ℝ) / (p : ℝ) + (q f_pos b p : ℝ) / p) Filter.atTop (nhds (φ' f_pos a + φ' f_pos b)) := by + have sequence_sum : Filter.Tendsto (fun p ↦ (q f a p : ℝ) / (p : ℝ) + (q f b p : ℝ) / p) Filter.atTop (nhds (φ' f a + φ' f b)) := by exact Filter.Tendsto.add a_spec b_spec - have : (fun p ↦ (q f_pos a p : ℝ) / (p : ℝ) + (q f_pos b p : ℝ) / p) = (fun p ↦ ((q f_pos a p : ℝ) + (q f_pos b p : ℝ) : ℝ) / (p : ℝ)) := by + have : (fun p ↦ (q f a p : ℝ) / (p : ℝ) + (q f b p : ℝ) / p) = (fun p ↦ ((q f a p : ℝ) + (q f b p : ℝ) : ℝ) / (p : ℝ)) := by ext z ring rw [this] at sequence_sum - have : ∀p : ℕ, ((q f_pos a p : ℝ) + (q f_pos b p : ℝ) : ℝ) ≤ (q f_pos (a*b) p : ℝ) := by + have : ∀p : ℕ, ((q f a p : ℝ) + (q f b p : ℝ) : ℝ) ≤ (q f (a*b) p : ℝ) := by intro p norm_cast obtain ⟨le, _⟩ := sequence_le p exact le - have (p : ℕ) (p_pos : 0 < p) : ((q f_pos a p : ℝ) + (q f_pos b p : ℝ) : ℝ) / (p : ℝ) ≤ (q f_pos (a*b) p : ℝ) / (p : ℝ) := by + have (p : ℕ) (p_pos : 0 < p) : ((q f a p : ℝ) + (q f b p : ℝ) : ℝ) / (p : ℝ) ≤ (q f (a*b) p : ℝ) / (p : ℝ) := by have rp_pos : (p : ℝ) > 0 := Nat.cast_pos'.mpr p_pos exact (div_le_div_iff_of_pos_right rp_pos).mpr (this p) - have : ∀ᶠ p in Filter.atTop, ((q f_pos a p : ℝ) + (q f_pos b p : ℝ) : ℝ) / (p : ℝ) ≤ (q f_pos (a*b) p : ℝ) / (p : ℝ) := by + have : ∀ᶠ p in Filter.atTop, ((q f a p : ℝ) + (q f b p : ℝ) : ℝ) / (p : ℝ) ≤ (q f (a*b) p : ℝ) / (p : ℝ) := by simp use 1 exact fun b a ↦ this b a have h1 := le_of_tendsto_of_tendsto sequence_sum ab_spec this - have h2 : φ' f_pos (a*b) ≤ φ' f_pos a + φ' f_pos b := by + have h2 : φ' f (a*b) ≤ φ' f a + φ' f b := by have : Filter.Tendsto (fun x : ℕ => 1 / (x : ℝ)) Filter.atTop (nhds 0) := by simp only [one_div] exact tendsto_inverse_atTop_nhds_zero_nat - have convergence : Filter.Tendsto (fun p ↦ ((q f_pos a p) + (q f_pos b p)) / (p : ℝ) + 1 / (p : ℝ)) Filter.atTop (nhds (φ' f_pos a + φ' f_pos b + 0)) := by + have convergence : Filter.Tendsto (fun p ↦ ((q f a p) + (q f b p)) / (p : ℝ) + 1 / (p : ℝ)) Filter.atTop (nhds (φ' f a + φ' f b + 0)) := by apply Filter.Tendsto.add <;> trivial - have : (fun p ↦ ((q f_pos a p) + (q f_pos b p)) / (p : ℝ) + 1 / (p : ℝ)) = (fun p ↦ ((q f_pos a p) + (q f_pos b p) + 1) / (p : ℝ)) := by + have : (fun p ↦ ((q f a p) + (q f b p)) / (p : ℝ) + 1 / (p : ℝ)) = (fun p ↦ ((q f a p) + (q f b p) + 1) / (p : ℝ)) := by field_simp rw [this] at convergence simp at convergence - have : ∀p : ℕ, (q f_pos (a*b) p : ℝ) ≤ q f_pos a p + q f_pos b p + 1 := by + have : ∀p : ℕ, (q f (a*b) p : ℝ) ≤ q f a p + q f b p + 1 := by intro p norm_cast obtain ⟨_, le⟩ := sequence_le p exact le - have (p : ℕ) (p_pos : 0 < p) : (q f_pos (a*b) p : ℝ) / (p : ℝ) ≤ (q f_pos a p + q f_pos b p + 1) / (p : ℝ) := by + have (p : ℕ) (p_pos : 0 < p) : (q f (a*b) p : ℝ) / (p : ℝ) ≤ (q f a p + q f b p + 1) / (p : ℝ) := by have rp_pos : (p : ℝ) > 0 := Nat.cast_pos'.mpr p_pos exact (div_le_div_iff_of_pos_right rp_pos).mpr (this p) - have : ∀ᶠ p in Filter.atTop, (q f_pos (a*b) p : ℝ) / (p : ℝ) ≤ (q f_pos a p + q f_pos b p + 1) / (p : ℝ) := by + have : ∀ᶠ p in Filter.atTop, (q f (a*b) p : ℝ) / (p : ℝ) ≤ (q f a p + q f b p + 1) / (p : ℝ) := by simp use 1 exact fun b a ↦ this b a exact le_of_tendsto_of_tendsto ab_spec convergence this - have := PartialOrder.le_antisymm (a := φ' f_pos a + φ' f_pos b) (b := φ' f_pos (a*b)) h1 h2 + have := PartialOrder.le_antisymm (a := φ' f a + φ' f b) (b := φ' f (a*b)) h1 h2 exact this.symm noncomputable def φ : α →* (Multiplicative ℝ) where - toFun := φ' f_pos + toFun := φ' f map_one' := by - have : ∀p : ℕ, q f_pos 1 p = 0 := by + have : ∀p : ℕ, q f 1 p = 0 := by intro p have : f^(0 : ℤ) ≤ 1^p := by simp - have zero_le := q_max_lt f_pos 1 p this + have zero_le := q_max_lt f 1 p this have : 1^p < f^(1 : ℤ) := by simp - exact f_pos - have := qplus1_min_gt f_pos 1 p this - have le_zero : q f_pos 1 p ≤ 0 := by exact (Int.add_le_add_iff_right 1).mp this + exact f_pos.out + have := qplus1_min_gt f 1 p this + have le_zero : q f 1 p ≤ 0 := by exact (Int.add_le_add_iff_right 1).mp this exact Eq.symm (Int.le_antisymm zero_le le_zero) - have eventually_zero : (fun p ↦ ((q f_pos 1 p) : ℝ)/(p : ℝ)) =ᶠ[Filter.atTop] 0 := by + have eventually_zero : (fun p ↦ ((q f 1 p) : ℝ)/(p : ℝ)) =ᶠ[Filter.atTop] 0 := by simp [Filter.EventuallyEq] use 1 intro b one_le_b left exact this b - have : Filter.Tendsto (fun p ↦ ((q f_pos 1 p) : ℝ)/(p : ℝ)) Filter.atTop (nhds 0) := by + have : Filter.Tendsto (fun p ↦ ((q f 1 p) : ℝ)/(p : ℝ)) Filter.atTop (nhds 0) := by have : Filter.Tendsto 0 (Filter.atTop : Filter ℕ) (nhds (0 : ℝ)) := tendsto_const_nhds apply Filter.Tendsto.congr' @@ -303,4 +302,66 @@ noncomputable def φ : α →* (Multiplicative ℝ) where trivial map_mul' := by simp - exact φ'_hom f_pos + exact φ'_hom f + +theorem order_preserving_φ {a b : α} (a_le_b : a ≤ b) : (φ f a) ≤ (φ f b) := by + have (p : ℕ) : (q f a p : ℝ) ≤ q f b p := by + norm_cast + apply q_max_lt + obtain ⟨le, _⟩ := q_spec f a p + have : a^p ≤ b^p := pow_le_pow_left' a_le_b p + exact Preorder.le_trans _ _ _ le this + have (p : ℕ) (p_pos : 0 < p) : (q f a p)/(p : ℝ) ≤ (q f b p)/(p : ℝ) := by + have rp_pos : 0 < (p : ℝ) := Nat.cast_pos'.mpr p_pos + exact (div_le_div_iff_of_pos_right rp_pos).mpr (this p) + have : ∀ᶠ p in Filter.atTop, (q f a p)/(p : ℝ) ≤ (q f b p)/(p : ℝ) := by + simp + use 1 + intro b one_le_b + exact this b one_le_b + have a_spec := φ'_spec f a + have b_spec := φ'_spec f b + have := le_of_tendsto_of_tendsto a_spec b_spec this + exact this + +theorem f_maps_one_φ : (φ f) f = (1 : ℝ) := by + have p_le (p : ℕ) : (p : ℤ) ≤ q f f p := q_max_lt f f p (t := p) (by simp) + have p_ge (p : ℕ) : q f f p ≤ (p : ℤ) := by + have one_lt_f := f_pos.out + have lt : 1*f^p < f*f^p := mul_lt_mul_right' one_lt_f (f ^ p) + simp only [one_mul] at lt + have : f * f^p = f^(p+1) := (pow_succ' f p).symm + rw [this] at lt + have := qplus1_min_gt f f p (t := p+1) (by norm_cast) + simp at this + trivial + have (p : ℕ) : q f f p = p := (Int.le_antisymm (p_le p) (p_ge p)).symm + have : ∀ᶠ p in Filter.atTop, (q f f p)/(p : ℝ) = 1 := by + simp + use 1 + intro b one_le_b + simp [this] + field_simp + have eventually_one : (fun p ↦ ((q f f p) : ℝ)/(p : ℝ)) =ᶠ[Filter.atTop] 1 := this + have : Filter.Tendsto (fun p ↦ ((q f f p) : ℝ)/(p : ℝ)) Filter.atTop (nhds 1) := by + apply Filter.Tendsto.congr' (f₁ := 1) + exact eventually_one.symm + exact tendsto_const_nhds + exact φ'_def f f this + +theorem injective_φ : Function.Injective (φ f) := by + rw [injective_iff_map_eq_one] + intro a a_image_one + by_contra h + obtain ⟨n, hn⟩ := arch.out a f h + have zero_le_one : (0 : ℝ) ≥ 1 := by + calc (0 : ℝ) + _ = (φ f) a := a_image_one.symm + _ = ((φ f) a)^n := by + simp [a_image_one] + _ = (φ f) (a ^ n) := (MonoidHom.map_zpow (φ f) a n).symm + _ ≥ (φ f) f := order_preserving_φ f hn.le + _ = (1 : ℝ) := f_maps_one_φ f + have zero_lt_one : (0 : ℝ) < 1 := Real.zero_lt_one + have : 0 < 0 := lt_imp_lt_of_le_imp_le (fun a ↦ zero_le_one) zero_lt_one + exact Nat.not_succ_le_zero 0 this