Zulip Chat Archive

Stream: maths

Topic: power series


view this post on Zulip Reid Barton (Jan 25 2019 at 23:26):

Has anyone built formal power series yet?

view this post on Zulip Kenny Lau (Jan 25 2019 at 23:27):

just take $$\varprojlim_{n \in \Bbb N} A[X]/(X^n)$$ :P

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 08:38):

This is an interesting question. I believe Patrick has done ring completions so that would be one approach. Alternatively one could just take the stuff on polynomial rings and just delete all the finite support hypotheses! In retrospect power series would have been easier to write than polynomials I guess?

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 08:43):

These seem like two genuinely different approaches. Which would be best?

view this post on Zulip Mario Carneiro (Jan 26 2019 at 08:44):

yes, power series are easier than polynomials, although you still need some finiteness for the monomials so that multiplication is well defined

view this post on Zulip Mario Carneiro (Jan 26 2019 at 08:46):

That said, it's not clear to me which power series ring is the most useful - there are many ways to generalize bits of the polynomial construction, like Laurent series

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 09:16):

From an algebraic geometry point of view, the power series ring R[[X]]R[[X]] is the most important missing thing, i.e. a ring structure on nat -> R.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 09:17):

If you import algebra.pi_instances I think you get a multiplication on these functions, which is pointwise multiplication on the target, but that's the wrong one.

view this post on Zulip Patrick Massot (Jan 26 2019 at 09:42):

This is clearly a case for type wrapping. Define power_series R = nat -> R and define the correct instance

view this post on Zulip Patrick Massot (Jan 26 2019 at 09:43):

Unfold and apply_instance for addition

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 09:43):

If I unfold power_series R will this then actually change what apply_instance finds for multiplication? i.e. can I get some code which changes behaviour if I insert an "unfold"?

view this post on Zulip Mario Carneiro (Jan 26 2019 at 09:53):

yes, well, the typeclass instance inferred can change

view this post on Zulip Mario Carneiro (Jan 26 2019 at 09:54):

if you just unfold you will still have the original instance, it will just be a nonstandard typeclass term at that point

view this post on Zulip Reid Barton (Jan 26 2019 at 12:00):

So there are also some new phenomena which arise for power series, for example:

  • If F(X) and G(X) are power series then we can make sense of F(G(X)) if the constant term of G is zero. I guess the proper generalization is that if F(X) in R[[X]], a in I and R is I-adically complete then we can evaluate F(a). Do we already have these latter notions (maybe in the perfectoid spaces project)?
  • If F(X) = u X + ... with u a unit in R then we can find an inverse power series G(X) = u^-1 X + ... Is this related to Hensel's lemma?

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 12:49):

The notion of II-adically complete will be in the perfectoid space project, although I am not sure we have a good API for it. The "correct" way to do this would be to go through some book like Atiyah--Macdonald I guess, whereas we just needed the definition. This stuff will come as I start actually having to use the notion of completeness in lemmas (this is imminent but has not yet happened; I've spent the last two weeks writing references and dealing with other work admin, but my urgent work job list is now very small). Inverse power series -- this is not Hensel. It's the statement that R[[X]]=R[[F]]R[[X]]=R[[F]] which is something else. Hensel (in its full generality -- we only have it for Zp\mathbb{Z}_p) provides roots in R[[X]]R[[X]] of polynomials with coefficients in R[[X]]R[[X]] in favourable circumstances.

view this post on Zulip Kevin Buzzard (Jan 26 2019 at 14:18):

https://github.com/leanprover-community/perfectoid-spaces/tree/master/src/for_mathlib is the topology on a ring generated by an ideal of the ring

view this post on Zulip Patrick Massot (Jan 26 2019 at 18:16):

We do have everything to define I-adically complete in the perfectoid project: the adic-topology and completeness for topological rings

view this post on Zulip Johan Commelin (Jul 12 2019 at 14:36):

Lean now knows that multivariate power series over a local ring form a local ring:
https://github.com/leanprover-community/mathlib/blob/power-series/src/data/power_series.lean#L749-L750

view this post on Zulip Kenny Lau (Jul 12 2019 at 14:40):

take a shot every time local appears in the proof

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 17:49):

