Outstanding Tasks V6

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

For V5, see here. 

Here are some outstanding tasks, all not too difficult. As always, please claim a task on zulip before you begin to work on it, so we don't duplicate efforts.

The first is to port @Chris Birkbeck, @David Loeffler, and @Michael Stoll's work on nonvanishing Dirichlet L-functions, in the form stated in the EulerProducts project, to connect it up with the Wiener-Ikehara theorem in PNT+.

Task 1. Port Lemma 9, Prop 2 and Theorem 2 to PNT+; see in particular the analogous theorems here. (Should not be too hard?)
Claimed by @Michael Stoll

This will finish off Dirichlet’s theorem, in asymptotic form.

Next we can return to PNT and try to get a “medium” quality error term. The next target there is an effective zero-free region and bounds for $\zeta'/\zeta$ of the form:

$|\zeta'/\zeta (s)| \ll (\log |t|)^9,$ 

for $s=\sigma+it$, as $|t|\to\infty$ in the region $1-A/(\log |t|)^9 < \sigma <2$. Here’s the last step to achieving this:

Task 2. DerivUpperBnd_aux7 This involves proving an elementary bound for a certain integral, using only integration by parts and some limits at infinity; should not be too hard for someone with experience with calculus in Lean. Done by @Alastair Irving

Looking back at it, that particular file, ZetaBounds, was quite a beast, in part because I at first didn’t realize how to properly spell that $|t|\to\infty$ while staying inside a region that depends on $\sigma$ (eventually I figured out how to use the principal filter, idiot), so made all the constants explicit. The file should really be refactored completely (a rather big task!) to systematically use big-Oh instead of moving explicit constants around everywhere. (In particular, I’m just noticing that the exact constant I put in the formal statement of DerivUpperBnd_aux7 does not match the one I get in the natural language proof. D’oh! This will cascade to a few other places where constants will need to be adjusted for everything else to match up again.)

Task 3. Big job if someone is up for it, but shouldn't take too much "brain-power" (in fact, this might be a particularly good AI task, if someone is handy with GPT!): refactor the ZetaBounds file to remove the use of explicit constants. I’ve given a version of the final statement in the desired form, namely LogDerivZetaBndAlt; ideally we could rework the whole file to systematically use big-Oh and filters.
Claimed by me

And turning our attention to the MediumPNT file and getting ready for pulling contours, here is a simple task to start.

Task 4. integrable_x_mul_Smooth1 The test function $F$ (called SmoothingF, for lack of better name) has compact support, so its convolution is integrable. (Again, should be quite straightforward for those with some calculus experience.) Done by @Arend Mellendijk

And here again are some corollaries of PNT, in case people want to work on them:
Task 5. Prime counting function asymptotic to logarithmic integral @Ruben Van de Velde has nearly finished it. Finished by Junqi Liu
Task 6. Prime counting function asymptotic to x/log x Follows from the previous bound and some more "easy" asymptotic manipulations. Done by Junqi Liu
Task 7. Asymptotic for n^th prime Should be a simple matter of "inverting" the previous result. Claimed by @Matteo Cipollina
Task 8. Bound for gaps between primes Follows from the previous bound and more "easy" asymptotic manipulations. Done by @Aaron Hill and @Austin Letson
Task 9. Primes in short intervals An equivalent form of the previous bound. Claimed by @Aaron Hill and @Austin Letson

Let’s start with these for now.

There's still the issue of figuring out what to PR to Mathlib, and how to organize the job. On this, I could really use some help and advice (please DM me)!

Thanks all for your help!

[Michael Stoll]

Alex Kontorovich said:

Task 1. Port Lemma 9, Prop 2 and Theorem 2 to PNT+; see in particular the analogous theorems here. (Should not be too hard?)

I'm planning to get the material from EulerProducts/Orthogonality (which is the main new ingredient for Lemma 9) into Mathlib fairly soon (modulo the review process -- anybody here is welcome to help with that, e.g. also for #18302, which is the non-vanishing at 1 for quadratic characters). But it is of course fine to copy it over to PNT+ for now.

A question: Does it make sense to also PR the material that leads to the non-vanishing of Dirichlet L-functions on Re s >= 1 to Mathlib? Or will this be made obsolete by stronger non-vanishing results anyway? (And if so, how quickly?)

[Ruben Van de Velde]

Alex Kontorovich said:

Task 5. Prime counting function asymptotic to logarithmic integral Claimed by Ruben Van de Velde who has nearly finished it.

