Certified Chebyshev theta(N) Bounds

This module provides computable upper and lower bounds on the first Chebyshev function theta(N) = sum_{p prime, p in Ioc 0 N} log p.

Main definitions

• logPrimeUB n depth / logPrimeLB n depth — upper/lower bounds on the n-th summand of theta.
• thetaUB N depth / thetaLB N depth — upper/lower bounds on theta(N).
• checkThetaLeMulWith / checkAllThetaLeMulWith — decide thetaUB(N) ≤ slope * N.
• checkThetaAbsError / checkAllThetaAbsError — decide |theta(N) - N| ≤ bound (both directions).

Design notes

The structure mirrors ChebyshevPsi almost exactly. The difference is that summands are log p (only primes) instead of vonMangoldt n (prime powers). For the absolute-error checker we need both an upper and a lower bound on theta; the lower bound uses logPrimeLB (the .lo endpoint of the interval enclosure).

Computable upper and lower bounds on the theta summand

def LeanCert.Engine.ChebyshevTheta.logPrimeUB (n : ℕ) (depth : ℕ := 20) : ℚ

Computable upper bound on the theta summand at n. Returns (logPointComputable n depth).hi when n is prime, 0 otherwise.

Equations

• LeanCert.Engine.ChebyshevTheta.logPrimeUB n depth = if Nat.Prime n then (LeanCert.Core.IntervalRat.logPointComputable (↑n) depth).hi else 0

def LeanCert.Engine.ChebyshevTheta.logPrimeLB (n : ℕ) (depth : ℕ := 20) : ℚ

Computable lower bound on the theta summand at n. Returns (logPointComputable n depth).lo when n is prime, 0 otherwise.

Equations

• LeanCert.Engine.ChebyshevTheta.logPrimeLB n depth = if Nat.Prime n then (LeanCert.Core.IntervalRat.logPointComputable (↑n) depth).lo else 0

def LeanCert.Engine.ChebyshevTheta.thetaUB (N : ℕ) (depth : ℕ := 20) : ℚ

Computable upper bound on theta(N): thetaUB N depth = sum n in Ioc 0 N, logPrimeUB n depth.

Equations

• LeanCert.Engine.ChebyshevTheta.thetaUB N depth = ∑ n ∈ Finset.Ioc 0 N, LeanCert.Engine.ChebyshevTheta.logPrimeUB n depth

def LeanCert.Engine.ChebyshevTheta.thetaLB (N : ℕ) (depth : ℕ := 20) : ℚ

Computable lower bound on theta(N): thetaLB N depth = sum n in Ioc 0 N, logPrimeLB n depth.

Equations

• LeanCert.Engine.ChebyshevTheta.thetaLB N depth = ∑ n ∈ Finset.Ioc 0 N, LeanCert.Engine.ChebyshevTheta.logPrimeLB n depth

Correctness theorems

theorem LeanCert.Engine.ChebyshevTheta.log_prime_le_logPrimeUB (n depth : ℕ) : (if Nat.Prime n then Real.log ↑n else 0) ≤ ↑(logPrimeUB n depth)

The theta summand log p is bounded above by our computable bound for primes, and is zero (hence bounded) for non-primes.

theorem LeanCert.Engine.ChebyshevTheta.logPrimeLB_le_log_prime (n depth : ℕ) : ↑(logPrimeLB n depth) ≤ if Nat.Prime n then Real.log ↑n else 0

The theta summand is bounded below by our computable bound.

theorem LeanCert.Engine.ChebyshevTheta.theta_le_thetaUB (N depth : ℕ) : Chebyshev.theta ↑N ≤ ↑(thetaUB N depth)

theta(N) is bounded above by thetaUB(N).

theorem LeanCert.Engine.ChebyshevTheta.thetaLB_le_theta (N depth : ℕ) : ↑(thetaLB N depth) ≤ Chebyshev.theta ↑N

theta(N) is bounded below by thetaLB(N).

Decidable comparison infrastructure

theorem LeanCert.Engine.ChebyshevTheta.theta_le_of_thetaUB_le (N depth : ℕ) (slope : ℚ) (h : decide (thetaUB N depth ≤ slope) = true) : Chebyshev.theta ↑N ≤ ↑slope

If thetaUB(N, depth) <= slope computationally, then theta(N) <= slope.

Generic slope checker: theta(N) <= slope * N

def LeanCert.Engine.ChebyshevTheta.checkThetaLeMulWith (N : ℕ) (slope : ℚ) (depth : ℕ := 20) : Bool

Computable check: does thetaUB(N) <= slope * N hold?

Equations

• LeanCert.Engine.ChebyshevTheta.checkThetaLeMulWith N slope depth = decide (LeanCert.Engine.ChebyshevTheta.thetaUB N depth ≤ slope * ↑N)

