Prove that not Archimedean implies anomalous pair

OrderedSemigroups/Archimedean.lean

@@ -15,14 +15,14 @@ variable {α : Type u}
 section OrderedSemigroup
 variable [OrderedSemigroup α]
 
-def is_archimedean_wrt (a b : α) :=
+abbrev is_archimedean_wrt (a b : α) :=
   ∃N : ℕ+, ∀n : ℕ+, n ≥ N → (is_positive b ∧ b < a^n) ∨ (is_negative b ∧ a^n < b)
 
-def anomalous_pair (a b : α) := ∀n : ℕ+, (a^n < b^n ∧ b^n < a^(n+1)) ∨ (a^n > b^n ∧ b^n > a^(n+1))
+abbrev anomalous_pair (a b : α) := ∀n : ℕ+, (a^n < b^n ∧ b^n < a^(n+1)) ∨ (a^n > b^n ∧ b^n > a^(n+1))
 
-def has_anomalous_pair := ∃a b : α, anomalous_pair a b
+abbrev has_anomalous_pair := ∃a b : α, anomalous_pair a b
 
-def is_archimedean := ∀a b : α, is_one a ∨ is_one b ∨ is_archimedean_wrt a b
+def is_archimedean := ∀a b : α, is_one a ∨ is_one b ∨ (same_sign a b → is_archimedean_wrt a b)
 
 class Archimedean (α : Type u) [OrderedSemigroup α] where
   arch : is_archimedean (α := α)
@@ -45,23 +45,102 @@ theorem archimedean_same_sign {a b : α} (arch : is_archimedean_wrt a b) : same_
     · exact pow_le_neg_neg neg_b N h.le
     · trivial
 
