1. FormalConjectures
  2. Wikipedia
  3. Mandelbrot
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

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:

open Topology Set Function Filter Bornology Metric MeasureTheorynamespace Mandelbrot

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.

def multibrotSet (n : ℕ) : Set ℂ := {c | ¬ Tendsto (fun k ↦ (fun z ↦ z ^ n + c)^[k] 0) atTop (cobounded ℂ)}

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.

abbrev mandelbrotSet := multibrotSet 2

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.

n:ℕhn:1 < nr:ℝ := 2 ^ (↑n - 1)⁻¹hr:0 < rhr':r ^ (n - 1) = 2hr'':r ^ n = 2 * rc:ℂh:∀ (k : ℕ), ‖(fun z ↦ z ^ n + c)^[k] 0‖ ≤ rh':∃ a, ∀ (b : ℕ), a ≤ b → b ∈ (fun k ↦ (fun z ↦ z ^ n + c)^[k] 0) ⁻¹' (closedBall 0 r)ᶜ⊢ False; n✝:ℕhn:1 < nr:ℝ := 2 ^ (↑n - 1)⁻¹hr:0 < rhr':r ^ (n - 1) = 2hr'':r ^ n = 2 * rc:ℂh:∀ (k : ℕ), ‖(fun z ↦ z ^ n + c)^[k] 0‖ ≤ rn:ℕh':∀ (b : ℕ), n ≤ b → b ∈ (fun k ↦ (fun z ↦ z ^ n✝ + c)^[k] 0) ⁻¹' (closedBall 0 r)ᶜ⊢ False exact not_lt_of_ge (h n) (n✝:ℕhn:1 < nr:ℝ := 2 ^ (↑n - 1)⁻¹hr:0 < rhr':r ^ (n - 1) = 2hr'':r ^ n = 2 * rc:ℂh:∀ (k : ℕ), ‖(fun z ↦ z ^ n + c)^[k] 0‖ ≤ rn:ℕh':∀ (b : ℕ), n ≤ b → b ∈ (fun k ↦ (fun z ↦ z ^ n✝ + c)^[k] 0) ⁻¹' (closedBall 0 r)ᶜ⊢ r < ‖(fun z ↦ z ^ n✝ + c)^[n] 0‖ All goals completed! 🐙)

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.

@[category API, AMS 37] theorem mandelbrotSet_eq : mandelbrotSet = {c | ∀ k, ‖(fun z ↦ z ^ 2 + c)^[k] 0‖ ≤ 2} := ⊢ mandelbrotSet = {c | ∀ (k : ℕ), ‖(fun z ↦ z ^ 2 + c)^[k] 0‖ ≤ 2} simpa [show (2 - 1 : ℝ) = 1 ⊢ mandelbrotSet = {c | ∀ (k : ℕ), ‖(fun z ↦ z ^ 2 + c)^[k] 0‖ ≤ 2} All goals completed! 🐙] using multibrotSet_eq le_rfl

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

@[category research open, AMS 37] theorem MLC : LocallyConnectedSpace mandelbrotSet := ⊢ LocallyConnectedSpace ↑mandelbrotSet All goals completed! 🐙

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.

@[category research open, AMS 37] theorem MLC_general_exponent (n : ℕ) : LocallyConnectedSpace (multibrotSet n) := n:ℕ⊢ LocallyConnectedSpace ↑(multibrotSet n) All goals completed! 🐙

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, ‖deriv f^[n] z‖ is strictly less than one, and n > 0.

def IsAttractingCycle (f : ℂ → ℂ) (n : ℕ) (z : ℂ) : Prop := (0 < n) ∧ f.IsPeriodicPt n z ∧ DifferentiableAt ℂ f^[n] z ∧ ‖deriv f^[n] z‖ < 1

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

@[category test, AMS 37] theorem isAttractingCycle_z_squared_minus_one : IsAttractingCycle (fun z ↦ z ^ 2 - 1) 2 0 := ⟨⊢ 0 < 2 All goals completed! 🐙, ⊢ IsPeriodicPt (fun z ↦ z ^ 2 - 1) 2 0 All goals completed! 🐙, ⊢ DifferentiableAt ℂ (fun z ↦ z ^ 2 - 1)^[2] 0 All goals completed! 🐙, ⊢ ‖deriv (fun z ↦ z ^ 2 - 1)^[2] 0‖ < 1 All goals completed! 🐙⟩

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

@[category test, AMS 37] theorem not_isAttractingCycle_z_squared_minus_two : ¬ IsAttractingCycle (fun z ↦ z ^ 2 - 2) 1 2 := ⊢ ¬IsAttractingCycle (fun z ↦ z ^ 2 - 2) 1 2 All goals completed! 🐙

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.

@[category test, AMS 37] theorem no_attractingCycle_period_zero (f : ℂ → ℂ) (z : ℂ) : ¬ IsAttractingCycle f 0 z := f:ℂ → ℂz:ℂ⊢ ¬IsAttractingCycle f 0 z All goals completed! 🐙

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.

@[category research open, AMS 37] theorem density_of_hyperbolicity : mandelbrotSet ⊆ closure {c | ∃ m z, IsAttractingCycle (fun z ↦ z ^ 2 + c) m z} := ⊢ mandelbrotSet ⊆ closure {c | ∃ m z, IsAttractingCycle (fun z ↦ z ^ 2 + c) m z} All goals completed! 🐙

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.

@[category research open, AMS 37] theorem density_of_hyperbolicity_general_exponent {n : ℕ} (hn : 2 ≤ n) : multibrotSet n ⊆ closure {c | ∃ m z, IsAttractingCycle (fun z ↦ z ^ n + c) m z} := n:ℕhn:2 ≤ n⊢ multibrotSet n ⊆ closure {c | ∃ m z, IsAttractingCycle (fun z ↦ z ^ n + c) m z} All goals completed! 🐙

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

@[category test, AMS 37] theorem multibrotSet_frontier_measurable {n : ℕ} : MeasurableSet (frontier (multibrotSet n)) := isClosed_frontier.measurableSet

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

@[category research open, AMS 37] theorem volume_frontier_mandelbrotSet_eq_zero : volume (frontier mandelbrotSet) = 0 := ⊢ volume (frontier mandelbrotSet) = 0 All goals completed! 🐙

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.

@[category research open, AMS 37] theorem volume_frontier_multibrotSet_eq_zero {n : ℕ} : volume (frontier (multibrotSet n)) = 0 := n:ℕ⊢ volume (frontier (multibrotSet n)) = 0 All goals completed! 🐙end Mandelbrot