Outstanding Tasks, V3

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

For V2, see here

Now that the Perron Formula is proved, we can turn to MellinInversion, which I've broken down into smaller steps. (In principle, a proof could be derived from @Sébastien Gouëzel's Fourier inversion PR. But given all we've developed, it might be faster to just continue the course.) So here are some targets:

1. PartialIntegration This is partial integration over $(0,\infty)$. May be useful to invoke intervalIntegral.integral_mul_deriv_eq_deriv_mul and MeasureTheory.intervalIntegral_tendsto_integral_Ioi.
2. MellinInversion_aux1 This is using partial integration to show that $\int_0^\infty f(x)x^s\frac{dx}{x} = \int_0^\infty f'(x)\frac{x^{s}}{s} dx$. We'll need to some minimal conditions under which this holds.
3. MellinInversion_aux2 Should be an application of MellinInversion_aux1 with (f := deriv f) and (s := s+1).
4. MellinInversion_aux3 This is the absolute integrability of $f(x)x^s/(s(s+1))$ for $(x,s)\in(0,\infty)\times\{\Re s = \sigma\}$. (In preparation for Fubini-Tonelli)
5. MellinInversion_aux4 This is Fubini-Tonelli in this context
6. MellinInversion Combining the above and following the proof outline should give Mellin Inversion.

And from @Terence Tao: now that the first two lemmas of Wiener-Ikehara are done:

7. Decay bounds This should be a straightforward integration by parts (and the constant C should be something very explicit, probably even 1 (one may need some numerical bound on $\pi$ for this)).
8. Limiting Fourier Identity This should also be straightforward - combine the two Fourier identities already proven, and invoke dominated convergence using the decay bound.
9. Limiting corollary Immediate from previous identity and the Riemann-Lebesgue lemma
10. Extension to Schwartz class This one is trickier: one wants to extend the identity in the previous corollary from C^2_c functions to Schwartz functions by applying smooth cutoffs (using the smooth Urysohn lemma) and take limits. There will be a moderate amount of estimation of error terms that needs to be done.

Thanks to all for the contributions!!

[Ruben Van de Velde]

Not sure if you're aware, but there's some approximations to a few decimal places of pi in mathlib

[Alex Kontorovich]

Ruben Van de Velde said:

Not sure if you're aware, but there's some approximations to a few decimal places of pi in mathlib

Sorry, should that be in reference to a different thread...?

[Ruben Van de Velde]

No, in response to the parenthetical in (7)

[Michael Stoll]

docs#Real.pi_gt_3141592 and docs#Real.pi_lt_3141593

[Alex Kontorovich]

(I was thinking of something much cruder, like $\pi<1000$... :blush:)

[Terence Tao]

Actually after working it out with pen and paper it seems the constant $C$ one gets in (7) is $C =(1 + \frac{1}{(2\pi)^2}) \int_{\bf R} \frac{dt}{1+t^2} = \pi + \frac{1}{4\pi} \approx 3.221\dots$. One could use upper and lower bounds on $\pi$ to get a bound for $C$, but actually for our application all we need is that a finite bound $C$ exists, so specific bounds on $\pi$ are not needed. (Alternatively, one could use such bounds to prove (7) with say $C=4$ to make it a slightly cleaner statement.)

[Alex Kontorovich]

