The limsup of a nonnegative real sequence is nonnegative.
Proposition 2.6.1 (Root test). Let x : ℕ → ℝ and set
L = limsup_{n→∞} (|x (n+1)|)^{1/(n+1)}. (i) If L < 1, then
∑_{n=1}^{∞} x n converges absolutely. (ii) If L > 1, then
∑_{n=1}^{∞} x n diverges.
A sequence tending to 0 is eventually within unit distance of 0.
Proposition 2.6.2 (Alternating series). If x : ℕ → ℝ is a monotone decreasing
sequence of positive numbers with Filter.Tendsto (fun n => x (n + 1)) Filter.atTop (𝓝 0),
then the alternating series ∑_{n=1}^∞ (-1)^n x_n converges.
Proposition 2.6.3. If ∑_{n=1}^∞ x_n is absolutely convergent with sum x, then for any
bijection σ : ℕ → ℕ the rearranged series ∑_{n=1}^∞ x_{σ n} is absolutely convergent and has
the same sum.
Theorem 2.6.5 (Mertens' theorem). Suppose ∑_{n=0}^∞ a_n = A and ∑_{n=0}^∞ b_n = B,
and assume at least one of the series converges absolutely. Define
c n = a 0 * b n + a 1 * b (n - 1) + ⋯ + a n * b 0 = ∑_{i=0}^n a i * b (n - i).
Then ∑_{n=0}^∞ c n converges to A * B.
Example 2.6.6. Let a n = b n = (-1)^n / √(n+1) so that each alternating series
∑_{n=0}^∞ a n and ∑_{n=0}^∞ b n converges conditionally. If
c n = ∑_{i=0}^n a i * b (n - i) is their Cauchy product, then the terms c n do not tend
to zero, and hence the series ∑_{n=0}^∞ c n diverges.
Example 2.6.7. The power series ∑_{n=0}^∞ (1 / n!) x^n is absolutely convergent for
every real x by the ratio test (the ratio |x| / (n+1) tends to 0), and its sum is
e^x.
Example 2.6.8. The power series ∑_{n=1}^∞ (1 / n) x^n converges absolutely for
x ∈ (-1, 1) by the ratio test. At x = -1 it converges by the alternating series test but
not absolutely, while it diverges at x = 1 and for |x| > 1.
A conditional sum is preserved by the identity permutation.
The quotient n/(n+1) tends to 1.
The sequence (c ^ n)^(1/(n+1)) tends to c in ℝ≥0∞.
Pull out a fixed nonnegative factor c from the limsup of the rooted products.
Pull out the scaling factor |x - x₀| from the limsup of the scaled series.
Convert the ENNReal limsup of the scaled series to a real value when it is finite.
For a summable real series, the limsup of the norms is finite.
If the limsup of ‖b n‖ is infinite, then the series ∑ b n diverges.
Proposition 2.6.11. For the power series ∑_{n=0}^∞ aₙ (x - x₀)^n, let
R = limsup_{n→∞} ‖aₙ‖^{1/n}. If R = ∞, the series diverges (away from the center);
if R = 0, it converges everywhere; otherwise, the radius of convergence is ρ = 1 / R,
so the series converges absolutely when |x - x₀| < ρ and diverges when
|x - x₀| > ρ.
Proposition 2.6.10. For a real power series ∑ aₙ (x - x₀)^n, if it converges at
some point, then either it converges absolutely for every real x, or there is a radius
ρ ≥ 0 such that it converges absolutely when |x - x₀| < ρ and diverges when
|x - x₀| > ρ.
Proposition 2.6.12. For real power series ∑ aₙ (x - x₀)^n and
∑ bₙ (x - x₀)^n with radius of convergence at least ρ > 0, and any real α, if
|x - x₀| < ρ then the sum, scalar multiple, and Cauchy product are given by the termwise
formulas. The Cauchy product coefficients are cₙ = a₀ bₙ + a₁ b_{n-1} + ⋯ + aₙ b₀.
Example 2.6.13. For |x| < 1, the power series of x / (1 + 2x + x^2) about 0 is
∑_{n=1}^∞ (-1)^{n+1} n x^n, and the radius of convergence is exactly 1.