Further statements from the paper

Theorem 4.3 and Corollary 4.4 follow from eventual covering of two prescribed nonzero targets. Observation 5.2 follows from the exponential norm identity and the chain rule. The sensitivity theorem uses the paper's Definition 2.3, with arbitrary positive constants as in Exercise 8.7, and even holds at every sufficiently late time.

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.

theorem ExponentialJuliaSetMisiurewicz.eventually_hits_negative_realAxis {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) : ∃ (N : ℕ), ∀ n ≥ N, ∃ z ∈ U, (expIterate n z).im = 0 ∧ (expIterate n z).re < 0

Every sufficiently late image of a nonempty open set meets the negative real axis.

theorem ExponentialJuliaSetMisiurewicz.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 meet the negative real axis.

theorem ExponentialJuliaSetMisiurewicz.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 and Exercise 8.7. The paper's spherical sensitivity condition holds for every pair of positive constants, at every sufficiently late time.

theorem ExponentialJuliaSetMisiurewicz.EscapesToInfinity.tendsto_re {z : ℂ} (hz : EscapesToInfinity z) : Filter.Tendsto (fun (n : ℕ) => (expIterate n z).re) Filter.atTop Filter.atTop

Observation 5.2, first clause. Real parts tend to positive infinity along escaping orbits.

theorem ExponentialJuliaSetMisiurewicz.EscapesToInfinity.tendsto_norm_deriv {z : ℂ} (hz : EscapesToInfinity z) : Filter.Tendsto (fun (n : ℕ) => ‖deriv (expIterate n) z‖) Filter.atTop Filter.atTop

Observation 5.2, second clause. Derivative norms tend to infinity along escaping orbits. After finitely many factors, every factor in the chain rule has norm at least two.