+theorem pos_ge_once_archimedean {a b : α} (pos : is_positive b) (h : ∃n : ℕ+, a^n ≥ b) : is_archimedean_wrt a b := by
+  rcases h with ⟨n, hn⟩
+  use n+1
+  intro x hx
+  left
+  constructor
+  · trivial
+  · exact lt_of_le_of_lt hn (pos_ppow_lt_ppow n x (pos_le_pow_pos pos n hn) hx)
+
+theorem neg_ge_once_archimedean {a b : α} (neg : is_negative b) (h : ∃n : ℕ+, a^n ≤ b) : is_archimedean_wrt a b := by
+  rcases h with ⟨n, hn⟩
+  use n+1
+  intro x hx
+  right
+  constructor
+  · trivial
+  · exact gt_of_ge_of_gt hn (neg_ppow_lt_ppow n x (pow_le_neg_neg neg n hn) hx)
+
+theorem pos_not_archimedean_wrt_forall_lt {a b : α} (pos : is_positive b) (h : ¬is_archimedean_wrt a b) :
+    ∀n : ℕ+, a^n < b := by
+  have := mt (pos_ge_once_archimedean pos) h
+  simpa
+
+theorem neg_not_archimedean_wrt_forall_gt {a b : α} (neg : is_negative b) (h : ¬is_archimedean_wrt a b) :
+    ∀n : ℕ+, b < a^n := by
+  have := mt (neg_ge_once_archimedean neg) h
+  simpa
+
+theorem pos_not_arch_anomalous_pair {a b : α} (pos_a : is_positive a) (pos_b : is_positive b)
+    (not_arch : ¬is_archimedean_wrt a b) (comm : a*b ≤ b*a) : anomalous_pair b (a*b) := by
+  intro n
+  left
+  constructor
+  · exact gt_of_ge_of_gt (comm_factor_le comm n) ((pos_pow_pos pos_a n) (b ^ n))
+  · calc
+      (a * b) ^ n ≤ (b * a) ^ n := le_pow comm n
+      _           ≤ b ^ n * a ^ n := comm_dist_le comm n
+      _           < b ^ n * b := mul_lt_mul_left' (pos_not_archimedean_wrt_forall_lt pos_b not_arch n) (b ^ n)
+      _           = b ^ (n + 1) := Eq.symm (ppow_succ n b)
+
+theorem pos_not_arch_anomalous_pair' {a b : α} (pos_a : is_positive a) (pos_b : is_positive b)
+    (not_arch : ¬is_archimedean_wrt a b) (comm : b*a ≤ a*b) : anomalous_pair b (a*b) := by
+  intro n
+  left
+  constructor
+  · calc
+      b ^ n < b ^ n * a ^ n := pos_right (pos_pow_pos pos_a n) (b ^ n)
+      _     ≤ (b * a) ^ n := comm_factor_le comm n
+      _     ≤ (a * b) ^ n := comm_swap_le comm n
+  · calc
+      (a * b) ^ n ≤ a ^ n * b ^ n := comm_dist_le comm n
+      _           < b * b ^ n := mul_lt_mul_right' (pos_not_archimedean_wrt_forall_lt pos_b not_arch n) (b ^ n)
+      _           = b ^ (n + 1) := Eq.symm (ppow_succ' n b)
+
+theorem neg_not_archimedean_anomalous_pair {a b : α} (neg_a : is_negative a) (neg_b : is_negative b)
+    (not_arch : ¬is_archimedean_wrt a b) (comm : a*b ≤ b*a) : anomalous_pair b (a*b) := by
+  intro n
+  right
+  constructor
+  · calc
+      (a * b) ^ n ≤ (b * a) ^ n := comm_swap_le comm n
+      _           ≤ b ^ n * a ^ n := comm_dist_le comm n
+      _           < b ^ n := neg_right (neg_pow_neg neg_a n) (b ^ n)
+  · calc
+      (a * b) ^ n ≥ a ^ n * b ^ n := comm_factor_le comm n
+      _           > b * b ^ n := mul_lt_mul_right' (neg_not_archimedean_wrt_forall_gt neg_b not_arch n ) (b ^ n)
+      _           = b ^ (n + 1) := Eq.symm (ppow_succ' n b)
+
+theorem neg_not_archimedean_anomalous_pair' {a b : α} (neg_a : is_negative a) (neg_b : is_negative b)
+    (not_arch : ¬is_archimedean_wrt a b) (comm : b*a ≤ a*b) : anomalous_pair b (a*b) := by
+  intro n
+  right
+  constructor
+  · exact lt_of_le_of_lt (comm_dist_le comm n) ((neg_pow_neg neg_a n) (b ^ n))
+  · calc
+      (a * b) ^ n ≥ (b * a) ^ n := comm_swap_le comm n
+      _           ≥ b ^ n * a ^ n := comm_factor_le comm n
+      _           > b ^ n * b := mul_lt_mul_left' (neg_not_archimedean_wrt_forall_gt neg_b not_arch n) (b ^ n)
+      _           = b ^ (n + 1) := Eq.symm (ppow_succ n b)
+
 theorem non_archimedean_anomalous_pair (non_arch : ¬is_archimedean (α := α)) : has_anomalous_pair (α := α) := by
-  simp [is_archimedean] at non_arch
-  rcases non_arch with ⟨a, not_one_a, b, not_one_b, hab⟩
+  unfold is_archimedean at non_arch
+  push_neg at non_arch
+  rcases non_arch with ⟨a, b, not_one_a, not_one_b, same_sign_ab, hab⟩
   rcases pos_neg_or_one a with pos_a | neg_a | one_a
   <;> rcases pos_neg_or_one b with pos_b | neg_b | one_b
-  sorry
-  /-
+  <;> try contradiction
   · rcases le_total (a*b) (b*a) with h | h
-    ·
-  simp [is_archimedean_wrt] at hab
-  rcases hab 1 with ⟨x, hx, hab_pos, hab_neg⟩
-  -/
-
+    <;> use b, (a*b)
+    · exact pos_not_arch_anomalous_pair pos_a pos_b hab h
+    · exact pos_not_arch_anomalous_pair' pos_a pos_b hab h
+  · exact False.elim (pos_neg_same_sign_false pos_a neg_b same_sign_ab)
+  · exact False.elim (pos_neg_same_sign_false pos_b neg_a (same_sign_symm same_sign_ab))
+  · rcases le_total (a*b) (b*a) with h | h
+    <;> use b, (a*b)
+    · exact neg_not_archimedean_anomalous_pair neg_a neg_b hab h
+    · exact neg_not_archimedean_anomalous_pair' neg_a neg_b hab h
 
 end LinearOrderedCancelSemigroup
-
-section Archimedean
-variable [Archimedean α]
-
-end Archimedean

OrderedSemigroups/Basic.lean

@@ -12,11 +12,6 @@ universe u
 
 variable {α : Type u}
 
-@[simp]
-lemma add_sub_eq (x y : ℕ+) : x + y - y = x := by
-  apply PNat.eq
-  simp [PNat.sub_coe, PNat.lt_add_left y x]
-
 section Semigroup'
 variable [Semigroup' α]
 
@@ -36,6 +31,11 @@ theorem ppow_comm (n : ℕ+) (x : α) : x^n * x = x * x^n := by
 theorem ppow_succ' (n : ℕ+) (x : α) : x ^ (n + 1) = x * x^n := by
   rw [ppow_succ, ppow_comm]
 
+theorem ppow_add (a : α) (m n : ℕ+) : a ^ (m + n) = a ^ m * a ^ n := by
+  induction n using PNat.recOn with
+  | p1 => simp [ppow_succ]
+  | hp n ih => rw [ppow_succ, ←mul_assoc, ←ih, ←ppow_succ]; exact rfl
+
 theorem split_first_and_last_factor_of_product [Semigroup' α] {a b : α} {n : ℕ+} :
   (a*b)^(n+1) = a*(b*a)^n*b := by
   induction n using PNat.recOn with

OrderedSemigroups/Defs.lean

@@ -1,6 +1,6 @@
 import Mathlib.Algebra.Order.Group.Basic
 import Mathlib.Algebra.Order.Monoid.Unbundled.Basic
-import Mathlib.Data.PNat.Basic
+import OrderedSemigroups.PNat
 
 /-!
 # Ordered Semigroups

OrderedSemigroups/PNat.lean

@@ -0,0 +1,29 @@
+import Mathlib.Data.PNat.Basic
+
+lemma add_sub_eq (x y : ℕ+) : x + y - y = x := by
+  apply PNat.eq
+  simp [PNat.sub_coe, PNat.lt_add_left y x]
+
+lemma gt_one_sub_eq {x : ℕ+} (h : 1 < x) : (x : ℕ) - 1 = ((x - 1) : ℕ+) := by
+  simp [PNat.sub_coe, h]
+
+lemma lt_sub {x y : ℕ+} (h : x + 1 < y) : x < y - 1 := by
+  rw [←PNat.coe_lt_coe]
+  exact Nat.lt_of_lt_of_eq (Nat.lt_sub_of_add_lt h) (gt_one_sub_eq (PNat.one_lt_of_lt h))
+
+lemma le.dest : ∀{n m : ℕ+}, n < m → ∃k : ℕ+, n + k = m := by
+  intro n
+  induction n using PNat.recOn with
+  | p1 =>
+    intro m h
+    use (m - 1)
+    exact PNat.add_sub_of_lt h
+  | hp n ih =>
+    intro m h
+    have : n < m - 1 := lt_sub h
+    obtain ⟨k, hk⟩ := ih this
+    use k
+    have : n + 1 + k = m := by
+      simp [add_right_comm, congrFun (congrArg HAdd.hAdd hk) 1,
+        AddCommMagma.add_comm (m - 1) 1, PNat.add_sub_of_lt (PNat.one_lt_of_lt h)]
+    exact this

OrderedSemigroups/Sign.lean

@@ -85,6 +85,29 @@ def same_sign (a b : α) :=
   (is_negative a ∧ is_negative b) ∨
   (is_one a ∧ is_one b)
 
+theorem same_sign_symm {a b : α} (h : same_sign a b) : same_sign b a := by
+  unfold same_sign at *
+  tauto
+
+theorem pos_neg_same_sign_false {a b : α} (pos : is_positive a) (neg : is_negative b) (ss : same_sign a b) : False := by
+  unfold same_sign at ss
+  rcases ss with ⟨_, pos_b⟩ | ⟨neg_a, _⟩ | ⟨one_a, _⟩
+  · exact pos_not_neg pos_b neg
+  · exact pos_not_neg pos neg_a
+  · exact one_not_pos one_a pos
+
+theorem pos_ppow_lt_ppow {a : α} (n m : ℕ+) (pos : is_positive a)
+    (h : n < m) : a ^ n < a ^ m := by
+  obtain ⟨k, hk⟩ := le.dest h
+  rw [←hk, ←AddCommMagma.add_comm k n, ppow_add]
+  exact (pos_pow_pos pos k) (a ^ n)
+
+theorem neg_ppow_lt_ppow {a : α} (n m : ℕ+) (neg : is_negative a)
+    (h : n < m) : a ^ m < a ^ n := by
+  obtain ⟨k, hk⟩ := le.dest h
+  rw [←hk, ←AddCommMagma.add_comm k n, ppow_add]
+  exact (neg_pow_neg neg k) (a ^ n)
+
 end OrderedSemigroup
 
 section LinearOrderedCancelSemigroup
@@ -114,6 +137,27 @@ lemma one_right_one_forall {a b : α} (h : b * a = b) : is_one a := by
   have : b * a * x = b * x := congrFun (congrArg HMul.hMul h) x
   simpa [mul_assoc]
 
+theorem pos_right {a : α} (pos : is_positive a) : ∀x : α, x * a > x := by
+  intro x
+  rcases lt_trichotomy (x*a) x with h | h | h
+  · exact False.elim (neg_not_pos (neg_right_neg_forall h) pos)
+  · exact False.elim (one_not_pos (one_right_one_forall h) pos)
+  · trivial
+
+theorem neg_right {a : α} (neg : is_negative a) : ∀x : α, x * a < x := by
+  intro x
+  rcases lt_trichotomy (x*a) x with h | h | h
+  · trivial
+  · exact False.elim (one_not_neg (one_right_one_forall h) neg)
+  · exact False.elim (pos_not_neg (pos_right_pos_forall h) neg)
+
+theorem one_right {a : α} (one : is_one a) : ∀x : α, x * a = x := by
+  intro x
+  rcases lt_trichotomy (x*a) x with h | h | h
+  · exact False.elim (neg_not_one (neg_right_neg_forall h) one)
+  · trivial
+  · exact False.elim (pos_not_one (pos_right_pos_forall h) one)
+
 /-- Every element of a LinearOrderedCancelSemigroup is either positive, negative, or one. -/
 theorem pos_neg_or_one : ∀a : α, is_positive a ∨ is_negative a ∨ is_one a := by
   intro a