Ostrowski's theorem

Stream: Is there code for X?

[Alex Kontorovich]

Do we have Ostrowski's theorem for p-adic/archimedean(/trivial) norms? Seems like low-hanging fruit, but I didn't see it in mathlib...? Thanks!

[Adam Topaz]

Someone did it a while ago, but it never made it to mathlib as far as I know. I don't remember where it was (it was some separate repo on github)

[Adam Topaz]

If you search zulip for "Ostrowski" then it should come up (I'm on mobile, so I can't search zulip right now)

[Alex Kontorovich]

Hmm so might it be worth it to do it again?... (As a student project?)

[Alex Kontorovich]

Adam Topaz said:

If you search zulip for "Ostrowski" then it should come up (I'm on mobile, so I can't search zulip right now)

Ah ok, thanks; I'll try...

[Adam Topaz]

Found the repo: https://github.com/RaitoBezarius/berkovich-spaces

[Alex Kontorovich]

Thanks! Looks like last commit was Aug 2021... So a student could take that and try to clean it up?...

[Adam Topaz]

Sure! I wonder if the author of that repo ( @Ryan Lahfa ) is still around?

[Ryan Lahfa]

Yes :)

[Eric Rodriguez]

Some people at Kevin's Xena meeting in 2022 were working on the generalised version for local/global fields, iirc

[Eric Rodriguez]

I'm not sure how far that got, or who ran it (I think it may have been Maria Ines but not sure so won't @)

[Adam Topaz]

what's Ostrowski for local fields?

[Kevin Buzzard]

It was Maria Ines' students. @Billy Miao do you have an update?

[Jiale Miao]

Yeah, we are currently working on Ostrowski theorem for rationals and rational function field. Rationals are almost done and we have started to PR some of the results. The project page is here: https://github.com/mariainesdff/ostrowski.

[Alex Kontorovich]

That's great, thanks! How much of Tate's thesis (say, over Q) do we have? (I'm teaching a grad course this spring; wondering how much of it I can do with Lean!...)

[Adam Topaz]

I would say we have very very little of the stuff in Tate's thesis. But this would be a very fun project! I would be happy to help with this! (I'm also teaching a graduate NT course this term, but will mostly cover the "basics")

[Adam Topaz]

ha! we actually have docs#pontryagin_dual that's a good start :)

[Johan Commelin]

Yeah, I also noticed that.

[Johan Commelin]

Unfortunately it doesn't come with many instances yet.

[Oisin McGuinness]

Per Research Seminars.org, a talk on this by Billy Miao https://researchseminars.org/talk/LondonLearningLean/21/is scheduled for Jan 12.

Looking forward to it! (I see the project source https://github.com/mariainesdff/ostrowski refers to one of Keith Conrad's excellent expositions, the others for Q, Q(i), F(T) and general number fields fields are all here: https://kconrad.math.uconn.edu/blurbs/ )

[Alex Kontorovich]

Adam Topaz said:

I would say we have very very little of the stuff in Tate's thesis. But this would be a very fun project! I would be happy to help with this! (I'm also teaching a graduate NT course this term, but will mostly cover the "basics")

That's great, I'd love help! I'm really unsure of how much I can get through, even before I try adding Lean to the mix. The course is for ≥2nd year PhD students who haven't seen p-adic numbers before, and I was (very ambitiously) hoping to cover Tate's thesis (just over Q, doing adelic Poisson summation and functional equation for zeta and Dirichlet L-functions), followed by Gelfand-Graev-PS (that is, adelic automorphic representations on GL(2), again just over Q). I had in mind for the first lecture to prove Ostrowski, which is very fun, and to me "explains" why there're the reals and p-adics and nothing else. But then I was shocked that even that's not in mathlib (yet). I suppose I'll experiment with whether trying to formalize live (with lots of sorrys everywhere) turns out to be a terrifically bad idea... I might abandon the experiment after a lecture or two and reach for the safety blanket of the blackboard...