IwaniecKowalski

Stream: PrimeNumberTheorem+

[Alex Kontorovich]

FYI Some students/postdocs and I met today and added a chapter to the blueprint called IwaniecKowalski. The idea is to see how far we can get through formalizing that text, starting in Chapter 1. An immediate decision was the generality in which we'd like to work. There was a discussion of $L$-functions, and the fact that, if we use the Mathlib definition (summing over $\N$ with ArithmeticFunctions, which satisfy $f(0)=0$), then we'll have problems if/when we move to $L$-functions over number fields (and sums over elements in arithmetic groups, etc etc). I would like the code in this part of the blueprint to be rather clean, unlike the rest of PNT+, and hope to upstream everything to Mathlib almost immediately. (Of course this means we'll move much more slowly, to develop the API in the "right" way, etc). We started with a definition generalizing ArithmeticFunction, namely, GenArithFunction, which by the end was just an abbrev for ZeroHom. We also defined additive and completely additive functions in this generality. Hopefully we'll make more progress next time. Anyone who wants to work on such things is welcome to join us!...

[Alex Kontorovich]

PS Many thanks to @Pietro Monticone for also joining us over zoom, and helping with blueprint issues!

[Michael Stoll]

Alex Kontorovich said:

There was a discussion of $L$-functions, and the fact that, if we use the Mathlib definition (summing over $\N$ with ArithmeticFunctions, which satisfy $f(0)=0$)

Note that it is not the case that Mathlib's L-functions use docs#ArithmeticFunction s as input. Rather, the input is a function ℕ → ℂ, and the value at zero is discarded; see docs#LSeries and docs#LSeries.term .

[Aayush Rajasekaran]

Alex Kontorovich said:

Anyone who wants to work on such things is welcome to join us!...

Thanks for sharing! How can one join you folks?

[Steven Rossi]

^ I'm going through Iwaniec right now and contributing to PNTAnd to learn ANT, so very down to contribute more to the blueprint/formalization decisions

[Harald Helfgott]

This is really ambitious :). I'd be a bit more confident that the Lean/Mathlib world is ready for a full formalization of Montgomery-Vaughan (I am working on Appendix A right now) but lots of good can come out of this braver project.

[Steven Rossi]

I remember trying to formalize some of Shintani's results from Hida and it was a nightmare

[Alex Kontorovich]

Michael Stoll said:

Note that it is not the case that Mathlib's L-functions use docs#ArithmeticFunction s as input. Rather, the input is a function ℕ → ℂ, and the value at zero is discarded; see docs#LSeries and docs#LSeries.term .

Sorry, what I meant is that $L$-functions currently have domain ℕ, but we may eventually want more general domains (e.g., summing over integral ideal classes...). The jury is still out whether we really want to build this theory now, or if we want to stick to ℕ and do more "mathematically interesting" work, less API...

[Alex Kontorovich]

Harald Helfgott said:

This is really ambitious :). I'd be a bit more confident that the Lean/Mathlib world is ready for a full formalization of Montgomery-Vaughan (I am working on Appendix A right now) but lots of good can come out of this braver project.

At the moment our target is Chapter 1, so that's not too ambitious! (And we've already gotten stuck on the first few paragraphs, debating the desired generality... :sweat_smile: )

[Alex Kontorovich]

Anyone who wants to join our meetings can DM me for the zoom link (Wed's at 2), though we'll be prioritizing the in-person attendees...

[Harald Helfgott]

Already in section 1.5 you will need the Riemann-Stieltjes theory I've been implementing this week on my non-existent free time :P.

[Steven Rossi]

I can't make the meeting but if you have any notes of it after let me know

[Aayush Rajasekaran]

@Alex Kontorovich Some of the new text we inserted today made LaTeX angry -- I think this should fix it: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/877/changes/e5b8186df73df48aa0946ae5acc74bab47d945ff.

I've included this as part of PNT#877

[Alex Kontorovich]

Thanks! But that's strange that it's having trouble with markdown vs TeX? It used to be fine to intersperse either...

[Aayush Rajasekaran]

Interesting, perhaps something changed -- you can see the failure here.

It generally looked like:

Missing character: There is no ≠ (U+2260) in font [lmroman10-regular]:mapping=t
ex-text;!
Missing character: There is no ∑ (U+2211) in font [lmroman10-regular]:mapping=t
ex-text;!
Missing character: There is no μ (U+03BC) in font [lmroman10-regular]:mapping=t
ex-text;!
Missing character: There is no ∏ (U+220F) in font [lmroman10-regular]:mapping=t
ex-text;!
Missing character: There is no ∈ (U+2208) in font [lmroman10-regular]:mapping=t
ex-text;!
)

[Aayush Rajasekaran]

PNT#888 is a PR for PNT#876 (LSeries_tau_eq_riemannZeta_sq)

[Alex Kontorovich]

FYI the discussion on $\sigma$ is taking place here, so that people not following PNT+ can chime in: #mathlib4 > The Arithmetic Function `σ` @ 💬

[Aayush Rajasekaran]

PNT#1010 is a PR for PNT#931 (LSeries_d_eq_riemannZeta_pow)

[Aayush Rajasekaran]

PNT#1016 is a proof of PNT#1013, that also refactors the proof of LSeries_d_eq_riemannZeta_pow, as discussed.

[Aayush Rajasekaran]

@Alex Kontorovich I took a stab at porting some of the theorems about sigma to sigmaR. Very simple ones are easy, but it quickly bogs down into a series of additional needed hypotheses. I opened this PNT#1018 to demonstrate some of that. I also don't know what to do about statements like sigma_pos.

I'm curious what you think. It's possible I'm doing something wrong, or maybe this is as you expected?

[Alastair Irving]

This looks difficult because the Pow or HPow classes just define an arbitrary operation which doesn't satisfy any of the usual properties you'd expect. Are there any classes that extend them to have more properties? I'm worried that the results in your PR don't actually specialize to the real or complex numbers. Your condition (hmul : ∀ x y : R, (x * y) ^ k = x ^ k * y ^ k) isn't satisfied because docs#mul_rpow has additional positivity assumptions.

[Aayush Rajasekaran]

Are there any classes that extend them to have more properties?

Yeah, that's kinda the question I want Alex (and anyone else who has thoughts) to chime in on. And I feel like there's also a meta-question of how we want this "new" sigma to be used -- that shapes how we build it.

(Basically, I'm demonstrating a problem, and hoping others will supply the solution :blush: )

[Alex Kontorovich]

Thanks @Aayush Rajasekaran! For sigmaR, I had in mind that we would add whatever conditions were needed for each particular API lemma. At first we might follow the same structure as for sigma, but then we might learn that some conditions are not needed in later API lemmas, so it would be better to reorder them so as to build up what one can say with as few assumptions as possible. (Anyway, our main "goal" is to be able to work over Nat or Real or Complex, so whatever [HasPow]s we have to add will all be fine...)

[Aayush Rajasekaran]

Some housekeeping:
I think PNT#873 was closed by @Alex Kontorovich in PNT#1014
I think PNT#875 and PNT#935 were both closed by @Preston T in PNT#1006

Perhaps we can quickly confirm these at the start of today's meeting and close the issues if so?