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 #
IsCauSeq
: a predicate that saysf : ℕ → β
is Cauchy.CauSeq
: the type of Cauchy sequences valued in typeβ
with respect to an absolute value functionabv
.
Tags #
sequence, cauchy, abs val, absolute value
A sequence is Cauchy if the distance between its entries tends to zero.
Equations
Instances For
Alias of the forward direction of isCauSeq_neg
.
Alias of the reverse direction of isCauSeq_neg
.
CauSeq β abv
is the type of β
-valued Cauchy sequences, with respect to the absolute value
function abv
.
Equations
Instances For
Equations
Given a Cauchy sequence f
, create a Cauchy sequence from a sequence g
with
the same values as f
.
Equations
Instances For
Equations
The constant Cauchy sequence.
Equations
Instances For
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
LimZero f
holds when f
approaches 0.
Equations
Instances For
Equations
Given a Cauchy sequence f
with nonzero limit, create a Cauchy sequence with values equal to
the inverses of the values of f
.
Equations
Instances For
The entries of a positive Cauchy sequence eventually have a positive lower bound.
Equations
Instances For
Equations
Equations
Equations
Equations
Equations
Note that DistribLattice (CauSeq α abs)
is not true because there is no PartialOrder
.