The weak prime number theorem

We deduce the prime number theorem, and its version for primes in arithmetic progressions, from the Wiener–Ikehara Tauberian theorem WienerIkehara.tendsto_sum_div.

Here ψ x = ∑ n ≤ x, Λ n and θ x = ∑ p ≤ x, log p (the sum running over primes) are the Chebyshev functions Chebyshev.psi and Chebyshev.theta.

Main results

• ArithmeticFunction.vonMangoldt.tendsto_sum_modEq_div_atTop: the von Mangoldt form of the prime number theorem in arithmetic progressions: for a coprime to q, ∑ n ≤ x, n ≡ a [MOD q], Λ n = x / φ q + o(x).
• Chebyshev.isEquivalent_psi_id: the ψ-form of the prime number theorem, ψ x ~ x (equivalently Chebyshev.tendsto_psi_div_atTop, ψ x / x → 1); this is the q = 1 case of the previous result.
• Chebyshev.isEquivalent_theta_id: the θ-form, θ x ~ x.
• Nat.isEquivalent_primeCounting: the prime number theorem π x ~ x / log x, deduced from the θ-form by Abel summation (Chebyshev.isLittleO_primeCounting_mul_log_sub_theta).
• Nat.isEquivalent_card_prime_modEq: the prime number theorem in arithmetic progressions: for a coprime to q, the number of primes p ≤ x with p ≡ a [MOD q] is asymptotic to x / (φ q * log x).
• Nat.eventually_exists_prime_mem_Ioc: for every ε > 0 and every sufficiently large x, there is a prime in (x, (1 + ε) * x]; Nat.eventually_exists_prime_mem_Ioc_sub gives one in ((1 - ε) * x, x].
• Nat.isEquivalent_nth_prime_succ: consecutive primes are asymptotically equal, pₙ₊₁ ~ pₙ.
• Nat.isEquivalent_log_primorial_id: log (primorial n) ~ n.
• Nat.isEquivalent_log_lcmUpto_id: log (Nat.lcmUpto n) ~ n.

Future directions

• Versions of Nat.eventually_exists_prime_mem_Ioc and Nat.eventually_exists_prime_mem_Ioc_sub for arithmetic progressions
• Showing that the nth prime is asymptotic to n * log n

Note though that all the results here could eventually be superseded by other approaches to the prime number theorem with stronger error terms.

theorem ArithmeticFunction.vonMangoldt.tendsto_sum_residueClass_div_atTop {q : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) : Filter.Tendsto (fun (x : ℝ) => (∑ n ∈ Finset.Icc 0 ⌊x⌋₊, residueClass a n) / x) Filter.atTop (nhds (↑q.totient)⁻¹)

The prime number theorem in arithmetic progressions, von Mangoldt form, stated for a unit a of ZMod q: the average of residueClass a over [0, x] tends to (φ q)⁻¹.

theorem ArithmeticFunction.vonMangoldt.tendsto_sum_modEq_div_atTop {q a : ℕ} [NeZero q] (ha : a.Coprime q) : Filter.Tendsto (fun (x : ℝ) => (∑ n ∈ Finset.Icc 0 ⌊x⌋₊ with n ≡ a [MOD q], vonMangoldt n) / x) Filter.atTop (nhds (↑q.totient)⁻¹)

The prime number theorem in arithmetic progressions, von Mangoldt form. For a coprime to q, the von Mangoldt function summed over n ≤ x with n ≡ a [MOD q] grows like x / φ q.

theorem Chebyshev.tendsto_psi_div_atTop : Filter.Tendsto (fun (x : ℝ) => psi x / x) Filter.atTop (nhds 1)

The prime number theorem, ψ form: ψ x / x → 1 as x → ∞, where ψ x = ∑ n ≤ x, Λ n is the Chebyshev function Chebyshev.psi.

theorem Chebyshev.isEquivalent_psi_id : Asymptotics.IsEquivalent Filter.atTop psi id

The prime number theorem, ψ form: ψ x ∼ x, where ψ x = ∑ n ≤ x, Λ n is the Chebyshev function Chebyshev.psi.

theorem Chebyshev.tendsto_theta_div_atTop : Filter.Tendsto (fun (x : ℝ) => theta x / x) Filter.atTop (nhds 1)

The prime number theorem, θ form: θ x / x → 1 as x → ∞, where θ x = ∑ p ≤ x, log p (over primes p) is the Chebyshev function Chebyshev.theta.

theorem Chebyshev.isEquivalent_theta_id : Asymptotics.IsEquivalent Filter.atTop theta id