It's good I saw this before trying to implement power series myself. Do you plan to redefine exp/sin/... in any complete normed algebra?

view this post on Zulip Johan Commelin (Jul 13 2019 at 17:53):

Hmm... I've only done formal power series. Next on my list is formal Laurent series.

view this post on Zulip Johan Commelin (Jul 13 2019 at 17:53):

I've not made any connections to topology/analysis.

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 18:08):

Could you please poke me once formal power series will be merged into master branch? I'll start working on connections to topology/analysis.

view this post on Zulip Johan Commelin (Jul 13 2019 at 18:10):

Sure, I might PR the basics within the next few days

view this post on Zulip Johan Commelin (Jul 13 2019 at 18:11):

I was planning on adding has_inv for formal power series over a field, and then I think there is a nice basis that should be ready for PR.

view this post on Zulip Johan Commelin (Jul 13 2019 at 18:12):

General question: should I call this data structure mv_power_series or mv_formal_power_series?

view this post on Zulip Chris Hughes (Jul 13 2019 at 18:15):

Hmm... I've only done formal power series. Next on my list is formal Laurent series.

How do you do that? I skim read a paper about that and there are multiple ways over several variables.

view this post on Zulip Johan Commelin (Jul 13 2019 at 18:18):

I will PR formal power series first. Not sure if I'll do formal Laurent series with multiple variables... In practice I very rarely see the multivariate case. Of course I will be angry with myself if I only do the single variable case...
But like you said, there are several approaches, and it's not clear to me which one I should/want to take.

view this post on Zulip Yury G. Kudryashov (Jul 13 2019 at 18:40):

I think, mv_power_series is OK, because we can add topological properties to the same type.

view this post on Zulip Johan Commelin (Jul 20 2019 at 05:26):

@Yury G. Kudryashov #1244

view this post on Zulip Kevin Buzzard (Jul 20 2019 at 09:56):

Well done Johan!

view this post on Zulip Johan Commelin (Jul 22 2019 at 00:58):

I've now made the name mv_formal_power_series. Is this too long?

view this post on Zulip Johan Commelin (Jul 22 2019 at 06:29):

@Chris Hughes @Sebastien Gouezel @Patrick Massot What do you think of the name? Should it be power_series α or formal_power_series α? If we decide on the latter, I should also change the file name.

view this post on Zulip Johan Commelin (Jul 22 2019 at 06:30):

The disadvantage is that the name is quite long.

view this post on Zulip Chris Hughes (Jul 22 2019 at 06:33):

What's an informal power series? I would stick to just power_series.

view this post on Zulip Johan Commelin (Jul 22 2019 at 06:48):

I guess it is an infinite sum in a topological ring?

view this post on Zulip Johan Commelin (Jul 22 2019 at 06:48):

I don't know. I don't do analysis.

view this post on Zulip Johan Commelin (Jul 22 2019 at 06:49):

Wikipedia says that Laurent_series has unbounded below coefficients, whereas formal_Laurent_series has bounded below coefficients.

view this post on Zulip Johan Commelin (Jul 22 2019 at 06:49):

I thought that maybe for power series there is also a distinction that matters.

view this post on Zulip Johan Commelin (Jul 22 2019 at 08:25):

Another related question (@Mario Carneiro): Should this go into data/power_series.lean or ring_theory/power_series.lean?

view this post on Zulip Mario Carneiro (Jul 22 2019 at 08:26):

if you can remove the dependency on ring_theory then it can go in data

view this post on Zulip Johan Commelin (Jul 22 2019 at 08:28):

I think I would rather not remove that dep. I'll just move the file to ring_theory. After all, this isn't a generic data structure that will be used all over the place.

