Convergence of p-series

In this file we prove that the series ∑' k in ℕ, 1 / k ^ p converges if and only if p > 1. The proof is based on the Cauchy condensation test: ∑ k, f k converges if and only if so does ∑ k, 2 ^ k f (2 ^ k). We prove this test in NNReal.summable_condensed_iff and summable_condensed_iff_of_nonneg, then use it to prove summable_one_div_rpow. After this transformation, a p-series turns into a geometric series.

Tags

p-series, Cauchy condensation test

Schlömilch's generalization of the Cauchy condensation test

In this section we prove the Schlömilch's generalization of the Cauchy condensation test: for a strictly increasing u : ℕ → ℕ with ratio of successive differences bounded and an antitone f : ℕ → ℝ≥0 or f : ℕ → ℝ, ∑ k, f k converges if and only if so does ∑ k, (u (k + 1) - u k) * f (u k). Instead of giving a monolithic proof, we split it into a series of lemmas with explicit estimates of partial sums of each series in terms of the partial sums of the other series.

def SuccDiffBounded (C : ℕ) (u : ℕ → ℕ) : Prop

A sequence u has the property that its ratio of successive differences is bounded when there is a positive real number C such that, for all n ∈ ℕ, (u (n + 2) - u (n + 1)) ≤ C * (u (n + 1) - u n)

theorem Finset.le_sum_schlomilch' {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M} {u : ℕ → ℕ} (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ (n : ℕ), 0 < u n) (hu : Monotone u) (n : ℕ) : ∑ k ∈ Ico (u 0) (u n), f k ≤ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)

theorem Finset.le_sum_condensed' {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M} (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) (n : ℕ) : ∑ k ∈ Ico 1 (2 ^ n), f k ≤ ∑ k ∈ range n, 2 ^ k • f (2 ^ k)

theorem Finset.le_sum_schlomilch {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M} {u : ℕ → ℕ} (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ (n : ℕ), 0 < u n) (hu : Monotone u) (n : ℕ) : ∑ k ∈ range (u n), f k ≤ ∑ k ∈ range (u 0), f k + ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)

theorem Finset.le_sum_condensed {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M} (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) (n : ℕ) : ∑ k ∈ range (2 ^ n), f k ≤ f 0 + ∑ k ∈ range n, 2 ^ k • f (2 ^ k)

theorem Finset.sum_schlomilch_le' {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M} {u : ℕ → ℕ} (hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ (n : ℕ), 0 < u n) (hu : Monotone u) (n : ℕ) : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k

theorem Finset.sum_condensed_le' {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M} (hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) (n : ℕ) : ∑ k ∈ range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k ∈ Ico 2 (2 ^ n + 1), f k

theorem Finset.sum_schlomilch_le {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M} {u : ℕ → ℕ} {C : ℕ} (hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ (n : ℕ), 0 < u n) (h_nonneg : ∀ (n : ℕ), 0 ≤ f n) (hu : Monotone u) (h_succ_diff : SuccDiffBounded C u) (n : ℕ) : ∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u k) ≤ (u 1 - u 0) • f (u 0) + C • ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k

