Archimedean groups and fields.

This file defines the archimedean property for ordered groups and proves several results connected to this notion. Being archimedean means that for all elements x and y>0 there exists a natural number n such that x ≤ n • y.

Main definitions

• Archimedean is a typeclass for an ordered additive commutative monoid to have the archimedean property.
• MulArchimedean is a typeclass for an ordered commutative monoid to have the "mul-archimedean property" where for x and y > 1, there exists a natural number n such that x ≤ y ^ n.
• Archimedean.floorRing defines a floor function on an archimedean linearly ordered ring making it into a floorRing.

Main statements

• ℕ, ℤ, and ℚ are archimedean.

class Archimedean (α : Type u_2) [OrderedAddCommMonoid α] : Prop

An ordered additive commutative monoid is called Archimedean if for any two elements x, y such that 0 < y, there exists a natural number n such that x ≤ n • y.

• arch (x : α) {y : α} : 0 < y → ∃ (n : ℕ), x ≤ n • y

  For any two elements x, y such that 0 < y, there exists a natural number n such that x ≤ n • y.

class MulArchimedean (α : Type u_2) [OrderedCommMonoid α] : Prop

An ordered commutative monoid is called MulArchimedean if for any two elements x, y such that 1 < y, there exists a natural number n such that x ≤ y ^ n.

• arch (x : α) {y : α} : 1 < y → ∃ (n : ℕ), x ≤ y ^ n

  For any two elements x, y such that 1 < y, there exists a natural number n such that x ≤ y ^ n.

instance OrderDual.instMulArchimedean {α : Type u_1} [OrderedCommGroup α] [MulArchimedean α] : MulArchimedean αᵒᵈ

instance OrderDual.instAddArchimedean {α : Type u_1} [OrderedAddCommGroup α] [Archimedean α] : Archimedean αᵒᵈ

instance Additive.instArchimedean {α : Type u_1} [OrderedCommGroup α] [MulArchimedean α] : Archimedean (Additive α)

instance Multiplicative.instMulArchimedean {α : Type u_1} [OrderedAddCommGroup α] [Archimedean α] : MulArchimedean (Multiplicative α)

theorem exists_lt_pow {M : Type u_2} [OrderedCommMonoid M] [MulArchimedean M] [MulLeftStrictMono M] {a : M} (ha : 1 < a) (b : M) : ∃ (n : ℕ), b < a ^ n

theorem exists_lt_nsmul {M : Type u_2} [OrderedAddCommMonoid M] [Archimedean M] [AddLeftStrictMono M] {a : M} (ha : 0 < a) (b : M) : ∃ (n : ℕ), b < n • a

theorem existsUnique_zpow_near_of_one_lt {α : Type u_1} [LinearOrderedCommGroup α] [MulArchimedean α] {a : α} (ha : 1 < a) (g : α) : ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)

An archimedean decidable linearly ordered CommGroup has a version of the floor: for a > 1, any g in the group lies between some two consecutive powers of a.

