A collection of specific limit computations #
This file, by design, is independent of NormedSpace
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∞
.
Alias of tendsto_inverse_atTop_nhds_zero_nat
.
Alias of tendsto_const_div_atTop_nhds_zero_nat
.
Alias of tendsto_one_div_atTop_nhds_zero_nat
.
Alias of tendsto_one_div_add_atTop_nhds_zero_nat
.
Alias of NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat
.
The limit of n / (n + x)
is 1, for any constant x
(valid in ℝ
or any topological division
algebra over ℝ
, e.g., ℂ
).
TODO: introduce a typeclass saying that 1 / n
tends to 0 at top, making it possible to get this
statement simultaneously on ℚ
, ℝ
and ℂ
.
Powers #
Alias of tendsto_pow_atTop_nhds_zero_of_lt_one
.
Alias of tendsto_pow_atTop_nhds_zero_iff
.
Alias of uniformity_basis_dist_pow_of_lt_one
.
Geometric series #
Alias of summable_geometric_of_lt_one
.
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
, 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 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 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 countable types #
For any positive ε
, define on an encodable type a positive sequence with sum less than ε
Equations
- One or more equations did not get rendered due to their size.