The prime number theorem states that $\lim_{x \rightarrow \infty} \pi(x)/Li(x) = 1$, if we denote $\pi(x) := \sum_{p \le x} 1$ for the prime counting function and $Li(x) = \int_2^x \frac{ dt}{\log t}$ for the logarithmic integral.
Since we are integrating the function $1/\log t$ to get $Li(x)$, we may informally interpret the above statement as prime numbers having density $1/\log x$ around each number $x > 0$. I'm curious of the sharpest rigorous formulation of this insight. One formulation of this would be to find the smallest function $a(x)$ so that: $$\lim_{x \rightarrow \infty} \frac{\pi(x) - \pi(x-a)}{Li(x) - Li(x-a)} = 1$$
If there is a more illuminating / alternative existing result that distills the above intuition, please let me know too!
Here is a proof that $a(x) = \sqrt x (\log x)^3$ satisfies the above criterion, if the Riemann hypothesis (RH) is true.
Under the RH, Schoenfeld showed that $|\pi(x) - Li(x)| < \sqrt{x} \log x$ (There is a sharper version that comes with the constant $\frac 1{8\pi}$ and $x>2700$ but I'll use this simpler version here, which I read to be true). Then for $a(x) = \sqrt x (\log x)^3$, we have: \begin{align*} & |(\pi(x)-\pi(x-a)) - (Li(x) - Li(x-a))| \\ =& |(\pi(x)-Li(x)) - (\pi(x-a) - Li(x-a))| \\ <& |\pi(x)-Li(x))| + |\pi(x-a) - Li(x-a)| \\ <& 2 \sqrt x \log x \end{align*} (here $a = a(x)$) Then we note that: $$\frac{2\sqrt x \log x }{Li(x) - Li(x-a)} < \frac{2\sqrt x \log x }{a / \log x} = \frac{2 \sqrt x \log x}{\sqrt x (\log x)^2} = \frac{2}{\log x}$$ so that \begin{align*} & \frac{|(\pi(x)-\pi(x-a)) - (Li(x) - Li(x-a))|}{Li(x) - Li(x-a)} < \frac{2}{\log x} \\ \implies & \lim_{x \rightarrow \infty} \frac{\pi(x)-\pi(x-a)}{Li(x) - Li(x-a)} = 1 \end{align*}
Remark. Even though $\lim_{x \rightarrow \infty} \frac{\sqrt x (\log x)^3}{x} = 0$, in fact $\sqrt x (\log x)^3$ is larger than $x$ even for $x = 10^7$, although the inequality is reversed for $x = 10^8$. In view of this, we can instead say that $a(x) = x^{\frac12 + \epsilon}$ works for every $\epsilon>0$ too, and also we are free to use any $x$ in this case.