theorem Finset.sum_condensed_le {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {f : ℕ → M} (hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) (n : ℕ) : ∑ k ∈ range (n + 1), 2 ^ k • f (2 ^ k) ≤ f 1 + 2 • ∑ k ∈ Ico 2 (2 ^ n + 1), f k

theorem ENNReal.le_tsum_schlomilch {u : ℕ → ℕ} {f : ℕ → ENNReal} (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ (n : ℕ), 0 < u n) (hu : StrictMono u) : ∑' (k : ℕ), f k ≤ ∑ k ∈ Finset.range (u 0), f k + ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k)

theorem ENNReal.le_tsum_condensed {f : ℕ → ENNReal} (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) : ∑' (k : ℕ), f k ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)

theorem ENNReal.tsum_schlomilch_le {u : ℕ → ℕ} {f : ℕ → ENNReal} {C : ℕ} (hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ (n : ℕ), 0 < u n) (h_nonneg : ∀ (n : ℕ), 0 ≤ f n) (hu : Monotone u) (h_succ_diff : SuccDiffBounded C u) : ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k) ≤ (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑' (k : ℕ), f k

theorem ENNReal.tsum_condensed_le {f : ℕ → ENNReal} (hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) : ∑' (k : ℕ), 2 ^ k * f (2 ^ k) ≤ f 1 + 2 * ∑' (k : ℕ), f k

theorem NNReal.summable_schlomilch_iff {C : ℕ} {u : ℕ → ℕ} {f : ℕ → NNReal} (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ (n : ℕ), 0 < u n) (hu_strict : StrictMono u) (hC_nonzero : C ≠ 0) (h_succ_diff : SuccDiffBounded C u) : (Summable fun (k : ℕ) => (↑(u (k + 1)) - ↑(u k)) * f (u k)) ↔ Summable f

for a series of NNReal version.

theorem NNReal.summable_condensed_iff {f : ℕ → NNReal} (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) : (Summable fun (k : ℕ) => 2 ^ k * f (2 ^ k)) ↔ Summable f

theorem summable_schlomilch_iff_of_nonneg {C : ℕ} {u : ℕ → ℕ} {f : ℕ → ℝ} (h_nonneg : ∀ (n : ℕ), 0 ≤ f n) (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ (n : ℕ), 0 < u n) (hu_strict : StrictMono u) (hC_nonzero : C ≠ 0) (h_succ_diff : SuccDiffBounded C u) : (Summable fun (k : ℕ) => (↑(u (k + 1)) - ↑(u k)) * f (u k)) ↔ Summable f

for series of nonnegative real numbers.

theorem summable_condensed_iff_of_nonneg {f : ℕ → ℝ} (h_nonneg : ∀ (n : ℕ), 0 ≤ f n) (h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) : (Summable fun (k : ℕ) => 2 ^ k * f (2 ^ k)) ↔ Summable f

Cauchy condensation test for antitone series of nonnegative real numbers.

Convergence of the p-series

In this section we prove that for a real number p, the series ∑' n : ℕ, 1 / (n ^ p) converges if and only if 1 < p. There are many different proofs of this fact. The proof in this file uses the Cauchy condensation test we formalized above. This test implies that ∑ n, 1 / (n ^ p) converges if and only if ∑ n, 2 ^ n / ((2 ^ n) ^ p) converges, and the latter series is a geometric series with common ratio 2 ^ {1 - p}.

@[simp]

theorem Real.summable_nat_rpow_inv {p : ℝ} : (Summable fun (n : ℕ) => (↑n ^ p)⁻¹) ↔ 1 < p

Test for convergence of the p-series: the real-valued series ∑' n : ℕ, (n ^ p)⁻¹ converges if and only if 1 < p.

@[simp]

theorem Real.summable_nat_rpow {p : ℝ} : (Summable fun (n : ℕ) => ↑n ^ p) ↔ p < -1

theorem Real.summable_one_div_nat_rpow {p : ℝ} : (Summable fun (n : ℕ) => 1 / ↑n ^ p) ↔ 1 < p

Test for convergence of the p-series: the real-valued series ∑' n : ℕ, 1 / n ^ p converges if and only if 1 < p.

@[simp]

theorem Real.summable_nat_pow_inv {p : ℕ} : (Summable fun (n : ℕ) => (↑n ^ p)⁻¹) ↔ 1 < p

Test for convergence of the p-series: the real-valued series ∑' n : ℕ, (n ^ p)⁻¹ converges if and only if 1 < p.

theorem Real.summable_one_div_nat_pow {p : ℕ} : (Summable fun (n : ℕ) => 1 / ↑n ^ p) ↔ 1 < p

Test for convergence of the p-series: the real-valued series ∑' n : ℕ, 1 / n ^ p converges if and only if 1 < p.

theorem Real.summable_one_div_int_pow {p : ℕ} : (Summable fun (n : ℤ) => 1 / ↑n ^ p) ↔ 1 < p

Summability of the p-series over ℤ.

theorem Real.summable_abs_int_rpow {b : ℝ} (hb : 1 < b) : Summable fun (n : ℤ) => |↑n| ^ (-b)

theorem Real.not_summable_natCast_inv : ¬Summable fun (n : ℕ) => (↑n)⁻¹

Harmonic series is not unconditionally summable.

theorem Real.not_summable_one_div_natCast : ¬Summable fun (n : ℕ) => 1 / ↑n

Harmonic series is not unconditionally summable.

theorem Real.tendsto_sum_range_one_div_nat_succ_atTop : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, 1 / (↑i + 1)) Filter.atTop Filter.atTop

Divergence of the Harmonic Series

@[simp]

theorem NNReal.summable_rpow_inv {p : ℝ} : (Summable fun (n : ℕ) => (↑n ^ p)⁻¹) ↔ 1 < p

@[simp]

theorem NNReal.summable_rpow {p : ℝ} : (Summable fun (n : ℕ) => ↑n ^ p) ↔ p < -1

theorem NNReal.summable_one_div_rpow {p : ℝ} : (Summable fun (n : ℕ) => 1 / ↑n ^ p) ↔ 1 < p

theorem sum_Ioc_inv_sq_le_sub {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {k n : ℕ} (hk : k ≠ 0) (h : k ≤ n) : ∑ i ∈ Finset.Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹

theorem sum_Ioo_inv_sq_le {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (k n : ℕ) : ∑ i ∈ Finset.Ioo k n, (↑i ^ 2)⁻¹ ≤ 2 / (↑k + 1)

theorem Real.not_summable_indicator_one_div_natCast {m : ℕ} (hm : m ≠ 0) (k : ZMod m) : ¬Summable ({n : ℕ | ↑n = k}.indicator fun (n : ℕ) => 1 / ↑n)

The harmonic series restricted to a residue class is not summable.

Translating the p-series by a real number

theorem Real.summable_one_div_nat_add_rpow (a s : ℝ) : (Summable fun (n : ℕ) => 1 / |↑n + a| ^ s) ↔ 1 < s

theorem Real.summable_one_div_int_add_rpow (a s : ℝ) : (Summable fun (n : ℤ) => 1 / |↑n + a| ^ s) ↔ 1 < s

theorem summable_pow_div_add {α : Type u_1} (x : α) [RCLike α] (q k : ℕ) (hq : 1 < q) : Summable fun (n : ℕ) => ‖x / (↑n + ↑k) ^ q‖