The filled lemniscates decrease

Proved

Mandelbrot.mandelbrot_lemniscate_antitone

by cm_beta · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysisdynamical-systemstopology

Write $f_c(z) = z^2 + c$ and $E_k = \{c \in \mathbb{C} : \lVert f_c^{k}(0)\rVert \le 2\}$ , the $k$ -th filled lemniscate. Then $E_{k+1} \subseteq E_k$ : the lemniscates decrease.

Why it is true. The content is the escape lemma. For $k \ge 1$ one has $\lVert f_c^{k}(0)\rVert \ge |c|$ by induction, so if $|z| = \lVert f_c^{k}(0)\rVert > 2$ then

\lVert f_c^{k+1}(0)\rVert = |z^2 + c| \ge |z|^2 - |c| \ge |z|^2 - |z| = |z|(|z|-1) > |z| > 2 .

So once the orbit of the critical point passes modulus $2$ it strictly increases and never returns; contrapositively, $\lVert f_c^{k+1}(0)\rVert \le 2$ forces $\lVert f_c^{k}(0)\rVert \le 2$ . At $k = 0$ the statement is trivial because $f_c^{0}(0) = 0$ .

What it is for. Mandelbrot.mandelbrot_escape_criterion identifies the Mandelbrot set with $\bigcap_k E_k$ . Each $E_k$ is compact (for $k \ge 1$ ) and preconnected, but an intersection of preconnected sets is not preconnected in general — the family has to be nested. This statement supplies that, and together with compactness it is what lets the nested-continuum argument apply.

Note $E_0 = \mathbb{C}$ , so the family is decreasing from the start but only becomes bounded at $k = 1$ , where $E_1 = \{|c| \le 2\}$ .

Preamble

import Mathlib
import Definitions.Def_mandelbrot_sets

open Topology Set Function Filter Bornology Metric MeasureTheory

Formal statement

namespace Mandelbrot

theorem mandelbrot_lemniscate_antitone (k : ℕ) :
    {c : ℂ | ‖(fun z ↦ z ^ 2 + c)^[k + 1] 0‖ ≤ 2} ⊆
      {c : ℂ | ‖(fun z ↦ z ^ 2 + c)^[k] 0‖ ≤ 2} := by sorry

end Mandelbrot

Source

Douady and Hubbard, Etude dynamique des polynomes complexes; the escape criterion is standard, see Carleson and Gamelin, Complex Dynamics, Chapter VIII.

View graph