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.

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
def cau_seq.completion.mk {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :

The map from Cauchy sequences into the Cauchy completion.

Equations
@[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) :
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} :
def cau_seq.completion.of_rat {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (x : β) :

The map from the original ring into the Cauchy completion.

Equations
@[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] :
Equations
@[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] :
Equations
@[protected, instance]
def cau_seq.completion.Cauchy.inhabited {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
Equations
theorem cau_seq.completion.of_rat_zero {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
theorem cau_seq.completion.of_rat_one {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] :
@[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} :
@[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] :
Equations
@[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) :
@[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] :
Equations
@[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) :
@[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] :
Equations
@[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) :
@[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] :
Equations
@[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) :
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 : β) :
theorem cau_seq.completion.of_rat_neg {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [comm_ring β] {abv : β → α} [is_absolute_value abv] (x : β) :
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 : β) :
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 : β) :
@[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] :
Equations
@[simp]
theorem cau_seq.completion.inv_zero {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] :
0⁻¹ = 0
@[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) :
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
theorem cau_seq.completion.zero_ne_one {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] :
0 1
@[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 0x⁻¹ * x = 1
noncomputable def cau_seq.completion.field {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] :

The Cauchy completion forms a field. See note [reducible non-instances].

Equations
theorem cau_seq.completion.of_rat_inv {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] (x : β) :
theorem cau_seq.completion.of_rat_div {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [field β] {abv : β → α} [is_absolute_value abv] (x y : β) :
@[class]
structure cau_seq.is_complete {α : Type u_1} [linear_ordered_field α] (β : Type u_2) [ring β] (abv : β → α) [is_absolute_value abv] :
Type

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

Instances
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
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
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) :
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
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
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
@[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
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
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
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
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
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) :
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)⁻¹
theorem cau_seq.lim_le {α : Type u_1} [linear_ordered_field α] [cau_seq.is_complete α abs] {f : cau_seq α abs} {x : α} (h : f cau_seq.const abs x) :
f.lim x
theorem cau_seq.le_lim {α : Type u_1} [linear_ordered_field α] [cau_seq.is_complete α abs] {f : cau_seq α abs} {x : α} (h : cau_seq.const abs x f) :
x f.lim
theorem cau_seq.lt_lim {α : Type u_1} [linear_ordered_field α] [cau_seq.is_complete α abs] {f : cau_seq α abs} {x : α} (h : cau_seq.const abs x < f) :
x < f.lim
theorem cau_seq.lim_lt {α : Type u_1} [linear_ordered_field α] [cau_seq.is_complete α abs] {f : cau_seq α abs} {x : α} (h : f < cau_seq.const abs x) :
f.lim < x