Mandelbrot set

DefinitionThe quadratic family#✓fully proved

For \(c \in \mathbb{C}\), \(T_c \colon \mathbb{C} \to \mathbb{C}\) is the map \(T_c(z) = z^2 + c\).

def Tc (c : ℂ) (z : ℂ) : ℂ := z ^ 2 + c

Used by 1

Used byThe Mandelbrot set

DefinitionThe Mandelbrot set#✓fully proved

The Mandelbrot set is the set of all \(c \in \mathbb{C}\) for which the orbit of \(0\) under \(T_c(z) = z^2 + c\) is bounded: there is a real number \(M\) with \(|T_c^n(0)| \le M\) for every \(n \in \mathbb{N}\), where \(T_c^n\) is the \(n\)-th iterate of \(T_c\) and \(T_c^0\) is the identity.

def Mandelbrot : Set ℂ :=
  { c : ℂ | ∃ M : ℝ, ∀ n : ℕ, ‖(Tc c)^[n] 0‖ ≤ M }

Uses 1 · Used by 1

Statement usesThe quadratic family

Used byThe Mandelbrot set is connected (Douady–Hubbard)

TheoremThe Mandelbrot set is connected (Douady–Hubbard)#●ready to prove

The Mandelbrot set, the set of all \(c \in \mathbb{C}\) for which the sequence \((T_c^n(0))_{n \ge 0}\) of iterates of \(0\) under \(T_c(z) = z^2 + c\) is bounded, is a nonempty connected subset of \(\mathbb{C}\).

public theorem_wanted mandelbrot_connected : IsConnected Mandelbrot

Sources

• 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). Problem mandelbrot_connected of the lean-eval benchmark.

Uses 1

Statement usesThe Mandelbrot set

DefinitionQuadratic family#✓fully proved

For each complex number \(c\), the map \(T_c : \mathbb{C} \to \mathbb{C}\) is given by \(T_c(z) = z^2 + c\).

def Tc (c : ℂ) (z : ℂ) : ℂ :=
  z ^ 2 + c

Used by 1

Used byMandelbrot set

DefinitionMandelbrot set#✓fully proved

The Mandelbrot set is the set \(M\) of complex numbers \(c\) for which the orbit of \(0\) under the quadratic map \(T_c(z) = z^2 + c\) is bounded: there is a real number \(R\) with \(|T_c^n(0)| \le R\) for every \(n \in \mathbb{N}\), where \(T_c^n\) is the \(n\)-th iterate of \(T_c\) and \(T_c^0\) is the identity.

def Mandelbrot : Set ℂ :=
  { c : ℂ | ∃ R : ℝ, ∀ n : ℕ, ‖(Tc c)^[n] 0‖ ≤ R }

Uses 1 · Used by 1

Statement usesQuadratic family

Used byHausdorff dimension of the Mandelbrot boundary (Shishikura)

TheoremHausdorff dimension of the Mandelbrot boundary (Shishikura)#●ready to prove

The boundary of the Mandelbrot set \(M \subseteq \mathbb{C}\) has Hausdorff dimension \(2\).

public theorem_wanted mandelbrot_boundary_dimh :
    dimH (frontier Mandelbrot) = 2

Sources

• M. Shishikura, The Hausdorff dimension of the boundary of the Mandelbrot set and Julia sets, Ann. of Math. 147 (1998). Listed as §260 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Knill, §260. Problem mandelbrot_boundary_dimh of the lean-eval benchmark.

Uses 1

Statement usesMandelbrot set

4 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.