I'm clearly not finding time to continue on this - I guess either you could merge https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/191 and release the rest of the task, or someone could take over the PR

[Alex Kontorovich]

Michael Stoll said:

A question: Does it make sense to also PR the material that leads to the non-vanishing of Dirichlet L-functions on Re s >= 1 to Mathlib? Or will this be made obsolete by stronger non-vanishing results anyway? (And if so, how quickly?)

I don't have a good sense of what should or should not go into Mathlib and in what form. (Thankfully we don't have to answer such questions for PNT+!..) My understanding is that people want the "final" version (at least for a while) to go into Mathlib. For Task 1, I just had in mind to copy it over to PNT+ and plow ahead... Would you like to do that? (I'm assuming you have more pressing things to do right now...?)

[Alex Kontorovich]

Ruben Van de Velde said:

I'm clearly not finding time to continue on this - I guess either you could merge https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/191 and release the rest of the task, or someone could take over the PR

No worries, you did a lot of great work! I'll merge what you've done, and someone can hopefully take over from there.

[Michael Stoll]

Alex Kontorovich said:

For Task 1, I just had in mind to copy it over to PNT+ and plow ahead... Would you like to do that? (I'm assuming you have more pressing things to do right now...?)

I'm currently polishing the Orthogonality file. I can probably do the copying once I'm finished with the polishing.

[Michael Stoll]

Alex Kontorovich said:

I don't have a good sense of what should or should not go into Mathlib and in what form. (Thankfully we don't have to answer such questions for PNT+!..) My understanding is that people want the "final" version (at least for a while) to go into Mathlib.

I definitely want some version of PNT and of Dirichlet's Theorem in Mathlib rather sooner than later. So I think it will make sense for me to continue PRing the EulerProducts material to Mathlib (and it would be very nice if somebody else would do the same for the Wiener-Ikehara Theorem) so that the non-vanishing on Re s > 1 and eventually the "weak" form of PNT/Dirichlet will be available. Once stronger forms have been formalized, things can be refactored.

[Alex Kontorovich]

Sounds great, I'll put you down for Task 1, thanks!

[Alex Kontorovich]

I'll claim Task 3. I'm quite curious to see how far I can get with AI doing this kind of task...

[Terence Tao]

I extended the elementary consequences blueprint at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/202 to also add the standard form of Dirichlet's theorem (primitive residue classes contain infinitely many primes) that should be an "easy" consequence of the PNT in AP, though I have found in practice that the small amount of analytic estimates one needs to get from the latter to the former is tricky in Lean...

[Junqi Liu]

we have done Task 6 already, but Task 5 maybe have some problem because it is not true when x = 2.So we change it to

theorem pi_asymp :
    ∃ c : ℝ → ℝ, c =o[atTop] (fun _ ↦ (1 : ℝ)) ∧
    ∀ᶠ (x : ℝ) in atTop, Nat.primeCounting ⌊x⌋₊ = (1 + c x) * ∫ t in Set.Icc 2 x, 1 / (log t) ∂ volume := by
   sorry

, and then finished Task 6 which is pi_alt.

[Alex Kontorovich]

That's great! I don't see a PR though?...

[Junqi Liu]

yeah! I have not done a pr now because I'm doing Task 5. I'll make a PR after finishing Task 5. But I don't understand the proof of Task 5. Why $\forall \epsilon, \pi(x) = (1 + O(\epsilon))\int_2^x \frac{dt}{\log t}$, then we can deduce $\pi(x) = (1 + o(1))\int_2^x \frac{dt}{\log t}$? For each $\epsilon$ we ​​have a bound, but I think we need to find a common bound to get $o(1)$. Is this possible? But there may be something wrong with my understanding.

[Terence Tao]

Let $c(x)$ be the quantity $\frac{\pi(x)}{\int_2^x \frac{dt}{\log t}} - 1$, then our task is to show that $c(x) = o(1)$ as $x \to \infty$, i.e., that $c(x) \to 0$ as $x \to \infty$. Unpacking the asymptotic notation, the previous analysis shows that there exists a constant $C>0$ such that for every $\varepsilon>0$ there exists $N$ one has $|c(x)| \leq C \varepsilon$ for $x > N$ (a key point here is that the implied constant $C$ is independent of epsilon). This is enough to show that $c(x)$ goes to zero as $x \to \infty$.

If one is to use big-O notation and little-o notation here, one should work with functions of both $\varepsilon$ and $x$, and use an appropriate filter, one to capture bounds that are allowed to depend on $\varepsilon$, and ones that are not. Or one can discard asymptotic notation completely and work with explicit epsilons and deltas throughout the proof. I'm hoping that these tasks will help clarify what type of asymptotic analysis works best in Lean.

[Alex Kontorovich]

I wonder if people have thought about trying to create API to package big-O and little-o notation in Lean in the way it's used in practice? That is, in natural language, we would much prefer to write $\pi(x)=(1+o_{x\to\infty}(1))Li(x)$ (where $Li(x):=\int_2^x\frac{dt}{\log t}$) versus moving everything to one side so that we can use the currently available spelling, $\pi(x)/Li(x) - 1 = o_{x\to\infty}1$...

[Terence Tao]

I started a discussion about this a while back at #Is there code for X? > Working with big-O notation like an analyst . The consensus was that it was quite difficult to refactor Lean to work with this sort of notation.

[Alex Kontorovich]

Ok, good to know, that's too bad... (Maybe at some much later point, there'll be a good way to refactor things...)

