Escaping points, dense orbits, and Devaney chaos

The remaining dynamical consequences use covering, periodic points, and Baire category.

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.

Escaping points, transitivity, and dense orbits

The compact-covering theorem makes the remaining conclusions of Shen and Rempe-Gillen's Theorem 1.1 particularly short. Escaping is expressed directly by eventual escape from every Euclidean ball. Dense orbits are constructed by applying the Baire theorem to the sets of points whose orbit visits each member of a fixed countable basis of the plane.

def ExponentialJuliaSetMisiurewicz.EscapesToInfinity (z : ℂ) : Prop

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

Equations

• ExponentialJuliaSetMisiurewicz.EscapesToInfinity z = ∀ (R : ℝ), ∃ (N : ℕ), ∀ n ≥ N, R ≤ ‖ExponentialJuliaSetMisiurewicz.expIterate n z‖

def ExponentialJuliaSetMisiurewicz.escapingSetExp : Set ℂ

The escaping set of the complex exponential map.

Equations

• ExponentialJuliaSetMisiurewicz.escapingSetExp = {z : ℂ | ExponentialJuliaSetMisiurewicz.EscapesToInfinity z}

theorem ExponentialJuliaSetMisiurewicz.escapesToInfinity_of_im_eq_zero {z : ℂ} (hz : z.im = 0) : EscapesToInfinity z

Every real point escapes to infinity under iteration of the exponential map.

theorem ExponentialJuliaSetMisiurewicz.escapesToInfinity_of_eventually_onRealAxis {z : ℂ} {m : ℕ} (hm : OnRealAxis (expIterate m z)) : EscapesToInfinity z

Any point whose orbit reaches the real axis subsequently escapes to infinity.

theorem ExponentialJuliaSetMisiurewicz.dense_escapingSet_exp : Dense escapingSetExp

Theorem 4.1. The escaping set of the complex exponential map is dense in the plane.

theorem ExponentialJuliaSetMisiurewicz.topologically_transitive_exp : MulAction.IsTopologicallyTransitive (IterateMulAct Complex.exp) ℂ

Theorem 5.1. The complex exponential map is topologically transitive.

def ExponentialJuliaSetMisiurewicz.orbitVisitSet (U : Set ℂ) : Set ℂ

The set of starting points whose orbit visits a specified set.

Equations

• ExponentialJuliaSetMisiurewicz.orbitVisitSet U = ⋃ (n : ℕ), ExponentialJuliaSetMisiurewicz.expIterate n ⁻¹' U

theorem ExponentialJuliaSetMisiurewicz.isOpen_dense_orbitVisitSet {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) : IsOpen (orbitVisitSet U) ∧ Dense (orbitVisitSet U)

The orbit-visit set of a nonempty open set is itself open and dense.

def ExponentialJuliaSetMisiurewicz.denseOrbitSetExp : Set ℂ

The set of points whose forward orbit under the exponential is dense in the plane.

Equations

• ExponentialJuliaSetMisiurewicz.denseOrbitSetExp = {z : ℂ | Dense (MulAction.orbit (IterateMulAct Complex.exp) z)}

theorem ExponentialJuliaSetMisiurewicz.mem_denseOrbitSetExp_iff_visit_countableBasis {z : ℂ} : z ∈ denseOrbitSetExp ↔ z ∈ ⋂ (U : ↑(TopologicalSpace.countableBasis ℂ)), orbitVisitSet ↑U

Visiting every member of mathlib's countable basis is equivalent to having dense orbit.

theorem ExponentialJuliaSetMisiurewicz.dense_denseOrbitSet_exp : Dense denseOrbitSetExp

Corollary 5.6. Points with dense forward orbit are dense in the plane.

theorem ExponentialJuliaSetMisiurewicz.dense_denseOrbitSet_exp_diff_countable {C : Set ℂ} (hC : C.Countable) : Dense (denseOrbitSetExp \ C)

Removing a countable set still leaves a dense set of points with dense orbit.

theorem ExponentialJuliaSetMisiurewicz.not_countable_denseOrbitSet_exp : ¬denseOrbitSetExp.Countable

Corollary 5.6. The set of points with dense orbit is uncountable.

def ExponentialJuliaSetMisiurewicz.IsDevaneyChaotic (f : ℂ → ℂ) : Prop

Devaney chaos on the plane: continuity, dense periodic points, and transitivity.

Equations

• ExponentialJuliaSetMisiurewicz.IsDevaneyChaotic f = (Continuous f ∧ Dense (Function.periodicPts f) ∧ MulAction.IsTopologicallyTransitive (IterateMulAct f) ℂ)

theorem ExponentialJuliaSetMisiurewicz.devaney_chaotic_exp : IsDevaneyChaotic Complex.exp

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