Exponential iterates and differentiation

Basic notation and differentiation of iterates. Normality is defined in LeanPool.ExpChaotic.Normality using Mathlib's locally uniform convergence.

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.

@[reducible, inline]

noncomputable abbrev ExponentialJuliaSetMisiurewicz.exponentialMap : ℂ → ℂ

The complex exponential map.

Equations

• ExponentialJuliaSetMisiurewicz.exponentialMap = Complex.exp

@[reducible, inline]

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

The n-th iterate of the complex exponential map.

Equations

• ExponentialJuliaSetMisiurewicz.expIterate n = ExponentialJuliaSetMisiurewicz.exponentialMap^[n]

@[simp]

theorem ExponentialJuliaSetMisiurewicz.expIterate_zero (z : ℂ) : expIterate 0 z = z

The zeroth iterate is the identity map.

@[simp]

theorem ExponentialJuliaSetMisiurewicz.expIterate_succ (n : ℕ) (z : ℂ) : expIterate (n + 1) z = Complex.exp (expIterate n z)

Apply one more exponential after the n-th iterate.

def ExponentialJuliaSetMisiurewicz.centralStrip : Set ℂ

The closed horizontal strip used in Misiurewicz's proof.

Equations

• ExponentialJuliaSetMisiurewicz.centralStrip = {z : ℂ | |z.im| ≤ Real.pi / 3}

def ExponentialJuliaSetMisiurewicz.rightHalfPlane : Set ℂ

The right half-plane used in Misiurewicz's proof.

Equations

• ExponentialJuliaSetMisiurewicz.rightHalfPlane = {z : ℂ | 4 < z.re}

def ExponentialJuliaSetMisiurewicz.wideStrip : Set ℂ

The wider closed strip occurring in Lemma 5.

Equations

• ExponentialJuliaSetMisiurewicz.wideStrip = {z : ℂ | |z.im| ≤ 2 * Real.pi}

def ExponentialJuliaSetMisiurewicz.OnRealAxis (z : ℂ) : Prop

A complex number lies on the embedded real axis.

Equations

• ExponentialJuliaSetMisiurewicz.OnRealAxis z = (z.im = 0)

def ExponentialJuliaSetMisiurewicz.EventuallyMeetsRealAxis (V : Set ℂ) : Prop

Some forward image of V meets the real axis.

Equations

• ExponentialJuliaSetMisiurewicz.EventuallyMeetsRealAxis V = ∃ (n : ℕ), ∃ z ∈ V, ExponentialJuliaSetMisiurewicz.OnRealAxis (ExponentialJuliaSetMisiurewicz.expIterate n z)

Basic analytic infrastructure corresponding to the HOL preliminaries

theorem ExponentialJuliaSetMisiurewicz.hasDerivAt_exp_comp {f : ℂ → ℂ} {f' z : ℂ} (hf : HasDerivAt f f' z) : HasDerivAt (Complex.exp ∘ f) (f' * Complex.exp (f z)) z

Chain rule for the exponential, corresponding to HAS_COMPLEX_DERIVATIVE_CEXP_COMPOSE in HOL Light.

theorem ExponentialJuliaSetMisiurewicz.differentiableAt_exp_comp {f : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℂ f z) : DifferentiableAt ℂ (fun (w : ℂ) => Complex.exp (f w)) z

Composition with the exponential preserves complex differentiability at a point.

theorem ExponentialJuliaSetMisiurewicz.hasDerivAt_exp_comp' {f : ℂ → ℂ} {f' z : ℂ} (hf : HasDerivAt f f' z) : HasDerivAt (Complex.exp ∘ f) (Complex.exp (f z) * f') z

The exponential chain rule with the outer derivative written first.

theorem ExponentialJuliaSetMisiurewicz.differentiable_expIterate (n : ℕ) : Differentiable ℂ (expIterate n)

Every iterate of the exponential is complex differentiable.

theorem ExponentialJuliaSetMisiurewicz.continuous_expIterate (n : ℕ) : Continuous (expIterate n)

Every iterate of the exponential is continuous.

theorem ExponentialJuliaSetMisiurewicz.differentiableOn_expIterate (n : ℕ) (s : Set ℂ) : DifferentiableOn ℂ (expIterate n) s

Every iterate of the exponential is complex differentiable on every set.