view this post on Zulip Johan Commelin (Jul 22 2019 at 08:29):

@Mario Carneiro Do you have an opinion on the name mv_formal_power_series vs mv_power_series?

view this post on Zulip Mario Carneiro (Jul 22 2019 at 08:30):

no

view this post on Zulip Mario Carneiro (Jul 22 2019 at 08:30):

I think chris has a point that it's not like we have some other definition we need to distinguish

view this post on Zulip Johan Commelin (Jul 22 2019 at 08:33):

Ok, I undid the name change.

view this post on Zulip Sebastien Gouezel (Jul 22 2019 at 08:47):

I prefer power_series instead of formal_power_series. For converging power series, we will mainly use analytic or something like that, and if necessary we can also use converging_power_series.

view this post on Zulip Yao Liu (Jul 24 2019 at 20:34):

Sorry if this is obvious: Does this implementation allow one to define a power series indexed by any monoid? Laurent series would be indexed by an additive group (lattice), "supported" in a cone. Not sure if that's good for proving anything, but one may regard Weyl's character formula as a formula in such a ring.

view this post on Zulip Jesse Michael Han (Jul 24 2019 at 21:36):

no , i don't think so---the "indexing" you're referring to is in the degrees, and I think the current implementation hard-codes those as being in the natural numbers

however, the only structure enforced on sigma (the variables) in the definition is decidable_eq, so you can additionally put whatever structure you like on that

view this post on Zulip Yao Liu (Jul 24 2019 at 21:39):

that's what I meant, the terms (monomials) are indexed by points on a lattice. Thanks for the clarification

view this post on Zulip Kevin Buzzard (Jul 24 2019 at 21:43):

I guess in general you will need some sort of filter on your abelian group with some finiteness hypothesis involving how it interacts with the group law in order to define the object and to prove that multiplication of power series makes sense.

view this post on Zulip Jesse Michael Han (Jul 24 2019 at 21:43):

@Yao Liu you make a good point though---if we work with e.g. valued fields later, we'll need formal laurent series indexed by an arbitrary ordered abelian group, so why not generalize the definition and remove the hardcoded nat from power_series.lean?

it might make a good exercise

view this post on Zulip Kevin Buzzard (Jul 24 2019 at 21:47):

You'll have to think about exactly what is allowed. You can't make formal power series nZanzn\sum_{n\in\mathbb{Z}}a_nz^n because there are convergence issue when multiplying. You need to make sure that the series are zero on some set in some filter with some finiteness property wrt addition

view this post on Zulip Kevin Buzzard (Jul 24 2019 at 21:49):

For all I know, polynomials, Laurent series, formal power series, multivariate polynomials, multivariate power series etc are all special cases of some general notion about functions with support in or disjoint from some element of a filter

view this post on Zulip Kevin Buzzard (Jul 24 2019 at 21:49):

it might make a good exercise

view this post on Zulip Kevin Buzzard (Jul 24 2019 at 21:50):

but my point is that "indexed by an arbitrary ordered abelian group" needs some thought

view this post on Zulip Jesse Michael Han (Jul 24 2019 at 22:11):

ah yeah, i guess we want the inner terms of the cauchy product to be finite sums, so for Laurent series you need something like all intervals being finite

view this post on Zulip Johan Commelin (Jul 25 2019 at 01:50):

Right, there are all sorts of generalisations, but I didn't know the "one generalisation that rules them all".
Also, in real world math, you just wave your hands and say "the sum is finite". In Lean that's quite a subtle thing to do, and so even plain old formal Laurent series are non-trivial to write down. (That is, if you want to write them as a series. Of course I can just define them as the field of fractions of power series, but that is "cheating".)

view this post on Zulip Chris Hughes (Jul 30 2019 at 13:39):

Is there a nice way of adding together infinitely many power series, such that the corresponding sum for each coefficient is finite? Is there some topology that makes this work?

view this post on Zulip Kenny Lau (Jul 30 2019 at 13:40):

