A collection of specific limit computations #
This file, by design, is independent of normed_space
in the import hierarchy. It contains
important specific limit computations in metric spaces, in ordered rings/fields, and in specific
instances of these such as ℝ
, ℝ≥0
and ℝ≥0∞
.
Powers #
Geometric series #
Sequences with geometrically decaying distance in metric spaces #
In this paragraph, we discuss sequences in metric spaces or emetric spaces for which the distance between two consecutive terms decays geometrically. We show that such sequences are Cauchy sequences, and bound their distances to the limit. We also discuss series with geometrically decaying terms.
If edist (f n) (f (n+1))
is bounded by C * r^n
, C ≠ ∞
, r < 1
,
then f
is a Cauchy sequence.
If edist (f n) (f (n+1))
is bounded by C * r^n
, then the distance from
f n
to the limit of f
is bounded above by C * r^n / (1 - r)
.
If edist (f n) (f (n+1))
is bounded by C * r^n
, then the distance from
f 0
to the limit of f
is bounded above by C / (1 - r)
.
If edist (f n) (f (n+1))
is bounded by C * 2^-n
, then f
is a Cauchy sequence.
If edist (f n) (f (n+1))
is bounded by C * 2^-n
, then the distance from
f n
to the limit of f
is bounded above by 2 * C * 2^-n
.
If edist (f n) (f (n+1))
is bounded by C * 2^-n
, then the distance from
f 0
to the limit of f
is bounded above by 2 * C
.
If dist (f n) (f (n+1))
is bounded by C * r^n
, r < 1
, then f
is a Cauchy sequence.
Note that this lemma does not assume 0 ≤ C
or 0 ≤ r
.
If dist (f n) (f (n+1))
is bounded by C * r^n
, r < 1
, then the distance from
f n
to the limit of f
is bounded above by C * r^n / (1 - r)
.
If dist (f n) (f (n+1))
is bounded by C * r^n
, r < 1
, then the distance from
f 0
to the limit of f
is bounded above by C / (1 - r)
.
If dist (f n) (f (n+1))
is bounded by (C / 2) / 2^n
, then f
is a Cauchy sequence.
If dist (f n) (f (n+1))
is bounded by (C / 2) / 2^n
, then the distance from
f 0
to the limit of f
is bounded above by C
.
If dist (f n) (f (n+1))
is bounded by (C / 2) / 2^n
, then the distance from
f n
to the limit of f
is bounded above by C / 2^n
.
Summability tests based on comparison with geometric series #
Positive sequences with small sums on encodable types #
For any positive ε
, define on an encodable type a positive sequence with sum less than ε