No results found

ray

Formalizing results about the Mandelbrot set in Lean

The Mandelbrot set is connected

build

The goal of this repository is to formalize standard results about the Mandelbrot set in Lean. The main result is that the Mandelbrot set and its complement are connected, by exhibiting the analytic Böttcher homeomorphism from the exterior of the Mandelbrot set to the exterior of the closed unit disk. But I'm also using it to learn Lean generally, which means detours along the way. The main results are

  • Hartogs's theorem - Hartogs.lean: Let be a separable Banach space, and a function which is analytic along each axis at each point in an open set . Then is jointly analytic in .

  • Bottcher's theorem - BottcherNear.lean: Let be analytic with a monic superattracting fixpoint at 0, so that . Then there is an analytic near 0 s.t. . If is also analytic in a parameter , then is also analytic in .

  • Analytic continuation of the Böttcher map up to the critical value - Bottcher.lean, Ray.lean: Let be a compact, 1D complex manifold, a holomorphic map with a fixpoint , and assume has no other preimages of . Starting with the local Böttcher map defined in a neighborhood of , we get a continuous potential map s.t. near and everywhere. Let be the critical potential. Then can be analytically continued throughout the postcritical region , and gives an analytic homeomorphism from to the open disk . If is also analytic in a parameter , then can be analytically continued throughout .

  • Böttcher map for the Multibrot set - Multibrot.lean: Let be the Multibrot set for the family , viewed as a subset of the Riemann sphere . Then is postcritical for each , so the diagonal of the Böttcher map is holomorphic throughout , and defines an analytic bijection from to the open unit disk .

  • Multibrot connectness - MultibrotConnected.lean, Mandelbrot.lean: Each Multibrot set and its complement are corrected, including the Mandelbrot set .

References

  1. Adrien Douady, John Hubbard (1984-5). Exploring the Mandelbrot set. The Orsay Notes
  2. John Milnor (1990), Dynamics in one complex variable
  3. Dierk Schleicher (1998), Rational parameter rays of the Mandelbrot set
  4. Paul Garrett (2005), Hartogs’ Theorem: separate analyticity implies joint
  5. Hartog's theorem
  6. Böttcher's theorem

Building

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

Optimization and debugging tricks

I'm going to keep a list here, since otherwise I will forget them.

-- Tracing options
set_option trace.aesop true in

-- Print compiler IR, such as to see how well inlining worked:
set_option trace.compiler.ir.result true in
def ...