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 : ℕ) : ↑(N.roughNumbersUpTo k).card ≤ ↑N * ∑ p ∈ N.succ.primesBelow \ k.primesBelow, 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 ≤ ∑ p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow, 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 ({p : ℕ | Nat.Prime p}.indicator fun (n : ℕ) => 1 / ↑n)

The sum over the reciprocals of the primes diverges.

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

The sum over the reciprocals of the primes diverges.

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

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