Mertens' Theorems

Stream: mathlib4

[Arend Mellendijk]

I've wanted for Mertens' third theorem for a while now. With the recent development of Euler products (due to @Michael Stoll ), the result shouldn't be too hard to prove. Having looked at Tenenbaum, I believe the only thing missing for the proof is $\psi(x) \ll x$, which follows from an elementary sieve estimate already present in PNT+. Has anybody worked on this?

There is also the point that Mertens' theorems can be derived from the prime number theorem. Here we get to steal the error term from PNT. That said I think this argument is only simple if you have an error term of at most $\psi(x)-x \ll x/\log x$, so the version of PNT which we have in PNT+ is not quite enough. I'm tempted to say we shouldn't wait for a suitable version of PNT to land in mathlib.

[Bhavik Mehta]

$\psi(x) \ll x$ and $x \ll \psi(x)$ are both in the unit-fractions project: https://github.com/b-mehta/unit-fractions/blob/10ef71a300cf29e5f19beb2bbc723a035a0678de/src/for_mathlib/basic_estimates.lean#L1163 (Lean 3)

[Michael Stoll]

Are there plans to upstream these (and related) results from there to Mathlib?

[Bhavik Mehta]

I was under the impression that PNT+ would improve them all, so I never made such plans. The exception is the divisor bound stuff, which I'm planning to upstream soon.