Divergence of the Prime Reciprocal Series

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

1. Assume that the sum of the reciprocals of the primes converges.
2. 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).
3. For any x : ℕ, we can partition range x into two subsets (range_sdiff_eq_biUnion):
   • 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.
4. 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).
5. 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).
6. 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

def Theorems100.P (x : ℕ) (k : ℕ) : Finset ℕ

The primes in (k, x].

Equations

• Theorems100.P x k = Finset.filter (fun (p : ℕ) => k < p ∧ p.Prime) (Finset.range (x + 1))

def Theorems100.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

• Theorems100.U x k = (Theorems100.P x k).biUnion fun (p : ℕ) => Finset.filter (fun (e : ℕ) => p ∣ e + 1) (Finset.range x)

noncomputable def Theorems100.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

• Theorems100.M x k = Finset.filter (fun (e : ℕ) => ∀ (p : ℕ), p.Prime ∧ p ∣ e + 1 → p ≤ k) (Finset.range x)

theorem Theorems100.sum_lt_half_of_not_tendsto (h : ¬Filter.Tendsto (fun (n : ℕ) => (Finset.filter (fun (p : ℕ) => p.Prime) (Finset.range n)).sum fun (p : ℕ) => 1 / ↑p) Filter.atTop Filter.atTop) : ∃ (k : ℕ), ∀ (x : ℕ), ((Theorems100.P x k).sum fun (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.

theorem Theorems100.range_sdiff_eq_biUnion {x : ℕ} {k : ℕ} : Finset.range x \ Theorems100.M x k = Theorems100.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.

theorem Theorems100.card_le_mul_sum {x : ℕ} {k : ℕ} : ↑(Theorems100.U x k).card ≤ ↑x * (Theorems100.P x k).sum fun (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].

theorem Theorems100.card_le_two_pow {x : ℕ} {k : ℕ} : (Finset.filter (fun (e : ℕ) => Squarefree (e + 1)) (Theorems100.M x k)).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].

theorem Theorems100.card_le_two_pow_mul_sqrt {x : ℕ} {k : ℕ} : (Theorems100.M x k).card ≤ 2 ^ k * x.sqrt

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.

theorem Theorems100.Real.tendsto_sum_one_div_prime_atTop : Filter.Tendsto (fun (n : ℕ) => (Finset.filter (fun (p : ℕ) => p.Prime) (Finset.range n)).sum fun (p : ℕ) => 1 / ↑p) Filter.atTop Filter.atTop