Skip to content

Commit

Permalink
Finish proof that not anomalous pair means commutative
Browse files Browse the repository at this point in the history
  • Loading branch information
@ericluap
ericluap committed Aug 22, 2024
1 parent 5d48255 commit 9555cca
Show file tree
Hide file tree
Showing 3 changed files with 92 additions and 36 deletions.
108 changes: 84 additions & 24 deletions OrderedSemigroups/Archimedean.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,27 +15,29 @@ variable {α : Type u}
section OrderedSemigroup
variable [OrderedSemigroup α]

/-- `a` is Archimedean with respect to `b` if there exists an `N : ℕ+` such that
for all `n ≥ N`, either `b` is positive and `b < a^n` or `b` is negative and `a^n < b`. -/
abbrev is_archimedean_wrt (a b : α) :=
∃N : ℕ+, ∀n : ℕ+, n ≥ N → (is_positive b ∧ b < a^n) ∨ (is_negative b ∧ a^n < b)

/-- A pair of elements `a` and `b` form an anomalous pair if for all `n : ℕ+`,
either `a^n < b^n` and `b^n < a^(n+1)` or `a^n > b^n` and `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))

/-- An ordered semigroup has an anomalous pair if there exist elements `a` and `b` such that
`a` and `b` form an anomalous pair. -/
abbrev has_anomalous_pair := ∃a b : α, anomalous_pair a b

/-- An ordered semigroup is Archimedean if for all elements `a` and `b` of it, either
`a` is one, `b` is one, or if `a` and `b` have the same sign, then `a` is Archimedean with respect to `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 (α := α)

theorem not_has_anomalous_not_pair (not_anomalous : ¬has_anomalous_pair (α := α)) (a b : α) : ¬anomalous_pair a b := by
simp at *
tauto

end OrderedSemigroup

section LinearOrderedCancelSemigroup
variable [LinearOrderedCancelSemigroup α]

/-- If `a` is Archimedean with respect to `b`, then `a` and `b` have the same sign. -/
theorem archimedean_same_sign {a b : α} (arch : is_archimedean_wrt a b) : same_sign a b := by
obtain ⟨N, arch⟩ := arch
rcases arch N (by simp) with ⟨pos_b, h⟩ | ⟨neg_b , h⟩
Expand All @@ -49,6 +51,7 @@ theorem archimedean_same_sign {a b : α} (arch : is_archimedean_wrt a b) : same_
· exact pow_le_neg_neg neg_b N h.le
· trivial

/-- If `b` is positive and there exists an `n : ℕ+` such that `a^n ≥ b`, then `a` is Archimedean with respect to `b`. -/
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
Expand All @@ -58,6 +61,7 @@ theorem pos_ge_once_archimedean {a b : α} (pos : is_positive b) (h : ∃n : ℕ
· trivial
· exact lt_of_le_of_lt hn (pos_ppow_lt_ppow n x (pos_le_pow_pos pos n hn) hx)

/-- If `b` is negative and there exists an `n : ℕ+` such that `a^n ≤ b`, then `a` is Archimedean with respect to `b`. -/
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
Expand All @@ -67,16 +71,19 @@ theorem neg_ge_once_archimedean {a b : α} (neg : is_negative b) (h : ∃n : ℕ
· trivial
· exact gt_of_ge_of_gt hn (neg_ppow_lt_ppow n x (pow_le_neg_neg neg n hn) hx)

/-- If `b` is positive and `a` is not Archimedean with respect to `b`, then for all `n : ℕ+`, `a^n < b`. -/
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

/-- If `b` is negative and `a` is not Archimedean with respect to `b`, then for all `n : ℕ+`, `b < a^n`. -/
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

/-- If `a` and `b` are positive, `a` is not Archimedean with respect to `b`, and `a*b ≤ b*a`, then `b` and `a*b` form an anomalous pair. -/
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
Expand All @@ -89,6 +96,7 @@ theorem pos_not_arch_anomalous_pair {a b : α} (pos_a : is_positive a) (pos_b :
_ < 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)

/-- If `a` and `b` are positive, `a` is not Archimedean with respect to `b`, and `b*a ≤ a*b`, then `b` and `a*b` form an anomalous pair. -/
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
Expand All @@ -103,6 +111,7 @@ theorem pos_not_arch_anomalous_pair' {a b : α} (pos_a : is_positive a) (pos_b :
_ < 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)

/-- If `a` and `b` are negative, `a` is not Archimedean with respect to `b`, and `a*b ≤ b*a`, then `b` and `a*b` form an anomalous pair. -/
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
Expand All @@ -117,6 +126,7 @@ theorem neg_not_archimedean_anomalous_pair {a b : α} (neg_a : is_negative a) (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)

/-- If `a` and `b` are negative, `a` is not Archimedean with respect to `b`, and `b*a ≤ a*b`, then `b` and `a*b` form an anomalous pair. -/
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
Expand All @@ -129,6 +139,7 @@ theorem neg_not_archimedean_anomalous_pair' {a b : α} (neg_a : is_negative a) (
_ > 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)

