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
• Chebyshev.lcmUpto n gives the least common multiple of {1,...,n}

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.theta_ge gives Chebyshev's lower bound on θ.
• Chebyshev.psi_eq_log_lcmUpto shows that ψ n is the log of the lcm of {1,...,n}.
• Chebyshev.psi_eq_sum_theta and Chebyshev.psi_eq_theta_add_sum_theta relate ψ to θ.
• Chebyshev.psi_sub_theta_le_mul_sqrt gives an upper bound on ψ - θ.
• Chebyshev.psi_sub_theta_le_psi_add_psi_add_psi and Chebyshev.psi_sub_theta_ge_psi_add_psi_add_psi establish the Costa-Pereira inequalities for ψ - θ.
• Chebyshev.psi_le_const_mul_self gives Chebyshev's upper bound on ψ.
• Chebyshev.psi_ge gives Chebyshev's lower bound on ψ.
• Chebyshev.primeCounting_eq_theta_div_log_add_integral relates the prime counting function to θ
• Chebyshev.eventually_primeCounting_le gives an asymptotic upper bound on the prime counting function.
• Chebyshev.pi_le_log4_mul_div gives an explicit upper bound on the prime counting function.
• Chebyshev.pi_ge gives an explicit lower 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.

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.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.theta_eq_sum_primesLE (x : ℝ) : theta x = ∑ p ∈ ⌊x⌋₊.primesLE, Real.log ↑p

theorem Chebyshev.theta_eq_sum_primesLE_log (n : ℕ) : theta ↑n = ∑ p ∈ n.primesLE, Real.log ↑p

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

@[simp]

theorem Chebyshev.psi_eq_zero_iff {x : ℝ} : psi x = 0 ↔ x < 2

theorem Chebyshev.psi_eq_zero_of_le_one {x : ℝ} (hx : x ≤ 1) : psi x = 0

@[simp]

theorem Chebyshev.psi_zero : psi 0 = 0

@[simp]

theorem Chebyshev.psi_one : psi 1 = 0

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

@[simp]

theorem Chebyshev.theta_eq_zero_iff {x : ℝ} : theta x = 0 ↔ x < 2

theorem Chebyshev.theta_eq_zero_of_le_one {x : ℝ} (hx : x ≤ 1) : theta x = 0

@[simp]

theorem Chebyshev.theta_zero : theta 0 = 0

@[simp]

theorem Chebyshev.theta_one : theta 1 = 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.

Least common multiple of {1,...,n}

Basic facts about the least common multiple of the first n natural numbers

def Nat.lcmUpto (n : ℕ) : ℕ

Least common multiple of Icc 1 n.

Equations

• n.lcmUpto = (Finset.Icc 1 n).lcm id

theorem Nat.lcmUpto_ne_zero (n : ℕ) : n.lcmUpto ≠ 0

theorem Nat.lcmUpto_pos (n : ℕ) : 0 < n.lcmUpto

theorem Nat.factorization_lcmUpto (n : ℕ) {p : ℕ} (hp : Prime p) : n.lcmUpto.factorization p = log p n

theorem Nat.lcmUpto_dvd_factorial (n : ℕ) : n.lcmUpto ∣ n.factorial

theorem Nat.primeFactors_lcmUpto (n : ℕ) : n.lcmUpto.primeFactors = n.primesLE

theorem Nat.primorial_dvd_lcmUpto (n : ℕ) : primorial n ∣ n.lcmUpto

theorem Nat.lcmUpto_eq_prod (n : ℕ) : n.lcmUpto = ∏ p ∈ n.primesLE, p ^ n.lcmUpto.factorization p

theorem Nat.lcmUpto_eq_prod_pow_log (n : ℕ) : n.lcmUpto = ∏ p ∈ n.primesLE, p ^ log p n

theorem Nat.lcmUpto_eq_prod_pow_floor (n : ℕ) : n.lcmUpto = ∏ p ∈ n.primesLE, p ^ ⌊Real.log ↑n / Real.log ↑p⌋₊

theorem Chebyshev.psi_eq_sum_mul_log_prime (n : ℕ) : psi ↑n = ∑ p ∈ n.primesLE, ↑(Nat.log p n) * Real.log ↑p

theorem Chebyshev.psi_le_primeCounting_mul_log (n : ℕ) : psi ↑n ≤ ↑n.primeCounting * Real.log ↑n

theorem Chebyshev.psi_le_primeCounting_mul_log' (x : ℝ) : psi x ≤ ↑⌊x⌋₊.primeCounting * Real.log x

theorem Chebyshev.psi_eq_log_lcmUpto (n : ℕ) : psi ↑n = Real.log ↑n.lcmUpto

