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

The Cauchy completion forms a field.

Equations
@[protected, instance]

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.

@[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
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)⁻¹