[Junqi Liu]

We have the previous result is $\forall \epsilon, \pi(x) = (1 + O(\epsilon))\int_2^x \frac{dt}{\log t}$. I think that this means that for every $\epsilon > 0$, there exists a constant $C_\epsilon > 0$ such that there exists $N$ one has $∣c(x)∣ \leqslant C_\epsilon \epsilon$ for $x > N$, but it doesn't mean that there exists a constant $C > 0$ such that for every $\epsilon > 0$ there exists $N$ one has $∣c(x)∣ \leqslant C \epsilon$ for $x > N$.

[Junqi Liu]

We are trying to prove this theorem by using $\epsilon - \delta$ language. We did not use the $\sum_{p \leq t} \log p = t + O(\epsilon t)$ substitution step.

[Terence Tao]

In the blueprint, if the $O()$ notation appears without an epsilon subscript, this means that the implied constant $C$ is not dependent on epsilon. If instead one has an epsilon subscript such as $O_\varepsilon(1)$, then this indicates that the implied constant $C$ is permitted to depend on $\varepsilon$. For instance, with this convention, the assertion $\sum_{p \leq t} \log p = t + O(\varepsilon t)$ for $t \geq x_\varepsilon$ means that there is a constant $C>0$ (not depending on $\varepsilon$) such that for every $\varepsilon > 0$, one has $|\sum_{p \leq t} \log p - t| \leq C \varepsilon t$ for $t \geq x_\varepsilon$. If instead we had the much weaker bound $\sum_{p \leq t} \log p = t + O_\varepsilon(\varepsilon t)$ one could only say that for every $\varepsilon$ there existed $C_\varepsilon>0$ such that $|\sum_{p \leq t} \log p - t| \leq C_\varepsilon \varepsilon t$ for $t \geq x_\varepsilon$. This latter bound will not be strong enough to give this theorem, but the former bound (which is available from Theorem 17) will be.

This type of dependency on constants is very convenient for human analytic number theory proofs, but is not well supported by Lean syntax unfortunately.

[Junqi Liu]

oh! Thanks a lot! I get you! The key to my question may be that the $O()$ notation in blueprint and mathlib have different meanings. Don't worry! We have changed the proof. Let me have a try.

[Terence Tao]

