Verified computation of the Mandelbrot Böttcher series

Verified computation of the Böttcher series of the Mandelbrot set: the power series around infinity of the analytic homeomorphism from the complement of the closed unit disk to the complement of the Mandelbrot set. This repo builds on top of three other Lean repositories:

1. ray: Definitions and basic results about complex dynamics, including Böttcher coordinates and the connectivity of the Mandelbrot set.
2. interval: Conservative interval arithmetic using software floating point.
3. series: Conservative power series arithmetic.

All of which of course build on top of the wonderful mathlib base!

Building

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