Zulip Chat Archive

Stream: maths

Topic: Hahn Series


view this post on Zulip Aaron Anderson (Feb 14 2021 at 00:20):

I currently have a stack of PRs forming on Hahn series, so I’m starting a thread.

view this post on Zulip Aaron Anderson (Feb 14 2021 at 00:22):

#6208 is needed to define multiplication, and #6226 is needed to show the product is an actual Hahn series.

view this post on Zulip Aaron Anderson (Feb 14 2021 at 00:22):

These are put to work in branch#hahn_series.

view this post on Zulip Aaron Anderson (Feb 14 2021 at 00:25):

I’m interested in any thoughts as to whether Laurent series should actually be defined as hahn_series Z _, or if I should just give an iso when both are done.

view this post on Zulip Aaron Anderson (Feb 14 2021 at 00:25):

@Kevin Buzzard

view this post on Zulip Kevin Buzzard (Feb 14 2021 at 08:31):

My plan was to define Laurent series as Hahn series with coefficients in Z and to prove that that were a localisation of power series in one variable at the variable. Thanks so much for doing this!

view this post on Zulip Aaron Anderson (Feb 15 2021 at 04:50):

Ok, #6237 gets up to the comm_ring structure.

view this post on Zulip Johan Commelin (Feb 15 2021 at 05:37):

Cool! You are moving fast!

view this post on Zulip Xavier Xarles (Feb 15 2021 at 10:16):

How nice! You did a really nice job, I am learning a lot reading what you did.

view this post on Zulip Aaron Anderson (Feb 15 2021 at 16:23):

Let me know if you have any further questions about it, it'd help the documentation.

view this post on Zulip Aaron Anderson (Feb 15 2021 at 16:24):

Other than the order theory, creating a new type of series with a convolution product is a bit boilerplate, except for a few small things that can go wrong in the distributivity/associativity proofs, which go wrong differently in each different context it seems...

view this post on Zulip Filippo A. E. Nuccio (Feb 16 2021 at 10:57):

While @Aaron Anderson was developing the more powerful theory of Hahn Series, I've amused myself defining Laurent series (in one variable), and PR it in #6258. There are still some sorrys left concerning associativity, but the basics of it being a comm_ring (when the coefficients are) is there. I've also defined coefficients (as a function from Z\mathbb{Z} to the base ring). Being much less experienced then @Aaron Anderson , my code is by far less efficient and I wonder if anything of what I've done should be kept or if the approach through Hahn series makes everything obsolete. Before going further, I'd appreciate if anyone can have a look and tell me if it is worth spending more time on my approach, or not.

view this post on Zulip Aaron Anderson (Feb 16 2021 at 17:59):

I think the biggest issue is that working with quotients is difficult.

view this post on Zulip Aaron Anderson (Feb 16 2021 at 18:03):

Personally I think it's much easier to define Laurent series as a subtype of a type of functions like how I defined Hahn series, or if you want to use ordered pairs, make the pair representation unique, like perhaps by representing it as a pair of a coefficient function with a rank, where the rank lives in with_top Z, with the rule that the rank is the largest possible rank such that all coefficients below that rank are 0.

view this post on Zulip Aaron Anderson (Feb 16 2021 at 18:09):

The benefit of your sort of pair representation is in defining the embedding of power series into Laurent series, and I'll admit I haven't gotten there yet, but I think it should still not be too bad with Hahn series

view this post on Zulip Aaron Anderson (Feb 23 2021 at 22:26):

The actual Hahn series PR #6237 is now unblocked. I've started developing the valuation at branch#hahn_series2, but won't be able to get around to it again for at least a week.

view this post on Zulip Aaron Anderson (Apr 09 2021 at 04:20):

An update on the Hahn series project if anyone wants it:

view this post on Zulip Aaron Anderson (Apr 09 2021 at 04:21):

I'm inching closer towards being able to define the field structure. The critical step that remains is proving Higman's Lemma.

view this post on Zulip Aaron Anderson (Apr 09 2021 at 04:22):

To do that, I started expanding the API on partial well-orderings, and in the process of looking into all of this, found that with partial well-orderings, we can drop the linearity assumption on the monomial group, which means that things like multivariable Laurent series should be possible. This is what #7131 is for.

view this post on Zulip Aaron Anderson (Apr 09 2021 at 04:23):

I've delayed defining Laurent series until I have the field structure, so I can define the localization map as a localization map, but if anyone has any requests for Laurent series API, I'd be happy to discuss it.

view this post on Zulip Johan Commelin (Apr 09 2021 at 05:27):

@Aaron Anderson This is becoming a pretty huge project, but I'm really happy you are doing it. I don't have a pressing need for Laurent series right now. But probably in a couple of months, yes.
And it's just great to know that by that time there will be a solid API in place!

view this post on Zulip Kevin Buzzard (Apr 09 2021 at 06:02):

Yes this is a much overdue API. Many thanks!

view this post on Zulip Aaron Anderson (Apr 09 2021 at 15:03):

Yes, this is rather more complicated than just defining Laurent series, but we should also be able to get Puiseux series for cheap, and Hahn series themselves are nice.

view this post on Zulip Aaron Anderson (Apr 09 2021 at 18:50):

Aaron Anderson said:

I'm inching closer towards being able to define the field structure. The critical step that remains is proving Higman's Lemma.

Apparently Higman's Lemma was already done in lean by @Minchao Wu in the Kruskal's Tree Theorem project

view this post on Zulip Minchao Wu (Apr 09 2021 at 23:03):

@Aaron Anderson Higman’s Lemma was done in a very early version of Lean 3 and has not yet been ported to the current mathlib. I can modernize it and make a PR if people want it.

view this post on Zulip Aaron Anderson (Apr 09 2021 at 23:06):

I am already working on it, taking inspiration from your strategy. It would need to be connected to my definitions about well-quasi orders anyway.

view this post on Zulip Aaron Anderson (Apr 10 2021 at 03:15):

branch#higmans_lemma

view this post on Zulip Aaron Anderson (Apr 12 2021 at 22:23):

Starting this at #7165

view this post on Zulip Minchao Wu (Apr 18 2021 at 13:40):

I have been trapped by other tasks last week and just came back to this. It seems that the formalization is almost done (and looks very nice), but I’ll try to see if there’s anything I can do.

view this post on Zulip Aaron Anderson (Apr 23 2021 at 21:35):

It occurs to me that finsum can probably cut a lot of the nasty proofs way down

view this post on Zulip Aaron Anderson (Apr 24 2021 at 22:31):

Hrmm... I'm not so sure. I've started at branch#hahn_finsum, and I'd like some input as to whether this is better.


Last updated: May 11 2021 at 17:39 UTC