From befa35c36b4433099f49f579e3e0245bcb24c9e0 Mon Sep 17 00:00:00 2001 From: Eric Date: Tue, 26 Nov 2024 12:03:15 -0800 Subject: [PATCH] Progress of phi homomorphism proof --- .../OrderedGroup/Approximate.lean | 83 ++++++++++++++++++- OrderedSemigroups/OrderedGroup/Basic.lean | 35 ++++++++ OrderedSemigroups/OrderedGroup/Defs.lean | 10 ++- 3 files changed, 125 insertions(+), 3 deletions(-) diff --git a/OrderedSemigroups/OrderedGroup/Approximate.lean b/OrderedSemigroups/OrderedGroup/Approximate.lean index cc8b0c5..8125ffd 100644 --- a/OrderedSemigroups/OrderedGroup/Approximate.lean +++ b/OrderedSemigroups/OrderedGroup/Approximate.lean @@ -1,5 +1,6 @@ import OrderedSemigroups.OrderedGroup.Basic import OrderedSemigroups.Convergence +import OrderedSemigroups.Basic /-- Every nonempty set of integers that is bounded above has a maximum element. @@ -158,7 +159,87 @@ noncomputable def φ' : α → ℝ := 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 +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 + 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 + 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 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 + simp [←zpow_add] at this + exact q_max_lt f_pos (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) := + 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 + 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 := + Int.sub_le_sub_right this 1 + ring_nf at this + ring_nf + trivial + · constructor + · 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' + simp [←zpow_add] at this + have := q_max_lt f_pos (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 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 + 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 + 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 + 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) + 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 + 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 + 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 + 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 rp_pos : (p : ℝ) > 0 := Nat.cast_pos'.mpr p_pos + exact (div_le_div_iff_of_pos_right rp_pos).mpr (this p) + have h1 : φ' f_pos a + φ' f_pos b ≤ φ' f_pos (a*b) := by sorry + have h2 : φ' f_pos (a*b) ≤ φ' f_pos a + φ' f_pos b := by sorry + have := PartialOrder.le_antisymm (a := φ' f_pos a + φ' f_pos b) (b := φ' f_pos (a*b)) h1 h2 + exact this.symm noncomputable def φ : α →* ℝ where toFun := φ' f_pos diff --git a/OrderedSemigroups/OrderedGroup/Basic.lean b/OrderedSemigroups/OrderedGroup/Basic.lean index c93dc11..76b73e5 100644 --- a/OrderedSemigroups/OrderedGroup/Basic.lean +++ b/OrderedSemigroups/OrderedGroup/Basic.lean @@ -4,6 +4,25 @@ universe u variable {α : Type u} +section Group +variable [Group α] + +theorem pnat_pow_eq_nat_pow (x : α) (n : ℕ+) : x^(n.val) = x^n := by + induction n using PNat.recOn with + | p1 => simp + | hp n ih => + simp [ppow_succ, pow_succ, ih] + +theorem split_first_and_last_factor_of_product_group {a b : α} {n : ℕ} : + (a*b)^(n+1) = a*(b*a)^n*b := by + obtain n_eq_0 | n_gt_0 := Nat.eq_zero_or_pos n + · simp [n_eq_0] + · set n' : ℕ+ := ⟨n, n_gt_0⟩ + have : (a*b)^(n'+1) = a*(b*a)^n'*b := split_first_and_last_factor_of_product + simpa [←pnat_pow_eq_nat_pow] + +end Group + section LeftOrdered variable [LeftOrderedGroup α] @@ -159,6 +178,22 @@ section LinearOrderedGroup variable [LinearOrderedGroup α] +theorem comm_factor_le_group {a b : α} (h : a*b ≤ b*a) (n : ℕ) : a^n * b^n ≤ (a*b)^n := by + obtain n_eq_0 | n_gt_0 := Nat.eq_zero_or_pos n + · simp [n_eq_0] + · set n' : ℕ+ := ⟨n, n_gt_0⟩ + have := comm_factor_le h n' + simpa [←pnat_pow_eq_nat_pow] + +theorem comm_swap_le_group {a b : α} (h : a*b ≤ b*a) (n : ℕ) : (a*b)^n ≤ (b*a)^n := pow_le_pow_left' h n + +theorem comm_dist_le_group {a b : α} (h : a*b ≤ b*a) (n : ℕ) : (b*a)^n ≤ b^n * a^n := by + obtain n_eq_0 | n_gt_0 := Nat.eq_zero_or_pos n + · simp [n_eq_0] + · set n' : ℕ+ := ⟨n, n_gt_0⟩ + have := comm_dist_le h n' + simpa [←pnat_pow_eq_nat_pow] + 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 diff --git a/OrderedSemigroups/OrderedGroup/Defs.lean b/OrderedSemigroups/OrderedGroup/Defs.lean index a761aaa..ed9fcb6 100644 --- a/OrderedSemigroups/OrderedGroup/Defs.lean +++ b/OrderedSemigroups/OrderedGroup/Defs.lean @@ -1,4 +1,5 @@ import Mathlib.Algebra.Order.Group.Basic +import OrderedSemigroups.Basic universe u @@ -7,8 +8,6 @@ variable {α : Type u} class LeftOrderedGroup (α : Type u) extends Group α, PartialOrder α where mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b -variable [LeftOrderedGroup α] - instance leftOrderedCovariant [LeftOrderedGroup α] : CovariantClass α α (· * ·) (· ≤ ·) where elim a b c bc := LeftOrderedGroup.mul_le_mul_left b c bc a @@ -26,8 +25,15 @@ instance rightOrderedContravariant [RightOrderedGroup α] : ContravariantClass class OrderedGroup (α : Type u) extends LeftOrderedGroup α, RightOrderedGroup α +instance [OrderedGroup α] : OrderedSemigroup α where + mul_le_mul_left := OrderedGroup.toLeftOrderedGroup.mul_le_mul_left + mul_le_mul_right := OrderedGroup.toRightOrderedGroup.mul_le_mul_right + class LeftLinearOrderedGroup (α : Type u) extends LeftOrderedGroup α, LinearOrder α class RightLinearOrderedGroup (α : Type u) extends RightOrderedGroup α, LinearOrder α class LinearOrderedGroup (α : Type u) extends LeftLinearOrderedGroup α, RightLinearOrderedGroup α + +instance [LinearOrderedGroup α] : OrderedGroup α where + mul_le_mul_right := LinearOrderedGroup.toRightLinearOrderedGroup.mul_le_mul_right