Infinite sums of power series

Stream: maths

[Antoine Chambert-Loir]

I need to to teach Lean about power_series, substitution of other power_series, etc.
I can imagine three possibilities:

• for algebraic purposes, what is really needed is to have (infinite) sums of power series which have finite support coefficientwise,
  which requires to build an API for something like pointwise_finsupp (or locally_finsupp).

• but the easiest mathematical way to say it is to endow the ring of coefficients with the discrete topology, the ring of power series with the product topology, and then it's the classical theory of summable families, as for docs#tsum
  This is what Bourbaki does (Algebra, chapter IV, §4).

• and if the ring of coefficients already has some topology, we could in principle deal with it, except that if the topology is not Hausdorff, there is no uniqueness of limits, which is ridiculous in the case of interest.

Do you have an opinion of the best way to handle this? Define a continuous docs#ring_equiv from mv_power_series S (discrete R) to mv_power_series S R, where discrete R is the topological ring given by R and the discrete topology, and observe that it maps pointwise finitely supported families to summable families?

[Johan Commelin]

Do we know any real-world maths examples where there is a relevant topology on the ring of coefficients?

[Johan Commelin]

If not, I think it would be best to hide the discrete topology behind some API, so that users never have to think about a topology on the coefficients.
And yes, linking to tsum asap sounds like a good idea.

[Jireh Loreaux]

I mean, what about \Q or \R? Surely that comes up.

[Michael Stoll]

If you have a power series expansion of a holomorphic function, you may want to "shift" it, e.g.

$$\exp(x+1) = \sum_{n=0}^\infty \frac{(x+1)^n}{n!} = \sum_{n=0}^\infty e \frac{x^n}{n!}\,$$

Here you get infinite sums for the coefficients of the result (which you need to converge), so this is slightly different from the original question, but it might still be reasonable to allow for this.

[Yury G. Kudryashov]

We have a very general version of this shift in docs#FormalMultilinearSeries.changeOrigin

[Anatole Dedecker]

To me the natural thing to do would be to define evaluation of a power series and the topology on power series when we have a topology on the ring, and then in places where the topology doesn't matter (typically substitution by a multiple of X) you can just remove it from the assumptions and add the discrete topology by hand (maybe we need a discretize tactic?). But of course if we want to substitute power series with a nonzero constant coefficient we need to care about the topology (and prove everything converges).

[Anatole Dedecker]

To define evaluation a naive hope would be to construct a docs#FormalMultilinearSeries from a power series, but I'm guessing assumptions don't match up

[Kevin Buzzard]

This is extremely delicate in number theory because there are various power series rings which genuinely have more than one topology on them (in the sense that number theorists want more than one topology on them). For example I have seen papers talking about the $p$-adic, the $X$-adic, and the $(p,X)$-adic topology on $\mathbb{Z}_p[[X]]$. My instinct is that we should not be putting any topology on $R[[X]]$ globally, but make the $X$-adic topology (the one where neighbourhoods of 0 are $X^nR[[X]]$) available as a def and so people can add it as a local instance when it's the one they care about. When $R$ has a topology one has to decide whether $X^n$ tends to zero or not as $n\to\infty$, and in number theory sometimes the answer is yes and sometimes it's no.

[Antoine Chambert-Loir]

Yury G. Kudryashov said:

We have a very general version of this shift in docs#FormalMultilinearSeries.changeOrigin

This is over fields only, and that does not suffice for algebra.

[Anatole Dedecker]

I think Yury was answering Michael's comment.

[Anatole Dedecker]

Kevin Buzzard said:

This is extremely delicate in number theory because there are various power series rings which genuinely have more than one topology on them (in the sense that number theorists want more than one topology on them). For example I have seen papers talking about the $p$-adic, the $X$-adic, and the $(p,X)$-adic topology on $\mathbb{Z}_p[[X]]$. My instinct is that we should not be putting any topology on $R[[X]]$ globally, but make the $X$-adic topology (the one where neighbourhoods of 0 are $X^nR[[X]]$) available as a def and so people can add it as a local instance when it's the one they care about. When $R$ has a topology one has to decide whether $X^n$ tends to zero or not as $n\to\infty$, and in number theory sometimes the answer is yes and sometimes it's no.

I'm no number theorist so don't take my opinion too seriously, but to me this seems like a "we will need type aliases anyways", and since the product topology on coefficients (I think this is the $(X, p)$-adic topology in your case?) works and gives a natural result in all cases we shouldn't be afraid to make it an instance. This is similar to how we have docs#ContinousLineaMap.hasOpNorm and then things like docs#WeakDual for more specific cases.

[Kevin Buzzard]

The $X$-adic topology is: "ignore any topology on $R$ and make $X^nR[[X]]$ a basis of neighbourhoods of 0", so it's "give R the discrete topology, identify $R[[X]]$ with Nat -> R and give it the product topology"

[Antoine Chambert-Loir]

Apparently, most lemmas assume the topology is given as an instance. Once thing I don't know how to do then, is how to make Lean work with multiple topologies at the same time.

[Kevin Buzzard]

You can use a type synonym. Def Y := X will forget any topology on X so you can put a new topology on Y.

[Kevin Buzzard]

Alternatively you just put @ everywhere and feed the right topology into the lemmas.

[Johan Commelin]

@Antoine Chambert-Loir I will revise my recommendation: assume that R has a topology, and use that for the full development.

Also, in the first attempt, just make everything an instance. We can worry about uninstancing things once the development is done.

[Johan Commelin]

Note that if we require that R has a topology, then we can add [DiscreteTopology R] as a condition to require that it is discrete, in case where we want to do abstract algebra.

We can figure out later whether that means we will sometimes use Discrete \Z_p as ring of coefficients, or whether there will be an AlgebraicPowerSeries \Z_p that forces a discrete topology on \Z_p. Or whether we manage the whole thing with instances that are locally switched on and off.