Derivative growth and quantitative open mapping

Lemmas 1–3 in the proof architecture adapted from John Harrison's HOL Light formalization.

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.

The six lemmas in the HOL Light proof

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

Derivative recursion for the iterates of the exponential.

theorem ExponentialJuliaSetMisiurewicz.abs_im_exp_le (w : ℂ) : |(Complex.exp w).im| ≤ |w.im| * ‖Complex.exp w‖

The imaginary part of an exponential is controlled by the imaginary part of its argument and the norm of the exponential.

theorem ExponentialJuliaSetMisiurewicz.abs_im_le_norm_aux (w : ℂ) : |w.im| ≤ ‖w‖

The absolute value of the imaginary part is at most the complex norm.

theorem ExponentialJuliaSetMisiurewicz.lemma1_im_le_norm_deriv {n : ℕ} (hn : 1 ≤ n) (z : ℂ) : |(expIterate n z).im| ≤ ‖deriv (expIterate n) z‖

Lemma 1. The imaginary part of an exponential iterate is bounded by the norm of its derivative. HOL Light: LEMMA_1.

theorem ExponentialJuliaSetMisiurewicz.lemma2a_real_growth {z : ℂ} (hz : z ∈ centralStrip) : z.re + (1 - Real.log 2) ≤ (Complex.exp z).re

Lemma 2(a). In the central strip, the real part increases by at least 1 - log 2. HOL Light: LEMMA_2a.

theorem ExponentialJuliaSetMisiurewicz.lemma2b_eventually_leaves_strip {z : ℂ} (hz : ¬OnRealAxis z) : ∃ (n : ℕ), expIterate n z ∉ centralStrip

Lemma 2(b). Every non-real orbit eventually leaves the central strip. HOL Light: LEMMA_2b.

theorem ExponentialJuliaSetMisiurewicz.isOpen_image_of_injOn {g : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U) (hg : DifferentiableOn ℂ g U) (hinj : Set.InjOn g U) : IsOpen (g '' U)

The image of an open set under an injective holomorphic map is open.

theorem ExponentialJuliaSetMisiurewicz.lemma3_isOpen_image {g : ℂ → ℂ} {b : ℂ} {r : ℝ} (hg : DifferentiableOn ℂ g (Metric.ball b r)) (hinj : Set.InjOn g (Metric.ball b r)) : IsOpen (g '' Metric.ball b r)

The image of the ball under an injective holomorphic map is open.

theorem ExponentialJuliaSetMisiurewicz.lemma3_hasDerivAt_invFunOn {g : ℂ → ℂ} {b : ℂ} {r : ℝ} (hg : DifferentiableOn ℂ g (Metric.ball b r)) (hinj : Set.InjOn g (Metric.ball b r)) (hne : ∀ z ∈ Metric.ball b r, deriv g z ≠ 0) {w : ℂ} (hw : w ∈ g '' Metric.ball b r) : HasDerivAt (Function.invFunOn g (Metric.ball b r)) (deriv g (Function.invFunOn g (Metric.ball b r) w))⁻¹ w

The inverse of an injective holomorphic map with non-vanishing derivative is itself complex differentiable, with the reciprocal derivative. This is the Lean analogue of HOL Light's HOLOMORPHIC_ON_INVERSE, which Mathlib does not currently provide. Continuity of the inverse comes from the open mapping property, after which HasDerivAt.of_local_left_inverse supplies the derivative.

theorem ExponentialJuliaSetMisiurewicz.lemma3_ball_image_of_deriv_lower_bound {g : ℂ → ℂ} {b : ℂ} {r m : ℝ} (hr : 0 < r) (hm : 0 ≤ m) (hgc : ContinuousOn g (Metric.closedBall b r)) (hg : DifferentiableOn ℂ g (Metric.ball b r)) (hinj : Set.InjOn g (Metric.ball b r)) (hderiv : ∀ z ∈ Metric.ball b r, m ≤ ‖deriv g z‖) : Metric.ball (g b) (r * m) ⊆ g '' Metric.ball b r

Lemma 3. Quantitative open mapping estimate, following Harrison's LEMMA_3. The proof uses his closest-point device: t is the distance from g b to the complement of the image, so ball (g b) t lies in the image and is convex, which is exactly what the mean value inequality needs.