/-- If a linear ordered cancel semigroup is not Archimedean, then it has an anomalous pair. -/
theorem non_archimedean_anomalous_pair (non_arch : ¬is_archimedean (α := α)) : has_anomalous_pair (α := α) := by
unfold is_archimedean at non_arch
push_neg at non_arch
Expand All @@ -147,6 +158,7 @@ theorem non_archimedean_anomalous_pair (non_arch : ¬is_archimedean (α := α))
· exact neg_not_archimedean_anomalous_pair neg_a neg_b hab h
· exact neg_not_archimedean_anomalous_pair' neg_a neg_b hab h

/-- If `a` and `b` are positive and `a * b < b * a`, then `a*b` and `b*a` form an anomalous pair. -/
theorem pos_not_comm_anomalous_pair {a b : α} (pos_a : is_positive a) (pos_b : is_positive b)
(h : a * b < b * a) : anomalous_pair (a*b) (b*a) := by
intro n
Expand All @@ -159,6 +171,7 @@ theorem pos_not_comm_anomalous_pair {a b : α} (pos_a : is_positive a) (pos_b :
left
exact ⟨comm_swap_lt h n, this n⟩

/-- If `a` and `b` are negative and `a * b < b * a`, then `b*a` and `a*b` form an anomalous pair. -/
theorem neg_not_comm_anomalous_pair {a b : α} (neg_a : is_negative a) (neg_b : is_negative b)
(h : a * b < b * a) : anomalous_pair (b*a) (a*b) := by
intro n
Expand All @@ -171,6 +184,7 @@ theorem neg_not_comm_anomalous_pair {a b : α} (neg_a : is_negative a) (neg_b :
right
exact ⟨comm_swap_lt h n, this n⟩

/-- If `a` and `b` are positive and there is no anomalous pair, then `a` and `b` commute. -/
theorem pos_not_anomalous_comm {a b : α} (pos_a : is_positive a) (pos_b : is_positive b)
(not_anomalous : ¬has_anomalous_pair (α := α)): a * b = b * a := by
rcases lt_trichotomy (a*b) (b*a) with h | h | h
Expand All @@ -184,6 +198,7 @@ theorem pos_not_anomalous_comm {a b : α} (pos_a : is_positive a) (pos_b : is_po
exact pos_not_comm_anomalous_pair pos_b pos_a h
contradiction

/-- If `a` and `b` are negative and there is no anomalous pair, then `a` and `b` commute. -/
theorem neg_not_anomalous_comm {a b : α} (neg_a : is_negative a) (neg_b : is_negative b)
(not_anomalous : ¬has_anomalous_pair (α := α)): a * b = b * a := by
rcases lt_trichotomy (a*b) (b*a) with h | h | h
Expand All @@ -197,15 +212,68 @@ theorem neg_not_anomalous_comm {a b : α} (neg_a : is_negative a) (neg_b : is_ne
exact neg_not_comm_anomalous_pair neg_b neg_a h
contradiction

/-- If `a * b < b * a` and `(b * a)` commutes with `b`, then we have a contradiction and so `a` and `b` commute. -/
theorem not_comm_once_comm {a b : α} (h : a * b < b * a) (comm : (b * a) * b = b * (b * a)) :
a * b = b * a := by
have : a * b * a * b > a * b * a * b := calc
a * b * a * b = a * ((b * a) * b) := by simp [mul_assoc]
_ = a * (b * (b * a)) := by simp [←comm]
_ = (a * b) * (b * a) := by simp [mul_assoc]
_ > (a * b) * (a * b) := by exact mul_lt_mul_left' h (a * b)
_ = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b)
exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this)

/-- If `b * a < a * b` and `(b * a)` commutes with `b`, then we have a contradiction and so `a` and `b` commute. -/
theorem not_comm_once_comm' {a b : α} (h : b * a < a * b) (comm : (b * a) * b = b * (b * a)) :
a * b = b * a := by
have : a * b * a * b > a * b * a * b := calc
a * b * a * b = a * ((b * a) * b) := by simp [mul_assoc]
_ = a * (b * (b * a)) := by simp [←comm]
_ = (a * b) * (b * a) := by simp [mul_assoc]
_ < (a * b) * (a * b) := by exact mul_lt_mul_left' h (a * b)
_ = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b)
exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this)

/-- If `a * b < b * a` and `(b * a)` commutes with `a`, then we have a contradiction and so `a` and `b` commute. -/
theorem not_comm_once_comm'' {a b : α} (h : a * b < b * a) (comm : (b * a) * a = a * (b * a)) :
a * b = b * a := by
have : a * b * a * b > a * b * a * b := calc
a * b * a * b = (a * (b * a)) * b := by simp [mul_assoc]
_ = ((b * a) * a) * b := by simp [←comm]
_ = (b * a) * (a * b) := by simp [mul_assoc]
_ > (a * b) * (a * b) := by exact mul_lt_mul_right' h (a * b)
_ = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b)
exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this)

