From 1dcedd8c0edf2413b04cade308235006f5198b3e Mon Sep 17 00:00:00 2001 From: Eric P Date: Wed, 21 Aug 2024 15:55:48 -0700 Subject: [PATCH] Prove that not Archimedean implies anomalous pair --- OrderedSemigroups/Archimedean.lean | 115 ++++++++++++++++++++++++----- OrderedSemigroups/Basic.lean | 10 +-- OrderedSemigroups/Defs.lean | 2 +- OrderedSemigroups/PNat.lean | 29 ++++++++ OrderedSemigroups/Sign.lean | 44 +++++++++++ 5 files changed, 176 insertions(+), 24 deletions(-) create mode 100644 OrderedSemigroups/PNat.lean diff --git a/OrderedSemigroups/Archimedean.lean b/OrderedSemigroups/Archimedean.lean index 938e9be..2cb1913 100644 --- a/OrderedSemigroups/Archimedean.lean +++ b/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 diff --git a/OrderedSemigroups/Basic.lean b/OrderedSemigroups/Basic.lean index 2603d93..1f3c5ba 100644 --- a/OrderedSemigroups/Basic.lean +++ b/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 diff --git a/OrderedSemigroups/Defs.lean b/OrderedSemigroups/Defs.lean index 6649a0f..23821a8 100644 --- a/OrderedSemigroups/Defs.lean +++ b/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 diff --git a/OrderedSemigroups/PNat.lean b/OrderedSemigroups/PNat.lean new file mode 100644 index 0000000..a34bdef --- /dev/null +++ b/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 diff --git a/OrderedSemigroups/Sign.lean b/OrderedSemigroups/Sign.lean index 032cec6..6f4478f 100644 --- a/OrderedSemigroups/Sign.lean +++ b/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