Divergence of the Prime Reciprocal Series #

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

This file proves Theorem 81 from the 100 Theorems List. The theorem states that the sum of the reciprocals of all prime numbers diverges. The formalization follows Erdős's proof by upper and lower estimates.

Proof outline #

Assume that the sum of the reciprocals of the primes converges.
Then there exists a k : ℕ such that, for any x : ℕ, the sum of the reciprocals of the primes between k and x + 1 is less than 1/2 (sum_lt_half_of_not_tendsto).
For any x : ℕ, we can partition range x into two subsets (range_sdiff_eq_bUnion):
- M x k, the subset of those e for which e + 1 is a product of powers of primes smaller than or equal to k;
- U x k, the subset of those e for which there is a prime p > k that divides e + 1.
Then |U x k| is bounded by the sum over the primes p > k of the number of multiples of p in (k, x], which is at most x / p. It follows that |U x k| is at most x times the sum of the reciprocals of the primes between k and x + 1, which is less than 1/2 as noted in (2), so |U x k| < x / 2 (card_le_mul_sum).
By factoring e + 1 = (m + 1)² * (r + 1), r + 1 squarefree and m + 1 ≤ √x, and noting that squarefree numbers correspond to subsets of [1, k], we find that |M x k| ≤ 2 ^ k * √x (card_le_two_pow_mul_sqrt).
Finally, setting x := (2 ^ (k + 1))² (√x = 2 ^ (k + 1)), we find that |M x k| ≤ 2 ^ k * 2 ^ (k + 1) = x / 2. Combined with the strict bound for |U k x| from (4), x = |M x k| + |U x k| < x / 2 + x / 2 = x.

References #

https://en.wikipedia.org/wiki/Divergence_of_the_sum_of_the_reciprocals_of_the_primes

source

noncomputable def theorems_100.P (x k : ℕ) :

finset ℕ

The primes in (k, x].

Equations

theorems_100.P x k = {p ∈ finset.range (x + 1) | k < p ∧ nat.prime p}

source

noncomputable def theorems_100.U (x k : ℕ) :

finset ℕ

The union over those primes p ∈ (k, x] of the sets of e < x for which e + 1 is a multiple of p, i.e., those e < x for which there is a prime p ∈ (k, x] that divides e + 1.

Equations

theorems_100.U x k = (theorems_100.P x k).bUnion (λ (p : ℕ), {e ∈ finset.range x | p ∣ e + 1})

source

noncomputable def theorems_100.M (x k : ℕ) :

finset ℕ

Those e < x for which e + 1 is a product of powers of primes smaller than or equal to k.

Equations

theorems_100.M x k = {e ∈ finset.range x | ∀ (p : ℕ), nat.prime p ∧ p ∣ e + 1 → p ≤ k}

source

theorem theorems_100.sum_lt_half_of_not_tendsto (h : ¬filter.tendsto (λ (n : ℕ), {p ∈ finset.range n | nat.prime p}.sum (λ (p : ℕ), 1 / ↑p)) filter.at_top filter.at_top) :

∃ (k : ℕ), ∀ (x : ℕ), (theorems_100.P x k).sum (λ (p : ℕ), 1 / ↑p) < 1 / 2

If the sum of the reciprocals of the primes converges, there exists a k : ℕ such that the sum of the reciprocals of the primes greater than k is less than 1/2.

More precisely, for any x : ℕ, the sum of the reciprocals of the primes between k and x + 1 is less than 1/2.

source

theorem theorems_100.range_sdiff_eq_bUnion {x k : ℕ} :

finset.range x \ theorems_100.M x k = theorems_100.U x k

Removing from {0, ..., x - 1} those elements e for which e + 1 is a product of powers of primes smaller than or equal to k leaves those e for which there is a prime p > k that divides e + 1, or the union over those primes p > k of the sets of es for which e + 1 is a multiple of p.

source

theorem theorems_100.card_le_mul_sum {x k : ℕ} :

↑((theorems_100.U x k).card) ≤ ↑x * (theorems_100.P x k).sum (λ (p : ℕ), 1 / ↑p)

The number of e < x for which e + 1 has a prime factor p > k is bounded by x times the sum of reciprocals of primes in (k, x].

source

theorem theorems_100.card_le_two_pow {x k : ℕ} :

{e ∈ theorems_100.M x k | squarefree (e + 1)}.card ≤ 2 ^ k

The number of e < x for which e + 1 is a squarefree product of primes smaller than or equal to k is bounded by 2 ^ k, the number of subsets of [1, k].

source

theorem theorems_100.card_le_two_pow_mul_sqrt {x k : ℕ} :

(theorems_100.M x k).card ≤ 2 ^ k * nat.sqrt x

The number of e < x for which e + 1 is a product of powers of primes smaller than or equal to k is bounded by 2 ^ k * nat.sqrt x.

source

theorem theorems_100.real.tendsto_sum_one_div_prime_at_top :

filter.tendsto (λ (n : ℕ), {p ∈ finset.range n | nat.prime p}.sum (λ (p : ℕ), 1 / ↑p)) filter.at_top filter.at_top