Mandelbrot set is connected (Douady–Hubbard)

mandelbrot_connected

Submitter: Kim Morrison.

Notes: The Mandelbrot set for the quadratic family T_c(z) = z² + c is the parameter set for which the critical orbit of 0 is bounded. This problem states Douady–Hubbard's connectedness theorem. §62 of Knill's 'Some Fundamental Theorems in Mathematics'.

Source: A. Douady and J. H. Hubbard, *Étude dynamique des polynômes complexes I, II*, Publ. Math. Orsay 84-02, 85-04. Listed as §62 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Use the Douady–Hubbard uniformisation: the Böttcher coordinate at infinity gives a conformal isomorphism from ℂ \ M to the exterior of the closed unit disk. Equivalently, after adjoining ∞, the complement of M in the Riemann sphere is simply connected, hence M is connected.

theorem declaration uses `sorry`mandelbrot_connected : IsConnected LeanEval.ComplexAnalysis.MandelbrotProblem.Mandelbrot := by⊢ IsConnected Mandelbrot
  sorryAll goals completed! 🐙

Solved by

Not yet solved.