Conjectures about the Mandelbrot and Multibrot sets

This file adds three conjectures about the Mandelbrot and Multibrot sets:

• the MLC conjecture, stating that these sets are locally connected
• the density of hyperbolicity conjecture, stating that parameters with attracting cycles are dense in the Mandelbrot and Multibrot sets
• the conjecture that the boundaries of these sets have zero area. The first two conjectures are related in that the former implies the latter.

References:

• Wikipedia
• arxiv/math/9902155
• mathoverflow/37229

def Mandelbrot.multibrotSet (n : ℕ) : Set ℂ

The Multibrot set of power n is the set of all parameters c : ℂ for which 0 does not escape to infinity under repeated application of z ↦ z ^ n + c.

Equations

• Mandelbrot.multibrotSet n = {c : ℂ | ¬Filter.Tendsto (fun (k : ℕ) => (fun (z : ℂ) => z ^ n + c)^[k] 0) Filter.atTop (Bornology.cobounded ℂ)}

@[reducible, inline]

abbrev Mandelbrot.mandelbrotSet : Set ℂ

The Mandelbrot set is the special case of the multibrot set for n = 2. In other words, it is the set of all parameters c : ℂ for which 0 does not escape to infinity under repeated application of z ↦ z ^ 2 + c.

Equations

• Mandelbrot.mandelbrotSet = Mandelbrot.multibrotSet 2

theorem Mandelbrot.multibrotSet_eq {n : ℕ} (hn : 2 ≤ n) : multibrotSet n = {c : ℂ | ∀ (k : ℕ), ‖(fun (z : ℂ) => z ^ n + c)^[k] 0‖ ≤ 2 ^ (↑n - 1)⁻¹}

The multibrotSet n is equivalently the set of all parameters c for which the orbit of 0 under z ↦ z ^ n + c does not leave the closed disk of radius 2 ^ (n - 1)⁻¹ around the origin.

theorem Mandelbrot.mandelbrotSet_eq : mandelbrotSet = {c : ℂ | ∀ (k : ℕ), ‖(fun (z : ℂ) => z ^ 2 + c)^[k] 0‖ ≤ 2}

The mandelbrot set is equivalently the set of all parameters c for which the orbit of 0 under z ↦ z ^ 2 + c does not leave the closed disk of radius two around the origin.

theorem Mandelbrot.MLC : LocallyConnectedSpace ↑mandelbrotSet

The MLC conjecture, stating that the mandelbrot set is locally connected.

theorem Mandelbrot.MLC_general_exponent (n : ℕ) : LocallyConnectedSpace ↑(multibrotSet n)

A stronger version of the MLC conjecture, stating that all multibrots are locally connected. Note that we don't need to require 2 ≤ n because the conjecture holds in the trivial cases n = 0 and n = 1 too.

def Mandelbrot.IsAttractingCycle (f : ℂ → ℂ) (n : ℕ) (z : ℂ) : Prop

We say that z : ℂ is part of an attracting cycle of period n of f : ℂ → ℂ if it is an n-periodic point (i.e. f^[n] z = z), f^[n] is differentiable at z and ‖deriv f^[n] z‖ is strictly less than one.

Equations

• Mandelbrot.IsAttractingCycle f n z = (Function.IsPeriodicPt f n z ∧ DifferentiableAt ℂ f^[n] z ∧ ‖deriv f^[n] z‖ < 1)

theorem Mandelbrot.isAttractingCycle_z_squared_minus_one : IsAttractingCycle (fun (z : ℂ) => z ^ 2 - 1) 2 0

For example, 0 is part of an attracting 2-cycle of z ↦ z ^ 2 - 1.

theorem Mandelbrot.not_isAttractingCycle_z_squared_minus_two : ¬IsAttractingCycle (fun (z : ℂ) => z ^ 2 - 2) 1 2

On the other hand, while 2 is part of a 1-cycle of z ↦ z ^ 2 - 2, that cycle is not attracting.

theorem Mandelbrot.no_attractingCycle_period_zero (f : ℂ → ℂ) (z : ℂ) : ¬IsAttractingCycle f 0 z

No function has an attracting cycle of period 0. This is important in that it means we don't need to require 0 < n in the conjectures below.

theorem Mandelbrot.density_of_hyperbolicity : mandelbrotSet ⊆ closure {c : ℂ | ∃ (n : ℕ) (z : ℂ), IsAttractingCycle (fun (z : ℂ) => z ^ 2 + c) n z}

The density of hyperbolicity conjecture, stating that the set of all parameters c for which fun z ↦ z ^ 2 + c has an attracting cycle is dense in the Mandelbrot set.

theorem Mandelbrot.density_of_hyperbolicity_general_exponent {n : ℕ} (hn : 2 ≤ n) : multibrotSet n ⊆ closure {c : ℂ | ∃ (n : ℕ) (z : ℂ), IsAttractingCycle (fun (z : ℂ) => z ^ n + c) n z}

The density of hyperbolicity conjecture for Multibrot sets, stating that the set of all parameters c for which fun z ↦ z ^ n + c has an attracting cycle is dense in multibrotSet n. Note that we need to require 2 ≤ n because the conjecture is trivially false for n = 1.

theorem Mandelbrot.multibrotSet_frontier_measurable {n : ℕ} : MeasurableSet (frontier (multibrotSet n))

The boundary of any Multibrot set is measurable because it is closed, so it makes sense to ask about its area.

theorem Mandelbrot.volume_frontier_mandelbrotSet_eq_zero : MeasureTheory.volume (frontier mandelbrotSet) = 0

The boundary of the Mandelbrot set is conjectured to have zero area.

theorem Mandelbrot.volume_frontier_multibrotSet_eq_zero {n : ℕ} : MeasureTheory.volume (frontier (multibrotSet n)) = 0

The boundary of any Multibrot set is conjectured to have zero area. Note that we don't need to exclude the trivial cases n = 0 and n = 1 because the conjecture holds for them.