Does the interval $(a,11a/5]$ always contain at least $\lfloor\sqrt a\rfloor$ primes?

I observed experimentally that for every positive integer $a$, the interval

$$ (a,11a/5] $$

seems to contain at least $\lfloor\sqrt a\rfloor$ primes.

Equivalently, if $\pi(x)$ denotes the prime-counting function, the claim is

$$ \pi(11a/5)-\pi(a)\ge \lfloor\sqrt a\rfloor $$

for every positive integer $a$.

I believe the following gives an unconditional proof.

Theorem. For every positive integer $a$,

$$ \pi(11a/5)-\pi(a)\ge \lfloor\sqrt a\rfloor. $$

Thus $(a,11a/5]$ contains at least $\lfloor\sqrt a\rfloor$ primes.

Here $\log$ denotes the natural logarithm.

Proof

I use Theorem 6.9 of Pierre Dusart, Estimates of Some Functions Over Primes without R.H. (2010), arXiv:1002.0442, which gives

$$\pi(x)\ge \frac{x}{\log x}\left(1+\frac1{\log x}\right)$$

for $x>599$, and

$$\pi(x)\le \frac{x}{\log x}\left(1+\frac{1.2762}{\log x}\right)$$

for $x>1$.

Suppose first that $a\ge273$. Then

$$ \frac{11a}{5}>599, $$

so Dusart's inequalities give

$$ \begin{aligned} \pi(11a/5)-\pi(a) &\ge \frac{11a/5}{\log(11a/5)} \left(1+\frac{1}{\log(11a/5)}\right)\\ &\quad- \frac{a}{\log a} \left(1+\frac{1.2762}{\log a}\right). \end{aligned} $$ Put

$$ t=\log a $$

and

$$ c=\log(11/5). $$

Then

$$ \log(11a/5)=t+c. $$

I will show that the right-hand side above is at least $a/\log a=a/t$.

After dividing by $a/t$, this amounts to proving

$$ \begin{aligned} \frac{11t}{5(t+c)} +\frac{11t}{5(t+c)^2} -2 -\frac{1.2762}{t} \ge 0. \end{aligned} $$

Define

$$ F(t)= \frac{11t}{5(t+c)} +\frac{11t}{5(t+c)^2} -2 -\frac{1.2762}{t}. $$

Since

$$ c=\log(11/5)\approx0.7884573604, $$

differentiation gives

$$ F'(t)= \frac{11c}{5(t+c)^2} + \frac{11(c-t)}{5(t+c)^3} + \frac{1.2762}{t^2}. $$

Combining the first two terms,

$$ F'(t)= \frac{11((c-1)t+c^2+c)}{5(t+c)^3} + \frac{1.2762}{t^2}. $$

Since $c^2+c>0$,

$$ F'(t)> -\frac{11(1-c)t}{5(t+c)^3} + \frac{1.2762}{t^2}. $$

As $(t+c)^3>t^3$,

$$ F'(t)> \frac{1.2762-\frac{11}{5}(1-c)}{t^2}. $$

But

$$ 1.2762-\frac{11}{5}(1-\log(11/5)) \approx0.8108>0. $$

Therefore

$$ F'(t)>0 $$

for $t>0$, so $F$ is increasing.

At $a=273$,

$$ t=\log273\approx5.609471795, $$

and direct substitution gives

$$ F(\log273)\approx0.002857>0. $$

Hence for every $a\ge273$,

$$ F(\log a)>0. $$

It follows that

$$ \pi(11a/5)-\pi(a)\ge\frac{a}{\log a}. $$

It remains to compare $a/\log a$ with $\sqrt a$. For $a\ge273$,

$$ \sqrt a>\log a, $$

and therefore

$$ \frac{a}{\log a}>\sqrt a. $$

Consequently,

$$ \pi(11a/5)-\pi(a)>\sqrt a\ge\lfloor\sqrt a\rfloor $$

for every $a\ge273$.

Thus only the finite range

$$ 1\le a\le272 $$

remains.

The following elementary Python computation checks those cases exactly. Since primes are integers, the upper endpoint $11a/5$ may be replaced by $\lfloor11a/5\rfloor$ when counting primes.

from math import isqrt

N = (11 * 272) // 5

# Sieve of Eratosthenes
is_prime = [True] * (N + 1)
is_prime[0] = is_prime[1] = False

p = 2
while p * p <= N:
    if is_prime[p]:
        for m in range(p * p, N + 1, p):
            is_prime[m] = False
    p += 1

# pi[n] = number of primes <= n
pi = [0] * (N + 1)

for n in range(1, N + 1):
    pi[n] = pi[n - 1] + int(is_prime[n])

exceptions = []

for a in range(1, 273):
    upper = (11 * a) // 5
    count = pi[upper] - pi[a]

    if count < isqrt(a):
        exceptions.append((a, count, isqrt(a)))

print(exceptions)

The output is

[]

so there are no exceptions in the remaining finite range.

Therefore

$$ \boxed{\pi(11a/5)-\pi(a)\ge\lfloor\sqrt a\rfloor} $$

for every positive integer $a$.

Equality in the finite range occurs at

$$ a=1,2,3,4,5,7,13. $$

My questions are:

1. Is the argument above correct, including the use of Dusart's explicit bounds?
2. Is this result already known in this form, or does it follow easily from a standard theorem on primes in intervals?
3. Can the constant $11/5$ be substantially reduced while retaining a bound of $\lfloor\sqrt a\rfloor$ primes for every positive integer $a$?