theorem LeanCert.Engine.ChebyshevTheta.theta_le_of_checkThetaLeMulWith (N depth : ℕ) (slope : ℚ) (h : checkThetaLeMulWith N slope depth = true) : Chebyshev.theta ↑N ≤ ↑slope * ↑N

If checkThetaLeMulWith N slope depth holds, then theta(N) <= slope * N.

Absolute error checker: |theta(N) - N| <= bound

def LeanCert.Engine.ChebyshevTheta.checkThetaAbsError (N : ℕ) (bound : ℚ) (depth : ℕ := 20) : Bool

Computable check for |theta(N) - N| <= bound. Checks both thetaUB(N) - N <= bound and N - thetaLB(N) <= bound.

Equations

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

theorem LeanCert.Engine.ChebyshevTheta.abs_theta_sub_le_of_checkThetaAbsError (N depth : ℕ) (bound : ℚ) (h : checkThetaAbsError N bound depth = true) : |Chebyshev.theta ↑N - ↑N| ≤ ↑bound

If checkThetaAbsError N bound depth holds, then |theta(N) - N| <= bound.

Efficient incremental checkers (O(N) for native_decide)

def LeanCert.Engine.ChebyshevTheta.thetaUBPrefix (n depth : ℕ) : ℚ

Helper: thetaUB for the prefix 1..n-1.

Equations

• LeanCert.Engine.ChebyshevTheta.thetaUBPrefix n depth = ∑ i ∈ Finset.Ioc 0 (n - 1), LeanCert.Engine.ChebyshevTheta.logPrimeUB i depth

def LeanCert.Engine.ChebyshevTheta.checkAllThetaLeMulWith (bound : ℕ) (slope : ℚ) (depth : ℕ := 20) : Bool

Efficient O(N) incremental checker for thetaUB(N) <= slope * N for all N = 1..bound.

Equations

• LeanCert.Engine.ChebyshevTheta.checkAllThetaLeMulWith bound slope depth = LeanCert.Engine.ChebyshevTheta.checkAllThetaLeMulWith.go bound slope depth 1 0

@[irreducible]

def LeanCert.Engine.ChebyshevTheta.checkAllThetaLeMulWith.go (bound : ℕ) (slope : ℚ) (depth n : ℕ) (acc : ℚ) : Bool

Equations

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

Bridge: checkAllThetaLeMulWith.go → checkThetaLeMulWith

theorem LeanCert.Engine.ChebyshevTheta.checkAllThetaLeMulWith_implies_checkThetaLeMulWith (bound : ℕ) (slope : ℚ) (depth : ℕ) (h : checkAllThetaLeMulWith bound slope depth = true) (N : ℕ) (hN : 0 < N) (hNb : N ≤ bound) : checkThetaLeMulWith N slope depth = true

If checkAllThetaLeMulWith bound slope depth returns true, then checkThetaLeMulWith N slope depth is true for all N in {1, ..., bound}.

Efficient incremental absolute-error checker

def LeanCert.Engine.ChebyshevTheta.checkAllThetaAbsError (limit : ℕ) (bound : ℚ) (depth : ℕ := 20) : Bool

Efficient O(N) incremental checker for |theta(N) - N| <= bound for all N = 1..limit. Maintains both an upper-bound and a lower-bound accumulator.

Equations

• LeanCert.Engine.ChebyshevTheta.checkAllThetaAbsError limit bound depth = LeanCert.Engine.ChebyshevTheta.checkAllThetaAbsError.go limit bound depth 1 0 0

@[irreducible]

def LeanCert.Engine.ChebyshevTheta.checkAllThetaAbsError.go (limit : ℕ) (bound : ℚ) (depth n : ℕ) (accUB accLB : ℚ) : Bool

Equations

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

Bridge: checkAllThetaAbsError.go → checkThetaAbsError

theorem LeanCert.Engine.ChebyshevTheta.checkAllThetaAbsError_implies_checkThetaAbsError (limit : ℕ) (bound : ℚ) (depth : ℕ) (h : checkAllThetaAbsError limit bound depth = true) (N : ℕ) (hN : 0 < N) (hNb : N ≤ limit) : checkThetaAbsError N bound depth = true

If checkAllThetaAbsError limit bound depth returns true, then checkThetaAbsError N bound depth is true for all N in {1, ..., limit}.

Relative error checker: |theta(N) - N| / N <= bound, i.e. |theta(N) - N| <= bound * N

This is what Eθ(x) ≤ bound means in the PNT+ blueprint (Definition 2.0.7).

def LeanCert.Engine.ChebyshevTheta.checkThetaRelError (N : ℕ) (bound : ℚ) (depth : ℕ := 20) : Bool

Computable check for |theta(N) - N| <= bound * N. Checks thetaUB(N) <= (1 + bound) * N and thetaLB(N) >= (1 - bound) * N.

Equations

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

