Progress of phi homomorphism proof

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

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

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