Density of repelling periodic points

Section 6: contracting inverse branches and the fixed-point theorem give repelling points.

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 6: repelling periodic points and the density benchmarks

The full backward orbit means the union over all iterates. A single one-step preimage of a point is not asserted to be dense. Repelling means that there is a positive period for which the derivative of the return iterate has norm greater than one.

The proof uses real orbit centres equal to expIterate n 10. The first inverse branch returns to the original open set; iterated logarithms contract along the real orbit; two final logarithms close the return. Lipschitz constants suffice for construction, and differentiability of the inverse at its fixed point then gives the strict multiplier bound.

theorem ExponentialJuliaSetMisiurewicz.exists_lipschitz_local_inverse {f : ℂ → ℂ} {a : ℂ} (hf : HasStrictDerivAt f (deriv f a) a) (hne : deriv f a ≠ 0) : ∃ (g : ℂ → ℂ) (C : NNReal) (s : ℝ), 0 < s ∧ g (f a) = a ∧ LipschitzOnWith C g (Metric.ball (f a) s) ∧ ∀ z ∈ Metric.ball (f a) s, f (g z) = z

A noncritical holomorphic map has a Lipschitz inverse on a small image disk.

@[reducible, inline]

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

The n-fold iterate of the principal logarithm. Inverse identities below are asserted only on the indicated disks, where this branch applies.

Equations

• ExponentialJuliaSetMisiurewicz.logIterate n = Complex.log^[n]

theorem ExponentialJuliaSetMisiurewicz.log_lipschitz_real_ball {x : ℂ} (hx : x.im = 0) (hx10 : 10 ≤ x.re) : LipschitzOnWith (1 / 2) Complex.log (Metric.ball (Complex.exp x) 8)

The principal logarithm contracts by a factor of at most 1/2 on a radius-eight disk about exp x, for real x ≥ 10. This disk lies in Re z ≥ 2, so |1/z| ≤ 1/2.

theorem ExponentialJuliaSetMisiurewicz.log_maps_real_ball {x : ℂ} (hx : x.im = 0) (hx10 : 10 ≤ x.re) : Set.MapsTo Complex.log (Metric.ball (Complex.exp x) 8) (Metric.ball x 8)

The principal logarithm sends the radius-eight disk about exp x into the radius-eight disk about x, for real x ≥ 10.

theorem ExponentialJuliaSetMisiurewicz.logIterate_real_ball {x : ℂ} (hx : x.im = 0) (hx10 : 10 ≤ x.re) (n : ℕ) : logIterate n (expIterate n x) = x ∧ Set.MapsTo (logIterate n) (Metric.ball (expIterate n x) 8) (Metric.ball x 8) ∧ LipschitzOnWith ((1 / 2) ^ n) (logIterate n) (Metric.ball (expIterate n x) 8) ∧ ∀ z ∈ Metric.ball (expIterate n x) 8, expIterate n (logIterate n z) = z

Principal logarithms pull disks back along a far right real orbit.

theorem ExponentialJuliaSetMisiurewicz.log_lipschitz_upper : LipschitzOnWith 1 Complex.log {z : ℂ | 1 ≤ z.im}

The principal logarithm is 1-Lipschitz on the closed half-plane Im z ≥ 1.

theorem ExponentialJuliaSetMisiurewicz.exists_closing_inverse {D : Set ℂ} {a : ℂ} {L : ℂ → ℂ} {C : NNReal} (hL : LipschitzOnWith C L D) (hclose : ∀ z ∈ D, ‖L z - L a‖ ≤ 1) (hinv : ∀ z ∈ D, Complex.exp (L z) = z) : ∃ (ρ : ℝ), ∀ (x : ℝ), ρ ≤ x → ∃ (ψ : ℂ → ℂ), LipschitzOnWith C ψ D ∧ Set.MapsTo ψ D (Metric.ball (↑x) 8) ∧ ∀ z ∈ D, expIterate 2 (ψ z) = z

The closing step in Lemma 6.2. A bounded branch of logarithm can be translated vertically and logged again into any radius-eight disk sufficiently far to the right.

theorem ExponentialJuliaSetMisiurewicz.exists_repelling_fixedPoint_of_inverse {f h : ℂ → ℂ} {a : ℂ} {r : ℝ} (hr : 0 < r) (hlip : LipschitzOnWith (1 / 2) h (Metric.closedBall a r)) (hmaps : Set.MapsTo h (Metric.closedBall a r) (Metric.ball a (r / 2))) (hinv : ∀ z ∈ Metric.closedBall a r, f (h z) = z) (hf : Differentiable ℂ f) (hf0 : ∀ (z : ℂ), deriv f z ≠ 0) : ∃ p ∈ Metric.ball a r, f p = p ∧ 1 < ‖deriv f p‖

A strictly contracting inverse branch produces a repelling fixed point.

theorem ExponentialJuliaSetMisiurewicz.closing_inverse_on_small_ball {a : ℂ} (ha : a ≠ 0) {ε : ℝ} (hε : 0 < ε) : ∃ (r : ℝ), 0 < r ∧ r ≤ ε ∧ ∃ (C : NNReal) (ρ : ℝ), ∀ (x : ℝ), ρ ≤ x → ∃ (ψ : ℂ → ℂ), LipschitzOnWith C ψ (Metric.closedBall a r) ∧ Set.MapsTo ψ (Metric.closedBall a r) (Metric.ball (↑x) 8) ∧ ∀ z ∈ Metric.closedBall a r, expIterate 2 (ψ z) = z

A uniform family of two-step inverse branches on a small closed disk.

theorem ExponentialJuliaSetMisiurewicz.exists_repelling_near_real_preimage {a : ℂ} (ha : a ≠ 0) {m : ℕ} (hm : expIterate m a = 10) {ε : ℝ} (hε : 0 < ε) : ∃ p ∈ Metric.ball a ε, ∃ (N : ℕ), 0 < N ∧ expIterate N p = p ∧ 1 < ‖deriv (expIterate N) p‖

A point mapping to a far right real point is approximated by repelling periodic points.

theorem ExponentialJuliaSetMisiurewicz.exists_nonzero_mem_open {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) : ∃ z ∈ U, z ≠ 0

A nonempty open subset of the plane contains a nonzero point.

theorem ExponentialJuliaSetMisiurewicz.exists_repelling_periodic_mem_open {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) : ∃ p ∈ U, ∃ (n : ℕ), 0 < n ∧ expIterate n p = p ∧ 1 < ‖deriv (expIterate n) p‖

Theorem 6.1. Every nonempty open set contains a repelling periodic point.

theorem ExponentialJuliaSetMisiurewicz.dense_repelling_periodic_points : Dense {p : ℂ | ∃ (n : ℕ), 0 < n ∧ expIterate n p = p ∧ 1 < ‖deriv (expIterate n) p‖}

Repelling periodic points of the exponential are dense in the complex plane.

theorem ExponentialJuliaSetMisiurewicz.dense_periodic_points : Dense {p : ℂ | ∃ (n : ℕ), 0 < n ∧ expIterate n p = p}

Periodic points of the exponential are dense in the plane.

theorem ExponentialJuliaSetMisiurewicz.dense_periodicPts_exp : Dense (Function.periodicPts Complex.exp)

The periodic-point benchmark using mathlib's standard periodicPts set.