power series

Stream: maths

[Reid Barton]

Has anyone built formal power series yet?

[Kenny Lau]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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

[Patrick Massot]

Unfold and apply_instance for addition

[Kevin Buzzard]

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]

yes, well, the typeclass instance inferred can change

[Mario Carneiro]

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

[Reid Barton]

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]

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]

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]

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

[Johan Commelin]

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]

take a shot every time local appears in the proof

[Yury G. Kudryashov]

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]

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

[Johan Commelin]

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

[Yury G. Kudryashov]

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]

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

[Johan Commelin]

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]

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

[Chris Hughes]

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]

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]

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

[Johan Commelin]

@Yury G. Kudryashov #1244

[Kevin Buzzard]

Well done Johan!

[Johan Commelin]

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

[Johan Commelin]

@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]

The disadvantage is that the name is quite long.

[Chris Hughes]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

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

[Mario Carneiro]

no

[Mario Carneiro]

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

[Johan Commelin]

Ok, I undid the name change.

[Sebastien Gouezel]

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]

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]

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]

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

[Kevin Buzzard]

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]

@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]

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]

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]

it might make a good exercise

[Kevin Buzzard]

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

[Jesse Michael Han]

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]

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]

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]

yes, the p-adic topology!

[Kenny Lau]

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

[Chris Hughes]

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]

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

[Kenny Lau]

and then take the Cauchy sequences blah blah blah

[Kenny Lau]

just like how you construct the p-adic integers

[Kenny Lau]

this is an ultrametric

[Kenny Lau]

so an is summable iff an -> 0

[Patrick Massot]

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

[Kenny Lau]

oh right, the local basis is I^n right

[Kenny Lau]

at 0

[Kenny Lau]

I being the ideal (X)

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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.

[Kenny Lau]

oh right

[Kevin Buzzard]

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]

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]

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

[Johan Commelin]

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

[Kenny Lau]

but you already have it...?

[Johan Commelin]

@Kenny Lau What do you mean?

[Kenny Lau]

we have p-adics in mathlib

[Kevin Buzzard]

But this is polynomials

[Kenny Lau]

aren't the constructions isomorphic

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

maybe you have unused arguments

[Johan Commelin]

Haha. Who knows.

[Johan Commelin]

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]

A compiling version exists in the history.

[Johan Commelin]

@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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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]

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

[Johan Commelin]

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

[Jan-David Salchow]

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]

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

[Jan-David Salchow]

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

[Johan Commelin]

Ok, mathlib can do that already.

[Filippo A. E. Nuccio]

I see that docs#power_series.inv_of_unit is supposed to be the theorem that "A formal power series is invertible if the constant coefficient is invertible." It is a def:

noncomputable def power_series.inv_of_unit {R : Type u_1} [ring R] (φ : power_series R) (u : Rˣ) :
power_series R

