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 #
Archimedeanis a typeclass for an ordered additive commutative monoid to have the archimedean property.MulArchimedeanis a typeclass for an ordered commutative monoid to have the "mul-archimedean property" where forxandy > 1, there exists a natural numbernsuch thatx ≤ y ^ n.Archimedean.floorRingdefines a floor function on an archimedean linearly ordered ring making it into afloorRing.
Main statements #
ℕ,ℤ, andℚare archimedean.
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.
For any two elements
x,ysuch that0 < y, there exists a natural numbernsuch thatx ≤ n • y.
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.
For any two elements
x,ysuch that1 < y, there exists a natural numbernsuch thatx ≤ y ^ n.
instance
OrderDual.instMulArchimedean
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
[MulArchimedean α]
:
instance
OrderDual.instAddArchimedean
{α : Type u_1}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[Archimedean α]
:
instance
Additive.instArchimedean
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[MulArchimedean α]
:
Archimedean (Additive α)
instance
Multiplicative.instMulArchimedean
{α : Type u_1}
[AddCommGroup α]
[PartialOrder α]
[Archimedean α]
:
theorem
exists_lt_pow
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[MulArchimedean M]
[MulLeftStrictMono M]
{a : M}
(ha : 1 < a)
(b : M)
:
theorem
exists_lt_nsmul
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[Archimedean M]
[AddLeftStrictMono M]
{a : M}
(ha : 0 < a)
(b : M)
:
theorem
existsUnique_zpow_near_of_one_lt
{α : Type u_1}
[CommGroup α]
[LinearOrder α]
[IsOrderedMonoid α]
[MulArchimedean α]
{a : α}
(ha : 1 < a)
(g : α)
:
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}
[AddCommGroup α]
[LinearOrder α]
[IsOrderedAddMonoid α]
[Archimedean α]
{a : α}
(ha : 0 < a)
(g : α)
:
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}
[CommGroup α]
[LinearOrder α]
[IsOrderedMonoid α]
[MulArchimedean α]
{a : α}
(ha : 1 < a)
(g : α)
:
theorem
existsUnique_zsmul_near_of_pos'
{α : Type u_1}
[AddCommGroup α]
[LinearOrder α]
[IsOrderedAddMonoid α]
[Archimedean α]
{a : α}
(ha : 0 < a)
(g : α)
:
theorem
existsUnique_div_zpow_mem_Ico
{α : Type u_1}
[CommGroup α]
[LinearOrder α]
[IsOrderedMonoid α]
[MulArchimedean α]
{a : α}
(ha : 1 < a)
(b c : α)
:
theorem
existsUnique_sub_zsmul_mem_Ico
{α : Type u_1}
[AddCommGroup α]
[LinearOrder α]
[IsOrderedAddMonoid α]
[Archimedean α]
{a : α}
(ha : 0 < a)
(b c : α)
:
theorem
existsUnique_mul_zpow_mem_Ico
{α : Type u_1}
[CommGroup α]
[LinearOrder α]
[IsOrderedMonoid α]
[MulArchimedean α]
{a : α}
(ha : 1 < a)
(b c : α)
:
theorem
existsUnique_add_zsmul_mem_Ico
{α : Type u_1}
[AddCommGroup α]
[LinearOrder α]
[IsOrderedAddMonoid α]
[Archimedean α]
{a : α}
(ha : 0 < a)
(b c : α)
:
theorem
existsUnique_add_zpow_mem_Ioc
{α : Type u_1}
[CommGroup α]
[LinearOrder α]
[IsOrderedMonoid α]
[MulArchimedean α]
{a : α}
(ha : 1 < a)
(b c : α)
:
theorem
existsUnique_add_zsmul_mem_Ioc
{α : Type u_1}
[AddCommGroup α]
[LinearOrder α]
[IsOrderedAddMonoid α]
[Archimedean α]
{a : α}
(ha : 0 < a)
(b c : α)
:
theorem
existsUnique_sub_zpow_mem_Ioc
{α : Type u_1}
[CommGroup α]
[LinearOrder α]
[IsOrderedMonoid α]
[MulArchimedean α]
{a : α}
(ha : 1 < a)
(b c : α)
:
theorem
existsUnique_sub_zsmul_mem_Ioc
{α : Type u_1}
[AddCommGroup α]
[LinearOrder α]
[IsOrderedAddMonoid α]
[Archimedean α]
{a : α}
(ha : 0 < a)
(b c : α)
:
theorem
exists_nat_ge
{α : Type u_1}
[Semiring α]
[PartialOrder α]
[IsOrderedRing α]
[Archimedean α]
(x : α)
:
@[instance 100]
instance
instIsDirectedLeOfIsOrderedRingOfArchimedean
{α : Type u_1}
[Semiring α]
[PartialOrder α]
[IsOrderedRing α]
[Archimedean α]
:
IsDirected α fun (x1 x2 : α) => x1 ≤ x2
theorem
exists_nat_gt
{α : Type u_1}
[Semiring α]
[PartialOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
(x : α)
:
theorem
add_one_pow_unbounded_of_pos
{α : Type u_1}
[Semiring α]
[PartialOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{y : α}
(x : α)
(hy : 0 < y)
:
theorem
pow_unbounded_of_one_lt
{α : Type u_1}
[Semiring α]
[PartialOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{y : α}
[ExistsAddOfLE α]
(x : α)
(hy1 : 1 < y)
:
theorem
exists_int_ge
{R : Type u_3}
[Ring R]
[PartialOrder R]
[IsOrderedRing R]
[Archimedean R]
(x : R)
:
theorem
exists_int_le
{R : Type u_3}
[Ring R]
[PartialOrder R]
[IsOrderedRing R]
[Archimedean R]
(x : R)
:
@[instance 100]
instance
instIsDirectedGe
{R : Type u_3}
[Ring R]
[PartialOrder R]
[IsOrderedRing R]
[Archimedean R]
:
IsDirected R fun (x1 x2 : R) => x1 ≥ x2
theorem
exists_int_gt
{α : Type u_1}
[Ring α]
[PartialOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
(x : α)
:
theorem
exists_int_lt
{α : Type u_1}
[Ring α]
[PartialOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
(x : α)
:
theorem
exists_floor
{α : Type u_1}
[Ring α]
[PartialOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
(x : α)
:
theorem
exists_nat_pow_near
{α : Type u_1}
[Semiring α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
[ExistsAddOfLE α]
{x y : α}
(hx : 1 ≤ x)
(hy : 1 < y)
:
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}
[Semifield α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{ε : α}
(hε : 0 < ε)
:
theorem
exists_mem_Ico_zpow
{α : Type u_1}
[Semifield α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{x y : α}
[ExistsAddOfLE α]
(hx : 0 < x)
(hy : 1 < y)
:
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}
[Semifield α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{x y : α}
[ExistsAddOfLE α]
(hx : 0 < x)
(hy : 1 < y)
:
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}
[Semifield α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{x y : α}
[ExistsAddOfLE α]
(hx : 0 < x)
(hy : y < 1)
:
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}
[Semifield α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{x y : α}
[ExistsAddOfLE α]
(xpos : 0 < x)
(hx : x ≤ 1)
(ypos : 0 < y)
(hy : y < 1)
:
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_pow_btwn_of_lt_mul
{α : Type u_1}
[Semifield α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
[ExistsAddOfLE α]
{a b c : α}
(h : a < b * c)
(hb₀ : 0 < b)
(hb₁ : b ≤ 1)
(hc₀ : 0 < c)
(hc₁ : c < 1)
:
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.
theorem
exists_zpow_btwn_of_lt_mul
{α : Type u_1}
[Semifield α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
[ExistsAddOfLE α]
{a b c : α}
(h : a < b * c)
(hb₀ : 0 < b)
(hc₀ : 0 < c)
(hc₁ : c < 1)
:
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.
theorem
exists_rat_gt
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
(x : α)
:
theorem
exists_rat_lt
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
(x : α)
:
theorem
exists_rat_btwn
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{x y : α}
(h : x < y)
:
theorem
exists_pow_btwn
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{n : ℕ}
(hn : n ≠ 0)
{x y : α}
(h : x < y)
(hy : 0 < y)
:
@[deprecated exists_pow_btwn (since := "2024-12-26")]
theorem
exists_rat_pow_btwn_rat
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{n : ℕ}
(hn : n ≠ 0)
{x y : α}
(h : x < y)
(hy : 0 < y)
:
Alias of exists_pow_btwn.
theorem
exists_rat_pow_btwn
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{n : ℕ}
(hn : n ≠ 0)
{x y : α}
(h : x < y)
(hy : 0 < y)
:
There is a rational power between any two positive elements of an archimedean ordered field.
theorem
le_of_forall_rat_lt_imp_le
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{x y : α}
(h : ∀ (q : ℚ), ↑q < x → ↑q ≤ y)
:
theorem
le_of_forall_lt_rat_imp_le
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{x y : α}
(h : ∀ (q : ℚ), y < ↑q → x ≤ ↑q)
:
theorem
le_iff_forall_rat_lt_imp_le
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{x y : α}
:
theorem
le_iff_forall_lt_rat_imp_le
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{x y : α}
:
theorem
eq_of_forall_rat_lt_iff_lt
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{x y : α}
(h : ∀ (q : ℚ), ↑q < x ↔ ↑q < y)
:
theorem
eq_of_forall_lt_rat_iff_lt
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{x y : α}
(h : ∀ (q : ℚ), x < ↑q ↔ y < ↑q)
:
theorem
exists_pos_rat_lt
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{x : α}
(x0 : 0 < x)
:
theorem
exists_rat_near
{α : Type u_1}
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
{ε : α}
(x : α)
(ε0 : 0 < ε)
:
instance
Nonneg.instArchimedean
{α : Type u_1}
[AddCommMonoid α]
[PartialOrder α]
[IsOrderedAddMonoid α]
[Archimedean α]
:
instance
Nonneg.instMulArchimedean
{α : Type u_1}
[CommSemiring α]
[PartialOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
[ExistsAddOfLE α]
:
noncomputable def
Archimedean.floorRing
(α : Type u_3)
[Ring α]
[LinearOrder α]
[IsStrictOrderedRing α]
[Archimedean α]
:
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)
[Field α]
[LinearOrder α]
[IsStrictOrderedRing α]
[FloorRing α]
:
A linear ordered field that is a floor ring is archimedean.
instance
Units.instMulArchimedean
(α : Type u_3)
[CommMonoid α]
[PartialOrder α]
[MulArchimedean α]
:
instance
AddUnits.instAddArchimedean
(α : Type u_3)
[AddCommMonoid α]
[PartialOrder α]
[Archimedean α]
:
Archimedean (AddUnits α)
instance
WithBot.instArchimedean
(α : Type u_3)
[AddCommMonoid α]
[PartialOrder α]
[Archimedean α]
:
Archimedean (WithBot α)
instance
WithZero.instMulArchimedean
(α : Type u_3)
[CommMonoid α]
[PartialOrder α]
[MulArchimedean α]
: