Rosser--Schoenfeld theta lower bound: high range, final sub-shard 504
ProvedTaoFivePrimes.rosser_schoenfeld_theta_lower_finite_large_high_cert504analytic-number-theorychebyshev-functionsnumber-theoryprimes
For every integer with , , and the certificate's accumulated bound satisfies ; the hypothesis is the quantitative carry handed on by the previous shard. This is a final sub-shard of the finite endpoint certificate of the high sub-range in Rosser and Schoenfeld's Theorem 19.
Preamble
import Mathlib.NumberTheory.Chebyshev
Formal statement
namespace TaoFivePrimes
theorem rosser_schoenfeld_theta_lower_finite_large_high_cert504
(hbase : (109361633821191791334 : Real) / 2 ^ 40 <= Chebyshev.theta (99477217 : Real))
(n : Nat) (h1 : 99477217 <= n) (h2 : n <= 99999999) :
(((n : Real) + 1) - 2 * Real.sqrt ((n : Real) + 1) <= Chebyshev.theta (n : Real)) /\
((109937568534278953594 : Real) / 2 ^ 40 <= Chebyshev.theta (100000000 : Real)) := by sorry
end TaoFivePrimesSource
J. B. Rosser and L. Schoenfeld, Approximate formulas for some functions of prime numbers, Illinois J. Math. 6 (1962), Theorem 19, p. 82, eq. (4.6), https://doi.org/10.1215/ijm/1255631807 (finite integer endpoint certificate, high sub-range 10^6 <= n <= 10^8, final split)