Summing Laurent Series

Stream: maths

[Aaron Anderson]

We now have formal docs#laurent_series, so I started looking towards an API for the sum of a Laurent series. However, when poking around the analysis library for the connection between analytic function and power_series, I found that it looks like there is none at the moment.

[Aaron Anderson]

I can still define some infinite sums, and prove some relations between them, but it will have little relation to any real API in the analysis folder.

[Aaron Anderson]

Does anyone with experience with that part of the analysis library have opinions on whether any of this is worth doing now, without waiting for a better connection to formalpower_series first?

[Johan Commelin]

cc @Sebastien Gouezel

[Sebastien Gouezel]

There are two different things here:

• specializing the existing analytic functions to one variables, to create a link with power series. This will really be a specialization of what we have for analytic functions (all the file analysis/analytic/basic.lean makes sense when you specialize it to think of p n as a number instead of an n-multilinear map). So here, there will be no need to reprove any theorem, only reexpress them in the more specialized language. (Just like naive one-dimensional derivatives are a specialization of the general Frechet derivative).

• considering finite order singularities of meromorphic functions (i.e., Laurent series). There, we will not be able to specialize the general facts, as this is a more specific one-dimensional phenomenon. So an API will be built from scratch here. However, it would probably make sense to state and prove the results by separating the finitely many terms with negative exponents, and the power series parts. So, doing first the power series part seems more reasonable.