If a function tends to infinity along a filter, then this function multiplied by a positive
constant (on the left) also tends to infinity. The archimedean assumption is convenient to get a
statement that works on ℕ, ℤ and ℝ, although not necessary (a version in ordered fields is
given in tendsto_at_top_mul_left').
If a function tends to infinity along a filter, then this function multiplied by a positive
constant (on the right) also tends to infinity. The archimedean assumption is convenient to get a
statement that works on ℕ, ℤ and ℝ, although not necessary (a version in ordered fields is
given in tendsto_at_top_mul_right').
If a function tends to infinity along a filter, then this function multiplied by a positive
constant (on the left) also tends to infinity. For a version working in ℕ or ℤ, use
tendsto_at_top_mul_left instead.
If a function tends to infinity along a filter, then this function multiplied by a positive
constant (on the right) also tends to infinity. For a version working in ℕ or ℤ, use
tendsto_at_top_mul_right instead.
If a function tends to infinity along a filter, then this function divided by a positive constant also tends to infinity.
The function x ↦ x⁻¹ tends to +∞ on the right of 0.
The function r ↦ r⁻¹ tends to 0 on the right as r → +∞.
Powers
If a sequence v of real numbers satisfies k*v n < v (n+1) with 1 < k,
then it goes to +∞.
In a normed ring, the powers of an element x with ∥x∥ < 1 tend to zero.
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.
If ∥f n∥ ≤ C * r ^ n for all n : ℕ and some r < 1, then the partial sums of f form a
Cauchy sequence. This lemma does not assume 0 ≤ r or 0 ≤ C.
If ∥f n∥ ≤ C * r ^ n for all n : ℕ and some r < 1, then the partial sums of f are within
distance C * r ^ n / (1 - r) of the sum of the series. This lemma does not assume 0 ≤ r or
0 ≤ C.
A geometric series in a complete normed ring is summable. Proved above (same name, different namespace) for not-necessarily-complete normed fields.
Bound for the sum of a geometric series in a normed ring. This formula does not assume that the
normed ring satisfies the axiom ∥1∥ = 1.
Positive sequences with small sums on encodable types
For any positive ε, define on an encodable type a positive sequence with sum less than ε
Harmonic series
Here we define the harmonic series and prove some basic lemmas about it, leading to a proof of its divergence to +∞
The harmonic series 1 + 1/2 + 1/3 + ... + 1/n
Equations
- harmonic_series n = (finset.range n).sum (λ (i : ℕ), 1 / (↑i + 1))
The harmonic series diverges to +∞