mathlib documentation

algebra.order.archimedean

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 #

Main statements #

@[class]
structure archimedean (α : Type u_2) [ordered_add_comm_monoid α] :
Prop
  • arch : ∀ (x : α) {y : α}, 0 < y(∃ (n : ), x n y)

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.

Instances
@[protected, instance]
theorem exists_unique_zsmul_near_of_pos {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a : α} (ha : 0 < a) (g : α) :
∃! (k : ), k a g g < (k + 1) a

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

theorem exists_unique_zsmul_near_of_pos' {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a : α} (ha : 0 < a) (g : α) :
∃! (k : ), 0 g - k a g - k a < a
theorem exists_unique_add_zsmul_mem_Ico {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a : α} (ha : 0 < a) (b c : α) :
∃! (m : ), b + m a set.Ico c (c + a)
theorem exists_unique_add_zsmul_mem_Ioc {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a : α} (ha : 0 < a) (b c : α) :
∃! (m : ), b + m a set.Ioc c (c + a)
theorem exists_nat_gt {α : Type u_1} [ordered_semiring α] [nontrivial α] [archimedean α] (x : α) :
∃ (n : ), x < n
theorem exists_nat_ge {α : Type u_1} [ordered_semiring α] [archimedean α] (x : α) :
∃ (n : ), x n
theorem add_one_pow_unbounded_of_pos {α : Type u_1} [ordered_semiring α] [nontrivial α] [archimedean α] (x : α) {y : α} (hy : 0 < y) :
∃ (n : ), x < (y + 1) ^ n
theorem pow_unbounded_of_one_lt {α : Type u_1} [linear_ordered_ring α] [archimedean α] (x : α) {y : α} (hy1 : 1 < y) :
∃ (n : ), x < y ^ n
theorem exists_nat_pow_near {α : Type u_1} [linear_ordered_ring α] [archimedean α] {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_int_gt {α : Type u_1} [linear_ordered_ring α] [archimedean α] (x : α) :
∃ (n : ), x < n
theorem exists_int_lt {α : Type u_1} [linear_ordered_ring α] [archimedean α] (x : α) :
∃ (n : ), n < x
theorem exists_floor {α : Type u_1} [linear_ordered_ring α] [archimedean α] (x : α) :
∃ (fl : ), ∀ (z : ), z fl z x
theorem exists_mem_Ico_zpow {α : Type u_1} [linear_ordered_field α] [archimedean α] {x y : α} (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} [linear_ordered_field α] [archimedean α] {x y : α} (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} [linear_ordered_field α] [archimedean α] {x y : α} (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} [linear_ordered_field α] [archimedean α] {x y : α} (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 sub_floor_div_mul_nonneg {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : α) {y : α} (hy : 0 < y) :
0 x - (x / y) * y
theorem sub_floor_div_mul_lt {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : α) {y : α} (hy : 0 < y) :
x - (x / y) * y < y
@[protected, instance]
@[protected, instance]
noncomputable def archimedean.floor_ring (α : Type u_1) [linear_ordered_ring α] [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
theorem archimedean_iff_nat_lt {α : Type u_1} [linear_ordered_field α] :
archimedean α ∀ (x : α), ∃ (n : ), x < n
theorem archimedean_iff_nat_le {α : Type u_1} [linear_ordered_field α] :
archimedean α ∀ (x : α), ∃ (n : ), x n
theorem exists_rat_gt {α : Type u_1} [linear_ordered_field α] [archimedean α] (x : α) :
∃ (q : ), x < q
theorem archimedean_iff_rat_lt {α : Type u_1} [linear_ordered_field α] :
archimedean α ∀ (x : α), ∃ (q : ), x < q
theorem archimedean_iff_rat_le {α : Type u_1} [linear_ordered_field α] :
archimedean α ∀ (x : α), ∃ (q : ), x q
theorem exists_rat_lt {α : Type u_1} [linear_ordered_field α] [archimedean α] (x : α) :
∃ (q : ), q < x
theorem exists_rat_btwn {α : Type u_1} [linear_ordered_field α] [archimedean α] {x y : α} (h : x < y) :
∃ (q : ), x < q q < y
theorem exists_nat_one_div_lt {α : Type u_1} [linear_ordered_field α] [archimedean α] {ε : α} (hε : 0 < ε) :
∃ (n : ), 1 / (n + 1) < ε
theorem exists_pos_rat_lt {α : Type u_1} [linear_ordered_field α] [archimedean α] {x : α} (x0 : 0 < x) :
∃ (q : ), 0 < q q < x
def round {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : α) :

round rounds a number to the nearest integer. round (1 / 2) = 1

Equations
@[simp]
theorem round_zero {α : Type u_1} [linear_ordered_field α] [floor_ring α] :
round 0 = 0
@[simp]
theorem round_one {α : Type u_1} [linear_ordered_field α] [floor_ring α] :
round 1 = 1
theorem abs_sub_round {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : α) :
|x - (round x)| 1 / 2
@[simp, norm_cast]
theorem rat.floor_cast {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : ) :
@[simp, norm_cast]
theorem rat.ceil_cast {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : ) :
@[simp, norm_cast]
theorem rat.round_cast {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : ) :
@[simp, norm_cast]
theorem rat.cast_fract {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : ) :
theorem exists_rat_near {α : Type u_1} [linear_ordered_field α] [archimedean α] (x : α) {ε : α} (ε0 : 0 < ε) :
∃ (q : ), |x - q| < ε
@[protected, instance]