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 [AZ98]. The proof is due to Erdős.

theorem Nat.Primes.tprod_eq_tprod_ite {M : Type u_1} [CommMonoid M] [TopologicalSpace M] (f : ℕ → M) : ∏' (p : Primes), f ↑p = ∏' (n : ℕ), if Prime n then f n else 1

Reindex a product over Nat.Primes as a product over ℕ, extending f by 1.

theorem Nat.Primes.tsum_eq_tsum_ite {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] (f : ℕ → M) : ∑' (p : Primes), f ↑p = ∑' (n : ℕ), if Prime n then f n else 0

Reindex a sum over Nat.Primes as a sum over ℕ, extending f by 0.

theorem Nat.Primes.multipliable_iff_multipliable_ite {M : Type u_1} [CommMonoid M] [TopologicalSpace M] (f : ℕ → M) : (Multipliable fun (p : Primes) => f ↑p) ↔ Multipliable fun (n : ℕ) => if Prime n then f n else 1

Multipliable over Nat.Primes iff over ℕ extending f by 1.

theorem Nat.Primes.summable_iff_summable_ite {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] (f : ℕ → M) : (Summable fun (p : Primes) => f ↑p) ↔ Summable fun (n : ℕ) => if Prime n then f n else 0

Summable over Nat.Primes iff over ℕ extending f by 0.

theorem Nat.Primes.hasProd_iff_hasProd_ite {M : Type u_1} [CommMonoid M] [TopologicalSpace M] (f : ℕ → M) {a : M} : HasProd (fun (p : Primes) => f ↑p) a ↔ HasProd (fun (n : ℕ) => if Prime n then f n else 1) a

HasProd over Nat.Primes iff over ℕ extending f by 1.

theorem Nat.Primes.hasSum_iff_hasSum_ite {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] (f : ℕ → M) {a : M} : HasSum (fun (p : Primes) => f ↑p) a ↔ HasSum (fun (n : ℕ) => if Prime n then f n else 0) a

HasSum over Nat.Primes iff over ℕ extending f by 0.

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.