Normal sequences and the Julia set

Normality is defined for sequences of maps from a topological space to a uniform space. Every subsequence must have a further subsequence that converges locally uniformly on the specified domain, using Mathlib's TendstoLocallyUniformly directly. Neither holomorphy nor any special value at infinity is built into this general definition.

For the exponential, the codomain is the Riemann sphere and the domain remains the complex plane. Classical complex analysis describes which locally uniform spherical limits of holomorphic or meromorphic functions can occur. That characterization is unnecessary here: LeanPool.ExpChaotic.Spherical directly rules out every possible sphere-valued limit.

Part of Lasse Rempe's formalisation of Shen and Rempe-Gillen's exponential-map paper, with generative AI assistance including Copilot, Claude, and particularly ChatGPT. The initial proof architecture uses John Harrison's HOL Light formalisation. See LeanPool.ExpChaotic for attribution and the upstream source.

def ExponentialJuliaSetMisiurewicz.IsNormalSequenceOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] (F : ℕ → α → β) (U : Set α) : Prop

A sequence of maps is normal on U if each subsequence has a further subsequence converging locally uniformly on the subtype U to some function U → β.

This definition makes sense for any topological domain and uniform codomain. It does not require U to be open; openness is imposed when defining a local Fatou set.

Equations

• One or more equations did not get rendered due to their size.

def ExponentialJuliaSetMisiurewicz.fatouSet (f : ℂ → ℂ) : Set ℂ

The Fatou set consists of points having an open neighbourhood on which the sphere-valued iterates form a normal sequence. The map f itself is defined only on ℂ.

Equations

• ExponentialJuliaSetMisiurewicz.fatouSet f = {z : ℂ | ∃ (U : Set ℂ), IsOpen U ∧ z ∈ U ∧ ExponentialJuliaSetMisiurewicz.IsNormalSequenceOn (fun (n : ℕ) (z : ℂ) => ↑(f^[n] z)) U}

def ExponentialJuliaSetMisiurewicz.juliaSet (f : ℂ → ℂ) : Set ℂ

The Julia set, defined as the complement of the Fatou set.

Equations

• ExponentialJuliaSetMisiurewicz.juliaSet f = (ExponentialJuliaSetMisiurewicz.fatouSet f)ᶜ

Restriction

theorem ExponentialJuliaSetMisiurewicz.IsNormalSequenceOn.mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] {F : ℕ → α → β} {U V : Set α} (h : IsNormalSequenceOn F U) (hVU : V ⊆ U) : IsNormalSequenceOn F V

Normality is inherited by subsets. A limit on U restricts along the continuous inclusion V → U.

theorem ExponentialJuliaSetMisiurewicz.mem_fatouSet_iff_exists_ball {f : ℂ → ℂ} {z : ℂ} : z ∈ fatouSet f ↔ ∃ (r : ℝ), 0 < r ∧ IsNormalSequenceOn (fun (n : ℕ) (w : ℂ) => ↑(f^[n] w)) (Metric.ball z r)

The local Fatou-set definition can be tested on open disks.

Non-normality and Misiurewicz's theorem

theorem ExponentialJuliaSetMisiurewicz.not_isNormalSequenceOn_sphericalExpIterate {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) : ¬IsNormalSequenceOn sphericalExpIterate U

The sphere-valued exponential iterates are not normal on a nonempty open set.

theorem ExponentialJuliaSetMisiurewicz.misiurewicz_fatouSet_exp : fatouSet exponentialMap = ∅

Misiurewicz's theorem in Fatou-set form: the sphere-valued iterates are normal on no neighbourhood.

theorem ExponentialJuliaSetMisiurewicz.misiurewicz_juliaSet_exp : juliaSet exponentialMap = Set.univ

Misiurewicz's theorem: the Julia set of the complex exponential is the plane.