scratch on power series

[t6s]

This draft PR is an attempt to formalize power series.
The goals are

• to prove useful convergence tests
• to provide arithmetic for power series
• to abstract already available definitions and lemmas (e.g. exp and trigonometric functions)

[CohenCyril]

You might find this relevant: math-comp/newtonsums#2
CC: @hivert

[hivert]

@CohenCyril Thanks for mentioning me. Concerning power series, if you only want the formal side I've a fairly developed code on /~https://github.com/hivert/FormalPowerSeries. It is largely based on Cyril's newtonsums which only dealt with truncated power series. In my code I've 2*3 differents proof for the formula for Catalan numbers. The first series uses truncated power series, the second one normal powerseries. The later are formalized as inverse limits of truncated thanks to the classical axioms of analysis. For two series, I've formalised 3 proof (generalized newton formula, lagrange inversion and differential holonomic equation). I wanted to compare how much work is required by using only truncated power series (constructive, no axioms).

As usual with me, it is work in progress and nothing is published...