Research proof index

For the Selberg sieve that removes primes up to $z$ from an interval $[x,x+y]$, with $x,y>0$ and $z\ge1$, the remainder in the expected count of multiples of every nonzero integer $d$ is uniformly bounded: $|r_d|\le5$.

Suppose sequences $f,g:\mathbb N\to\mathbb R$ satisfy $f(n)=O(g(n))$ as $n\to\infty$, and $f(n)=0$ whenever $g(n)=0$. Then a single constant bounds $|f(n)|$ by that constant times $|g(n)|$ for every natural number $n$, not only for all sufficiently large $n$.

An explicit upper bound for the number of primes below $N$: $|\{p<N:p\text{ is prime}\}|\le \frac{4N}{\log N}+6\sqrt N\left(1+\frac12\log N\right)^3.$ The formal statement also covers the small values of $N$ using Lean's totalized real operations.