Potentially useful results

Stream: PrimeNumberTheorem+

[Gareth Ma]

Hi! I haven't been following the progress closely of the project, but I have proved some results in the past that might be useful?
Dirichlet Hyperbola method: https://github.com/grhkm21/lean4/blob/master/Lean4/nt/DirichletHyperbola.lean#215
Partial Summation: https://github.com/grhkm21/lean4/blob/master/Lean4/nt/PartialSummation.lean#L139 translated from Bhavik and Thomas’ unit fraction project.

[Terence Tao]

Yes, these could potentially be quite useful! Partial summation could shorten the proof of this form of the prime number theorem, and the hyperbola method identities could potentially shorten the proof of this elementary estimate for the Mobius function, as well as the Mobius function version of the prime number theorem (and perhaps also the Liouville function version). I don't know though if the form you have of these identities is precisely what is needed for these arguments.

[Ruben Van de Velde]

So are we getting those into mathlib? :)

[Gareth Ma]

I will try the elementary estimate for the Mobius function ($\left|\sum_{n \leq x} \frac{\mu(n)}{n}\right| \ll 1$). Do you mind sketching how the hyperbola method may make the proof shorter? The paper proof seems to be three lines currently, and I have something similar from previous projects.
(I should clean them up and dump them all onto my repo, I suspect some results might be useful...)

[Terence Tao]

Gareth Ma said:

I will try the elementary estimate for the Mobius function ($\left|\sum_{n \leq x} \frac{\mu(n)}{n}\right| \ll 1$). Do you mind sketching how the hyperbola method may make the proof shorter? The paper proof seems to be three lines currently, and I have something similar from previous projects.
(I should clean them up and dump them all onto my repo, I suspect some results might be useful...)

Actually on closer inspection I guess it doesn't actually make it any shorter. The identity $\sum_{n \leq x} 1 * \mu(n) = \sum_{d \leq x} \mu(d) \sum_{m \leq x/d} 1$ is a degenerate case of the hyperbola identity that can give the assertion $1 = \sum_{d \leq x} \mu(d) \lfloor x/d \rfloor$ at the start of the proof, but one can just prove that identity by hand, the hyperbola identity doesn't save all that many lines of code. (But maybe it's worth stating this degenerate version of the hyperbola identity, viz. $\sum_{n \leq x} f*g(n) = \sum_{d \leq x} f(d) \sum_{m \leq x/d} g(m)$, as a standalone lemma, as it is also needed for the next two propositions.)

With a bit of care, by the way, one should be able to establish the bound $|\sum_{n \leq x} \mu(n)/n| \leq 1$ (i.e., one should not lose any constant at all), by reducing to the case when $x$ is an integer, and using the fact that $x/d = \lfloor x/d\rfloor$ when $d=x$, to show that the $O(x)$ term is in fact bounded in magnitude by $x-1$. It's not essential for the rest of the arguments, but aesthetically it would be nice to not lose any constant.

[Gareth Ma]

I got $1 = \sum_{d\leq x} \mu(d)\lfloor x/d\rfloor$ done, I will finish later (the concrete bound should be a lot easier than asymptotics especially in Lean). Do I make a PR when I'm done?

[Gareth Ma]

How do I add a ✓ next to the proposition?
Screenshot-2024-03-07-at-13.32.03.png

[Ruben Van de Velde]

Is that \leanok?

[Gareth Ma]

I think not (I don't know why my caps was on). This is not proven for example:

Screenshot-2024-03-07-at-13.38.18.png

[Gareth Ma]

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/112 :tada: The ✓ is still not appearing.

[llllvvuu]

It might relate to there being separate \leanok for the \begin{theorem} and \begin{proof}, which correspond to checkmarks next to the statement and proof respectively

[Gareth Ma]

Hmm I added more \leanok everywhere and I think the tick is still not showing up

[Gareth Ma]

Just to confirm, I just have to pip install plastex then make blueprint and open blueprint/web/index.html?

[Gareth Ma]

Oh wait no I need to install the plasTeX plugin, maybe that's why.

[Gareth Ma]

Sorry, I didn't install leanblueprint :tear: I will add pip install -r blueprint/requirements.txt to the README as well.

[Gareth Ma]

Sorry for the many messages, but I am slightly confused. Do we actually mean to say $|\sum_{n \leq x} \mu(n) / n| = O(1)$, or rather $|\sum_{n \leq x} \mu(n) / n| = o(1)$? @Terence Tao From my limited memory and knowledge, the latter follows from PNT as well.

[Gareth Ma]

oh, https://terrytao.wordpress.com/2009/08/30/an-elementary-inequality-involving-the-mobius-function/

[Terence Tao]

Gareth Ma said:

Sorry for the many messages, but I am slightly confused. Do we actually mean to say $|\sum_{n \leq x} \mu(n) / n| = O(1)$, or rather $|\sum_{n \leq x} \mu(n) / n| = o(1)$? Terence Tao From my limited memory and knowledge, the latter follows from PNT as well.

Yes, it does, but here we are just using the weaker O(1) bound to prove $\sum_{n \leq x} \mu(n) = o(x)$ in the next proposition. Once one has the latter bound, one can go back and improve the previous O(1) bound to a o(1) bound (using the argument in the blog post); if there is interest I can add that argument to the blueprint.