mathlib3 documentation

analysis.p_series

Convergence of `p`-series #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 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} [ordered_add_comm_monoid M] {f : ℕ → M} (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) (n : ℕ) :

(finset.Ico 1 (2 ^ n)).sum (λ (k : ℕ), f k) ≤ (finset.range n).sum (λ (k : ℕ), 2 ^ k • f (2 ^ k))

theorem finset.le_sum_condensed {M : Type u_1} [ordered_add_comm_monoid M] {f : ℕ → M} (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) (n : ℕ) :

(finset.range (2 ^ n)).sum (λ (k : ℕ), f k) ≤ f 0 + (finset.range n).sum (λ (k : ℕ), 2 ^ k • f (2 ^ k))

theorem finset.sum_condensed_le' {M : Type u_1} [ordered_add_comm_monoid M] {f : ℕ → M} (hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) (n : ℕ) :

(finset.range n).sum (λ (k : ℕ), 2 ^ k • f (2 ^ (k + 1))) ≤ (finset.Ico 2 (2 ^ n + 1)).sum (λ (k : ℕ), f k)

theorem finset.sum_condensed_le {M : Type u_1} [ordered_add_comm_monoid M] {f : ℕ → M} (hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m) (n : ℕ) :

(finset.range (n + 1)).sum (λ (k : ℕ), 2 ^ k • f (2 ^ k)) ≤ f 1 + 2 • (finset.Ico 2 (2 ^ n + 1)).sum (λ (k : ℕ), f 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_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_condensed_iff {f : ℕ → nnreal} (hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) :

summable (λ (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 < m → m ≤ n → f n ≤ f m) :

summable (λ (k : ℕ), 2 ^ k * f (2 ^ k)) ↔ summable f

Cauchy condensation test for 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 (λ (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 (λ (n : ℕ), ↑n ^ p) ↔ p < -1

theorem real.summable_one_div_nat_rpow {p : ℝ} :

summable (λ (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 (λ (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 (λ (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 (λ (n : ℤ), 1 / ↑n ^ p) ↔ 1 < p

Summability of the p-series over ℤ.

theorem real.summable_abs_int_rpow {b : ℝ} (hb : 1 < b) :

summable (λ (n : ℤ), |↑n| ^ -b)

theorem real.not_summable_nat_cast_inv :

¬summable (λ (n : ℕ), (↑n)⁻¹)

Harmonic series is not unconditionally summable.

theorem real.not_summable_one_div_nat_cast :

¬summable (λ (n : ℕ), 1 / ↑n)

Harmonic series is not unconditionally summable.

theorem real.tendsto_sum_range_one_div_nat_succ_at_top :

filter.tendsto (λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), 1 / (↑i + 1))) filter.at_top filter.at_top

Divergence of the Harmonic Series

@[simp]

theorem nnreal.summable_rpow_inv {p : ℝ} :

summable (λ (n : ℕ), (↑n ^ p)⁻¹) ↔ 1 < p

@[simp]

theorem nnreal.summable_rpow {p : ℝ} :

summable (λ (n : ℕ), ↑n ^ p) ↔ p < -1

theorem nnreal.summable_one_div_rpow {p : ℝ} :

summable (λ (n : ℕ), 1 / ↑n ^ p) ↔ 1 < p

theorem sum_Ioc_inv_sq_le_sub {α : Type u_1} [linear_ordered_field α] {k n : ℕ} (hk : k ≠ 0) (h : k ≤ n) :

(finset.Ioc k n).sum (λ (i : ℕ), (↑i ^ 2)⁻¹) ≤ (↑k)⁻¹ - (↑n)⁻¹

theorem sum_Ioo_inv_sq_le {α : Type u_1} [linear_ordered_field α] (k n : ℕ) :

(finset.Ioo k n).sum (λ (i : ℕ), (↑i ^ 2)⁻¹) ≤ 2 / (↑k + 1)