theorem existsUnique_zsmul_near_of_pos {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {a : α} (ha : 0 < a) (g : α) : ∃! k : ℤ, k • a ≤ g ∧ g < (k + 1) • a

An archimedean decidable linearly ordered AddCommGroup has a version of the floor: for a > 0, any g in the group lies between some two consecutive multiples of a. -/

theorem existsUnique_zpow_near_of_one_lt' {α : Type u_1} [LinearOrderedCommGroup α] [MulArchimedean α] {a : α} (ha : 1 < a) (g : α) : ∃! k : ℤ, 1 ≤ g / a ^ k ∧ g / a ^ k < a

theorem existsUnique_zsmul_near_of_pos' {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {a : α} (ha : 0 < a) (g : α) : ∃! k : ℤ, 0 ≤ g - k • a ∧ g - k • a < a

theorem existsUnique_div_zpow_mem_Ico {α : Type u_1} [LinearOrderedCommGroup α] [MulArchimedean α] {a : α} (ha : 1 < a) (b c : α) : ∃! m : ℤ, b / a ^ m ∈ Set.Ico c (c * a)

theorem existsUnique_sub_zsmul_mem_Ico {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {a : α} (ha : 0 < a) (b c : α) : ∃! m : ℤ, b - m • a ∈ Set.Ico c (c + a)

theorem existsUnique_mul_zpow_mem_Ico {α : Type u_1} [LinearOrderedCommGroup α] [MulArchimedean α] {a : α} (ha : 1 < a) (b c : α) : ∃! m : ℤ, b * a ^ m ∈ Set.Ico c (c * a)

theorem existsUnique_add_zsmul_mem_Ico {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {a : α} (ha : 0 < a) (b c : α) : ∃! m : ℤ, b + m • a ∈ Set.Ico c (c + a)

theorem existsUnique_add_zpow_mem_Ioc {α : Type u_1} [LinearOrderedCommGroup α] [MulArchimedean α] {a : α} (ha : 1 < a) (b c : α) : ∃! m : ℤ, b * a ^ m ∈ Set.Ioc c (c * a)

theorem existsUnique_add_zsmul_mem_Ioc {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {a : α} (ha : 0 < a) (b c : α) : ∃! m : ℤ, b + m • a ∈ Set.Ioc c (c + a)

theorem existsUnique_sub_zpow_mem_Ioc {α : Type u_1} [LinearOrderedCommGroup α] [MulArchimedean α] {a : α} (ha : 1 < a) (b c : α) : ∃! m : ℤ, b / a ^ m ∈ Set.Ioc c (c * a)

theorem existsUnique_sub_zsmul_mem_Ioc {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {a : α} (ha : 0 < a) (b c : α) : ∃! m : ℤ, b - m • a ∈ Set.Ioc c (c + a)

theorem exists_nat_ge {α : Type u_1} [OrderedSemiring α] [Archimedean α] (x : α) : ∃ (n : ℕ), x ≤ ↑n

@[instance 100]

instance instIsDirectedLeOfArchimedean {α : Type u_1} [OrderedSemiring α] [Archimedean α] : IsDirected α fun (x1 x2 : α) => x1 ≤ x2

theorem exists_nat_gt {α : Type u_1} [StrictOrderedSemiring α] [Archimedean α] (x : α) : ∃ (n : ℕ), x < ↑n

theorem add_one_pow_unbounded_of_pos {α : Type u_1} [StrictOrderedSemiring α] [Archimedean α] {y : α} (x : α) (hy : 0 < y) : ∃ (n : ℕ), x < (y + 1) ^ n

theorem pow_unbounded_of_one_lt {α : Type u_1} [StrictOrderedSemiring α] [Archimedean α] {y : α} [ExistsAddOfLE α] (x : α) (hy1 : 1 < y) : ∃ (n : ℕ), x < y ^ n

theorem exists_int_ge {R : Type u_3} [OrderedRing R] [Archimedean R] (x : R) : ∃ (n : ℤ), x ≤ ↑n

theorem exists_int_le {R : Type u_3} [OrderedRing R] [Archimedean R] (x : R) : ∃ (n : ℤ), ↑n ≤ x

@[instance 100]

instance instIsDirectedGe {R : Type u_3} [OrderedRing R] [Archimedean R] : IsDirected R fun (x1 x2 : R) => x1 ≥ x2

theorem exists_int_gt {α : Type u_1} [StrictOrderedRing α] [Archimedean α] (x : α) : ∃ (n : ℤ), x < ↑n

theorem exists_int_lt {α : Type u_1} [StrictOrderedRing α] [Archimedean α] (x : α) : ∃ (n : ℤ), ↑n < x

theorem exists_floor {α : Type u_1} [StrictOrderedRing α] [Archimedean α] (x : α) : ∃ (fl : ℤ), ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x

theorem exists_nat_pow_near {α : Type u_1} [LinearOrderedSemiring α] [Archimedean α] [ExistsAddOfLE α] {x y : α} (hx : 1 ≤ x) (hy : 1 < y) : ∃ (n : ℕ), y ^ n ≤ x ∧ x < y ^ (n + 1)

Every x greater than or equal to 1 is between two successive natural-number powers of every y greater than one.

theorem exists_nat_one_div_lt {α : Type u_1} [LinearOrderedSemifield α] [Archimedean α] {ε : α} (hε : 0 < ε) : ∃ (n : ℕ), 1 / (↑n + 1) < ε

theorem exists_mem_Ico_zpow {α : Type u_1} [LinearOrderedSemifield α] [Archimedean α] {x y : α} [ExistsAddOfLE α] (hx : 0 < x) (hy : 1 < y) : ∃ (n : ℤ), x ∈ Set.Ico (y ^ n) (y ^ (n + 1))

Every positive x is between two successive integer powers of another y greater than one. This is the same as exists_mem_Ioc_zpow, but with ≤ and < the other way around.

theorem exists_mem_Ioc_zpow {α : Type u_1} [LinearOrderedSemifield α] [Archimedean α] {x y : α} [ExistsAddOfLE α] (hx : 0 < x) (hy : 1 < y) : ∃ (n : ℤ), x ∈ Set.Ioc (y ^ n) (y ^ (n + 1))

Every positive x is between two successive integer powers of another y greater than one. This is the same as exists_mem_Ico_zpow, but with ≤ and < the other way around.

theorem exists_pow_lt_of_lt_one {α : Type u_1} [LinearOrderedSemifield α] [Archimedean α] {x y : α} [ExistsAddOfLE α] (hx : 0 < x) (hy : y < 1) : ∃ (n : ℕ), y ^ n < x

For any y < 1 and any positive x, there exists n : ℕ with y ^ n < x.

theorem exists_nat_pow_near_of_lt_one {α : Type u_1} [LinearOrderedSemifield α] [Archimedean α] {x y : α} [ExistsAddOfLE α] (xpos : 0 < x) (hx : x ≤ 1) (ypos : 0 < y) (hy : y < 1) : ∃ (n : ℕ), y ^ (n + 1) < x ∧ x ≤ y ^ n

Given x and y between 0 and 1, x is between two successive powers of y. This is the same as exists_nat_pow_near, but for elements between 0 and 1

theorem exists_rat_gt {α : Type u_1} [LinearOrderedField α] [Archimedean α] (x : α) : ∃ (q : ℚ), x < ↑q

theorem exists_rat_lt {α : Type u_1} [LinearOrderedField α] [Archimedean α] (x : α) : ∃ (q : ℚ), ↑q < x

theorem exists_rat_btwn {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x y : α} (h : x < y) : ∃ (q : ℚ), x < ↑q ∧ ↑q < y

theorem le_of_forall_rat_lt_imp_le {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x y : α} (h : ∀ (q : ℚ), ↑q < x → ↑q ≤ y) : x ≤ y

theorem le_of_forall_lt_rat_imp_le {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x y : α} (h : ∀ (q : ℚ), y < ↑q → x ≤ ↑q) : x ≤ y

theorem le_iff_forall_rat_lt_imp_le {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x y : α} : x ≤ y ↔ ∀ (q : ℚ), ↑q < x → ↑q ≤ y

theorem le_iff_forall_lt_rat_imp_le {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x y : α} : x ≤ y ↔ ∀ (q : ℚ), y < ↑q → x ≤ ↑q

theorem eq_of_forall_rat_lt_iff_lt {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x y : α} (h : ∀ (q : ℚ), ↑q < x ↔ ↑q < y) : x = y

theorem eq_of_forall_lt_rat_iff_lt {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x y : α} (h : ∀ (q : ℚ), x < ↑q ↔ y < ↑q) : x = y

theorem exists_pos_rat_lt {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x : α} (x0 : 0 < x) : ∃ (q : ℚ), 0 < q ∧ ↑q < x

theorem exists_rat_near {α : Type u_1} [LinearOrderedField α] [Archimedean α] {ε : α} (x : α) (ε0 : 0 < ε) : ∃ (q : ℚ), |x - ↑q| < ε

theorem archimedean_iff_nat_lt {α : Type u_1} [LinearOrderedField α] : Archimedean α ↔ ∀ (x : α), ∃ (n : ℕ), x < ↑n

theorem archimedean_iff_nat_le {α : Type u_1} [LinearOrderedField α] : Archimedean α ↔ ∀ (x : α), ∃ (n : ℕ), x ≤ ↑n

theorem archimedean_iff_int_lt {α : Type u_1} [LinearOrderedField α] : Archimedean α ↔ ∀ (x : α), ∃ (n : ℤ), x < ↑n

theorem archimedean_iff_int_le {α : Type u_1} [LinearOrderedField α] : Archimedean α ↔ ∀ (x : α), ∃ (n : ℤ), x ≤ ↑n

theorem archimedean_iff_rat_lt {α : Type u_1} [LinearOrderedField α] : Archimedean α ↔ ∀ (x : α), ∃ (q : ℚ), x < ↑q

theorem archimedean_iff_rat_le {α : Type u_1} [LinearOrderedField α] : Archimedean α ↔ ∀ (x : α), ∃ (q : ℚ), x ≤ ↑q

instance instArchimedeanNat : Archimedean ℕ

instance instArchimedeanInt : Archimedean ℤ

instance instArchimedeanRat : Archimedean ℚ

instance Nonneg.instArchimedean {α : Type u_1} [OrderedAddCommMonoid α] [Archimedean α] : Archimedean { x : α // 0 ≤ x }

instance Nonneg.instMulArchimedean {α : Type u_1} [StrictOrderedCommSemiring α] [Archimedean α] [ExistsAddOfLE α] : MulArchimedean { x : α // 0 ≤ x }

instance instArchimedeanNNRat : Archimedean ℚ≥0

instance instMulArchimedeanNNRat : MulArchimedean ℚ≥0

noncomputable def Archimedean.floorRing (α : Type u_3) [LinearOrderedRing α] [Archimedean α] : FloorRing α

A linear ordered archimedean ring is a floor ring. This is not an instance because in some cases we have a computable floor function.

Equations

• Archimedean.floorRing α = FloorRing.ofFloor α (fun (a : α) => Classical.choose ⋯) ⋯

@[instance 100]

instance FloorRing.archimedean (α : Type u_3) [LinearOrderedField α] [FloorRing α] : Archimedean α

A linear ordered field that is a floor ring is archimedean.

instance Units.instMulArchimedean (α : Type u_3) [OrderedCommMonoid α] [MulArchimedean α] : MulArchimedean αˣ

instance AddUnits.instAddArchimedean (α : Type u_3) [OrderedAddCommMonoid α] [Archimedean α] : Archimedean (AddUnits α)