Chebyshev functions

This file defines the Chebyshev functions theta and psi. These give logarithmically weighted sums of primes and prime powers.

Main definitions

• Chebyshev.psi gives the sum of ArithmeticFunction.vonMangoldt
• Chebyshev.theta gives the sum of log p over primes

Main results

• Chebyshev.theta_eq_log_primorial shows that θ x is the log of the product of primes up to x
• Chebyshev.theta_le_log4_mul_x gives Chebyshev's upper bound on θ
• Chebyshev.psi_eq_sum_theta and Chebyshev.psi_eq_theta_add_sum_theta relate psi to theta.
• Chebyshev.psi_le_const_mul_self gives Chebyshev's upper bound on ψ.
• Chebyshev.primeCounting_eq_theta_div_log_add_integral relates the prime counting function to θ
• Chebyshev.eventually_primeCounting_le gives an upper bound on the prime counting function.

Notation

We introduce the scoped notations θ and ψ in the Chebyshev namespace for the Chebyshev functions.

References

Parts of this file were upstreamed from the PrimeNumberTheoremAnd project by Kontorovich et al, https://github.com/alexKontorovich/PrimeNumberTheoremAnd.

TODOS

• Prove Chebyshev's lower bound.

noncomputable def Chebyshev.psi (x : ℝ) : ℝ

The sum of ArithmeticFunction.vonMangoldt over integers n ≤ x.

def Chebyshev.termψ : Lean.ParserDescr

The sum of ArithmeticFunction.vonMangoldt over integers n ≤ x.

noncomputable def Chebyshev.theta (x : ℝ) : ℝ

The sum of log p over primes p ≤ x.

def Chebyshev.termθ : Lean.ParserDescr

The sum of log p over primes p ≤ x.

theorem Chebyshev.psi_nonneg (x : ℝ) : 0 ≤ psi x

theorem Chebyshev.theta_nonneg (x : ℝ) : 0 ≤ theta x

theorem Chebyshev.theta_pos {x : ℝ} (hy : 2 ≤ x) : 0 < theta x

theorem Chebyshev.psi_eq_sum_Icc (x : ℝ) : psi x = ∑ n ∈ Finset.Icc 0 ⌊x⌋₊, ArithmeticFunction.vonMangoldt n

theorem Chebyshev.theta_eq_sum_Icc (x : ℝ) : theta x = ∑ p ∈ Finset.Icc 0 ⌊x⌋₊ with Nat.Prime p, Real.log ↑p

theorem Chebyshev.psi_eq_zero_of_lt_two {x : ℝ} (hx : x < 2) : psi x = 0

theorem Chebyshev.theta_eq_zero_of_lt_two {x : ℝ} (hx : x < 2) : theta x = 0

theorem Chebyshev.psi_eq_psi_coe_floor (x : ℝ) : psi x = psi ↑⌊x⌋₊

theorem Chebyshev.theta_eq_theta_coe_floor (x : ℝ) : theta x = theta ↑⌊x⌋₊

theorem Chebyshev.psi_mono : Monotone psi

theorem Chebyshev.theta_mono : Monotone theta

theorem Chebyshev.theta_eq_log_primorial (x : ℝ) : theta x = Real.log ↑(primorial ⌊x⌋₊)

θ x is the log of the product of the primes up to x.

theorem Chebyshev.theta_le_log4_mul_x {x : ℝ} (hx : 0 ≤ x) : theta x ≤ Real.log 4 * x

Chebyshev's upper bound: θ x ≤ c x with the constant c = log 4.

Relating ψ and θ

We isolate the contributions of different prime powers to ψ and use this to show that ψ and θ are close.

theorem Chebyshev.sum_PrimePow_eq_sum_sum {R : Type u_1} [AddCommMonoid R] (f : ℕ → R) {x : ℝ} (hx : 0 ≤ x) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n = ∑ k ∈ Finset.Icc 1 ⌊Real.log x / Real.log 2⌋₊, ∑ p ∈ Finset.Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)

A sum over prime powers may be written as a double sum over exponents and then primes.

