Do we really need Stieltjes integral?

Stream: PrimeNumberTheorem+

[Yongxi Lin (Aaron)]

In the Secondary explicit estimates, we want to prove the following formula:

$\sum_{p \leq x} f(p)=\frac{f(x) \vartheta(x)}{\log x}-\int_2^x \vartheta(y) \frac{d}{d y}\left(\frac{f(y)}{\log y}\right) d y.$

This is hard to formalize if we use Stieltjes integral to prove this because we don't have the integration by parts formula for Stieltjes integral right now in Mathlib. However, there's an elementary proof of this formula that I found in Ingham's book about the distribution of prime numbers. I'll include the proof here:

$$\begin{align*} (\sum_{p\le x}\log p )\frac{f(x)}{\log x}-(\sum_{p\le x}\log p \frac{f(p)}{\log p})&=\sum_{p\le x}\log p(\frac{f(x)}{\log x}-\frac{f(p)}{\log p})\\ &=\sum_{p\le x}\log p (\int_p^x\frac{d}{dy}(\frac{f(y)}{\log y}))dy\\ &=\int_2^x\sum_{p\le x}\log p1_{y>p}\frac{d}{dy}(\frac{f(y)}{\log y}))dy\\ &=\int_2^x\sum_{p\le y}\log p1_{y>p}\frac{d}{dy}(\frac{f(y)}{\log y}))dy \end{align*}$$

and this approach is easy to formalize in lean (maybe I can finish it in these two days). I guess my ultimate question is do we want an elementary proof or waiting for more APIs about Stieltjes integral?

[Terence Tao]

Over on the other thread at #PrimeNumberTheorem+ > Explicit estimates, outstanding tasks v2. @ 💬 we are proposing a Stieltjes integration by parts lemma. Do you think that lemma might be suitable for this task? If so we can try to focus on proving that lemma, otherwise we can fall back to the elementary approach.

[Yongxi Lin (Aaron)]

That lemma certainly works, but I think it takes longer time and my understanding it that it is not really focus of this projects (unless integration by parts for Stieltjes integral is needed somewhere else in this project).

[Harald Helfgott]

My view is that part of the point of the formalization project is to expose glaring omissions in Mathlib, and if possible to remediate them. The lack of Stieltjes IBP is an issue that just came up in another project - that's a sign. If the lemma proposed there also works here, that's another sign; it arguably moves up into 'plausible Mathlib candidate' status. I'd suggest using it for now, rather than getting around the issue.

[Alastair Irving]

The elementary approach is essentially Abel summation which is already in Mathlib. As I commented on PNT#602 I used that in Mathlib to prove docs#Chebyshev.primeCounting_eq_theta_div_log_add_integral and we could prove the more general sum over primes similarly.