Some Rosser-Schoenfeld identities

Stream: PrimeNumberTheorem+

[Terence Tao]

Now that we have made a lot of progress on both some legacy PNT tasks and the tertiary tasks of studying LCMs and an Erdos problem, I'm opening up a new set of tasks PNT#597 PNT#598 PNT#599 PNT#600 PNT#601 PNT#602 PNT#603 PNT#604 to verify some classic identities of Rosser and Schoenfeld relating various sums over primes to the Chebyshev function, e.g., $\pi(x) = \frac{\vartheta(x)}{\log x} + \int_2^x \frac{\vartheta(y)\ dy}{y \log^2 y}$. These should all "just" be integration by parts, but as we have seen in some other parts of the project, the analytic side of these integrations can be slightly tricky.

For the Mertens theorem identity $\sum_{p \leq x} \log p/p = \log x + E + \frac{\vartheta(x)-x}{x} - \int_2^x \frac{(\vartheta(y)-y)\ dy}{y^2}$ we will need a better asymptotic $\theta(x) = x + O(x/\log^2 x)$ than the estimate $\theta(x) = x + o(x)$ that we currently have in PNT+; in principle the mediumPNT, which is already proven, gives us this, but to get from the former to the latter is a moderately large task (PNT#597) which I judge to be among the more difficult of the ones listed above. But perhaps someone is up for the challenge? Several of the other tasks should be significantly simpler.

We will need these identities for formalizing the much more recent paper of Fiori, Kadiri, and Swidninsky converting estimates on the Chebyshev function to estimates on other sums over primes, but I will open separate tasks for that in the near future.

[Alex Kontorovich]

I would think that between Theorem 3.6.1 and AlphaProof/Aristotle, this kind of thing could be proved automatically, no? Is it really a moderately large task? I won't have time over the next few days, but if this is still unclaimed next week, I'll take it...

[Terence Tao]

Alex Kontorovich said:

I would think that between Theorem 3.6.1 and AlphaProof/Aristotle, this kind of thing could be proved automatically, no? Is it really a moderately large task? I won't have time over the next few days, but if this is still unclaimed next week, I'll take it...

I did mark this task as "large" in the project instead of "medium" but this could be personal bias, as every time I have tried to formalize big-O type arguments by hand I have ended up taking far time (and lines of code) than I expected... but it is also true that (a) autoformalizers are becoming a lot better at these, and (b) by using more modern tactics (e.g., bound) and intelligently using the asymptotic notation that already exists in Mathlib, many of my arguments could be significantly golfed. Anyway, would be interested to see the actual difficulty level of this task, it will help me calibrate future difficulty assessments.

[Harald Helfgott]

Well, this may be a good test of whether the heuristic that O^* results are easier to (auto)formalize than O results still holds, no?

[Terence Tao]

Small update: I realized that as a natural byproduct of proving these Rosser-Schoenfeld identities that one will also get proofs of Mertens' first and second theorems (with unspecified constants), so I have added the task of establishing those theorems to the relevant issues. These theorems are actually rather useful in applications; eventually they will be superseded by explicit versions, but we are still some distance away from being able to formalize such versions.

[Pietro Monticone]

Ok, I'll run Aristotle on this file later today or tomorrow.