ψ n is the logarithm of lcmUpto n.

theorem Chebyshev.choose_dvd_lcmUpto {n k : ℕ} (hkn : k ≤ n) : n.choose k ∣ n.lcmUpto

lcmUpto n is divisible by choose n k for all k ≤ n

theorem Chebyshev.two_pow_le_mul_lcmUpto (n : ℕ) : 2 ^ n ≤ (n + 1) * n.lcmUpto

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 : ℕ} (hN : ⌊Real.log x / Real.log 2⌋₊ ≤ N) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n = ∑ k ∈ Finset.Icc 1 N, ∑ 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.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)

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

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) {N : ℕ} (hN : ⌊Real.log x / Real.log 2⌋₊ ≤ N) : psi x = theta x + ∑ n ∈ Finset.Icc 2 N, 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. To remove the log, see psi_sub_theta_le_mul_sqrt.

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.

theorem Chebyshev.psi_ge (n : ℕ) : ↑n * Real.log 2 - Real.log (↑n + 1) ≤ psi ↑n

The Chebyshev lower bound for ψ.

theorem Chebyshev.psi_ge' {x : ℝ} (hx : 0 ≤ x) : (x - 1) * Real.log 2 - Real.log (x + 2) ≤ psi x

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

theorem Chebyshev.theta_ge (n : ℕ) : ↑n * Real.log 2 - Real.log (↑n + 1) - 2 * √↑n * Real.log ↑n ≤ theta ↑n

The Chebyshev lower bound for θ.

theorem Chebyshev.theta_ge' {x : ℝ} (hx : 1 ≤ x) : (x - 1) * Real.log 2 - Real.log (x + 2) - 2 * √x * Real.log x ≤ theta x

The Costa-Pereira inequalities

The Costa-Pereira inequalities give explicit upper and lower bounds on the difference ψ x - θ x, namely that they lie between ψ x^(1/2) + ψ x^(1/3) + ψ x^(1/7) and ψ x^(1/2) + ψ x^(1/3) + ψ x^(1/5). These are useful for applications in explicit analytic number theory.

theorem Chebyshev.psi_sub_theta_le_psi_add_psi_add_psi (x : ℝ) : psi x - theta x ≤ psi (x ^ 2⁻¹) + psi (x ^ 3⁻¹) + psi (x ^ 5⁻¹)

theorem Chebyshev.psi_sub_theta_ge_psi_add_psi_add_psi {x : ℝ} (hx : 0 ≤ x) : psi (x ^ 2⁻¹) + psi (x ^ 3⁻¹) + psi (x ^ 7⁻¹) ≤ psi x - theta x

theorem Chebyshev.psi_sub_theta_le_mul_sqrt : ∃ (C : ℝ), ∀ (x : ℝ), psi x - theta x ≤ C * √x

ψ x = θ x + O( √x ).

theorem Chebyshev.isBigO_psi_sub_theta_sqrt : (psi - theta) =O[Filter.atTop] Real.sqrt

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.theta_eq_primeCounting_mul_log_sub_integral {x : ℝ} (hx : 2 ≤ x) : theta x = ↑⌊x⌋₊.primeCounting * Real.log x - ∫ (t : ℝ) in 2..x, ↑⌊t⌋₊.primeCounting / t

Expresses the Chebyshev theta 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

theorem Chebyshev.pi_ge (n : ℕ) : (↑n * Real.log 2 - Real.log (↑n + 1)) / Real.log ↑n ≤ ↑n.primeCounting

theorem Chebyshev.pi_ge' {x : ℝ} (hx : 1 < x) : ((x - 1) * Real.log 2 - Real.log (x + 2)) / Real.log x ≤ ↑⌊x⌋₊.primeCounting

theorem Chebyshev.theta_le_pi_mul_log (n : ℕ) : theta ↑n ≤ ↑n.primeCounting * Real.log ↑n

theorem Chebyshev.theta_le_pi_mul_log' (x : ℝ) : theta x ≤ ↑⌊x⌋₊.primeCounting * Real.log x

theorem Chebyshev.pi_le_log4_mul_div {x : ℝ} (hx : 1 < x) : ↑⌊x⌋₊.primeCounting ≤ Real.log 4 * x / Real.log √x + √x

A weak but completely explicit upper bound on $\pi(x)$.

def Mathlib.Meta.Positivity.evalTheta : PositivityExt

Extension for the positivity tactic: the first Chebyshev function is nonnegative.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.Positivity.evalPsi : PositivityExt

Extension for the positivity tactic: the second Chebyshev function is nonnegative.

Equations

• One or more equations did not get rendered due to their size.