One can interpret both types of O() using the mathlib asymptotic notation, but one needs to work with two different filters. If $f(\epsilon,x)$ is a function of both $\epsilon, x$, then saying for instance $f = O(1)$ when $x$ is sufficiently large depending on $\varepsilon$ would be spelled in Lean as f =O[l] (fun _ ↦ 1) where l is a rather funny filter, it is generated by sets of the form $\{ (\varepsilon,x): x \geq x_\varepsilon\}$ for any function $\varepsilon \to x_\varepsilon$ (I don't know if this type of filter is already studied in Mathlib). Meanwhile, the weaker bound $f = O_\varepsilon(1)$ would be spelled in Lean as something like ∀ ε, (fun x ↦ f (ε, x) =O[atTop] (fun _ ↦ 1).

But yeah, the simplest thing here may be just to abandon the Mathlib O() notation and use epsilons and deltas.

[Junqi Liu]

yeah! We have finished Task 5 yet!

[Alex Kontorovich]

Terence Tao said:

would be spelled in Lean as f =O[l] (fun _ ↦ 1) where l is a rather funny filter, it is generated by sets of the form $\{ (\varepsilon,x): x \geq x_\varepsilon\}$ for any function $\varepsilon \to x_\varepsilon$ (I don't know if this type of filter is already studied in Mathlib).

Yes! This is the "Principal" filter. It took me a long time (merely due to my own ignorance) to figure out how to spell in Lean that $\zeta'/\zeta$ has a certain bound, as $t\to\infty$ while obeying the condition $1-A/\log t < \sigma$. That's why the ZetaBounds file, as it currently stands, uses explicit constants, and is being refactored. FYI, in the case above, the spelling is:

lemma LogDerivZetaBndAlt :
    ∃ A > 0, ∀ (σ) (hσ : σ ∈ Ico ((1 : ℝ) / 2) 1),
    (fun (t : ℝ) ↦ deriv ζ (σ + t * I) / ζ (σ + t * I)) =O[cocompact ℝ ⊓
      Filter.principal {t | 1 - A / Real.log |t| ^ 9 < σ}]
        fun t ↦ Real.log |t| ^ 9

[Terence Tao]

Actually, what I had in mind is not the principal filter coming from a single function $\varepsilon \mapsto x_\varepsilon$, but the filter generated by all such functions, to capture the concept of "$x$ is sufficiently large depending on $\varepsilon$". Though in this specific case one could probably identify an explicit function $\varepsilon \mapsto x_\varepsilon$ which would suffice for the analysis.

[Michael Stoll]

The orthogonality statement for Dirichlet characters is now in Mathlib:

import Mathlib.NumberTheory.DirichletCharacter.Orthogonality

#check DirichletCharacter.sum_char_inv_mul_char_eq

[Alex Kontorovich]

Fantastic! Sounds like we could use another mathlib bump...?

[Johan Commelin]

Dirichlet has landed in mathlib!

Huge congrats to @Michael Stoll, @David Loeffler and all others involved in the journey!

[Michael Stoll]

So I assume that everything that PNT+ needed from EulerProducts is now in Mathlib. In particular, Lemma 9 of Section 2.4 of the blueprint is docs#ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq and Proposition 2 in the same section is docs#ArithmeticFunction.vonMangoldt.continuousOn_LFunctionResidueClassAux (just merged; will take some time to show up on the docs pages; edited the name, which was fixed on Nov 26).

[Michael Stoll]

(And dirichlet_thm in PNT+ is (modulo an equivalent formulation of the modulo condition) docs#Nat.setOf_prime_and_eq_mod_infinite .)

[Michael Stoll]

What about a new task "upstream Wiener-Ikehara to Mathlib"?

[Terence Tao]

Sounds good to me, but I'll let Alex make it official.

[Alex Kontorovich]

Congrats!!! Yes indeed. Would it be worthwhile to break that into smaller, bite-sized pieces? Or perhaps the upstreaming to Mathlib is a complicated enough job that it really needs to be executed by a small team, not something that can be done leveraging large-scale collaboration?...

[Michael Stoll]

The usual procedure is to do it step by step with PRs that have a reasonable size (maybe 100-300 lines of code). This makes reviewing easier; also, the feedback from reviews of earlier PRs may lead to some changes affecting the later steps, and this is easier to deal with when one doesn't have to modify large parts of a huge PR. For comparison, the final sequence of PRs for Dirichlet's Theorem consisted of 15 PRs, some of which were quite small (and, e.g., adding some API lemmas).

The final version of Wiener-Ikehara is around line 2300 of Wiener.lean, so something like 10-20 PRs would seem like a reasonable estimate (unless there is more preparatory material needed, which should then be dealt with first).

[Alex Kontorovich]

Of course, but is the suggestion that this be a "line item" that someone can individually "claim" (in which case, there's not much for me to do but add one task to the list); or instead that I (or someone) break those 10-20 PRs down into individual TODOs, and allow people to claim those much smaller tasks? My worry about the latter is that it will really take some proper thought to get this right (if it's to get into Mathlib, with each component in the correct location, with the correct name, and proper generality, etc etc; and of course, those 20 PRs will each depend on each other, with changes in one breaking everything that follows)...

[Michael Stoll]

I haven't looked carefully at the file; maybe there are some well-identified intermediate steps, which could each be a task (and in turn best split into several PRs)?
But generally speaking, I think it makes sense if this is done either by a single person or a small team working closely together, with a good overview of the material.

[David Loeffler]

I think upstreaming is not a job which parallelises well, since it is an axiom that mathlib master must always compile correctly and be sorry-free. But the actual PR-making step can perhaps be made less laborious by a preliminary process of re-visiting proofs in the PNT+ repo and polishing them, and this could potentially be done in parallel.

[Vincent Beffara]

Besides Mathlib, there are dependencies in Fourier.lean and Sobolev.lean that would have to be upstreamed separately first, mostly W21_approximation about approximation by compactly supported functions

[Arend Mellendijk]

I'd like to claim task 4

[Alex Kontorovich]

It's yours!

[Alex Kontorovich]

Also thanks to @Junqi Liu for completing Tasks 5 and 6. Repeating @Terence Tao's message here (so we can discuss on zulip): "Wow, that was quite an argument! Is there anything you can think of that might have allowed for a simpler route to get these conclusions? It's remarkable how hard it is to manipulate these sorts of estimates involving O() and o() bounds even though it is "just" using the triangle inequality and summation by parts..."

[Alastair Irving]

I'm very new to Lean and currently just observing this project out of curiosity. I agree the asymptotic arguments in Consequences.lean seem unduly long. I wonder if there's at least some simplification by being more consistent in choices of how integrals and asymptotics are represented. For example I saved a few lines in lemmas pi_alt_Oaux1/2 by using interval integrals 2..x throughout. If the whole file used these there would be no need to convert. Those lemmas could also be stated using O (with some small changes to add absolute values).

For asymptotics, would it help if we used versions of results with ~ or o more consistently? Do we really need to write theorems in the form of chebyshev_asymptotic' where we assert the existence of a suitable error function rather than just collecting terms on the LHS and using o?

[Alastair Irving]

I've just noticed that Abel summation is now in Mathlib so if we bump we could use that.

[Ruben Van de Velde]

There's also a version of Abel in pnt already, but it'll be good to replace that at some point

[Alex Kontorovich]

Arend Mellendijk said:

I'd like to claim task 4

Thanks to @Arend Mellendijk for finishing Task 4! Since I don't think people look too much at the PNT+ github comments, I'll transfer the text here for others to see and respond to: Arend wrote:

"
Proving measurability was much more painful than expected. I hope that can be golfed down quite a bit. Then again, maybe the right thing to do here is to prove the relevant smoothness properties of the mellin convolution.

I also proved a lemma support_MellinConvolution_subsets that says if f , g are supported on A , B respectively then their mellin convolution is supported on A ∗ B . Annoyingly this wasn't actually useful here, since DeltaSpike is not generally supported on [ 0 , ∞ ) . Still, I think this is useful API to have.
"

[Arend Mellendijk]

The PR is https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/213, by the way

[Aaron Hill]

@Austin Letson and I would like to claim task 8

[Alastair Irving]

If noone is working on task 2 I could attempt that, unless it should wait until after task 3?

[Alex Kontorovich]

Aaron Hill said:

Austin Letson and I would like to claim task 8

Great thanks! They're yours.

[Alex Kontorovich]

Alastair Irving said:

If noone is working on task 2 I could attempt that, unless it should wait until after task 3?

That'd be great, thanks! I think that task is useful independently of task 3; I'm going to try to make some progress on the latter this week. (AI tools are really getting better and better, day by day...)

[Matteo Cipollina]

Hi, if still available I would like to claim task 7

[Alex Kontorovich]

Great, thanks! It's yours.

[Matteo Cipollina]

Alex Kontorovich ha scritto:

Great, thanks! It's yours.

Thanks!

[Alastair Irving]

Update on task 2: I've hopefully done all the difficult parts since I've bounded and evaluated the integral so just have an inequality to prove. Unfortunately the integration by parts given in the blueprint is just wrong, I actually get

$$\int_N^\infty x^{-\sigma-1}\log x\, dx = \frac{1}{\sigma^2}N^{-\sigma}+\frac{1}{\sigma}N^{-\sigma}\log N$$

This is fine but I'll have to add a constant into the bound and update the rest of the file. I could have been more careful and estimated the floor part by $\frac 12$ but I'm not sure that would have avoided changing the result as stated.

Is there a reason the result as stated includes the factor $\frac1{\sigma}$? Given our assumptions on $\sigma$ this is of constant size.

[Alex Kontorovich]

Yes, I mention above that the constant was wrong; the point of Task 3 (still ongoing, as it's a slog) is to remove the interdependence of explicit constants among the different auxiliary lemmas. (Of course in natural language, one simply writes $\ll$ and moves on...) I think don't worry too much about connecting DerivUpperBnd_aux7 to the rest of the file; just prove that theorem with some constant - the rest of the file will break, and I'll zip it all up after. Thanks!

[Alex Kontorovich]

Thanks @Alastair Irving for finishing Task 2! How did it feel to work out those integrals? It looks like it's still a slog to do something that's one line in natural language, due to all the auxiliary results needed on, e.g., measurability, positivity, etc etc. This is a place that's ripe, perhaps, for automation... I don't think the tactic would have to be all that powerful to be useful already, what do you think? Can you collect your general train of thought as to how you went about solving the various subgoals, and do you think that could fit into a framework amenable to metaprogramming?

[Alastair Irving]

Yes it was a bit of a slog but some of that could be down to my inexperience. For example I just realised that the bound tactic can be used in some places to get some of the positivity assumptions I needed. There's probably also some redundancy between what I did and what was already in the file, for example I think there's overlap in the integrability proofs.

An obvious candidate for automation would be the derivative calculation in DerivUpperBnd_aux7_3 where I just built up the derivative I needed using standard calculus rules. I no Mathlib has simp setup to work with deriv, rather than HasDerivAt, but I don't think that would work for something as complicated as this. Even if it did I'd then need differentiability, maybe with fun_prop, which feels like duplicating the work. Similar comments apply to DerivUpperBnd_aux7_tendsto where I prove something goes to 0 by splitting into pieces which each go to 0.

Another thought is that theorems which evaluate integrals should also include integrability in their conclusions. For example I evaluated an integral with integral_Ioi_of_hasDerivAt_of_nonneg' but also had to use integrableOn_Ioi_of_hasDerivAt_of_nonneg' with all the same arguments to know that the function was integrable. I don't see much point in knowing the integral without also knowing that its a meaningful result so why not package the two claims together?

[Alastair Irving]

What tasks are next? Is it time for more work on MediumPNT.lean? Looking over that file I think SmoothedChebyshevClose is incorrectly stated in Lean because the implied constant needs to be independent of $\epsilon$. Presumably that can be stated with a product of filters or maybe an explicit inequality is going to be simpler.

[Alastair Irving]

Digging further I think there might be more issues with the dependence on $\epsilon$. The proofs of lemmas Smooth1Properties_above/below make it clear that the constant is absolute but I think the way the lemmas are written in Lean means that the constant could depend on $\epsilon$. Am I misunderstanding either what the Lean statement means or what we need for the final proof, surely we will need to take $\epsilon \rightarrow 0$? Anyway this is hopefully easy to fix since the proofs are already with an absolute constant.

[Austin Letson]

@Aaron Hill and I would like to claim task 9

[Alex Kontorovich]

Alastair Irving said:

Digging further I think there might be more issues with the dependence on $\epsilon$. The proofs of lemmas Smooth1Properties_above/below make it clear that the constant is absolute but I think the way the lemmas are written in Lean means that the constant could depend on $\epsilon$. Am I misunderstanding either what the Lean statement means or what we need for the final proof, surely we will need to take $\epsilon \rightarrow 0$? Anyway this is hopefully easy to fix since the proofs are already with an absolute constant.

Yes, we'll eventually take $\epsilon = \exp(-c (\log X)^c)$ for some constant $c$, but I don't see why we wouldn't be able to do that (after converting from big-Oh to absolute constants) in the eventual application? This will be an interesting test of the tech... (In my mind it all works out, but we'll see...)

[Alex Kontorovich]

Austin Letson said:

Aaron Hill and I would like to claim task 9

It's yours. And thanks for doing task 8!

[Alex Kontorovich]

Alastair Irving said:

What tasks are next? Is it time for more work on MediumPNT.lean? Looking over that file I think SmoothedChebyshevClose is incorrectly stated in Lean because the implied constant needs to be independent of $\epsilon$. Presumably that can be stated with a product of filters or maybe an explicit inequality is going to be simpler.

I'll get the next set of tasks out this week (in between some travel...).

[Alastair Irving]

Alex Kontorovich said:

Yes, we'll eventually take $\epsilon = \exp(-c (\log X)^c)$ for some constant $c$, but I don't see why we wouldn't be able to do that (after converting from big-Oh to absolute constants) in the eventual application? This will be an interesting test of the tech... (In my mind it all works out, but we'll see...)

I agree the proofs are fine and the constants are absolute but I don't believe the current statement of the results in Lean reflects that. For example in Smooth1Properties_above/belowI think we're saying that for all $\epsilon$ there exists a c whereas we need to have the existence first. Similarly in MellinOfSmooth1b the $\epsilon$ is before the big O estimate so I think that implies a dependence of the constant and we'd need to restate using a filter which knows about $\epsilon, s$. Similar remarks apply to SmoothedChebyshevClose.

[Alex Kontorovich]

Ack, good catch! (We would've found out soon enough...) I'll fix the typos.

[Alex Kontorovich]

Yeah, this is what I get for systematically using Copilot to autoformalize my natural language statements! I have to live up to my own remark that mathematicians must hold themselves responsible for the proposed formalizations of AI. (Though again, we would have realized this issue soon enough when we would've gone to apply the statements... This is consistent with a conversation I had some time ago with Christian Szegedy. He argued that it's ok if the AI makes a mistake in the autoformalization, because eventually if the statements are wrong, you'll "feel" it; and as long as the AI has the freedom to re-evaluate, and go back to fix the statements, all will eventually work out...) I recall Terry making a comment recently that maybe we should go back to explicit constants for these kinds of analytic arguments; I might switch back to that (after spending quite a bit of time trying to systematize the Big-Oh approach). It's very annoying in natural language to keep around constants $C_1$ through $C_{27}$ in the middle of a long proof; when Lean is keeping track of everything for you, it's not a problem at all!

[Alex Kontorovich]

Or maybe I'm just not sufficiently versed in filters. For example, I tried changing the statement to:

lemma MellinOfSmooth1b {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν)
    (suppν : ν.support ⊆ Set.Icc (1 / 2) 2)
    {σ₁ σ₂ : ℝ} (σ₁pos : 0 < σ₁) :
    (fun (s, ε) ↦ ‖(𝓜 ((Smooth1 ν ε) ·) s)‖)
      =O[(principal {s : ℂ | σ₁ ≤ s.re ∧ s.re ≤ σ₂}) ×ˢ
        (principal {ε | 0 < ε})]
      fun (s, ε) ↦ 1 / (ε * ‖s‖ ^ 2) := sorry

But this causes all kinds of other problems, because after rw [Asymptotics.isBigO_iff], in order to apply MellinOfPsi, I need the $\epsilon$, which I can't access until I supply the constant. Ack!

[Alastair Irving]

Alex Kontorovich said:

But this causes all kinds of other problems, because after rw [Asymptotics.isBigO_iff], in order to apply MellinOfPsi, I need the $\epsilon$, which I can't access until I supply the constant. Ack!

I've just looked at this very briefly, is there maybe a mathematical issue here? The implied constant in MellinOfPsi depends on the $\sigma$ and you're then using this with a $\sigma$ which depends on $\epsilon$.

[Alex Kontorovich]

Argh. Yeah, just like the constant shouldn't depend on $\epsilon$, it shouldn't depend on $\sigma_1$ either. (But it does depend on $\sigma_2$, which is not a big deal, since we can make that absolute...) More clean-up to do...

[Alastair Irving]

I think we need some more properties of the Mellin transform of Smooth1, in particular that it's differentiable for $\Re s > 0$. Here's a plan which I'm happy to work on and don't think will be too difficult:

1. Show that Smooth1 is integrable. We can do that by simplifying the proof of integrable_x_mul_Smooth1 to drop the x factor.
2. It then follows from a result in Mathlib and the existing bounds on Smooth1 that it is Mellin convergent for $\Re s > 0$. In particular this subsumes integrable_x_mul_Smooth1.
3. A similar result in Mathlib gives us differentiability.

We could also tidy up the Blueprint around Mellin Inversion, we're not actually doing the proof stated in the blueprint we're just getting it from Mathlib. That means that we don't need the PerronInverseMellin lemmas. Actually I don't think we need Perron's formula at all but its useful to keep around as an example of how to do contour integration.

Another thing to tidy at some point would be to drop our definitions of Melin transform and inverse and just use the ones from Mathlib. That should be easy but tedious.

[Alex Kontorovich]

Oh this is great, thanks! (Came in while I was preparing V7.)

[Alex Kontorovich]

Yes, we can reuse the same techniques from PerronInverseMellin to do the contour pull for zeta'/zeta