# 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.

source
class Archimedean (M : Type u_5) [AddCommMonoid M] [PartialOrder M] :
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 : M) {y : M} : 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`.

Instances

source
class MulArchimedean (M : Type u_5) [CommMonoid M] [PartialOrder M] :
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 : M) {y : M} : 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`.

Instances

source
theorem MulArchimedean.comap {G : Type u_1} {M : Type u_2} [CommMonoid G] [LinearOrder G] [CommMonoid M] [PartialOrder M] [MulArchimedean M] (f : G →* M) (hf : StrictMono ⇑f) :
MulArchimedean G
source
theorem Archimedean.comap {G : Type u_1} {M : Type u_2} [AddCommMonoid G] [LinearOrder G] [AddCommMonoid M] [PartialOrder M] [Archimedean M] (f : G →+ M) (hf : StrictMono ⇑f) :
Archimedean G
source
instance OrderDual.instMulArchimedean {G : Type u_1} [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] [MulArchimedean G] :
MulArchimedean G ᵒᵈ
source
instance OrderDual.instAddArchimedean {G : Type u_1} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [Archimedean G] :
Archimedean G ᵒᵈ
source
instance Additive.instArchimedean {G : Type u_1} [CommGroup G] [PartialOrder G] [MulArchimedean G] :
Archimedean (Additive G)
source
instance Multiplicative.instMulArchimedean {G : Type u_1} [AddCommGroup G] [PartialOrder G] [Archimedean G] :
MulArchimedean (Multiplicative G)
source
theorem exists_lt_pow {M : Type u_2} [CommMonoid M] [PartialOrder M] [MulArchimedean M] [MulLeftStrictMono M] {a : M} (ha : 1 < a) (b : M) :
∃ (n : ℕ), b < a ^ n
source
theorem exists_lt_nsmul {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [Archimedean M] [AddLeftStrictMono M] {a : M} (ha : 0 < a) (b : M) :
∃ (n : ℕ), b < n • a
source
theorem existsUnique_zpow_near_of_one_lt {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G} (ha : 1 < a) (g : 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`.

source
theorem existsUnique_zsmul_near_of_pos {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (g : 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`.

source
theorem existsUnique_zpow_near_of_one_lt' {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G} (ha : 1 < a) (g : G) :
∃! k : ℤ, 1 ≤ g / a ^ k ∧ g / a ^ k < a
source
theorem existsUnique_zsmul_near_of_pos' {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (g : G) :
∃! k : ℤ, 0 ≤ g - k • a ∧ g - k • a < a
source
theorem existsUnique_div_zpow_mem_Ico {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G} (ha : 1 < a) (b c : G) :
∃! m : ℤ, b / a ^ m ∈ Set.Ico c (c * a)
source
theorem existsUnique_sub_zsmul_mem_Ico {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (b c : G) :
∃! m : ℤ, b - m • a ∈ Set.Ico c (c + a)
source
theorem existsUnique_mul_zpow_mem_Ico {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G} (ha : 1 < a) (b c : G) :
∃! m : ℤ, b * a ^ m ∈ Set.Ico c (c * a)
source
theorem existsUnique_add_zsmul_mem_Ico {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (b c : G) :
∃! m : ℤ, b + m • a ∈ Set.Ico c (c + a)
source
theorem existsUnique_add_zpow_mem_Ioc {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G} (ha : 1 < a) (b c : G) :
∃! m : ℤ, b * a ^ m ∈ Set.Ioc c (c * a)
source
theorem existsUnique_add_zsmul_mem_Ioc {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (b c : G) :
∃! m : ℤ, b + m • a ∈ Set.Ioc c (c + a)
source
theorem existsUnique_sub_zpow_mem_Ioc {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G} (ha : 1 < a) (b c : G) :
∃! m : ℤ, b / a ^ m ∈ Set.Ioc c (c * a)
source
theorem existsUnique_sub_zsmul_mem_Ioc {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : 0 < a) (b c : G) :
∃! m : ℤ, b - m • a ∈ Set.Ioc c (c + a)
source
theorem exists_pow_lt {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G} (ha : a < 1) (b : G) :
∃ (n : ℕ), a ^ n < b
source
theorem exists_nsmul_lt {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a : G} (ha : a < 0) (b : G) :
∃ (n : ℕ), n • a < b
source
theorem exists_nat_ge {R : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] (x : R) :
∃ (n : ℕ), x ≤ ↑n
source
@[instance 100]
instance instIsDirectedLe {R : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] :
IsDirected R fun (x1 x2 : R) => x1 ≤ x2
source
theorem exists_nat_gt {R : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] (x : R) :
∃ (n : ℕ), x < ↑n
source
theorem add_one_pow_unbounded_of_pos {R : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {y : R} (x : R) (hy : 0 < y) :
∃ (n : ℕ), x < (y + 1) ^ n
source
theorem pow_unbounded_of_one_lt {R : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {y : R} [ExistsAddOfLE R] (x : R) (hy1 : 1 < y) :
∃ (n : ℕ), x < y ^ n
source
theorem exists_int_ge {R : Type u_3} [Ring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] (x : R) :
∃ (n : ℤ), x ≤ ↑n
source
theorem exists_int_le {R : Type u_3} [Ring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] (x : R) :
∃ (n : ℤ), ↑n ≤ x
source
@[instance 100]
instance instIsDirectedGe {R : Type u_3} [Ring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] :
IsDirected R fun (x1 x2 : R) => x1 ≥ x2
source
theorem exists_int_gt {R : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] (x : R) :
∃ (n : ℤ), x < ↑n
source
theorem exists_int_lt {R : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] (x : R) :
∃ (n : ℤ), ↑n < x
source
theorem exists_floor {R : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] (x : R) :
∃ (fl : ℤ), ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
source
theorem exists_nat_pow_near {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] [ExistsAddOfLE R] {x y : R} (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.

source
theorem exists_nat_one_div_lt {K : Type u_4} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {ε : K} (hε : 0 < ε) :
∃ (n : ℕ), 1 / (↑n + 1) < ε
source
theorem exists_mem_Ico_zpow {K : Type u_4} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} [ExistsAddOfLE K] (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.

source
theorem exists_mem_Ioc_zpow {K : Type u_4} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} [ExistsAddOfLE K] (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.

source
theorem exists_pow_lt_of_lt_one {K : Type u_4} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} [ExistsAddOfLE K] (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`.

source
theorem exists_nat_pow_near_of_lt_one {K : Type u_4} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} [ExistsAddOfLE K] (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`

source
theorem exists_pow_btwn_of_lt_mul {K : Type u_4} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] [ExistsAddOfLE K] {a b c : K} (h : a < b * c) (hb₀ : 0 < b) (hb₁ : b ≤ 1) (hc₀ : 0 < c) (hc₁ : c < 1) :
∃ (n : ℕ), a < c ^ n ∧ c ^ n < b

If `a < b * c`, `0 < b ≤ 1` and `0 < c < 1`, then there is a power `c ^ n` with `n : ℕ` strictly between `a` and `b`.

source
theorem exists_zpow_btwn_of_lt_mul {K : Type u_4} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] [ExistsAddOfLE K] {a b c : K} (h : a < b * c) (hb₀ : 0 < b) (hc₀ : 0 < c) (hc₁ : c < 1) :
∃ (n : ℤ), a < c ^ n ∧ c ^ n < b

If `a < b * c`, `b` is positive and `0 < c < 1`, then there is a power `c ^ n` with `n : ℤ` strictly between `a` and `b`.

source
theorem archimedean_iff_nat_lt {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
Archimedean K ↔ ∀ (x : K), ∃ (n : ℕ), x < ↑n
source
theorem archimedean_iff_nat_le {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
Archimedean K ↔ ∀ (x : K), ∃ (n : ℕ), x ≤ ↑n
source
theorem archimedean_iff_int_lt {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
Archimedean K ↔ ∀ (x : K), ∃ (n : ℤ), x < ↑n
source
theorem archimedean_iff_int_le {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
Archimedean K ↔ ∀ (x : K), ∃ (n : ℤ), x ≤ ↑n
source
theorem archimedean_iff_rat_lt {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
Archimedean K ↔ ∀ (x : K), ∃ (q : ℚ), x < ↑q
source
theorem archimedean_iff_rat_le {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
Archimedean K ↔ ∀ (x : K), ∃ (q : ℚ), x ≤ ↑q
source
instance instArchimedeanRat :
Archimedean ℚ
source
theorem exists_rat_gt {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] (x : K) :
∃ (q : ℚ), x < ↑q
source
theorem exists_rat_lt {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] (x : K) :
∃ (q : ℚ), ↑q < x
source
theorem exists_div_btwn {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} {n : ℕ} (h : x < y) (nh : (y - x)⁻¹ < ↑n) :
∃ (z : ℤ), x < ↑z / ↑n ∧ ↑z / ↑n < y
source
theorem exists_rat_btwn {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} (h : x < y) :
∃ (q : ℚ), x < ↑q ∧ ↑q < y
source
theorem exists_rat_mem_uIoo {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} (h : x ≠ y) :
∃ (q : ℚ), ↑q ∈ Set.uIoo x y
source
theorem exists_pow_btwn {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {n : ℕ} (hn : n ≠ 0) {x y : K} (h : x < y) (hy : 0 < y) :
∃ (q : K), 0 < q ∧ x < q ^ n ∧ q ^ n < y
source
theorem exists_rat_pow_btwn {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {n : ℕ} (hn : n ≠ 0) {x y : K} (h : x < y) (hy : 0 < y) :
∃ (q : ℚ), 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

There is a rational power between any two positive elements of an archimedean ordered field.

source
theorem le_of_forall_rat_lt_imp_le {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} (h : ∀ (q : ℚ), ↑q < x → ↑q ≤ y) :
x ≤ y
source
theorem le_of_forall_lt_rat_imp_le {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} (h : ∀ (q : ℚ), y < ↑q → x ≤ ↑q) :
x ≤ y
source
theorem le_iff_forall_rat_lt_imp_le {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} :
x ≤ y ↔ ∀ (q : ℚ), ↑q < x → ↑q ≤ y
source
theorem le_iff_forall_lt_rat_imp_le {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} :
x ≤ y ↔ ∀ (q : ℚ), y < ↑q → x ≤ ↑q
source
theorem eq_of_forall_rat_lt_iff_lt {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} (h : ∀ (q : ℚ), ↑q < x ↔ ↑q < y) :
x = y
source
theorem eq_of_forall_lt_rat_iff_lt {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K} (h : ∀ (q : ℚ), x < ↑q ↔ y < ↑q) :
x = y
source
theorem exists_pos_rat_lt {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x : K} (x0 : 0 < x) :
∃ (q : ℚ), 0 < q ∧ ↑q < x
source
theorem exists_rat_near {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {ε : K} (x : K) (ε0 : 0 < ε) :
∃ (q : ℚ), |x - ↑q| < ε
source
instance instArchimedeanNat :
Archimedean ℕ
source
instance instArchimedeanInt :
Archimedean ℤ
source
instance Nonneg.instArchimedean {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [Archimedean M] :
Archimedean { x : M // 0 ≤ x }
source
instance Nonneg.instMulArchimedean {R : Type u_3} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] [ExistsAddOfLE R] :
MulArchimedean { x : R // 0 ≤ x }
source
instance instArchimedeanNNRat :
Archimedean ℚ≥0
source
instance instMulArchimedeanNNRat :
MulArchimedean ℚ≥0
source
noncomputable def Archimedean.floorRing (R : Type u_5) [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] :
FloorRing R

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 R = FloorRing.ofFloor R (fun (a : R) => Classical.choose ⋯) ⋯

Instances For

source
@[instance 100]
instance FloorRing.archimedean (K : Type u_5) [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] :
Archimedean K

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

source
instance Units.instMulArchimedean (M : Type u_5) [CommMonoid M] [PartialOrder M] [MulArchimedean M] :
MulArchimedean M ˣ
source
instance AddUnits.instAddArchimedean (M : Type u_5) [AddCommMonoid M] [PartialOrder M] [Archimedean M] :
Archimedean (AddUnits M)
source
instance WithBot.instArchimedean (M : Type u_5) [AddCommMonoid M] [PartialOrder M] [Archimedean M] :
Archimedean (WithBot M)
source
instance WithZero.instMulArchimedean (M : Type u_5) [CommMonoid M] [PartialOrder M] [MulArchimedean M] :
MulArchimedean (WithZero M)