Tricorn
DefinitionThe antiholomorphic quadratic map#✓fully proved
For \(c \in \mathbb{C}\), the map \(T_c : \mathbb{C} \to \mathbb{C}\) is \(T_c(z) = \bar z^2 + c\), where \(\bar z\) is the complex conjugate of \(z\).
def Tantibar (c : ℂ) (z : ℂ) : ℂ := (starRingEnd ℂ z) ^ 2 + cUsed by 1
DefinitionThe Mandelbar set (tricorn)#✓fully proved
The Mandelbar set is the set of \(c \in \mathbb{C}\) for which the orbit of \(0\) under the map \(T_c(z) = \bar z^2 + c\) is bounded: there is a real number \(M\) with \(|T_c^n(0)| \le M\) for all \(n \ge 0\), where \(T_c^n\) is the \(n\)-th iterate of \(T_c\) and \(T_c^0\) is the identity.
This set is the connectedness locus of the family \(z \mapsto \bar z^2 + c\).
def Mandelbar : Set ℂ :=
{ c : ℂ | ∃ M : ℝ, ∀ n : ℕ, ‖(Tantibar c)^[n] 0‖ ≤ M }def Tantibar (c : ℂ) (z : ℂ) : ℂ := (starRingEnd ℂ z) ^ 2 + cWantedExt/Analysis/MandelbarWanted.lean:64
Uses 1 · Used by 1
TheoremThe Mandelbar set is not path-connected#●ready to prove
The Mandelbar set (tricorn), the set of \(c \in \mathbb{C}\) for which the orbit of \(0\) under \(z \mapsto \bar z^2 + c\) is bounded, is not path-connected.
This is the degree-2 case of the Hubbard–Schleicher theorem that multicorns are not path-connected.
public theorem_wanted mandelbar_not_path_connected : ¬ IsPathConnected Mandelbardef Mandelbar : Set ℂ :=
{ c : ℂ | ∃ M : ℝ, ∀ n : ℕ, ‖(Tantibar c)^[n] 0‖ ≤ M }WantedExt/Analysis/MandelbarWanted.lean:67
Sources
- John H. Hubbard and Dierk Schleicher, Multicorns are not Path Connected, arXiv:1209.1753 (2012); published in Frontiers in Complex Dynamics (Princeton University Press, 2014), pp. 73-102. Listed as §62 (additional statement 2) in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem
mandelbar_not_path_connectedof the lean-eval benchmark.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.