which I understand as "given a power series and a unit in the coefficient ring, this defines a new power series". And then there is a theorem (namely docs#power_series.mul_inv_of_unit) saying that if the unit above happens to be the constant coefficient (so that this constant coefficient is, in particular, invertible), then the power series defined in power_series.inv_of_unit is really the inverse of the power series I started with. So I have two questions:

1. Isnt' the piece of docs saying "A formal power series is invertible if the constant coefficient is invertible." more pertinent to the final theorem power_series.mul_inv_of_unit rather than to the def?
2. Can someone explain to me the design choice? I would have naively defined power_series.inv_of_unit as follows

def power_series.inv_of_unit' {R : Type u_1} [ring R] (φ : power_series R)
  (h : is_unit (power_series.constant_coeff R φ)) : power_series R

but evidently this was not the right way to go.

[Riccardo Brasca]

Why not a term of type(power_series R)ˣ? The more boundled stuff the better I would say.

[Riccardo Brasca]

But I agree it's a little strange written like that.

[Filippo A. E. Nuccio]

Riccardo Brasca said:

Why not a term of type(power_series R)ˣ? The more boundled stuff the better I would say.

You mean a term of type Rˣ, I guess?

[Filippo A. E. Nuccio]

Yes, this would be even better, but at any rate I find it odd to define something that is potentially useless (when applied to u that is not the constant coefficient) and then to say that in the special case when we apply the def to the constant coefficient, we get something usfeul.

[Riccardo Brasca]

I misread the theorem, and indeed I am now confused. What is φ.inv_of_unit u? I mean mathematically.

[Filippo A. E. Nuccio]

It is the def: it is a power series built out of a pair (f, u) where f is a power series, and u is a unit in the coefficient ring.

[Filippo A. E. Nuccio]

When u is the constant coefficient f 0 (so that, in particular, this is invertible), the definition is precisely that of the inverse of f.

[Filippo A. E. Nuccio]

When u is not the constant coefficient, it is garbage.

[Riccardo Brasca]

Very weird, I agree

[Filippo A. E. Nuccio]

It somehow has something to do with non-uniqueness of inverses in disgusting types, but I wonder if we really want (multivariate) power series over types where inverses are not unique...

[Yaël Dillies]

Possibly better written using[invertible (f 0)]?

[Adam Topaz]

My guess is that mathematically it means to replace the constant coeff of phi with u, and take the inverse of the resulting power series. This is indeed a strange design decision

[Filippo A. E. Nuccio]

Yaël Dillies said:

Possibly better written using[invertible (f 0)]?

The problem is that this comes from multivariable power series so we cannot really " evaluate at 0".

[Filippo A. E. Nuccio]

Adam Topaz said:

My guess is that mathematically it means to replace the constant coeff of pho with u, and take the inverse of the resulting power series. This is indeed a strange design decision…

Yes, that' s correct.

[Filippo A. E. Nuccio]

I am open to perform some refactoring, if there is some consensus.

[Yaël Dillies]

Sorry, invertible f.constant_coeff

[Adam Topaz]

I think your approach using is_unit is perfectly sensible!

[Eric Wieser]

I like the invertible approach since in principle we could make it computable

[Filippo A. E. Nuccio]

I might add that definition with a prime and then a lemma saying that when u is the const coeff they yield the same thing?

[Eric Wieser]

Right now the only reason it's noncomputable is:

• It doesn't take decidable_eq sigma. I don't think it's contentious that you ought to be able to distinguish your variables in a power series.
• Stupid finsupp stuff that is really easy to fix, but is on the wrong side of the port

[Adam Topaz]

@Eric Wieser fair enough. I guess that’s one benefit of the current approach which boils down to docs#mv_power_series.inv.aux

[Eric Wieser]

Though invertible can be a pain, so the current units approach may not be any worse

[Yaël Dillies]

Yes, the current approach is weird only because it takes an element equal tof.constant_coeff and a two-sided inverse of it, rather than just the two-sided inverse.

[Eric Wieser]

AH, good point

[Eric Wieser]

This feels analogous to the matrix stuff where we link invertibility of the determinant and the matrix

[Eric Wieser]

docs#matrix.invertible_equiv_det_invertible is an example of the result there

[Filippo A. E. Nuccio]

Well, it would seem rather something like

1. (def) given a matrix A and a unita, define a matrix B
2. (thm) If a=det Athen B is the inverse of A.

[Eric Wieser]

That def and the thm combined are the fields of invertible ah nevermind, there's no requirement that a matches A

[Eric Wieser]

I think I'm sold on the invertible approach, which looks like

def invertible_of_invertible_constant_coeff [invertible f.constant_coeff] : invertible f :=
{ inv := -- the function in terms of `⅟f.constant_coeff` and `f`
  mul_inv := _,
  inv_mul := _ }

-- optional and presumably true
def invertible_constant_coeff_of_invertible [invertible f] : invertible f.constant_coeff :=
{ inv := (⅟f).constant_coeff, ... }

[Adam Topaz]

docs#invertible

[Violeta Hernández]

Filippo A. E. Nuccio said:

Yes, this would be even better, but at any rate I find it odd to define something that is potentially useless (when applied to u that is not the constant coefficient) and then to say that in the special case when we apply the def to the constant coefficient, we get something usfeul.

This sort of design is all over Mathlib. Unless you need a hypothesis in order to define data (as would be the case for a nonempty hypothesis, for instance), it's almost always more convenient to unbundle data and proofs.

[Violeta Hernández]

What happens otherwise is that you have to carry around your proof terms all over the place

[Violeta Hernández]

For an example of how this can get bad, look at docs#well_founded.min. It takes in a nonempty h assumption, which means that every time you want to refer to a minimum in your proof, you have to pass in that proof again.

[Violeta Hernández]

You can of course just use let, but you can still see how this gets a bit annoying

[Violeta Hernández]

Garbage data doesn't really change any of the non-garbage theorems. Very occasionally your garbage data will coincidentally allow you to weaken some assumptions, which while mathematically insignificant is certainly convenient.

[Violeta Hernández]

An exception would of course be if you want to construct a member of a subtype, or other type with bundled proofs. You gain some convenience by doing so, and lose other. So you should go with what works best for your application.