def partialSumsFromOne {α : Type u_1} [AddCommMonoid α] (x : ℕ → α) (k : ℕ) : α

Definition 2.5.1: For a sequence x : ℕ → α, the expression ∑_{n=1}^{∞} x n denotes the formal series. Its k-th partial sum is s k = ∑_{n=1}^k x n. The series converges to ℓ when the partial sums s k converge to ℓ as k → ∞; otherwise the series is divergent. When the series converges we identify its value with this limit.

Equations

• partialSumsFromOne x k = ∑ n ∈ Finset.Icc 1 k, x n

theorem partialSumsFromOne_eq_sum_range_succ {β : Type u_2} [AddCommMonoid β] (x : ℕ → β) (k : ℕ) : partialSumsFromOne x k = ∑ n ∈ Finset.range k, x (n + 1)

def SeriesConvergesTo {α : Type u_1} [NormedAddCommGroup α] (x : ℕ → α) (ℓ : α) : Prop

Convergence of the series ∑_{n=1}^{∞} x n to a limit ℓ, expressed via the convergence of the partial sums ∑_{n=1}^k x n as k → ∞.

Equations

• SeriesConvergesTo x ℓ = HasSum (fun (n : ℕ) => x (n + 1)) ℓ

def SeriesConvergent {α : Type u_1} [NormedAddCommGroup α] (x : ℕ → α) : Prop

The series ∑_{n=1}^{∞} x n is convergent if its partial sums admit some limit.

Equations

• SeriesConvergent x = Summable fun (n : ℕ) => x (n + 1)

def SeriesDivergent {α : Type u_1} [NormedAddCommGroup α] (x : ℕ → α) : Prop

A divergent series is one whose partial sums do not converge.

Equations

• SeriesDivergent x = ¬SeriesConvergent x

def SeriesCauchy {α : Type u_1} [NormedAddCommGroup α] (x : ℕ → α) : Prop

Definition 2.5.7: A series ∑_{n=1}^{∞} x n is called Cauchy (a Cauchy series) when its sequence of partial sums ∑_{n=1}^k x n forms a Cauchy sequence.

Equations

• SeriesCauchy x = CauchySeq fun (k : ℕ) => partialSumsFromOne x k

theorem seriesConvergesTo_iff_hasSum_shift {α : Type u_1} [NormedAddCommGroup α] (x : ℕ → α) (ℓ : α) : SeriesConvergesTo x ℓ ↔ HasSum (fun (n : ℕ) => x (n + 1)) ℓ

Bridge to mathlib's HasSum: using the shift starting at 1 our notion of converging series agrees with HasSum.

theorem seriesConvergent_iff_summable {α : Type u_1} [NormedAddCommGroup α] (x : ℕ → α) : SeriesConvergent x ↔ Summable fun (n : ℕ) => x (n + 1)

The book's notion of a convergent series agrees with mathlib's Summable for the shifted sequence starting at index 1.

theorem series_limit_eq_tsum {α : Type u_1} [NormedAddCommGroup α] {x : ℕ → α} {ℓ : α} : SeriesConvergesTo x ℓ ↔ (Summable fun (n : ℕ) => x (n + 1)) ∧ ∑' (n : ℕ), x (n + 1) = ℓ

When the series ∑_{n=1}^{∞} x n converges to ℓ, the limit equals the tsum of the underlying sequence indexed from 1.

theorem series_convergent_iff_convergent_tail {α : Type u_1} [NormedAddCommGroup α] (x : ℕ → α) (M : ℕ) : SeriesConvergent x ↔ SeriesConvergent fun (n : ℕ) => x (n + (M - 1))

Proposition 2.5.6: For a series ∑_{n=1}^{∞} x n and any M ∈ ℕ, convergence is unchanged by discarding the first M - 1 terms; equivalently ∑_{n=1}^{∞} x n converges if and only if the tail ∑_{n=M}^{∞} x n converges.

theorem geometric_series_sum {r : ℝ} (h₁ : -1 < r) (h₂ : r < 1) : (Summable fun (n : ℕ) => r ^ n) ∧ ∑' (n : ℕ), r ^ n = 1 / (1 - r)

Proposition 2.5.5: For a real number r with -1 < r < 1, the geometric series ∑_{n=0}^{∞} r^n converges and its sum equals 1 / (1 - r).

theorem geometric_half_partial_sum_closed_form (k : ℕ) : partialSumsFromOne (fun (n : ℕ) => (1 / 2) ^ n) k = 1 - (1 / 2) ^ k

A closed form for the partial sums of the geometric series with ratio 1/2.

theorem geometric_half_partial_sum_closed_form_inv (k : ℕ) : partialSumsFromOne (fun (n : ℕ) => (2 ^ n)⁻¹) k = 1 - (2 ^ k)⁻¹

theorem geometric_half_partial_sum_eq (k : ℕ) (hk : 1 ≤ k) : partialSumsFromOne (fun (n : ℕ) => (1 / 2) ^ n) k + (1 / 2) ^ k = 1