/-- If `b * a < a * b` and `(b * a)` commutes with `a`, then we have a contradiction and so `a` and `b` commute. -/
theorem not_comm_once_comm''' {a b : α} (h : b * a < a * b) (comm : (b * a) * a = a * (b * a)) :
a * b = b * a := by
have : a * b * a * b > a * b * a * b := calc
a * b * a * b = (a * (b * a)) * b := by simp [mul_assoc]
_ = ((b * a) * a) * b := by simp [←comm]
_ = (b * a) * (a * b) := by simp [mul_assoc]
_ < (a * b) * (a * b) := by exact mul_lt_mul_right' h (a * b)
_ = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b)
exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this)

/-- If a linear ordered cancel semigroup does not have an anomalous pair, then it is commutative. -/
theorem not_anomalous_pair_commutative (not_anomalous : ¬has_anomalous_pair (α := α)) (a b : α) : a * b = b * a := by
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
all_goals try simp [one_b a, one_right one_b a]
all_goals try simp [one_a b, one_right one_a b]
· exact pos_not_anomalous_comm pos_a pos_b not_anomalous
· rcases pos_neg_or_one (a*b) with pos_ab | neg_ab | one_ab
· sorry
· sorry
have := pos_not_anomalous_comm pos_ab pos_a not_anomalous
· rcases lt_trichotomy (a*b) (b*a) with h | h | h
· exact Eq.symm (not_comm_once_comm' h this)
· trivial
· exact Eq.symm (not_comm_once_comm h this)
have := neg_not_anomalous_comm neg_ab neg_b not_anomalous
· rcases lt_trichotomy (a*b) (b*a) with h | h | h
· exact Eq.symm (not_comm_once_comm''' h this)
· trivial
· exact Eq.symm (not_comm_once_comm'' h this)
· have : is_one (b * a) := by
apply one_right_one_forall (b := a)
rw [Eq.symm (mul_assoc a b a)]
Expand All @@ -214,22 +282,14 @@ theorem not_anomalous_pair_commutative (not_anomalous : ¬has_anomalous_pair (α
· rcases pos_neg_or_one (b*a) with pos_ba | neg_ba | one_ba
have := pos_not_anomalous_comm pos_ba pos_b not_anomalous
· rcases lt_trichotomy (a*b) (b*a) with h | h | h
· have : a * b * a * b > a * b * a * b := calc
a * b * a * b = a * ((b * a) * b) := by simp [mul_assoc]
_ = a * (b * (b * a)) := by simp [←this]
_ = (a * b) * (b * a) := by simp [mul_assoc]
_ > (a * b) * (a * b) := by exact mul_lt_mul_left' h (a * b)
_ = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b)
exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this)
· exact not_comm_once_comm h this
· trivial
· exact not_comm_once_comm' h this
have := neg_not_anomalous_comm neg_ba neg_a not_anomalous
· rcases lt_trichotomy (a*b) (b*a) with h | h | h
· exact not_comm_once_comm'' h this
· trivial
· have : a * b * a * b > a * b * a * b := calc
a * b * a * b = a * ((b * a) * b) := by simp [mul_assoc]
_ = a * (b * (b * a)) := by simp [←this]
_ = (a * b) * (b * a) := by simp [mul_assoc]
_ < (a * b) * (a * b) := by exact mul_lt_mul_left' h (a * b)
_ = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b)
exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this)
· sorry
· exact not_comm_once_comm''' h this
· have : is_one (a * b) := by
apply one_right_one_forall (b := b)
rw [Eq.symm (mul_assoc b a b)]
Expand Down
12 changes: 0 additions & 12 deletions OrderedSemigroups/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,16 +103,4 @@ theorem lt_pow {a b : α} (h : a < b) (n : ℕ+) : a^n < b^n := by

theorem comm_swap_lt {a b : α} (h : a*b < b*a) (n : ℕ+) : (a*b)^n < (b*a)^n := lt_pow h n

/-
theorem comm_dist_lt {a b : α} (h : a*b < b*a) (n : ℕ+) : n > 1 → (b*a)^n < b^n * a^n := by
induction n using PNat.recOn with
| p1 => intro; contradiction
| hp n ih =>
calc
(b*a)^(n+1) = b * (a*b)^n * a := by rw [split_first_and_last_factor_of_product]
_ ≤ b * (b*a)^n * a := middle_swap (le_pow h n)
_ ≤ b * (b^n * a^n) * a := middle_swap ih
_ = (b * b^n) * (a^n * a) := by simp [mul_assoc]
_ = b^(n+1) * a^(n+1) := by simp [ppow_succ, ←ppow_succ']-/

end OrderedCancelSemigroup
8 changes: 8 additions & 0 deletions OrderedSemigroups/PNat.lean
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,13 @@
import Mathlib.Data.PNat.Basic

/-!
# Positive Naturals
This file proves some basic lemmas about `PNat` (aka `ℕ+`)
that are used in relation to exponentiation of elements in a semigroup.
-/

lemma add_sub_eq (x y : ℕ+) : x + y - y = x := by
apply PNat.eq
simp [PNat.sub_coe, PNat.lt_add_left y x]
Expand Down

0 comments on commit 9555cca

Please sign in to comment.