evaluation of power series

Stream: Is there code for X?

[Antoine Chambert-Loir]

Power series (with coefficients in a ring, multiple indeterminates) can sometimes be evaluated.
This, itself, is a particular case of evaluation of power series in a topologized ring. (See Bourbaki, Algebra, IV, §4.)
In particular, endowing the ring of coefficients with the discrete topology, and the ring of formal power series its topology of simple convergence, one can substitute to the coefficients other power series, provided their order is > 0.

Is this already known to mathlib?

[Johan Commelin]

I think we don't have much. Of course there is an API for infinite sums (docs#tsum) but it hasn't really been linked up with power series.

[Antoine Chambert-Loir]

OK, “au boulot!”… (cries in silence)

[Eric Wieser]

Is docs#formal_multilinear_series.sum close?

[Antoine Chambert-Loir]

Not too far. At least, it can serve as a model. Thank you.

[Adam Topaz]

It would also be useful to be able to evaluate power series at nilpotent elements.

[Eric Wieser]

I think any power_series can be turned into a formal_multilinear_series via something like fun i, p i \smul continuous_linear_map.pi_algebra, though I don't see any evidence that we already have that result

[Antoine Chambert-Loir]

There are a few issues: 1) one needs results wrt any coefficient ring, not only fields.
2) it is tempting to have some topology on the coefficients, but most algebraic results go with the discrete topology.

If it already has another topology, stored as an instance, how can one change it locally? Does that mean that, for working about power series with coefficients in R, I have to introduce some discrete(R)?

[Eric Wieser]

Can you point to which definitions you're looking at which need fields and topologies?

[Eric Wieser]

The one I linked above needs the latter but not the former

[Jireh Loreaux]

Well, Eric, even though the def itself has minimal requirements, I think virtually all the API is for the case where 𝕜 is a normed field. The docstring itself even makes reference to the fact that it is only a priori well-behaved when the norm is less than the radius.

[Antoine Chambert-Loir]

What I mean is that docs#tsum assumes a topology on the range, something like mv_power_series S R, which I can define (topology of pointwise convergence, aka product topology) given any topology on R. If R is t2_space, then docs#has_sum.unique concludes the job.

[Antoine Chambert-Loir]

My first test was to prove that if fis a power series with coefficients given by a, then f = tsum (\lambda n, a n * T ^ n) (with obvious variations using docs#mv_power_series.monomial). If the topology on the coefficients makes it docs#t2_space, then this is true, otherwise, this can't be true because of the docs#classical.some used in the definition of tsum. On the other hand, such equalities which are true almost algebraically involve no explicit topology on the coefficients, and the discrete topology works.