The Mandelbrot lemniscate domains are connected
OpenMandelbrot.mandelbrot_lemniscate_isPreconnectedFor write and let
be the -th point of the critical orbit, a monic-up-to-scale polynomial in of degree for (with ). The -th Mandelbrot lemniscate domain is the filled sublevel set
The claim is that is connected for every .
These sets are the standard finite-time approximations of the Mandelbrot set: they decrease, , and by the radius- escape criterion their intersection is exactly . The first few are transparent: and is the closed disk of radius , while for the set is bounded by the lemniscate , a curve of degree .
Connectivity of a filled sublevel set of a complex polynomial is governed by the critical values of : the components of merge as grows past the moduli of the critical values, and the sublevel set is connected once dominates all of them. For the Mandelbrot polynomials the relevant fact is that every critical value of has modulus at most , so no splitting occurs at level . Equivalently, in the language of Douady and Hubbard, the Green's function of has no critical point in the region , which is the analytic heart of their proof that is connected.
Connectedness is stated in the preconnected form, which for these nonempty sets is equivalent to connectedness.
import Definitions.Def_mandelbrot_sets open Topology Set Function Filter Bornology Metric MeasureTheory
namespace Mandelbrot
/-- The `k`-th Mandelbrot lemniscate domain, the set of parameters whose critical orbit has
not yet left the closed disk of radius `2` at time `k`, is connected. -/
theorem mandelbrot_lemniscate_isPreconnected (k : ℕ) :
IsPreconnected {c : ℂ | ‖(fun z ↦ z ^ 2 + c)^[k] 0‖ ≤ 2} := by sorry
end Mandelbrot