## Stream: maths

### Topic: power series

#### Reid Barton (Jan 25 2019 at 23:26):

Has anyone built formal power series yet?

#### Kenny Lau (Jan 25 2019 at 23:27):

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

#### 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?

#### Kevin Buzzard (Jan 26 2019 at 08:43):

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

#### 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

#### 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

#### Kevin Buzzard (Jan 26 2019 at 09:16):

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

#### 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.

#### 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

#### 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"?

#### Mario Carneiro (Jan 26 2019 at 09:53):

yes, well, the typeclass instance inferred can change

#### 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

#### 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?

#### Kevin Buzzard (Jan 26 2019 at 12:49):

The notion of $I$-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]]$ which is something else. Hensel (in its full generality -- we only have it for $\mathbb{Z}_p$) provides roots in $R[[X]]$ of polynomials with coefficients in $R[[X]]$ in favourable circumstances.

#### 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

#### 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

#### 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

#### Kenny Lau (Jul 12 2019 at 14:40):

take a shot every time local appears in the proof

#### 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?

#### Johan Commelin (Jul 13 2019 at 17:53):

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

#### Johan Commelin (Jul 13 2019 at 17:53):

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

#### 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.

#### Johan Commelin (Jul 13 2019 at 18:10):

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

#### 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.

#### Johan Commelin (Jul 13 2019 at 18:12):

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

#### 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.

#### 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.

#### 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.

#### Johan Commelin (Jul 20 2019 at 05:26):

@Yury G. Kudryashov #1244

Well done Johan!

#### Johan Commelin (Jul 22 2019 at 00:58):

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

#### 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.

#### Johan Commelin (Jul 22 2019 at 06:30):

The disadvantage is that the name is quite long.

#### Chris Hughes (Jul 22 2019 at 06:33):

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

#### Johan Commelin (Jul 22 2019 at 06:48):

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

#### Johan Commelin (Jul 22 2019 at 06:48):

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

#### 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.

#### Johan Commelin (Jul 22 2019 at 06:49):

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

#### 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?

#### Mario Carneiro (Jul 22 2019 at 08:26):

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

#### 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.

#### 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?

no

#### 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

#### Johan Commelin (Jul 22 2019 at 08:33):

Ok, I undid the name change.

#### 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.

#### 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.

#### 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

#### 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

#### 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.

#### 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

#### 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 $\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

#### 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

#### Kevin Buzzard (Jul 24 2019 at 21:49):

it might make a good exercise

#### Kevin Buzzard (Jul 24 2019 at 21:50):

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

#### 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

#### 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".)

#### 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?

#### Kenny Lau (Jul 30 2019 at 13:40):

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

#### 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?

#### Kenny Lau (Jul 30 2019 at 13:46):

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

#### Kenny Lau (Jul 30 2019 at 13:47):

and then take the Cauchy sequences blah blah blah

#### Kenny Lau (Jul 30 2019 at 13:47):

just like how you construct the p-adic integers

#### Kenny Lau (Jul 30 2019 at 13:47):

this is an ultrametric

#### Kenny Lau (Jul 30 2019 at 13:48):

so an is summable iff an -> 0

#### Patrick Massot (Jul 30 2019 at 13:49):

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

#### Kenny Lau (Jul 30 2019 at 13:53):

oh right, the local basis is I^n right

at 0

#### Kenny Lau (Jul 30 2019 at 13:54):

I being the ideal (X)

#### Johan Commelin (Jul 30 2019 at 14:13):

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

#### Johan Commelin (Jul 30 2019 at 14:13):

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

#### 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+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.

oh right

#### Kevin Buzzard (Jul 30 2019 at 14:19):

Basically the norm of $cX^n+dX^{n+1}+\cdots$ is $2^{-n}$ if $c\not=0$. Now define the distance from $f$ to $g$ to be the norm of $f-g$ and there's your metric space.

#### 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 $X$ 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, $\sum_{n\geq0}a_n$ converges iff $a_n\to 0$, because $d(a,c)\leq\max\{d(a,b),d(b,c)\}$ which makes the partial sums Cauchy if $a_n\to 0$, and power series are complete so Cauchy sequences converge.

#### Johan Commelin (Jul 30 2019 at 14:31):

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

#### Johan Commelin (Jul 30 2019 at 14:31):

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

#### Johan Commelin (Jul 30 2019 at 14:33):

@Kenny Lau What do you mean?

#### Kevin Buzzard (Jul 30 2019 at 14:35):

But this is polynomials

#### Kenny Lau (Jul 30 2019 at 14:36):

aren't the constructions isomorphic

#### Kevin Buzzard (Jul 30 2019 at 14:36):

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

#### Johan Commelin (Jul 30 2019 at 14:39):

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

#### Johan Commelin (Jul 30 2019 at 14:39):

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

#### 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.

#### Johan Commelin (Jul 30 2019 at 14:40):

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

#### Kenny Lau (Jul 30 2019 at 14:40):

maybe you have unused arguments

Haha. Who knows.

#### 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.

#### Johan Commelin (Jul 30 2019 at 14:42):

A compiling version exists in the history.

#### 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

#### 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...)

#### Johan Commelin (Jul 31 2019 at 14:59):

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

#### Johan Commelin (Jul 31 2019 at 15:00):

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

#### Johan Commelin (Jul 31 2019 at 15:00):

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

#### 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.

#### 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.

#### 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...

#### Johan Commelin (Jul 31 2019 at 15:15):

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

#### 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!

#### 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 ;)

#### Johan Commelin (Aug 01 2019 at 06:47):

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

#### Jan-David Salchow (Aug 01 2019 at 06:48):

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

#### Johan Commelin (Aug 01 2019 at 06:49):

Ok, mathlib can do that already.

Last updated: May 11 2021 at 00:31 UTC