The sum of the reciprocals of the primes diverges

We show that the sum of 1/p, where p runs through the prime numbers, diverges. We follow the elementary proof by Erdős that is reproduced in "Proofs from THE BOOK". There are two versions of the main result: not_summable_one_div_on_primes, which expresses the sum as a sub-sum of the harmonic series, and Nat.Primes.not_summable_one_div, which writes it as a sum over Nat.Primes. We also show that the sum of p^r for r : ℝ converges if and only if r < -1; see Nat.Primes.summable_rpow.

References

See the sixth proof for the infinity of primes in Chapter 1 of [aigner1999proofs]. The proof is due to Erdős.

theorem Nat.roughNumbersUpTo_card_le' (N : ℕ) (k : ℕ) : ↑(Nat.roughNumbersUpTo N k).card ≤ ↑N * Finset.sum (Nat.primesBelow (Nat.succ N) \ Nat.primesBelow k) fun (p : ℕ) => 1 / ↑p

The cardinality of the set of k-rough numbers ≤ N is bounded by N times the sum of 1/p over the primes k ≤ p ≤ N.

theorem one_half_le_sum_primes_ge_one_div (k : ℕ) : 1 / 2 ≤ Finset.sum (Nat.primesBelow (Nat.succ (4 ^ ((Nat.primesBelow k).card + 1))) \ Nat.primesBelow k) fun (p : ℕ) => 1 / ↑p

The sum over primes k ≤ p ≤ 4^(π(k-1)+1) over 1/p (as a real number) is at least 1/2.

theorem not_summable_one_div_on_primes : ¬Summable (Set.indicator {p : ℕ | Nat.Prime p} fun (n : ℕ) => 1 / ↑n)

The sum over the reciprocals of the primes diverges.

theorem Nat.Primes.not_summable_one_div : ¬Summable fun (p : Nat.Primes) => 1 / ↑↑p

The sum over the reciprocals of the primes diverges.

theorem Nat.Primes.summable_rpow {r : ℝ} : (Summable fun (p : Nat.Primes) => ↑↑p ^ r) ↔ r < -1

The series over p^r for primes p converges if and only if r < -1.