theorem Chebyshev.psi_eq_sum_theta {x : ℝ} (hx : 0 ≤ x) : psi x = ∑ n ∈ Finset.Icc 1 ⌊Real.log x / Real.log 2⌋₊, theta (x ^ (1 / ↑n))

theorem Chebyshev.psi_eq_theta_add_sum_theta {x : ℝ} (hx : 2 ≤ x) : psi x = theta x + ∑ n ∈ Finset.Icc 2 ⌊Real.log x / Real.log 2⌋₊, theta (x ^ (1 / ↑n))

theorem Chebyshev.theta_le_psi (x : ℝ) : theta x ≤ psi x

theorem Chebyshev.abs_psi_sub_theta_le_sqrt_mul_log {x : ℝ} (hx : 1 ≤ x) : |psi x - theta x| ≤ 2 * √x * Real.log x

|ψ x - θ x| ≤ c √ x log x with an explicit constant c.

theorem Chebyshev.psi_le {x : ℝ} (hx : 1 ≤ x) : psi x ≤ Real.log 4 * x + 2 * √x * Real.log x

Explicit upper bound on ψ.

theorem Chebyshev.psi_le_const_mul_self {x : ℝ} (hx : 0 ≤ x) : psi x ≤ (Real.log 4 + 4) * x

Chebyshev's bound ψ x ≤ c x with an explicit constant. Note that Chebyshev.psi_le gives a sharper bound with a better main term.

theorem Chebyshev.psi_sub_theta_eq_sum_not_prime (x : ℝ) : psi x - theta x = ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊ with ¬Nat.Prime n, ArithmeticFunction.vonMangoldt n

ψ - θ is the sum of Λ over non-primes.

Relation to prime counting

We relate θ to the prime counting function π.

theorem Chebyshev.integrableOn_theta_div_id_mul_log_sq (x : ℝ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => theta t / (t * Real.log t ^ 2)) (Set.Icc 2 x) MeasureTheory.volume

Integrability for the integral in Chebyshev.primeCounting_eq_theta_div_log_add_integral.

theorem Chebyshev.primeCounting_eq_theta_div_log_add_integral {x : ℝ} (hx : 2 ≤ x) : ↑⌊x⌋₊.primeCounting = theta x / Real.log x + ∫ (t : ℝ) in 2..x, theta t / (t * Real.log t ^ 2)

Expresses the prime counting function π in terms of θ by using Abel summation.

theorem Chebyshev.intervalIntegrable_one_div_log_sq {a b : ℝ} (one_lt_a : 1 < a) (one_lt_b : 1 < b) : IntervalIntegrable (fun (x : ℝ) => 1 / Real.log x ^ 2) MeasureTheory.volume a b

theorem Chebyshev.integral_one_div_log_sq_isBigO : (fun (x : ℝ) => ∫ (t : ℝ) in 2..x, 1 / Real.log t ^ 2) =O[Filter.atTop] fun (x : ℝ) => x / Real.log x ^ 2

theorem Chebyshev.integral_theta_div_log_sq_isBigO : (fun (x : ℝ) => ∫ (t : ℝ) in 2..x, theta t / (t * Real.log t ^ 2)) =O[Filter.atTop] fun (x : ℝ) => x / Real.log x ^ 2

Bound on the integral in Chebyshev.primeCounting_eq_theta_div_log_add_integral.

theorem Chebyshev.integral_theta_div_log_sq_isLittleO : (fun (x : ℝ) => ∫ (t : ℝ) in 2..x, theta t / (t * Real.log t ^ 2)) =o[Filter.atTop] fun (x : ℝ) => x / Real.log x

theorem Chebyshev.primeCounting_sub_theta_div_log_isBigO : (fun (x : ℝ) => ↑⌊x⌋₊.primeCounting - theta x / Real.log x) =O[Filter.atTop] fun (x : ℝ) => x / Real.log x ^ 2

theorem Chebyshev.eventually_primeCounting_le {ε : ℝ} (εpos : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ↑⌊x⌋₊.primeCounting ≤ (Real.log 4 + ε) * x / Real.log x

Chebyshev's upper bound on the prime counting function