yes, the p-adic topology!

view this post on Zulip Kenny Lau (Jul 30 2019 at 13:40):

R[[X]] is the X-adic completion of R[X]

view this post on Zulip Chris Hughes (Jul 30 2019 at 13:42):

I see. Explain further. So you need a topology on R[X] to start with? And then how do you extend this topology? Is this a uniform space completion?

view this post on Zulip Kenny Lau (Jul 30 2019 at 13:46):

you define a norm on R[X] that assigns 2^-deg(p) to p

view this post on Zulip Kenny Lau (Jul 30 2019 at 13:47):

and then take the Cauchy sequences blah blah blah

view this post on Zulip Kenny Lau (Jul 30 2019 at 13:47):

just like how you construct the p-adic integers

view this post on Zulip Kenny Lau (Jul 30 2019 at 13:47):

this is an ultrametric

view this post on Zulip Kenny Lau (Jul 30 2019 at 13:48):

so an is summable iff an -> 0

view this post on Zulip Patrick Massot (Jul 30 2019 at 13:49):

Why do you want a norm? You can simply use the adic topology

view this post on Zulip Kenny Lau (Jul 30 2019 at 13:53):

oh right, the local basis is I^n right

view this post on Zulip Kenny Lau (Jul 30 2019 at 13:53):

at 0

view this post on Zulip Kenny Lau (Jul 30 2019 at 13:54):

I being the ideal (X)

view this post on Zulip Johan Commelin (Jul 30 2019 at 14:13):

Unfortunately we don't have adic topology in mathlib yet.

view this post on Zulip Johan Commelin (Jul 30 2019 at 14:13):

It's on the todo list to move it from the perfectoid project to mathlib

view this post on Zulip Kevin Buzzard (Jul 30 2019 at 14:18):

you define a norm on R[X] that assigns 2^-deg(p) to p

This isn't right. The idea is that X should be "small", so for example that 1+X+X2+X3+1+X+X^2+X^3+\cdots converges. So the norm on R[X] assigns 2^-v(p) to p, where v(p) is the largest power of X dividing p.

view this post on Zulip Kenny Lau (Jul 30 2019 at 14:18):

oh right

view this post on Zulip Kevin Buzzard (Jul 30 2019 at 14:19):

Basically the norm of cXn+dXn+1+cX^n+dX^{n+1}+\cdots is 2n2^{-n} if c0c\not=0. Now define the distance from ff to gg to be the norm of fgf-g and there's your metric space.

view this post on Zulip Kevin Buzzard (Jul 30 2019 at 14:22):

For an infinite sequence of power series, the property that the corresponding sum for each coefficient is finite is equivalent to the property that the max power of XX dividing the power series tends to infinity, so is equivalent to the property that the norms of the terms are tending to zero. And in this nonarchimedean (warning: this word is used in several different ways in maths) setting, n0an\sum_{n\geq0}a_n converges iff an0a_n\to 0, because d(a,c)max{d(a,b),d(b,c)}d(a,c)\leq\max\{d(a,b),d(b,c)\} which makes the partial sums Cauchy if an0a_n\to 0, and power series are complete so Cauchy sequences converge.

view this post on Zulip Johan Commelin (Jul 30 2019 at 14:31):

Btw, I'm defining v(p) right now.

view this post on Zulip Johan Commelin (Jul 30 2019 at 14:31):

Or actually, I've been working on it over the last few days.

view this post on Zulip Kenny Lau (Jul 30 2019 at 14:31):

but you already have it...?

view this post on Zulip Johan Commelin (Jul 30 2019 at 14:33):

@Kenny Lau What do you mean?

view this post on Zulip Kenny Lau (Jul 30 2019 at 14:33):

we have p-adics in mathlib

view this post on Zulip Kevin Buzzard (Jul 30 2019 at 14:35):

But this is polynomials

view this post on Zulip Kenny Lau (Jul 30 2019 at 14:36):

