Public results: the exponential map is chaotic

This module retains the upstream public interface while importing the complete proof development.

The goal is a formalisation of the main results in the paper "The Exponential Map is Chaotic: An Invitation to Transcendental Dynamics" by Zhaiming Shen and Lasse Rempe-Gillen.

The formalisation was carried out with the help of Generative AI, including Microsoft 365 Copilot, Claude and particularly ChatGPT.

The proofs use the paper and, for the initial proof architecture underlying density of the escaping set, John Harrison's HOL Light formalisation of Misiurewicz's original proof. See LeanPool.ExpChaotic for attribution and the upstream source.

@[reducible, inline]

noncomputable abbrev ExpChaotic.expIterate (n : ℕ) : ℂ → ℂ

The n-th iterate of the complex exponential map.

Equations

• ExpChaotic.expIterate n = ExponentialJuliaSetMisiurewicz.expIterate n

@[reducible, inline]

abbrev ExpChaotic.EscapesToInfinity (z : ℂ) : Prop

A point escapes if its orbit eventually leaves every centred Euclidean ball.

Equations

• ExpChaotic.EscapesToInfinity z = ExponentialJuliaSetMisiurewicz.EscapesToInfinity z

@[reducible, inline]

abbrev ExpChaotic.escapingSet : Set ℂ

The escaping set of the complex exponential map.

Equations

• ExpChaotic.escapingSet = ExponentialJuliaSetMisiurewicz.escapingSetExp

@[reducible, inline]

abbrev ExpChaotic.denseOrbitSet : Set ℂ

The set of points with dense forward orbit.

Equations

• ExpChaotic.denseOrbitSet = ExponentialJuliaSetMisiurewicz.denseOrbitSetExp

def ExpChaotic.repellingPeriodicSet : Set ℂ

The repelling periodic points of the complex exponential map.

Equations

• ExpChaotic.repellingPeriodicSet = {p : ℂ | ∃ (n : ℕ), 0 < n ∧ Function.IsPeriodicPt Complex.exp n p ∧ 1 < ‖deriv (ExpChaotic.expIterate n) p‖}

@[reducible, inline]

abbrev ExpChaotic.RiemannSphere : Type

The Riemann sphere as the one-point compactification of the complex plane.

Equations

• ExpChaotic.RiemannSphere = ExponentialJuliaSetMisiurewicz.RiemannSphere

@[reducible, inline]

noncomputable abbrev ExpChaotic.riemannSphereUniformSpace : UniformSpace RiemannSphere

Compatibility name for the implementation's canonical uniform structure. The implementation supplies the single registered instance.

Equations

• ExpChaotic.riemannSphereUniformSpace = ExponentialJuliaSetMisiurewicz.riemannSphereUniformSpace

@[reducible, inline]

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

A sequence of maps is normal on U if every subsequence has a further subsequence converging locally uniformly on U to some function from U to the uniform codomain.

Equations

• ExpChaotic.IsNormalSequenceOn F U = ExponentialJuliaSetMisiurewicz.IsNormalSequenceOn F U

@[reducible, inline]

abbrev ExpChaotic.fatouSet (f : ℂ → ℂ) : Set ℂ

The Fatou set defined by local normality of the sphere-valued iterates.

Equations

• ExpChaotic.fatouSet f = ExponentialJuliaSetMisiurewicz.fatouSet f

@[reducible, inline]

abbrev ExpChaotic.juliaSet (f : ℂ → ℂ) : Set ℂ

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

Equations

• ExpChaotic.juliaSet f = ExponentialJuliaSetMisiurewicz.juliaSet f

@[reducible, inline]

abbrev ExpChaotic.IsDevaneyChaotic (f : ℂ → ℂ) : Prop

Continuity, dense periodic points, and Mathlib's topological transitivity for the monoid action generated by iteration.

Equations

• ExpChaotic.IsDevaneyChaotic f = ExponentialJuliaSetMisiurewicz.IsDevaneyChaotic f

@[reducible, inline]

noncomputable abbrev ExpChaotic.sphericalExpIterate (n : ℕ) (z : ℂ) : RiemannSphere

The plane-valued exponential iterates, included into the Riemann sphere.

Equations

• ExpChaotic.sphericalExpIterate n z = ExponentialJuliaSetMisiurewicz.sphericalExpIterate n z

theorem ExpChaotic.eventually_covers_compact {U K : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) (hK : IsCompact K) (hK0 : 0 ∉ K) : ∃ (N : ℕ), ∀ n ≥ N, K ⊆ expIterate n '' U