I just pushed some progress on 1. PartialIntegration. When I leave unspecified the hypotheses for integrability (or decay), what I mean is: I can think of a variety of ways of spelling them, none seemingly better than others; so my modus operandi is just to start writing out the proof, and any time I apply an appropriate Mathlib lemma, I add any arising requisite hypotheses to the statement. (There's probably a better way to predict exactly which conditions will be needed?) In the case of PartialIntegration, it looks like the following should suffice:

lemma PartialIntegration {f g : ℝ → ℂ} (fDiff : DifferentiableOn ℝ f (Set.Ioi 0))
    (gDiff : DifferentiableOn ℝ g (Set.Ioi 0))
    (fDerivInt : IntegrableOn (deriv f) (Set.Ioi 0))
    (gDerivInt : IntegrableOn (deriv g) (Set.Ioi 0))
    (fDerivgInt : IntegrableOn (f * deriv g) (Set.Ioi 0))
    (gDerivfInt : IntegrableOn (deriv f * g) (Set.Ioi 0))
    (lim_at_zero : Tendsto (f * g) (𝓝[>]0) (𝓝 0))
    (lim_at_inf : Tendsto (f * g) atTop (𝓝 0)) :
    ∫ x in Set.Ioi 0, f x * (deriv g x) = -∫ x in Set.Ioi 0, f x * (g x) := by sorry

After what I have there, it should be a matter of chaining various limits together; maybe someone can help with those last steps (which require some finesse with filters...).

[David Loeffler]

Can I raise a contrary opinion here?

I think it's a pity to pursue this special-case argument for Mellin inversion when general Fourier inversion is available. My point is that developing the API to relate Mellin transforms restricted to vertical lines $\sigma + i\mathbb{R}$ to Fourier transforms is clearly something worth having anyway – it is bound to get added to mathlib at some point – and once this exists, deducing Mellin inversion from Sebastian's Fourier inversion results should be very quick indeed.

[llllvvuu]

I opened a mathlib PR for improper integration by parts: https://github.com/leanprover-community/mathlib4/pull/10874/files . I can add it to this project tomorrow (integral_Ioi_mul_deriv_eq_deriv_mul should give what we want)

[Alex Kontorovich]

David Loeffler said:

Can I raise a contrary opinion here?

I think it's a pity to pursue this special-case argument for Mellin inversion when general Fourier inversion is available. My point is that developing the API to relate Mellin transforms restricted to vertical lines $\sigma + i\mathbb{R}$ to Fourier transforms is clearly something worth having anyway – it is bound to get added to mathlib at some point – and once this exists, deducing Mellin inversion from Sebastian's Fourier inversion results should be very quick indeed.

Thanks David; that's certainly a very valid point, and one @Terence Tao and I discussed offline. We felt it was ok to have a bit of redundancy. But if someone wants to jump straight to 6.MellinInversion from Sebastien's work (certainly no need to wait for it to officially make it into Mathlib to incorporate it into PNT+...), that's perfectly fine with me. And then we can ignore the previous targets and move on to the next stage... Thoughts?

[Alex Kontorovich]

PS does the Fourier transform API allow non-unitary characters? (Of course we could deal with $x^\sigma$ explicitly, but that might be more of a pain than the proposed direct Mellin approach…?)

[llllvvuu]

llllvvuu said:

I opened a mathlib PR for improper integration by parts: https://github.com/leanprover-community/mathlib4/pull/10874/files . I can add it to this project tomorrow (integral_Ioi_mul_deriv_eq_deriv_mul should give what we want)

alright, copied over: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/81

[Terence Tao]

Alex Kontorovich said:

David Loeffler said:

Can I raise a contrary opinion here?

I think it's a pity to pursue this special-case argument for Mellin inversion when general Fourier inversion is available. My point is that developing the API to relate Mellin transforms restricted to vertical lines $\sigma + i\mathbb{R}$ to Fourier transforms is clearly something worth having anyway – it is bound to get added to mathlib at some point – and once this exists, deducing Mellin inversion from Sebastian's Fourier inversion results should be very quick indeed.

Thanks David; that's certainly a very valid point, and one Terence Tao and I discussed offline. We felt it was ok to have a bit of redundancy. But if someone wants to jump straight to 6.MellinInversion from Sebastien's work (certainly no need to wait for it to officially make it into Mathlib to incorporate it into PNT+...), that's perfectly fine with me. And then we can ignore the previous targets and move on to the next stage... Thoughts?

I think it makes sense to have Mellin inversion and Fourier inversion as sorries for now and work on the consequences of both; the decision of which implication between the two (or both) to actually formalize in our project can be done at a later stage. Even if only one of these implications ends up in Mathlib, I think there is some value in having multiple logical flows in our project (we already have three different ways to get to the prime number theorem, for instance), as they may generalize in different ways and also give us some general data points as to what types of arguments are easier to formalize than others.

[Alex Kontorovich]

We can certainly continue forward with sorrys, no need to give the proof "linearly". That said, now that we have PartialIntegration and Perron's formula, MellinInversion should follow almost immediately, could be at most a day or two of work. I think it would be nice to have a clean statement of it, with general conditions on the test function. Of course I could just state it for smooth functions with compact support in $(0,\infty)$, but we’re so close that I think we may as well finish this part now (while I prepare the next set of targets in Approach 2 - which also is mathematically extremely close to done…). What do you think?

[llllvvuu]

I played around with the Fourier inversion -> Mellin inversion implication a bit in mathlib and got it mostly done: https://github.com/leanprover-community/mathlib4/pull/10944

[llllvvuu]

llllvvuu said:

I played around with the Fourier inversion -> Mellin inversion implication a bit in mathlib and got it mostly done: https://github.com/leanprover-community/mathlib4/pull/10944

This is now sorry-free. I can later mirror it into PNT+ under a different name (MellinInversion') if desired.

[Alex Kontorovich]

Fantastic! Ok I'll make a new set of outstanding tasks then.

[Alex Kontorovich]

To that end, @Michael Stoll (or @David Loeffler), what bounds do we have on $\zeta'/\zeta$ on the 1-line? The "truth" is $\zeta'/\zeta ( 1 + it) \ll_\epsilon |t|^\epsilon$ (even something like $\ll \log^2 t$), as $t\to\infty$, but it would already be enough to have $\ll |t|^{1/2}$ (or even $\ll |t|^{1000}$, if we take more smoothing)... Which of these is closest to formalized?

[Michael Stoll]

So far, I think we only have that it is defined (i.e., $\zeta$ does not vanish on the 1-line).

[Alex Kontorovich]

Ok so I'll make that the next big target. I should have the list by tomorrow...

[Alex Kontorovich]

I’ll need a little more time to set up all the zeta bounds. In the meantime, there’s plenty to do in the MellinCalculus file. V4 coming right up.

[llllvvuu]

llllvvuu said:

I played around with the Fourier inversion -> Mellin inversion implication a bit in mathlib and got it mostly done: https://github.com/leanprover-community/mathlib4/pull/10944

Fourier inversion got merged, so I've added Mellin inversion to the mathlib review queue