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.
• Chevyshev.psi_le_const_mul_self gives Chebyshev's upper bound on ψ.

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

• Upstream the results relating theta and psi to the prime counting function.
• Prove Chebyshev's lower bound.

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

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

Equations

• Chebyshev.psi x = ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, ArithmeticFunction.vonMangoldt n

def Chebyshev.termψ : Lean.ParserDescr

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

Equations

• Chebyshev.termψ = Lean.ParserDescr.node `Chebyshev.termψ 1024 (Lean.ParserDescr.symbol "ψ")

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

The sum of log p over primes p ≤ x.

Equations

• Chebyshev.theta x = ∑ p ∈ Finset.Ioc 0 ⌊x⌋₊ with Nat.Prime p, Real.log ↑p

def Chebyshev.termθ : Lean.ParserDescr

The sum of log p over primes p ≤ x.

Equations

• Chebyshev.termθ = Lean.ParserDescr.node `Chebyshev.termθ 1024 (Lean.ParserDescr.symbol "θ")

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

theorem Chebyshev.theta_nonneg (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 √ 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

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.