Corollary 5.5. Given a prescribed compact set K that omits zero, every sufficiently high iterate of a nonempty open set covers K.

theorem ExpChaotic.dense_iteratedPreimages_nonzero {w : ℂ} (hw : w ≠ 0) : Dense {z : ℂ | ∃ (n : ℕ), expIterate n z = w}

The full iterated preimage of every nonzero point is dense.

theorem ExpChaotic.dense_iteratedPreimages_realAxis : Dense {z : ℂ | ∃ (n : ℕ), (expIterate n z).im = 0}

The full iterated preimage of the real axis is dense.

theorem ExpChaotic.dense_escapingSet : Dense escapingSet

Theorem 1.1, part 1., and Theorem 4.1: Escaping points are dense.

theorem ExpChaotic.dense_denseOrbitSet : Dense denseOrbitSet

Theorem 1.1, part 2.: Points with dense forward orbit are dense.

theorem ExpChaotic.not_countable_denseOrbitSet : ¬denseOrbitSet.Countable

Corollary 5.6. There are uncountably many points with dense forward orbit.

theorem ExpChaotic.dense_repellingPeriodicSet : Dense repellingPeriodicSet

Theorem 1.1, part 3., and Theorem 6.1: (Repelling) periodic points are dense.

theorem ExpChaotic.topologically_transitive : MulAction.IsTopologicallyTransitive (IterateMulAct Complex.exp) ℂ

Theorem 5.1. The action generated by iterating the exponential map is topologically transitive.

theorem ExpChaotic.devaney_chaotic : IsDevaneyChaotic Complex.exp

Theorem 1.2. The exponential map is chaotic in Devaney's sense.

theorem ExpChaotic.not_equicontinuousAt_sphericalExpIterate (z : ℂ) : ¬EquicontinuousAt sphericalExpIterate z

Corollary 4.4 (reformulated): The sphere-valued iterates are not equicontinuous at any point of the plane.

theorem ExpChaotic.infinitely_often_hits_negative_realAxis {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) : {n : ℕ | ∃ z ∈ U, (expIterate n z).im = 0 ∧ (expIterate n z).re < 0}.Infinite

Theorem 4.3: infinitely many iterated images of a nonempty open set meet the negative real axis. Strict negativity strengthens the nonpositive-axis statement in the paper.

theorem ExpChaotic.spherical_sensitive_dependence_paper {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) {R δ : ℝ} (hR : 0 < R) (hδ : 0 < δ) : ∃ (N : ℕ), ∀ n ≥ N, ∃ z ∈ U, ∃ w ∈ U, ‖expIterate n z‖ ≤ R ∧ δ ≤ ‖expIterate n z - expIterate n w‖

Corollary 4.4, in the precise form of Definition 2.3. The arbitrary positive constants give Exercise 8.7 as well; the conclusion even holds at every sufficiently late time.

theorem ExpChaotic.expansion_along_escaping_orbits {z : ℂ} (hz : EscapesToInfinity z) : Filter.Tendsto (fun (n : ℕ) => (expIterate n z).re) Filter.atTop Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => ‖deriv (expIterate n) z‖) Filter.atTop Filter.atTop

Observation 5.2: along any escaping orbit, the real parts and the norms of the derivatives of the iterates both tend to positive infinity.

theorem ExpChaotic.not_tendstoLocallyUniformly_sphericalExpIterate {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) {φ : ℕ → ℕ} (hφ : StrictMono φ) (g : ↑U → RiemannSphere) : ¬TendstoLocallyUniformly (fun (n : ℕ) (z : ↑U) => sphericalExpIterate (φ n) ↑z) g Filter.atTop

No increasing subsequence of the iterates has a locally uniform spherical limit on a nonempty open set. The arbitrary sphere-valued limit is defined only on that set.

theorem ExpChaotic.juliaSet_exp : juliaSet Complex.exp = Set.univ

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

theorem ExpChaotic.not_tendstoLocallyUniformlyOn_sphericalExpIterate {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) {φ : ℕ → ℕ} (hφ : StrictMono φ) (g : ℂ → RiemannSphere) : ¬TendstoLocallyUniformlyOn (fun (n : ℕ) => sphericalExpIterate (φ n)) g Filter.atTop U

No strictly increasing subsequence of the iterates has a locally uniform spherical limit on a nonempty open set. The limit is allowed to be any sphere-valued function. This directly rules out normality in the sphere-valued formulation, using Mathlib's TendstoLocallyUniformlyOn. All iterates have domain ℂ.