aren't the constructions isomorphic

view this post on Zulip Kevin Buzzard (Jul 30 2019 at 14:36):

Not in the sense that there's an isomorphism R[X] = Z_p

view this post on Zulip Johan Commelin (Jul 30 2019 at 14:39):

@Kenny Lau You're thinking too much about Witt vectors.

view this post on Zulip Johan Commelin (Jul 30 2019 at 14:39):

Unfortunately Witt vectors will not make it too mathlib in Lean 3.4.2

view this post on Zulip Johan Commelin (Jul 30 2019 at 14:39):

I've done the entire construction, but I'm hitting Lean bugs, and as a result the file is extremely slow.

view this post on Zulip Johan Commelin (Jul 30 2019 at 14:40):

Take a look at the history of the witt-vectors branch, if you're interested.

view this post on Zulip Kenny Lau (Jul 30 2019 at 14:40):

maybe you have unused arguments

view this post on Zulip Johan Commelin (Jul 30 2019 at 14:41):

Haha. Who knows.

view this post on Zulip Johan Commelin (Jul 30 2019 at 14:42):

At the moment the file doesn't compile. But I can't bring up the courage to make it cleaner if it will always be slow anyway.

view this post on Zulip Johan Commelin (Jul 30 2019 at 14:42):

A compiling version exists in the history.

view this post on Zulip Johan Commelin (Jul 31 2019 at 14:58):

@Chris Hughes I'm not completely done yet, but what I have is pushed to https://github.com/leanprover-community/mathlib/blob/power-series-order/src/ring_theory/power_series.lean#L1084

view this post on Zulip Johan Commelin (Jul 31 2019 at 14:59):

It is all in one variable. I guess there are solutions in the multivariate case (maybe if you have finitely many variables, and you order them...)

view this post on Zulip Johan Commelin (Jul 31 2019 at 14:59):

@Kevin Buzzard Do you know if the multivariate case has some use?

view this post on Zulip Johan Commelin (Jul 31 2019 at 15:00):

We will want to compose/eval multivariate power series when doing formal group laws.

view this post on Zulip Johan Commelin (Jul 31 2019 at 15:00):

But for that I guess we don't need a notion of order.

view this post on Zulip Johan Commelin (Jul 31 2019 at 15:01):

A unified treatment of compose/eval is not so easy. I guess the best way is to use topology, and show that in certain cases formal arguments suffice for the convergence hypothesis.

view this post on Zulip Kevin Buzzard (Jul 31 2019 at 15:14):

I guess in the multivariate case the valuations are the old-style way of doing algebraic geometry, there are all sorts of funny valuations on a multivariate power series ring I think, I don't know if these specific ones are any better than any others.

view this post on Zulip Kevin Buzzard (Jul 31 2019 at 15:15):

I guess one observation is that over k[[T]] the T-adic valuation is actually intrinsic, but over k[[X,Y]] there are a gazillion changes of variables which make your X-adic and Y-adic valuations less special. However I bet there will be some use for them somewhere...

view this post on Zulip Johan Commelin (Jul 31 2019 at 15:15):

Right... we'll develop it when we need it.

view this post on Zulip Johan Commelin (Jul 31 2019 at 17:42):

Hmm, I just realised that I've been very very stupid. I should have used Chris's multiplicity library. My apologies!

view this post on Zulip Jan-David Salchow (Aug 01 2019 at 06:46):

Formal power series in multiple variables are heavily used in symplectic topology ... as generating function, even in countably many variables, sometimes even completed in that direction ;)

view this post on Zulip Johan Commelin (Aug 01 2019 at 06:47):

We have those. The question is, do you compose them?

view this post on Zulip Jan-David Salchow (Aug 01 2019 at 06:48):

No, we only multiply and add them. Sometimes we act on them

view this post on Zulip Johan Commelin (Aug 01 2019 at 06:49):

Ok, mathlib can do that already.


Last updated: May 11 2021 at 00:31 UTC