theorem LeanCert.Engine.ChebyshevTheta.abs_theta_sub_le_mul_of_checkThetaRelError (N depth : ℕ) (bound : ℚ) (h : checkThetaRelError N bound depth = true) : |Chebyshev.theta ↑N - ↑N| ≤ ↑bound * ↑N

If checkThetaRelError N bound depth holds, then |theta(N) - N| <= bound * N.

def LeanCert.Engine.ChebyshevTheta.checkAllThetaRelError (start limit : ℕ) (bound : ℚ) (depth : ℕ := 20) : Bool

Efficient O(N) incremental checker for |theta(N) - N| <= bound * N for all N = start..limit. The start parameter allows skipping small N (e.g. start=3 for the range 2 < x ≤ 599).

Equations

• LeanCert.Engine.ChebyshevTheta.checkAllThetaRelError start limit bound depth = LeanCert.Engine.ChebyshevTheta.checkAllThetaRelError.go start limit bound depth 1 0 0

@[irreducible]

def LeanCert.Engine.ChebyshevTheta.checkAllThetaRelError.go (start limit : ℕ) (bound : ℚ) (depth n : ℕ) (accUB accLB : ℚ) : Bool

Equations

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

Bridge: checkAllThetaRelError.go → checkThetaRelError

theorem LeanCert.Engine.ChebyshevTheta.checkAllThetaRelError_implies_checkThetaRelError (start limit : ℕ) (bound : ℚ) (depth : ℕ) (h : checkAllThetaRelError start limit bound depth = true) (N : ℕ) (hN : 0 < N) (hN_start : start ≤ N) (hNb : N ≤ limit) : checkThetaRelError N bound depth = true

If checkAllThetaRelError start limit bound depth returns true, then checkThetaRelError N bound depth holds for all N in {start, ..., limit}.

Strengthened checker for real-valued Eθ

For real x ∈ [N, N+1), θ(x) = θ(N) but x can be as large as N+1-ε. The upper-bound direction still works from the integer check (worst at x = N), but the lower bound requires the strengthened condition θ(N) ≥ (1-a)·(N+1).

At the last integer N = limit we only need the regular check (x ≤ limit).

def LeanCert.Engine.ChebyshevTheta.checkThetaRelErrorReal (N : ℕ) (bound : ℚ) (depth : ℕ := 20) : Bool

Strengthened check for one integer N, covering all real x ∈ [N, N+1):

• upper: thetaUB(N) ≤ (1 + bound) * N
• lower: thetaLB(N) ≥ (1 - bound) * (N + 1)

Equations

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

theorem LeanCert.Engine.ChebyshevTheta.abs_theta_sub_le_mul_of_checkThetaRelErrorReal (N depth : ℕ) (bound : ℚ) (hbound : 0 ≤ bound) (hbound1 : bound ≤ 1) (h : checkThetaRelErrorReal N bound depth = true) (x : ℝ) (hxlo : ↑N ≤ x) (hxhi : x < ↑N + 1) : |Chebyshev.theta x - x| ≤ ↑bound * x

If checkThetaRelErrorReal N bound depth holds, then for all real x ∈ [N, N+1), |θ(x) - x| ≤ bound * x.

def LeanCert.Engine.ChebyshevTheta.checkAllThetaRelErrorReal (start limit : ℕ) (bound : ℚ) (depth : ℕ := 20) : Bool

Efficient O(N) incremental checker for the strengthened real-valued condition. For N = start .. limit-1: checks checkThetaRelErrorReal N bound depth (covers x ∈ [N, N+1)) For N = limit: checks checkThetaRelError N bound depth (covers only x = limit)

Equations

• LeanCert.Engine.ChebyshevTheta.checkAllThetaRelErrorReal start limit bound depth = LeanCert.Engine.ChebyshevTheta.checkAllThetaRelErrorReal.go start limit bound depth 1 0 0

@[irreducible]

def LeanCert.Engine.ChebyshevTheta.checkAllThetaRelErrorReal.go (start limit : ℕ) (bound : ℚ) (depth n : ℕ) (accUB accLB : ℚ) : Bool

Equations

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

Bridge: checkAllThetaRelErrorReal → pointwise

theorem LeanCert.Engine.ChebyshevTheta.checkAllThetaRelErrorReal_implies (start limit : ℕ) (bound : ℚ) (depth : ℕ) (h : checkAllThetaRelErrorReal start limit bound depth = true) (N : ℕ) (hN : 0 < N) (hN_start : start ≤ N) (hNb : N ≤ limit) : (if N < limit then checkThetaRelErrorReal N bound depth else checkThetaRelError N bound depth) = true

If checkAllThetaRelErrorReal start limit bound depth returns true, then:

• for N ∈ {start, ..., limit-1}: checkThetaRelErrorReal N bound depth holds
• for N = limit: checkThetaRelError N bound depth holds