# mathlib3documentation

data.real.cau_seq_completion

# Cauchy completion #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

def cau_seq.completion.Cauchy {α : Type u_1} {β : Type u_2} [ring β] (abv : β α) [is_absolute_value abv] :
Type u_2

The Cauchy completion of a ring with absolute value.

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

The map from Cauchy sequences into the Cauchy completion.

Equations
@[simp]
theorem cau_seq.completion.mk_eq_mk {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] (f : abv) :
theorem cau_seq.completion.mk_eq {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] {f g : abv} :
def cau_seq.completion.of_rat {α : Type u_1} {β : Type u_2} [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} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
@[protected, instance]
def cau_seq.completion.Cauchy.has_one {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
@[protected, instance]
def cau_seq.completion.Cauchy.inhabited {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
theorem cau_seq.completion.of_rat_zero {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] :
theorem cau_seq.completion.of_rat_one {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] :
@[simp]
theorem cau_seq.completion.mk_eq_zero {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] {f : abv} :
@[protected, instance]
def cau_seq.completion.Cauchy.has_add {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
@[simp]
theorem cau_seq.completion.mk_add {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] (f g : abv) :
@[protected, instance]
def cau_seq.completion.Cauchy.has_neg {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
@[simp]
theorem cau_seq.completion.mk_neg {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] (f : abv) :
@[protected, instance]
def cau_seq.completion.Cauchy.has_mul {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
@[simp]
theorem cau_seq.completion.mk_mul {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] (f g : abv) :
@[protected, instance]
def cau_seq.completion.Cauchy.has_sub {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
@[simp]
theorem cau_seq.completion.mk_sub {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] (f g : abv) :
@[protected, instance]
def cau_seq.completion.Cauchy.has_smul {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] {γ : Type u_3} [ β] [ β] :
Equations
@[simp]
theorem cau_seq.completion.mk_smul {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] {γ : Type u_3} [ β] [ β] (c : γ) (f : abv) :
@[protected, instance]
def cau_seq.completion.nat.has_pow {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
@[simp]
theorem cau_seq.completion.mk_pow {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] (n : ) (f : abv) :
@[protected, instance]
def cau_seq.completion.Cauchy.has_nat_cast {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
@[protected, instance]
def cau_seq.completion.Cauchy.has_int_cast {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
@[simp]
theorem cau_seq.completion.of_rat_nat_cast {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] (n : ) :
@[simp]
theorem cau_seq.completion.of_rat_int_cast {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] (z : ) :
theorem cau_seq.completion.of_rat_add {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] (x y : β) :
theorem cau_seq.completion.of_rat_neg {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] (x : β) :
theorem cau_seq.completion.of_rat_mul {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] (x y : β) :
@[protected, instance]
def cau_seq.completion.Cauchy.ring {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] :
Equations
• cau_seq.completion.Cauchy.ring = cau_seq.completion.Cauchy.ring._proof_3 cau_seq.completion.Cauchy.ring._proof_4 cau_seq.completion.Cauchy.ring._proof_5 cau_seq.completion.Cauchy.ring._proof_6 cau_seq.completion.Cauchy.ring._proof_7 cau_seq.completion.Cauchy.ring._proof_8 cau_seq.completion.Cauchy.ring._proof_9 cau_seq.completion.Cauchy.ring._proof_10 cau_seq.completion.Cauchy.ring._proof_11 cau_seq.completion.Cauchy.ring._proof_12 cau_seq.completion.Cauchy.ring._proof_13 cau_seq.completion.Cauchy.ring._proof_14
def cau_seq.completion.of_rat_ring_hom {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] :

cau_seq.completion.of_rat as a ring_hom

Equations
@[simp]
theorem cau_seq.completion.of_rat_ring_hom_apply {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] (x : β) :
theorem cau_seq.completion.of_rat_sub {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] (x y : β) :
@[protected, instance]
def cau_seq.completion.Cauchy.comm_ring {α : Type u_1} {β : Type u_2} [comm_ring β] {abv : β α} [is_absolute_value abv] :
Equations
• cau_seq.completion.Cauchy.comm_ring = cau_seq.completion.Cauchy.comm_ring._proof_3 cau_seq.completion.Cauchy.comm_ring._proof_4 cau_seq.completion.Cauchy.comm_ring._proof_5 cau_seq.completion.Cauchy.comm_ring._proof_6 cau_seq.completion.Cauchy.comm_ring._proof_7 cau_seq.completion.Cauchy.comm_ring._proof_8 cau_seq.completion.Cauchy.comm_ring._proof_9 cau_seq.completion.Cauchy.comm_ring._proof_10 cau_seq.completion.Cauchy.comm_ring._proof_11 cau_seq.completion.Cauchy.comm_ring._proof_12 cau_seq.completion.Cauchy.comm_ring._proof_13 cau_seq.completion.Cauchy.comm_ring._proof_14
@[protected, instance]
def cau_seq.completion.Cauchy.has_rat_cast {α : Type u_1} {β : Type u_2} {abv : β α} [is_absolute_value abv] :
Equations
@[simp]
theorem cau_seq.completion.of_rat_rat_cast {α : Type u_1} {β : Type u_2} {abv : β α} [is_absolute_value abv] (q : ) :
@[protected, instance]
noncomputable def cau_seq.completion.Cauchy.has_inv {α : Type u_1} {β : Type u_2} {abv : β α} [is_absolute_value abv] :
Equations
@[simp]
theorem cau_seq.completion.inv_zero {α : Type u_1} {β : Type u_2} {abv : β α} [is_absolute_value abv] :
0⁻¹ = 0
@[simp]
theorem cau_seq.completion.inv_mk {α : Type u_1} {β : Type u_2} {abv : β α} [is_absolute_value abv] {f : abv} (hf : ¬f.lim_zero) :
theorem cau_seq.completion.cau_seq_zero_ne_one {α : Type u_1} {β : Type u_2} {abv : β α} [is_absolute_value abv] :
¬0 1
theorem cau_seq.completion.zero_ne_one {α : Type u_1} {β : Type u_2} {abv : β α} [is_absolute_value abv] :
0 1
@[protected]
theorem cau_seq.completion.inv_mul_cancel {α : Type u_1} {β : Type u_2} {abv : β α} [is_absolute_value abv] {x : cau_seq.completion.Cauchy abv} :
x 0 x⁻¹ * x = 1
@[protected]
theorem cau_seq.completion.mul_inv_cancel {α : Type u_1} {β : Type u_2} {abv : β α} [is_absolute_value abv] {x : cau_seq.completion.Cauchy abv} :
x 0 x * x⁻¹ = 1
theorem cau_seq.completion.of_rat_inv {α : Type u_1} {β : Type u_2} {abv : β α} [is_absolute_value abv] (x : β) :
@[protected, instance]
noncomputable def cau_seq.completion.Cauchy.division_ring {α : Type u_1} {β : Type u_2} {abv : β α} [is_absolute_value abv] :

The Cauchy completion forms a division ring.

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

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.

@[protected, instance]
noncomputable def cau_seq.completion.Cauchy.field {α : Type u_1} {β : Type u_2} [field β] {abv : β α} [is_absolute_value abv] :

The Cauchy completion forms a field.

Equations
@[class]
structure cau_seq.is_complete {α : Type u_1} (β : Type u_2) [ring β] (abv : β α) [is_absolute_value abv] :
Prop
• is_complete : (s : abv), (b : β), s b

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} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] [ abv] (s : abv) :
(b : β), s b
noncomputable def cau_seq.lim {α : Type u_1} {β : Type u_2} [ring β] {abv : β α} [is_absolute_value abv] [ abv] (s : abv) :
β

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

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