New subproject: Ramanujan's inequality

Stream: PrimeNumberTheorem+

[Terence Tao]

I've started some tasks centered around Ramanujan's inequality
$\pi(x)^2 < \frac{ex}{\log x} \pi(x/e).$
This odd-looking inequality (typical for Ramanujan's work) can fail for small $x$, but the largest known failure is at $x = 38358837682$, and it is conjectured that it holds for all larger $x$. Platt and Trudgian verified this conjecture for $x \leq \exp(58)$ and $x \geq \exp(3915)$, and on the Riemann hypothesis they could also verify the intermediate range as well.

PNT#983 - PNT#999 contain the proof of the inequality for $x \geq \exp(3915)$. It is delicate because whereas both sides of the inequality are of order $x^2 / \log^2 x$, the difference between the two is only of order $O(x^2/\log^6 x)$. So one needs error estimates in the prime number theorem of relative accuracy $o(1/\log^4 x)$ or so, which without RH are only available for quite large $x$ at our current level of technology.

The computations are involved, but rather "low tech" in nature - the most advanced thing is repeated integrations by parts to estimate various logarithmic integrals. I think it is a good target for AI-assisted formalization - these are precisely the sorts of tedious computations that are not worth devoting human expert time to.

In view of the advances in explicit number theory since the 2018 Platt-Trudgian paper it is quite likely that the $\exp(3915)$ upper bound can now be improved, but the first task will be to formalize the 2018 result using 2018-level prime number theorem inputs, and then I will try to get my local team to perform some AI-assisted optimization of the bounds using modern inputs.

[Pietro Monticone]

Aristotle disproved pi_bound as follows:

theorem pi_bound (x : ℝ) (hx : 2 ≤ x) :
    Eπ x ≤ a x := by
    -- Wait, there's a mistake. We can actually prove the opposite.
    negate_state;
    -- Proof starts here:
    use 2;
    unfold Ramanujan.a Eπ;
    norm_num [ pi, Li ];
    rw [ show ( 2 : ℕ ).primeCounting = 1 by rfl ] ; norm_num ; ring_nf ; norm_num;
    -- We'll use that $Real.log 2 \approx 0.693$ to simplify the inequality.
    have h_log2 : Real.log 2 > 0.693 ∧ Real.log 2 < 0.694 := by
      -- We'll use the fact that $Real.log 2$ is approximately $0.693$ to estimate the value.
      apply And.intro; exact Real.log_two_gt_d9.trans_le' (by norm_num); exact Real.log_two_lt_d9.trans_le (by norm_num);
    -- Substitute the bounds for $Real.log 2$ into the inequality.
    nlinarith [pow_pos (sub_pos.mpr h_log2.left) 2, pow_pos (sub_pos.mpr h_log2.left) 3, pow_pos (sub_pos.mpr h_log2.left) 4, pow_pos (sub_pos.mpr h_log2.left) 5]

[Terence Tao]

Ah, right, all the $E_\pi$'s should be $E_\theta$'s. The newest version of the repo should have these fixes.

[Pietro Monticone]

Ok, thanks!

[Alejandro Radisic]

While building a ChebyshevTheta engine in LeanCert for Issue #990, I noticed the bound 1 - log(3)/3 in Sublemma 11.4.5 appears too tight: at x just below 5, θ(x) = log(6) gives Eθ ≈ 0.642 > 0.634. Details on the issue.