Example 2.5.4: The geometric series ∑_{n=1}^{∞} (1/2)^n converges to 1. For each k ≥ 1, the partial sum satisfies ∑_{n=1}^k (1/2)^n + (1/2)^k = 1, so the sequence of partial sums tends to 1.

theorem geometric_half_series_converges : SeriesConvergesTo (fun (n : ℕ) => (1 / 2) ^ n) 1

Example 2.5.4: Consequently, the series ∑_{n=1}^{∞} (1/2)^n converges and its sum equals 1.

theorem partialSumsFromOne_add_tail {β : Type u_2} [AddCommMonoid β] (x : ℕ → β) {n k : ℕ} (hnk : n ≤ k) : partialSumsFromOne x k = partialSumsFromOne x n + ∑ i ∈ Finset.Icc (n + 1) k, x i

Split partial sums into an initial segment plus a tail over Icc (n+1) k.

theorem partialSumsFromOne_sub_eq_tail {β : Type u_2} [AddCommGroup β] (x : ℕ → β) {n k : ℕ} (hnk : n ≤ k) : partialSumsFromOne x k - partialSumsFromOne x n = ∑ i ∈ Finset.Icc (n + 1) k, x i

The difference of partial sums is the tail sum over Icc (n+1) k.

theorem dist_partialSums_eq_norm_tail {α : Type u_1} [NormedAddCommGroup α] (x : ℕ → α) {n k : ℕ} (hnk : n ≤ k) : dist (partialSumsFromOne x n) (partialSumsFromOne x k) = ‖∑ i ∈ Finset.Icc (n + 1) k, x i‖

Distance between partial sums equals the norm of the corresponding tail sum.

theorem series_cauchy_iff_tail_norm_small {α : Type u_1} [NormedAddCommGroup α] (x : ℕ → α) : SeriesCauchy x ↔ ∀ ε > 0, ∃ (M : ℕ), ∀ ⦃n k : ℕ⦄, M ≤ n → n < k → ‖∑ i ∈ Finset.Icc (n + 1) k, x i‖ < ε

Proposition 2.5.8: The series ∑_{n=1}^{∞} x n is Cauchy if and only if for every ε > 0 there exists M ∈ ℕ such that for all n ≥ M and k > n, the tail sum ∑_{i=n+1}^k x i has norm less than ε.

theorem series_convergent_tendsto_zero {α : Type u_1} [NormedAddCommGroup α] {x : ℕ → α} (hx : SeriesConvergent x) : Filter.Tendsto (fun (n : ℕ) => x n) Filter.atTop (nhds 0)

Proposition 2.5.9: If the series ∑_{n=1}^{∞} x n converges, then the underlying sequence converges and its limit is 0; equivalently, lim_{n→∞} x n = 0.

theorem abs_ge_one_not_norm_lt_one {r : ℝ} (h : 1 ≤ |r|) : ¬‖r‖ < 1

If |r| ≥ 1, then ‖r‖ is not less than 1.

theorem geometric_series_diverges_of_abs_ge_one {r : ℝ} (h : 1 ≤ |r|) : ¬Summable fun (n : ℕ) => r ^ n

Example 2.5.10: If r ≥ 1 or r ≤ -1, the geometric series ∑_{n=0}^{∞} r^n diverges since the terms have absolute value at least 1 and do not tend to zero.

theorem harmonic_shift_not_summable : ¬Summable fun (n : ℕ) => 1 / (↑n + 1 + 1)

A shifted tail of the harmonic series is not summable.

theorem harmonic_series_diverges : SeriesDivergent fun (n : ℕ) => 1 / (↑n + 1)

Example 2.5.11: The harmonic series ∑_{n=1}^{∞} 1/n diverges even though its terms tend to 0. Grouping the terms in blocks of length 2^{k-1} shows that the partial sums s_{2^k} satisfy s_{2^k} ≥ 1 + k/2, which is unbounded by the Archimedean property; hence the whole sequence of partial sums is unbounded and the series diverges.

theorem series_convergesTo_smul {x : ℕ → ℝ} {α s : ℝ} (hx : SeriesConvergesTo x s) : SeriesConvergesTo (fun (n : ℕ) => α * x n) (α * s)

Proposition 2.5.12 (linearity of series). Let α : ℝ and suppose the series ∑_{n=1}^{∞} x n and ∑_{n=1}^{∞} y n converge. Then (i) the series ∑_{n=1}^{∞} α * x n converges and its value is α * ∑_{n=1}^{∞} x n; and (ii) the series ∑_{n=1}^{∞} (x n + y n) converges and its value is the sum of the two series.

theorem series_convergesTo_add {x y : ℕ → ℝ} {sx sy : ℝ} (hx : SeriesConvergesTo x sx) (hy : SeriesConvergesTo y sy) : SeriesConvergesTo (fun (n : ℕ) => x n + y n) (sx + sy)

