# 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 #

- 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_biUnion`

): - 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

The primes in `(k, x]`

.

## Equations

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

## Instances For

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)

## Instances For

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 : ℕ), Nat.Prime p ∧ p ∣ e + 1 → p ≤ k) (Finset.range x)

## Instances For

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.

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 `e`

s for which `e + 1`

is a multiple
of `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]`

.

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]`

.

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`

.