Documentation

Mathlib.Analysis.PSeries

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.

TODO #

It should be easy to generalize arguments to Schlömilch's generalization of the Cauchy condensation test once we need it.

Tags #

p-series, Cauchy condensation test

Cauchy condensation test #

In this section we prove the Cauchy condensation test: for an antitone f : ℕ → ℝ≥0 or f : ℕ → ℝ, ∑ k, f k converges if and only if so does ∑ k, 2 ^ k f (2 ^ 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.

theorem Finset.le_sum_condensed' {M : Type u_1} [OrderedAddCommMonoid M] {f : M} (hf : ∀ ⦃m n : ⦄, 0 < mm nf n f m) (n : ) :
(Finset.sum (Finset.Ico 1 (2 ^ n)) fun (k : ) => f k) Finset.sum (Finset.range n) fun (k : ) => 2 ^ k f (2 ^ k)
theorem Finset.le_sum_condensed {M : Type u_1} [OrderedAddCommMonoid M] {f : M} (hf : ∀ ⦃m n : ⦄, 0 < mm nf n f m) (n : ) :
(Finset.sum (Finset.range (2 ^ n)) fun (k : ) => f k) f 0 + Finset.sum (Finset.range n) fun (k : ) => 2 ^ k f (2 ^ k)
theorem Finset.sum_condensed_le' {M : Type u_1} [OrderedAddCommMonoid M] {f : M} (hf : ∀ ⦃m n : ⦄, 1 < mm nf n f m) (n : ) :
(Finset.sum (Finset.range n) fun (k : ) => 2 ^ k f (2 ^ (k + 1))) Finset.sum (Finset.Ico 2 (2 ^ n + 1)) fun (k : ) => f k
theorem Finset.sum_condensed_le {M : Type u_1} [OrderedAddCommMonoid M] {f : M} (hf : ∀ ⦃m n : ⦄, 1 < mm nf n f m) (n : ) :
(Finset.sum (Finset.range (n + 1)) fun (k : ) => 2 ^ k f (2 ^ k)) f 1 + 2 Finset.sum (Finset.Ico 2 (2 ^ n + 1)) fun (k : ) => f k
theorem ENNReal.le_tsum_condensed {f : ENNReal} (hf : ∀ ⦃m n : ⦄, 0 < mm nf n f m) :
∑' (k : ), f k f 0 + ∑' (k : ), 2 ^ k * f (2 ^ k)
theorem ENNReal.tsum_condensed_le {f : ENNReal} (hf : ∀ ⦃m n : ⦄, 1 < mm nf n f m) :
∑' (k : ), 2 ^ k * f (2 ^ k) f 1 + 2 * ∑' (k : ), f k
theorem NNReal.summable_condensed_iff {f : NNReal} (hf : ∀ ⦃m n : ⦄, 0 < mm nf n f m) :
(Summable fun (k : ) => 2 ^ k * f (2 ^ k)) Summable f

Cauchy condensation test for a series of NNReal version.

theorem summable_condensed_iff_of_nonneg {f : } (h_nonneg : ∀ (n : ), 0 f n) (h_mono : ∀ ⦃m n : ⦄, 0 < mm nf 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.

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)

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 : ) => Finset.sum (Finset.range n) fun (i : ) => 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} [LinearOrderedField α] {k : } {n : } (hk : k 0) (h : k n) :
(Finset.sum (Finset.Ioc k n) fun (i : ) => (i ^ 2)⁻¹) (k)⁻¹ - (n)⁻¹
theorem sum_Ioo_inv_sq_le {α : Type u_1} [LinearOrderedField α] (k : ) (n : ) :
(Finset.sum (Finset.Ioo k n) fun (i : ) => (i ^ 2)⁻¹) 2 / (k + 1)
theorem Real.not_summable_indicator_one_div_natCast {m : } (hm : m 0) (k : ZMod m) :
¬Summable (Set.indicator {n : | n = k} 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