Power series arithmetic in Lean

Exact and conservative power series arithmetic in Lean, built on top of the approximate arithmetic machinery in interval. The goal is reasonably fast, fully formalised, one-dimensional, truncated power series arithmetic over a variety of arithmetic classes: floating point interval arithmetic, naturals, rationals, dyadic rationals, etc.

We support the following power series operations, all of which are proven to approximate the low-order derivatives of their equivalent operations on -smooth functions:

1. Ring operations, using Karatsuba multiplication
2. Generic power series Newton solves, taking advantage of quadratic convergence for speed
3. Series inverse and square root via Newton's method, specialised so that they work on monic series without requiring scalar division (for square root, we need division by 2, so dyadic rationals are useful).
4. Miscellaneous: Shifts / multiplication by and sums of series coefficients.

For an example on a nontrivial power series, bottcher uses this repo to compute series coefficients of the Böttcher series of the Mandelbrot set at infinity. The Böttcher series describes the analytic homeomorphism from the complement of the closed unit disk to the complement of the Mandelbrot set, and can also be used to (weakly) upper bound the area of the set. The bottcher repo is also an example of a custom Newton solver, and indeed this custom Newton solver uses both inverse and square root (each Newton solvers), of which square root builds on inverse.

Building

1. Install elan (brew install elan-init on Mac)
2. lake build