Documentation

Mathlib.NumberTheory.Chebyshev

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 psi to theta.
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

Instances For

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 "ψ")

Instances For

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

Instances For

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 "θ")

Instances For

theorem Chebyshev.psi_nonneg (x : ℝ) :

theorem Chebyshev.theta_nonneg (x : ℝ) :

theorem Chebyshev.theta_pos {x : ℝ} (hy : 2 ≤ 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_zero :

psi 0 = 0

@[simp]

theorem Chebyshev.psi_one :

psi 1 = 0

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

@[simp]

theorem Chebyshev.theta_zero :

@[simp]

theorem Chebyshev.theta_one :

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 :

theorem Chebyshev.theta_mono :

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

Instances For

theorem Nat.lcmUpto_ne_zero (n : ℕ) :

n.lcmUpto ≠ 0

theorem Nat.lcmUpto_pos (n : ℕ) :

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 ∈ 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.

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

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)$.