Documentation

Mathlib.NumberTheory.SumPrimeReciprocals

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 * pN.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 : 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.