theorem series_convergent_nonneg_iff_bddAbove {x : ℕ → ℝ} (hx : ∀ (n : ℕ), 0 ≤ x n) : SeriesConvergent x ↔ BddAbove (Set.range fun (k : ℕ) => partialSumsFromOne x k)

Proposition 2.5.13: For a sequence of nonnegative real numbers, the series ∑_{n=1}^{∞} x n converges if and only if the sequence of partial sums is bounded above.

def SeriesAbsolutelyConvergent {α : Type u_1} [NormedAddCommGroup α] (x : ℕ → α) : Prop

Definition 2.5.14: A series ∑_{n=1}^{∞} x n converges absolutely if the series of norms ∑_{n=1}^{∞} ‖x n‖ converges. If the original series converges but does not converge absolutely, it is conditionally convergent.

Equations

• SeriesAbsolutelyConvergent x = SeriesConvergent fun (n : ℕ) => ‖x n‖

def SeriesConditionallyConvergent {α : Type u_1} [NormedAddCommGroup α] (x : ℕ → α) : Prop

Equations

• SeriesConditionallyConvergent x = (SeriesConvergent x ∧ ¬SeriesAbsolutelyConvergent x)

theorem series_convergent_of_abs_convergent {α : Type u_1} [NormedAddCommGroup α] [CompleteSpace α] {x : ℕ → α} (h : SeriesAbsolutelyConvergent x) : SeriesConvergent x

Proposition 2.5.15: An absolutely convergent series ∑_{n=1}^{∞} x n necessarily converges.

theorem series_convergent_of_le {x y : ℕ → ℝ} (hxy : ∀ (n : ℕ), 0 ≤ x n ∧ x n ≤ y n) (hy : SeriesConvergent y) : SeriesConvergent x

Proposition 2.5.16 (comparison test). Let ∑_{n=1}^{∞} x n and ∑_{n=1}^{∞} y n be series with 0 ≤ x n ≤ y n for all n ∈ ℕ. (i) If ∑_{n=1}^{∞} y n converges, then ∑_{n=1}^{∞} x n converges. (ii) If ∑_{n=1}^{∞} x n diverges, then ∑_{n=1}^{∞} y n diverges.

theorem series_divergent_of_le {x y : ℕ → ℝ} (hxy : ∀ (n : ℕ), 0 ≤ x n ∧ x n ≤ y n) (hx : SeriesDivergent x) : SeriesDivergent y

theorem p_series_converges_iff (p : ℝ) : (SeriesConvergent fun (n : ℕ) => 1 / ↑n.succ ^ p) ↔ 1 < p

Proposition 2.5.17 ($p$-series or the $p$-test). For p ∈ ℝ, the series ∑_{n=1}^{∞} 1 / n^p converges if and only if p > 1.

theorem series_convergent_one_div_sq_add_one : SeriesConvergent fun (n : ℕ) => 1 / (↑n ^ 2 + 1)

Example 2.5.18: The series ∑_{n=1}^{∞} 1 / (n^2 + 1) converges, for instance by comparison with the $p$-series ∑_{n=1}^{∞} 1 / n^2.

theorem ratio_test_converges {x : ℕ → ℝ} (hx : ∀ (n : ℕ), x n ≠ 0) {L : ℝ} (hlim : Filter.Tendsto (fun (n : ℕ) => |x (n + 1)| / |x n|) Filter.atTop (nhds L)) (hL : L < 1) : SeriesAbsolutelyConvergent x

Proposition 2.5.19 (ratio test). Let ∑_{n=1}^{∞} x n be a real series with x n ≠ 0 for all n, and suppose the limit L = lim_{n→∞} |x (n+1)| / |x n| exists. (i) If L < 1, the series converges absolutely. (ii) If L > 1, the series diverges.

theorem ratio_test_diverges {x : ℕ → ℝ} (_hx : ∀ (n : ℕ), x n ≠ 0) {L : ℝ} (hlim : Filter.Tendsto (fun (n : ℕ) => |x (n + 1)| / |x n|) Filter.atTop (nhds L)) (hL : 1 < L) : SeriesDivergent x

theorem summable_pow_div_factorial : Summable fun (n : ℕ) => 2 ^ n / ↑n.factorial

The base series with terms 2^n / n! is summable.

theorem summable_shift_pow_div_factorial : Summable fun (n : ℕ) => 2 ^ (n + 1) / ↑(n + 1).factorial

Shifting the index preserves summability for 2^n / n!.

theorem summable_norm_shift_pow_div_factorial : Summable fun (n : ℕ) => ‖2 ^ (n + 1) / ↑(n + 1).factorial‖

The series of norms of the shifted terms is summable.

theorem series_abs_convergent_two_pow_div_factorial : SeriesAbsolutelyConvergent fun (n : ℕ) => 2 ^ n / ↑n.factorial

Example 2.5.20: The series ∑_{n=1}^{∞} 2^n / n! converges absolutely. The ratio of successive terms tends to 0, so the ratio test applies.