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 θ

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 each other and 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.