Eventual compact covering and backward-orbit density

Section 5: real-axis expansion and two logarithms give eventual covering of compact sets.

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.

Section 5: eventual covering of compact sets

We use radius-eight disks instead of radius-2π disks to keep the estimates simple. Since Lemma 6 already supplies an orbit reaching the real axis in every open disk, we only need expansion along real orbits, rather than general escaping orbits.

theorem ExponentialJuliaSetMisiurewicz.exp_ball_real_expands {x : ℂ} (hx : x.im = 0) {r m : ℝ} (hr : 0 < r) (hr1 : r ≤ 1) (hm : 0 ≤ m) (hxm : m ≤ x.re) : Metric.ball (Complex.exp x) (r * m) ⊆ Complex.exp '' Metric.ball x r

A small disk centred on the real axis is expanded by a prescribed factor.

theorem ExponentialJuliaSetMisiurewicz.eventually_unit_ball_subset_iterate_real {x : ℂ} (hx : x.im = 0) (hx2 : 2 ≤ x.re) {r : ℝ} (hr : 0 < r) : ∃ (N : ℕ), ∀ n ≥ N, Metric.ball (expIterate n x) 1 ⊆ expIterate n '' Metric.ball x r

Iterated images of a disk on a sufficiently far right real orbit contain unit disks.

theorem ExponentialJuliaSetMisiurewicz.mem_exp_exp_ball_real {w : ℂ} (hw : w ≠ 0) {M x : ℝ} (hwM : |Real.log ‖w‖| ≤ M) (hx : M + 2 * Real.pi ≤ x) : w ∈ expIterate 2 '' Metric.ball (↑x) 8

Two exponentials of a radius-eight disk sufficiently far along the real axis cover any prescribed annulus. Integer translates of a logarithm supply the preimages.

theorem ExponentialJuliaSetMisiurewicz.compact_subset_exp_exp_ball_real {K : Set ℂ} (hK : IsCompact K) (hK0 : 0 ∉ K) : ∃ (ρ : ℝ), ∀ (x : ℝ), ρ ≤ x → K ⊆ expIterate 2 '' Metric.ball (↑x) 8

Compactness makes the preceding elementary covering estimate uniform.

theorem ExponentialJuliaSetMisiurewicz.eventually_covers_compact_of_real_ball {K : Set ℂ} (hK : IsCompact K) (hK0 : 0 ∉ K) {x : ℂ} (hx : x.im = 0) (hx2 : 2 ≤ x.re) {r : ℝ} (hr : 0 < r) : ∃ (N : ℕ), ∀ n ≥ N, K ⊆ expIterate n '' Metric.ball x r

Every sufficiently late image of a disk centred on a far right real point covers a given compact subset of the punctured plane.

theorem ExponentialJuliaSetMisiurewicz.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 (open sets spread everywhere). Every sufficiently late iterated image of a nonempty open set contains any given compact set omitting zero. Only real-axis Lemma 6 and the quantitative open-mapping Lemma 3 are needed.

theorem ExponentialJuliaSetMisiurewicz.eventually_covers_compact_ball {c : ℂ} {r : ℝ} (hr : 0 < r) {K : Set ℂ} (hK : IsCompact K) (hK0 : 0 ∉ K) : ∃ (N : ℕ), ∀ n ≥ N, K ⊆ expIterate n '' Metric.ball c r

The compact covering theorem specialised to an open ball of positive radius.

theorem ExponentialJuliaSetMisiurewicz.eventually_hits_nonzero {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) {w : ℂ} (hw : w ≠ 0) : ∃ (N : ℕ), ∀ n ≥ N, ∃ z ∈ U, expIterate n z = w

Every nonzero point belongs to every sufficiently late image of an open set.

theorem ExponentialJuliaSetMisiurewicz.exists_iterate_eq_nonzero {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) {w : ℂ} (hw : w ≠ 0) : ∃ (n : ℕ), 0 < n ∧ ∃ z ∈ U, expIterate n z = w

The point-hitting formulation, with an explicitly positive iterate.

theorem ExponentialJuliaSetMisiurewicz.lemma6_every_domain_eventually_meets_negative_real_axis {V : Set ℂ} (hVopen : IsOpen V) (_hVconn : IsConnected V) (hVne : V.Nonempty) : EventuallyMeetsNegativeRealAxis V

Lemma 6, negative-axis form. This now follows from the Section 5 theorem by taking the nonzero target to be -1. The connectedness hypothesis is retained for compatibility with the original statement.

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

The full iterated preimage of every nonzero point is dense in the plane.

theorem ExponentialJuliaSetMisiurewicz.dense_iterated_preimages_real_axis : Dense {z : ℂ | ∃ (n : ℕ), OnRealAxis (expIterate n z)}

The backward orbit of the real axis is dense.