mathlib documentation

data.real.cau_seq_completion

Cauchy completion #

This file generalizes the Cauchy completion of (ℚ, abs) to the completion of a commutative ring with absolute value.

source
def cau_seq.completion.Cauchy {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
Type u_2

The Cauchy completion of a commutative ring with absolute value.

Equations
Instances for cau_seq.completion.Cauchy
source
def cau_seq.completion.mk {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
cau_seq β abv → cau_seq.completion.Cauchy

The map from Cauchy sequences into the Cauchy completion.

Equations
source
@[simp]
theorem cau_seq.completion.mk_eq_mk {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (f : cau_seq β abv) :
⟦f⟧ = cau_seq.completion.mk f
source
theorem cau_seq.completion.mk_eq {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] {f g : cau_seq β abv} :
cau_seq.completion.mk f = cau_seq.completion.mk g ↔ f ≈ g
source
def cau_seq.completion.of_rat {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (x : β) :
cau_seq.completion.Cauchy

The map from the original ring into the Cauchy completion.

Equations
source
@[protected, instance]
def cau_seq.completion.Cauchy.has_zero {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
has_zero cau_seq.completion.Cauchy
Equations
source
@[protected, instance]
def cau_seq.completion.Cauchy.has_one {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
has_one cau_seq.completion.Cauchy
Equations
source
@[protected, instance]
def cau_seq.completion.Cauchy.inhabited {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
inhabited cau_seq.completion.Cauchy
Equations
source
theorem cau_seq.completion.of_rat_zero {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
cau_seq.completion.of_rat 0 = 0
source
theorem cau_seq.completion.of_rat_one {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
cau_seq.completion.of_rat 1 = 1
source
@[simp]
theorem cau_seq.completion.mk_eq_zero {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] {f : cau_seq β abv} :
cau_seq.completion.mk f = 0 ↔ f.lim_zero
source
@[protected, instance]
def cau_seq.completion.Cauchy.has_add {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
has_add cau_seq.completion.Cauchy
Equations
source
@[simp]
theorem cau_seq.completion.mk_add {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (f g : cau_seq β abv) :
cau_seq.completion.mk f + cau_seq.completion.mk g = cau_seq.completion.mk (f + g)
source
@[protected, instance]
def cau_seq.completion.Cauchy.has_neg {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
has_neg cau_seq.completion.Cauchy
Equations
source
@[simp]
theorem cau_seq.completion.mk_neg {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (f : cau_seq β abv) :
-cau_seq.completion.mk f = cau_seq.completion.mk (-f)
source
@[protected, instance]
def cau_seq.completion.Cauchy.has_mul {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
has_mul cau_seq.completion.Cauchy
Equations
source
@[simp]
theorem cau_seq.completion.mk_mul {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (f g : cau_seq β abv) :
cau_seq.completion.mk f * cau_seq.completion.mk g = cau_seq.completion.mk (f * g)
source
@[protected, instance]
def cau_seq.completion.Cauchy.has_sub {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
has_sub cau_seq.completion.Cauchy
Equations
source
@[simp]
theorem cau_seq.completion.mk_sub {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (f g : cau_seq β abv) :
cau_seq.completion.mk f - cau_seq.completion.mk g = cau_seq.completion.mk (f - g)
source
theorem cau_seq.completion.of_rat_add {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (x y : β) :
cau_seq.completion.of_rat (x + y) = cau_seq.completion.of_rat x + cau_seq.completion.of_rat y
source
theorem cau_seq.completion.of_rat_neg {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (x : β) :
cau_seq.completion.of_rat (-x) = -cau_seq.completion.of_rat x
source
theorem cau_seq.completion.of_rat_mul {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (x y : β) :
cau_seq.completion.of_rat (x * y) = cau_seq.completion.of_rat x * cau_seq.completion.of_rat y
source
@[protected, instance]
def cau_seq.completion.Cauchy.add_group {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
add_group cau_seq.completion.Cauchy
Equations
source
@[protected, instance]
def cau_seq.completion.Cauchy.add_group_with_one {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
add_group_with_one cau_seq.completion.Cauchy
Equations
source
@[simp]
theorem cau_seq.completion.of_rat_nat_cast {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (n : ℕ) :
cau_seq.completion.of_rat ↑n = ↑n
source
@[simp]
theorem cau_seq.completion.of_rat_int_cast {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (z : ℤ) :
cau_seq.completion.of_rat ↑z = ↑z
source
@[protected, instance]
def cau_seq.completion.Cauchy.comm_ring {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
comm_ring cau_seq.completion.Cauchy
Equations
source
@[protected, instance]
def cau_seq.completion.Cauchy.ring {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
ring cau_seq.completion.Cauchy
Equations
source
def cau_seq.completion.of_rat_ring_hom {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
β →+* cau_seq.completion.Cauchy

cau_seq.completion.of_rat as a ring_hom

Equations
source
@[simp]
theorem cau_seq.completion.of_rat_ring_hom_apply {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (x : β) :
⇑cau_seq.completion.of_rat_ring_hom x = cau_seq.completion.of_rat x
source
theorem cau_seq.completion.of_rat_sub {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (x y : β) :
cau_seq.completion.of_rat (x - y) = cau_seq.completion.of_rat x - cau_seq.completion.of_rat y
source
@[protected, instance]
def cau_seq.completion.Cauchy.has_rat_cast {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] :
has_rat_cast cau_seq.completion.Cauchy
Equations
source
@[simp]
theorem cau_seq.completion.of_rat_rat_cast {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] (q : ℚ) :
cau_seq.completion.of_rat ↑q = ↑q
source
@[protected, instance]
noncomputable def cau_seq.completion.Cauchy.has_inv {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] :
has_inv cau_seq.completion.Cauchy
Equations
source
@[simp]
theorem cau_seq.completion.inv_zero {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] :
0⁻¹ = 0
source
@[simp]
theorem cau_seq.completion.inv_mk {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] {f : cau_seq β abv} (hf : ¬f.lim_zero) :
(cau_seq.completion.mk f)⁻¹ = cau_seq.completion.mk (f.inv hf)
source
theorem cau_seq.completion.cau_seq_zero_ne_one {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] :
¬0 ≈ 1
source
theorem cau_seq.completion.zero_ne_one {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] :
0 ≠ 1
source
@[protected]
theorem cau_seq.completion.inv_mul_cancel {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] {x : cau_seq.completion.Cauchy} :
x ≠ 0 → x⁻¹ * x = 1
source
theorem cau_seq.completion.of_rat_inv {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] (x : β) :
cau_seq.completion.of_rat x⁻¹ = (cau_seq.completion.of_rat x)⁻¹
source
@[protected, instance]
noncomputable def cau_seq.completion.Cauchy.field {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] :
field cau_seq.completion.Cauchy

The Cauchy completion forms a field.

Equations
source
theorem cau_seq.completion.of_rat_div {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] (x y : β) :
cau_seq.completion.of_rat (x / y) = cau_seq.completion.of_rat x / cau_seq.completion.of_rat y
source
@[protected, instance]
meta def cau_seq.completion.Cauchy.has_repr {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] [has_repr β] :
has_repr cau_seq.completion.Cauchy

Show the first 10 items of a representative of this equivalence class of cauchy sequences.

The representative chosen is the one passed in the VM to quot.mk, so two cauchy sequences converging to the same number may be printed differently.

source
@[class]
structure cau_seq.is_complete {α : Type u_1} [linear_ordered_field α] (β : Type u_2) [ring β] (abv : β → α) [is_absolute_value abv] :
Prop

A class stating that a ring with an absolute value is complete, i.e. every Cauchy sequence has a limit.

Instances of this typeclass
source
theorem cau_seq.complete {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [ring β] {abv : β → α} [is_absolute_value abv] [cau_seq.is_complete β abv] (s : cau_seq β abv) :
∃ (b : β), s ≈ cau_seq.const abv b
source
noncomputable def cau_seq.lim {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [ring β] {abv : β → α} [is_absolute_value abv] [cau_seq.is_complete β abv] (s : cau_seq β abv) :
β

The limit of a Cauchy sequence in a complete ring. Chosen non-computably.

Equations
source
theorem cau_seq.equiv_lim {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [ring β] {abv : β → α} [is_absolute_value abv] [cau_seq.is_complete β abv] (s : cau_seq β abv) :
s ≈ cau_seq.const abv s.lim
source
theorem cau_seq.eq_lim_of_const_equiv {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [ring β] {abv : β → α} [is_absolute_value abv] [cau_seq.is_complete β abv] {f : cau_seq β abv} {x : β} (h : cau_seq.const abv x ≈ f) :
x = f.lim
source
theorem cau_seq.lim_eq_of_equiv_const {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [ring β] {abv : β → α} [is_absolute_value abv] [cau_seq.is_complete β abv] {f : cau_seq β abv} {x : β} (h : f ≈ cau_seq.const abv x) :
f.lim = x
source
theorem cau_seq.lim_eq_lim_of_equiv {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [ring β] {abv : β → α} [is_absolute_value abv] [cau_seq.is_complete β abv] {f g : cau_seq β abv} (h : f ≈ g) :
f.lim = g.lim
source
@[simp]
theorem cau_seq.lim_const {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [ring β] {abv : β → α} [is_absolute_value abv] [cau_seq.is_complete β abv] (x : β) :
(cau_seq.const abv x).lim = x
source
theorem cau_seq.lim_add {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [ring β] {abv : β → α} [is_absolute_value abv] [cau_seq.is_complete β abv] (f g : cau_seq β abv) :
f.lim + g.lim = (f + g).lim
source
theorem cau_seq.lim_mul_lim {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [ring β] {abv : β → α} [is_absolute_value abv] [cau_seq.is_complete β abv] (f g : cau_seq β abv) :
f.lim * g.lim = (f * g).lim
source
theorem cau_seq.lim_mul {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [ring β] {abv : β → α} [is_absolute_value abv] [cau_seq.is_complete β abv] (f : cau_seq β abv) (x : β) :
f.lim * x = (f * cau_seq.const abv x).lim
source
theorem cau_seq.lim_neg {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [ring β] {abv : β → α} [is_absolute_value abv] [cau_seq.is_complete β abv] (f : cau_seq β abv) :
(-f).lim = -f.lim
source
theorem cau_seq.lim_eq_zero_iff {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [ring β] {abv : β → α} [is_absolute_value abv] [cau_seq.is_complete β abv] (f : cau_seq β abv) :
f.lim = 0 ↔ f.lim_zero
source
theorem cau_seq.lim_inv {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] [cau_seq.is_complete β abv] {f : cau_seq β abv} (hf : ¬f.lim_zero) :
(f.inv hf).lim = (f.lim)⁻¹
source
theorem cau_seq.lim_le {α : Type u_1} [linear_ordered_field α] [cau_seq.is_complete α has_abs.abs] {f : cau_seq α has_abs.abs} {x : α} (h : f ≤ cau_seq.const has_abs.abs x) :
f.lim ≤ x
source
theorem cau_seq.le_lim {α : Type u_1} [linear_ordered_field α] [cau_seq.is_complete α has_abs.abs] {f : cau_seq α has_abs.abs} {x : α} (h : cau_seq.const has_abs.abs x ≤ f) :
x ≤ f.lim
source
theorem cau_seq.lt_lim {α : Type u_1} [linear_ordered_field α] [cau_seq.is_complete α has_abs.abs] {f : cau_seq α has_abs.abs} {x : α} (h : cau_seq.const has_abs.abs x < f) :
x < f.lim
source
theorem cau_seq.lim_lt {α : Type u_1} [linear_ordered_field α] [cau_seq.is_complete α has_abs.abs] {f : cau_seq α has_abs.abs} {x : α} (h : f < cau_seq.const has_abs.abs x) :
f.lim < x