Outstanding Tasks V7

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

For V6, click here.

Thanks all for the continued contributions! Here is a slightly shorter tasks list, and perhaps we can make good time getting through it...
Task 1. SmoothedChebyshevDirichlet_aux_integrable Prove that $x \mapsto \int_{(0,\infty)} t^{1+ix} \widetilde{1_{\epsilon}}(t) dt$ is integrable (pull absolute values inside and quote MellinSmooth1b). Done by @Alastair Irving

Task 2. SmoothedChebyshevDirichlet_aux_contAt Prove continuity of smooth function (easy...). Done by @Alastair Irving

Task 3. SmoothedChebyshevDirichlet_aux_tsum_integral Swap an integral with a tsum. (This should be a general theorem in Mathlib; I couldn't locate it, if it exists...?) Claimed by @Aaron Hill

Task 4. Formalize the Borel-Caratheodory theorem Claimed by @Shuhao Song

Up next will be more contour pulling, heading towards SmoothedChebyshevPull1, but I think I should break that up into smaller pieces before setting it as a task...

[Alastair Irving]

I can look at task 2 although I'm not sure it's as easy as you claim. In the blueprint you say the function is a sum of continuous functions but I can't see why that is. I think we have to do something like dominated convergence to justify that the inegral defines a continuous function.

[Aaron Hill]

For task 3, https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Integral/DominatedConvergence.html#MeasureTheory.integral_tsum_of_summable_integral_norm looks related

[Alastair Irving]

I've done task 2, will make a PR shortly. It was fairly tedious proving all the conditions for continuity via dominated convergence. The nice thing is that now we have smooth1 continuous we can get various properties of its Mellin transform without much work. I'm going to rearrange things a bit, I think properties of Smooth1 should all go in MellinCalculus.lean and MediumPNT should be more PNT specific results.

[Alex Kontorovich]

Great, thanks!

[Alex Kontorovich]

Aaron Hill said:

For task 3, https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Integral/DominatedConvergence.html#MeasureTheory.integral_tsum_of_summable_integral_norm looks related

Thanks!! I was looking for the word swap due to MeasureTheory.integral_integral_swap...

[Aaron Hill]

I'd like to claim task 3

[Alastair Irving]

I can work on task 1.

[Alastair Irving]

A couple of thoughts on the contour pulling part in MediumPNT:

1. The text before SmoothedChebyshevPull1 suggests that in that theorem the contour is remaining to the right of $s=1$ but then the theorem contains the residue term.
2. Might it be simpler to start with the Mellin inversion just to the right of 1, say $\sigma = 1 + 1/\log x$? We'd need some generalisations to a couple of existing lemmas but I don't think that would be too bad. I think we then just need to move the integral for $|t|\leq T$ and we can estimate the rest directly without pulling it.

[Alex Kontorovich]

The problem with pulling to $\sigma=1+1/\log t$ is that then the trivial bound there is $X^{1+1/\log X}/T$, not enough. I'm now adding some things to prove in the ZetaBounds file about holomorphicity (as a human, bounds imply holomorphicity, but of course that's not how it works formally!). Then there's no problem pulling to the 1-line when $|t|>T$. And for $|t|\le T$ we pull a little inside and pick up a residue...

[Alastair Irving]

Alex Kontorovich said:

The problem with pulling to $\sigma=1+1/\log t$ is that then the trivial bound there is $X^{1+1/\log X}/T$, not enough.

Surely $X^{1+1/\log X}= eX$ so this is only a constant factor worse than on the line $\sigma=1$. My point was that we can do the initial Mellin inversion on $\sigma=1+1/\log X$, rather than 2, and then we only need pull the $$|t|\leq T$ part because the $|t|\geq T$ part is only a constant factor worse than on $\sigma=1$.

[Alex Kontorovich]

Sorry, I can't read my own writing (tried to reply quickly and read $X^{1+\log X}$...) Yes of course. I'll think about refactoring things.