Cauchy sequences #
A basic theory of Cauchy sequences, used in the construction of the reals and p-adic numbers. Where applicable, lemmas that will be reused in other contexts have been stated in extra generality.
There are other "versions" of Cauchyness in the library, in particular Cauchy filters in topology. This is a concrete implementation that is useful for simplicity and computability reasons.
Important definitions #
is_cau_seq: a predicate that saysf : ℕ → βis Cauchy.cau_seq: the type of Cauchy sequences valued in typeβwith respect to an absolute value functionabv.
Tags #
sequence, cauchy, abs val, absolute value
theorem
rat_add_continuous_lemma
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
(abv : β → α)
[is_absolute_value abv]
{ε : α}
(ε0 : 0 < ε) :
theorem
rat_mul_continuous_lemma
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
(abv : β → α)
[is_absolute_value abv]
{ε K₁ K₂ : α}
(ε0 : 0 < ε) :
def
is_cau_seq
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
(abv : β → α)
(f : ℕ → β) :
Prop
A sequence is Cauchy if the distance between its entries tends to zero.
@[nolint]
theorem
is_cau_seq.cauchy₂
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f : ℕ → β}
(hf : is_cau_seq abv f)
{ε : α}
(ε0 : 0 < ε) :
theorem
is_cau_seq.cauchy₃
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f : ℕ → β}
(hf : is_cau_seq abv f)
{ε : α}
(ε0 : 0 < ε) :
def
cau_seq
{α : Type u_1}
[linear_ordered_field α]
(β : Type u_2)
[ring β]
(abv : β → α) :
Type u_2
cau_seq β abv is the type of β-valued Cauchy sequences, with respect to the absolute value
function abv.
Equations
- cau_seq β abv = {f // is_cau_seq abv f}
@[protected, instance]
def
cau_seq.has_coe_to_fun
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α} :
has_coe_to_fun (cau_seq β abv) (λ (_x : cau_seq β abv), ℕ → β)
Equations
- cau_seq.has_coe_to_fun = {coe := subtype.val (λ (f : ℕ → β), is_cau_seq abv f)}
@[simp]
theorem
cau_seq.mk_to_fun
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
(f : ℕ → β)
(hf : is_cau_seq abv f) :
theorem
cau_seq.ext
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
{f g : cau_seq β abv}
(h : ∀ (i : ℕ), ⇑f i = ⇑g i) :
f = g
theorem
cau_seq.is_cau
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
(f : cau_seq β abv) :
is_cau_seq abv ⇑f
def
cau_seq.of_eq
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
(f : cau_seq β abv)
(g : ℕ → β)
(e : ∀ (i : ℕ), ⇑f i = g i) :
cau_seq β abv
Given a Cauchy sequence f, create a Cauchy sequence from a sequence g with
the same values as f.
@[nolint]
theorem
cau_seq.cauchy₂
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv)
{ε : α} :
theorem
cau_seq.bounded
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv) :
theorem
cau_seq.bounded'
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv)
(x : α) :
@[protected, instance]
def
cau_seq.has_add
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
@[simp]
theorem
cau_seq.add_apply
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f g : cau_seq β abv)
(i : ℕ) :
def
cau_seq.const
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
(abv : β → α)
[is_absolute_value abv]
(x : β) :
cau_seq β abv
The constant Cauchy sequence.
Equations
- cau_seq.const abv x = ⟨λ (i : ℕ), x, _⟩
@[simp]
theorem
cau_seq.const_apply
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x : β)
(i : ℕ) :
⇑(cau_seq.const abv x) i = x
theorem
cau_seq.const_inj
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{x y : β} :
cau_seq.const abv x = cau_seq.const abv y ↔ x = y
@[protected, instance]
def
cau_seq.has_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.has_zero = {zero := cau_seq.const abv 0}
@[protected, instance]
def
cau_seq.has_one
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.has_one = {one := cau_seq.const abv 1}
@[protected, instance]
def
cau_seq.inhabited
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.inhabited = {default := 0}
@[simp]
theorem
cau_seq.zero_apply
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(i : ℕ) :
@[simp]
theorem
cau_seq.one_apply
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(i : ℕ) :
@[simp]
theorem
cau_seq.const_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
cau_seq.const abv 0 = 0
theorem
cau_seq.const_add
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
cau_seq.const abv (x + y) = cau_seq.const abv x + cau_seq.const abv y
@[protected, instance]
def
cau_seq.has_mul
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
@[simp]
theorem
cau_seq.mul_apply
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f g : cau_seq β abv)
(i : ℕ) :
theorem
cau_seq.const_mul
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
cau_seq.const abv (x * y) = (cau_seq.const abv x) * cau_seq.const abv y
@[protected, instance]
def
cau_seq.has_neg
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
@[simp]
theorem
cau_seq.neg_apply
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv)
(i : ℕ) :
theorem
cau_seq.const_neg
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x : β) :
cau_seq.const abv (-x) = -cau_seq.const abv x
@[protected, instance]
def
cau_seq.has_sub
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
@[simp]
theorem
cau_seq.sub_apply
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f g : cau_seq β abv)
(i : ℕ) :
theorem
cau_seq.const_sub
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(x y : β) :
cau_seq.const abv (x - y) = cau_seq.const abv x - cau_seq.const abv y
@[protected, instance]
def
cau_seq.ring
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.ring = {add := has_add.add cau_seq.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := nsmul_rec {add := has_add.add cau_seq.has_add}, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg cau_seq.has_neg, sub := has_sub.sub cau_seq.has_sub, sub_eq_add_neg := _, zsmul := zsmul_rec {neg := has_neg.neg cau_seq.has_neg}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul cau_seq.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec {mul := has_mul.mul cau_seq.has_mul}, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
@[protected, instance]
def
cau_seq.comm_ring
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv] :
Equations
- cau_seq.comm_ring = {add := ring.add cau_seq.ring, add_assoc := _, zero := ring.zero cau_seq.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul cau_seq.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg cau_seq.ring, sub := ring.sub cau_seq.ring, sub_eq_add_neg := _, zsmul := ring.zsmul cau_seq.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ring.mul cau_seq.ring, mul_assoc := _, one := ring.one cau_seq.ring, one_mul := _, mul_one := _, npow := ring.npow cau_seq.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
theorem
cau_seq.add_lim_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f g : cau_seq β abv}
(hf : f.lim_zero)
(hg : g.lim_zero) :
theorem
cau_seq.mul_lim_zero_right
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f : cau_seq β abv)
{g : cau_seq β abv}
(hg : g.lim_zero) :
theorem
cau_seq.mul_lim_zero_left
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv}
(g : cau_seq β abv)
(hg : f.lim_zero) :
theorem
cau_seq.neg_lim_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv}
(hf : f.lim_zero) :
theorem
cau_seq.sub_lim_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f g : cau_seq β abv}
(hf : f.lim_zero)
(hg : g.lim_zero) :
theorem
cau_seq.lim_zero_sub_rev
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f g : cau_seq β abv}
(hfg : (f - g).lim_zero) :
theorem
cau_seq.zero_lim_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
0.lim_zero
theorem
cau_seq.const_lim_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{x : β} :
(cau_seq.const abv x).lim_zero ↔ x = 0
@[protected, instance]
def
cau_seq.equiv
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv] :
theorem
cau_seq.add_equiv_add
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f1 f2 g1 g2 : cau_seq β abv}
(hf : f1 ≈ f2)
(hg : g1 ≈ g2) :
theorem
cau_seq.neg_equiv_neg
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f g : cau_seq β abv}
(hf : f ≈ g) :
theorem
cau_seq.lim_zero_congr
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f g : cau_seq β abv}
(h : f ≈ g) :
theorem
cau_seq.abv_pos_of_not_lim_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv}
(hf : ¬f.lim_zero) :
theorem
cau_seq.of_near
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(f : ℕ → β)
(g : cau_seq β abv)
(h : ∀ (ε : α), ε > 0 → (∃ (i : ℕ), ∀ (j : ℕ), j ≥ i → abv (f j - ⇑g j) < ε)) :
is_cau_seq abv f
theorem
cau_seq.not_lim_zero_of_not_congr_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv}
(hf : ¬f ≈ 0) :
theorem
cau_seq.mul_equiv_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
(g : cau_seq β abv)
{f : cau_seq β abv}
(hf : f ≈ 0) :
theorem
cau_seq.mul_not_equiv_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{f g : cau_seq β abv}
(hf : ¬f ≈ 0)
(hg : ¬g ≈ 0) :
theorem
cau_seq.const_equiv
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
{abv : β → α}
[is_absolute_value abv]
{x y : β} :
cau_seq.const abv x ≈ cau_seq.const abv y ↔ x = y
theorem
cau_seq.mul_equiv_zero'
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[comm_ring β]
{abv : β → α}
[is_absolute_value abv]
(g : cau_seq β abv)
{f : cau_seq β abv}
(hf : f ≈ 0) :
theorem
cau_seq.one_not_equiv_zero
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[ring β]
[is_domain β]
(abv : β → α)
[is_absolute_value abv] :
¬cau_seq.const abv 1 ≈ cau_seq.const abv 0
def
cau_seq.inv
{α : 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 β abv
Given a Cauchy sequence f with nonzero limit, create a Cauchy sequence with values equal to
the inverses of the values of f.
@[simp]
theorem
cau_seq.inv_apply
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv]
{f : cau_seq β abv}
(hf : ¬f.lim_zero)
(i : ℕ) :
theorem
cau_seq.inv_mul_cancel
{α : 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.const_inv
{α : Type u_1}
[linear_ordered_field α]
{β : Type u_2}
[field β]
{abv : β → α}
[is_absolute_value abv]
{x : β}
(hx : x ≠ 0) :
cau_seq.const abv x⁻¹ = (cau_seq.const abv x).inv _
theorem
cau_seq.const_pos
{α : Type u_1}
[linear_ordered_field α]
{x : α} :
(cau_seq.const abs x).pos ↔ 0 < x
@[protected]
@[protected, instance]
@[protected, instance]
theorem
cau_seq.lt_of_lt_of_eq
{α : Type u_1}
[linear_ordered_field α]
{f g h : cau_seq α abs}
(fg : f < g)
(gh : g ≈ h) :
f < h
theorem
cau_seq.lt_of_eq_of_lt
{α : Type u_1}
[linear_ordered_field α]
{f g h : cau_seq α abs}
(fg : f ≈ g)
(gh : g < h) :
f < h
theorem
cau_seq.lt_trans
{α : Type u_1}
[linear_ordered_field α]
{f g h : cau_seq α abs}
(fg : f < g)
(gh : g < h) :
f < h
theorem
cau_seq.le_of_eq_of_le
{α : Type u_1}
[linear_ordered_field α]
{f g h : cau_seq α abs}
(hfg : f ≈ g)
(hgh : g ≤ h) :
f ≤ h
theorem
cau_seq.le_of_le_of_eq
{α : Type u_1}
[linear_ordered_field α]
{f g h : cau_seq α abs}
(hfg : f ≤ g)
(hgh : g ≈ h) :
f ≤ h
@[protected, instance]
Equations
- cau_seq.preorder = {le := λ (f g : cau_seq α abs), f < g ∨ f ≈ g, lt := has_lt.lt cau_seq.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
theorem
cau_seq.le_antisymm
{α : Type u_1}
[linear_ordered_field α]
{f g : cau_seq α abs}
(fg : f ≤ g)
(gf : g ≤ f) :
f ≈ g
theorem
cau_seq.const_lt
{α : Type u_1}
[linear_ordered_field α]
{x y : α} :
cau_seq.const abs x < cau_seq.const abs y ↔ x < y
theorem
cau_seq.const_le
{α : Type u_1}
[linear_ordered_field α]
{x y : α} :
cau_seq.const abs x ≤ cau_seq.const abs y ↔ x ≤ y
theorem
cau_seq.exists_gt
{α : Type u_1}
[linear_ordered_field α]
(f : cau_seq α abs) :
∃ (a : α), f < cau_seq.const abs a
theorem
cau_seq.exists_lt
{α : Type u_1}
[linear_ordered_field α]
(f : cau_seq α abs) :
∃ (a : α), cau_seq.const abs a < f