The prime number theorem, θ form: θ x ~ x, where θ x = ∑ p ≤ x, log p (over primes p) is the Chebyshev function Chebyshev.theta.

theorem Chebyshev.tendsto_sum_log_prime_modEq_div_atTop {q a : ℕ} [NeZero q] (ha : a.Coprime q) : Filter.Tendsto (fun (x : ℝ) => (∑ p ∈ Finset.Ioc 0 ⌊x⌋₊ with Nat.Prime p ∧ p ≡ a [MOD q], Real.log ↑p) / x) Filter.atTop (nhds (↑q.totient)⁻¹)

The prime number theorem in arithmetic progressions, θ form. For a coprime to q, ∑ p ≤ x, p ≡ a [MOD q], log p (over primes p) is asymptotic to x / φ q.

theorem Chebyshev.exists_prime_of_theta_lt {a b : ℝ} (hab : theta a < theta b) : ∃ (p : ℕ), Nat.Prime p ∧ ↑p ∈ Set.Ioc a b

If the Chebyshev function θ is strictly larger at b than at a, then there is a prime in the half-open interval (a, b].

theorem Nat.isEquivalent_primeCounting : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => ↑⌊x⌋₊.primeCounting) fun (x : ℝ) => x / Real.log x

The prime number theorem: the prime counting function satisfies π x ~ x / Real.log x.

theorem Nat.tendsto_card_prime_modEq_mul_log_div_atTop {q a : ℕ} [NeZero q] (ha : a.Coprime q) : Filter.Tendsto (fun (x : ℝ) => ↑{p ∈ Finset.Ioc 0 ⌊x⌋₊ | Prime p ∧ p ≡ a [MOD q]}.card * Real.log x / x) Filter.atTop (nhds (↑q.totient)⁻¹)

The prime number theorem in arithmetic progressions: for a coprime to q, the number π(x; q, a) of primes p ≤ x with p ≡ a [MOD q] satisfies π(x; q, a) * log x / x → 1 / φ(q).

theorem Nat.isEquivalent_card_prime_modEq {q a : ℕ} [NeZero q] (ha : a.Coprime q) : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => ↑{p ∈ Finset.Ioc 0 ⌊x⌋₊ | Prime p ∧ p ≡ a [MOD q]}.card) fun (x : ℝ) => x / (↑q.totient * Real.log x)

The prime number theorem in arithmetic progressions: for a coprime to q, the number π(x; q, a) of primes p ≤ x with p ≡ a [MOD q] satisfies π(x; q, a) ~ x / (φ(q) log x).

theorem Nat.eventually_exists_prime_mem_Ioc {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∃ (p : ℕ), Prime p ∧ ↑p ∈ Set.Ioc x ((1 + ε) * x)

Small prime gaps. Let ε > 0. Then for every sufficiently large x, there exists a prime in the interval (x, (1 + ε) * x].

theorem Nat.eventually_exists_prime_mem_Ioc_sub {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∃ (p : ℕ), Prime p ∧ ↑p ∈ Set.Ioc ((1 - ε) * x) x

Small prime gaps, dual form. Let ε > 0. Then for every sufficiently large x, there exists a prime in the interval ((1 - ε) * x, x].

theorem Nat.isEquivalent_nth_prime_succ : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑(nth Prime (n + 1))) fun (n : ℕ) => ↑(nth Prime n)

Consecutive primes are asymptotically equal: the (n + 1)-th prime is asymptotic to the n-th prime.

theorem Nat.tendsto_log_lcmUpto_div_atTop : Filter.Tendsto (fun (n : ℕ) => Real.log ↑n.lcmUpto / ↑n) Filter.atTop (nhds 1)

Least common multiple asymptotics: Real.log (lcmUpto n) / n → 1.

theorem Nat.isEquivalent_log_lcmUpto_id : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => Real.log ↑n.lcmUpto) fun (x : ℕ) => ↑x

Least common multiple asymptotics: Real.log (lcmUpto n) ~ n.

theorem Nat.tendsto_log_primorial_div_atTop : Filter.Tendsto (fun (n : ℕ) => Real.log ↑(primorial n) / ↑n) Filter.atTop (nhds 1)

Primorial asymptotics: Real.log (primorial n) / n → 1.

theorem Nat.isEquivalent_log_primorial_id : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => Real.log ↑(primorial n)) fun (x : ℕ) => ↑x

Primorial asymptotics: Real.log (primorial n) ~ n.