theorem Real_Analysis.Series.comparison_test (x y : ℕ → ℝ) (hx : ∀ (n : ℕ), 0 ≤ x n) (hxy : ∀ (n : ℕ), x n ≤ y n) : (Summable y → Summable x) ∧ (¬Summable x → ¬Summable y)

Comparison Test for series of real numbers. If 0 ≤ x n ≤ y n for every n, then:

1. summability of y implies summability of x, and
2. non-summability of x implies non-summability of y (the latter being the contrapositive of the former).

theorem Real_Analysis.Series.root_test (x : ℕ → ℝ) (L : ℝ) (hL : Filter.Tendsto (fun (n : ℕ) => |x n| ^ (1 / ↑n)) Filter.atTop (nhds L)) : (L < 1 → Summable fun (n : ℕ) => |x n|) ∧ (1 < L → ¬Summable x)

Root Test (Cauchy's root test). Suppose L = lim |x n| ^ (1/n) exists. Then:

1. if L < 1, the series ∑ |x n| converges (so ∑ x n converges absolutely);
2. if L > 1, the series ∑ x n diverges.

theorem Real_Analysis.Series.ratio_test (x : ℕ → ℝ) (L : ℝ) (hx : ∀ (n : ℕ), x n ≠ 0) (hL : Filter.Tendsto (fun (n : ℕ) => |x (n + 1)| / |x n|) Filter.atTop (nhds L)) : (L < 1 → Summable fun (n : ℕ) => |x n|) ∧ (1 < L → ¬Summable x)

Ratio Test (d'Alembert's ratio test). Suppose x n ≠ 0 for every n and L = lim |x (n+1)| / |x n| exists. Then:

1. if L < 1, the series ∑ |x n| converges (so ∑ x n converges absolutely);
2. if L > 1, the series ∑ x n diverges.

theorem Real_Analysis.Series.alternating_series_test (x : ℕ → ℝ) (hpos : ∀ (n : ℕ), 0 ≤ x n) (hdec : Antitone x) (hlim : Filter.Tendsto x Filter.atTop (nhds 0)) : ∃ (l : ℝ), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i * x i) Filter.atTop (nhds l)

Alternating Series Test (Leibniz's test). If x : ℕ → ℝ is nonnegative, monotone decreasing (Antitone), and tends to 0, then the alternating series ∑ (-1)^i * x i converges, i.e. its partial sums converge to some real limit l.

theorem Real_Analysis.Series.alternating_harmonic_converges : ∃ (l : ℝ), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i / (↑i + 1)) Filter.atTop (nhds l)

Convergence of the alternating harmonic series. The series ∑ (-1)^i / (i + 1) converges, i.e. its partial sums converge to some real limit l. This is a direct corollary of the alternating series test, applied to the decreasing positive sequence 1 / (n + 1). Note that the corresponding series of absolute values (the harmonic series) diverges, so this is an example of a conditionally convergent series.