Chebyshev function bounds

TheoremChebyshev's explicit bounds for the theta function#✓fully proved

Let \(\theta(x) = \sum_{p \le x} \log p\), the sum running over primes, and let

\[A = \log \frac{2^{1/2} \, 3^{1/3} \, 5^{1/5}}{30^{1/30}}.\]

Then for every real \(x > 1\),

\[\theta(x) < \frac{6}{5}Ax - A\sqrt{x} + \frac{5}{4\log 6}(\log x)^2 + \frac{5}{2}\log x + 2\]

and

\[\theta(x) > Ax - \frac{12}{5}A\sqrt{x} - \frac{5}{8\log 6}(\log x)^2 - \frac{15}{4}\log x - 3.\]
public theorem chebyshev_theta_explicit_bounds (x : ℝ) (hx : 1 < x) :
    let A : ℝ :=
      Real.log (((2 : ℝ) ^ ((1 / 2 : ℝ)) * (3 : ℝ) ^ ((1 / 3 : ℝ)) *
        (5 : ℝ) ^ ((1 / 5 : ℝ))) / (30 : ℝ) ^ ((1 / 30 : ℝ)));
    Chebyshev.theta x <
      (6 / 5 : ℝ) * A * x - A * Real.sqrt x +
      (5 / (4 * Real.log 6)) * (Real.log x) ^ 2 +
      (5 / 2 : ℝ) * Real.log x + 2 ∧
    Chebyshev.theta x >
      A * x - (12 / 5 : ℝ) * A * Real.sqrt x -
      (5 / (8 * Real.log 6)) * (Real.log x) ^ 2 -
      (15 / 4 : ℝ) * Real.log x - 3
Sources
  • S. Nazardonyavi and S. Yakubovich, "Extremely Abundant Numbers and the Riemann Hypothesis," Journal of Integer Sequences 17 (2014), Article 14.2.8, Lemma citing Chebyshev p. 379, lines 288-298, https://cs.uwaterloo.ca/journals/JIS/VOL17/Nazar/nazar4.tex; original result: P. L. Chebyshev's memoir on prime numbers.

TheoremChebyshev's lower bound for the theta function#✓fully proved

Let \(\theta(x) = \sum_{p \le x} \log p\), the sum running over primes, be the first Chebyshev function. Then \(\theta(x) > x/3\) for every real \(x \ge 3\).

theorem chebyshev_theta_gt_one_third
    (x : ℝ) (hx : 3 ≤ x) :
    x / 3 < Chebyshev.theta x
Sources
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.