Rosser–Schoenfeld: $|\vartheta(y)-y|<y/(2\log y)$ for $y\ge 563$

Let $\vartheta(y)=\sum_{p\le y}\log p$ be Chebyshev's function, where the sum runs over the primes $p\le y$ and $\log$ is the natural logarithm. For every real $y\ge563$,

This is an explicit form of the prime number theorem, $\vartheta(y)\sim y$, with an error term of size $y/(2\log y)$ valid from $y=563$ onward. Harvey and van der Hoeven use it to prove Lemma 5.1, which finds many primes in short intervals $\big((1-2\eta)x,(1-\eta)x\big]$. Those primes are the transform lengths in their $O(n\log n)$ multiplication algorithm.

Formalization Note $\vartheta$ is Mathlib's Chebyshev.theta. The statement is the two-sided bound for $y\ge563$ exactly as Harvey and van der Hoeven quote it from Rosser–Schoenfeld (1962), Theorem 4, in the proof of their Lemma 5.1. Rosser and Schoenfeld's original theorem may state the two inequalities with different ranges of validity. Any such version implies this one on $y\ge563$.