Bounded holomorphic families and Cayley transforms

Cauchy estimates control bounded families; Cayley transforms apply them to the half-plane.

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.

Weak Montel: equicontinuity from a uniform bound

The Cauchy estimate bounds the derivative of a bounded holomorphic function, which makes a uniformly bounded family uniformly Lipschitz on a smaller ball. For the exponential iterates this is enough: if no image of V meets the real axis then each image, being connected, lies in one open half-plane, and a Möbius transformation makes the family bounded.

theorem ExponentialJuliaSetMisiurewicz.norm_deriv_le_of_bounded {f : ℂ → ℂ} {U : Set ℂ} {M r : ℝ} {z : ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (hr : 0 < r) (hzr : Metric.closedBall z r ⊆ U) (hb : ∀ w ∈ U, ‖f w‖ ≤ M) : ‖deriv f z‖ ≤ M / r

Cauchy's estimate: a holomorphic function bounded by M has ‖deriv f z‖ ≤ M / r whenever closedBall z r lies in the domain.

theorem ExponentialJuliaSetMisiurewicz.norm_sub_le_of_bounded {f : ℂ → ℂ} {M ρ : ℝ} {c : ℂ} (hρ : 0 < ρ) (hf : DifferentiableOn ℂ f (Metric.ball c (2 * ρ))) (hb : ∀ w ∈ Metric.ball c (2 * ρ), ‖f w‖ ≤ M) {x y : ℂ} (hx : x ∈ Metric.ball c ρ) (hy : y ∈ Metric.ball c ρ) : ‖f x - f y‖ ≤ 2 * M / ρ * ‖x - y‖

A holomorphic function bounded by M on ball c (2ρ) is 2M/ρ-Lipschitz on ball c ρ.

theorem ExponentialJuliaSetMisiurewicz.equicontinuous_of_bounded {ι : Type u_1} {F : ι → ℂ → ℂ} {M ρ : ℝ} {c : ℂ} (hρ : 0 < ρ) (hF : ∀ (i : ι), DifferentiableOn ℂ (F i) (Metric.ball c (2 * ρ))) (hb : ∀ (i : ι), ∀ w ∈ Metric.ball c (2 * ρ), ‖F i w‖ ≤ M) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ (i : ι), ∀ x ∈ Metric.ball c ρ, ∀ y ∈ Metric.ball c ρ, ‖x - y‖ < δ → ‖F i x - F i y‖ < ε

Weak Montel, equicontinuity form. A uniformly bounded family of holomorphic functions on ball c (2ρ) is equicontinuous on ball c ρ, with a modulus independent of the index.

The Cayley transform, used to bound the family

If no image of V meets the real axis then each image, being connected, lies in one open half-plane. A Cayley transform carries that half-plane into the unit disc, making the transformed family uniformly bounded, so equicontinuous_of_bounded applies.

theorem ExponentialJuliaSetMisiurewicz.norm_cayleyUp_lt_one {z : ℂ} (hz : 0 < z.im) : ‖(z - Complex.I) / (z + Complex.I)‖ < 1

z ↦ (z - i)/(z + i) maps the upper half-plane into the unit disc.

theorem ExponentialJuliaSetMisiurewicz.norm_cayleyDown_lt_one {z : ℂ} (hz : z.im < 0) : ‖(z + Complex.I) / (z - Complex.I)‖ < 1

z ↦ (z + i)/(z - i) maps the lower half-plane into the unit disc.

theorem ExponentialJuliaSetMisiurewicz.cayleyUp_inv {w : ℂ} (hw : w + Complex.I ≠ 0) : Complex.I * (1 + (w - Complex.I) / (w + Complex.I)) / (1 - (w - Complex.I) / (w + Complex.I)) = w

The Cayley transform of the upper half-plane is inverted by u ↦ i(1+u)/(1-u).

theorem ExponentialJuliaSetMisiurewicz.cayleyDown_inv {w : ℂ} (hw : w - Complex.I ≠ 0) : Complex.I * (1 + (w + Complex.I) / (w - Complex.I)) / ((w + Complex.I) / (w - Complex.I) - 1) = w

The Cayley transform of the lower half-plane is inverted by u ↦ i(u+1)/(u-1).

theorem ExponentialJuliaSetMisiurewicz.add_I_ne_zero {z : ℂ} (h : 0 < z.im) : z + Complex.I ≠ 0

The denominator of the upper-half-plane Cayley transform does not vanish there.

theorem ExponentialJuliaSetMisiurewicz.sub_I_ne_zero {z : ℂ} (h : z.im < 0) : z - Complex.I ≠ 0

The denominator of the lower-half-plane Cayley transform does not vanish there.

theorem ExponentialJuliaSetMisiurewicz.image_in_half_plane {V : Set ℂ} (hVconn : IsConnected V) (hnoreal : ∀ (n : ℕ), ∀ z ∈ V, (expIterate n z).im ≠ 0) (n : ℕ) : (∀ z ∈ V, 0 < (expIterate n z).im) ∨ ∀ z ∈ V, (expIterate n z).im < 0

Each image lies wholly in one open half-plane. If no forward image of the connected set V meets the real axis, then for each n the image is entirely in the upper half-plane or entirely in the lower one — by the intermediate value theorem applied to Im.

theorem ExponentialJuliaSetMisiurewicz.differentiableOn_cayleyUp {U : Set ℂ} {n : ℕ} (hpos : ∀ z ∈ U, 0 < (expIterate n z).im) : DifferentiableOn ℂ (fun (w : ℂ) => (expIterate n w - Complex.I) / (expIterate n w + Complex.I)) U

The Cayley transform of an iterate is holomorphic wherever the iterate has positive imaginary part.

theorem ExponentialJuliaSetMisiurewicz.differentiableOn_cayleyDown {U : Set ℂ} {n : ℕ} (hneg : ∀ z ∈ U, (expIterate n z).im < 0) : DifferentiableOn ℂ (fun (w : ℂ) => (expIterate n w + Complex.I) / (expIterate n w - Complex.I)) U

The lower-half-plane Cayley transform of an iterate is holomorphic wherever that iterate has negative imaginary part.

theorem ExponentialJuliaSetMisiurewicz.equicontinuous_cayleyUp {c : ℂ} {ρ : ℝ} (hρ : 0 < ρ) {T : Set ℕ} (hT : ∀ n ∈ T, ∀ z ∈ Metric.ball c (2 * ρ), 0 < (expIterate n z).im) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ (n : ↑T), ∀ x ∈ Metric.ball c ρ, ∀ y ∈ Metric.ball c ρ, ‖x - y‖ < δ → ‖(expIterate (↑n) x - Complex.I) / (expIterate (↑n) x + Complex.I) - (expIterate (↑n) y - Complex.I) / (expIterate (↑n) y + Complex.I)‖ < ε

The transformed family is uniformly bounded, hence equicontinuous. Along any set of times whose images all lie in the upper half-plane, the Cayley transforms of the iterates are bounded by 1 on ball c (2ρ), so equicontinuous_of_bounded applies on ball c ρ.

theorem ExponentialJuliaSetMisiurewicz.cayleyUp_ne_one {w : ℂ} (hw : w + Complex.I ≠ 0) : (w - Complex.I) / (w + Complex.I) ≠ 1

The Cayley transform never takes the value 1.

theorem ExponentialJuliaSetMisiurewicz.norm_sub_lt_of_cayley_close {p : ℂ} (hp : p + Complex.I ≠ 0) {η : ℝ} (hη : 0 < η) : ∃ ε > 0, ∀ (w : ℂ), w + Complex.I ≠ 0 → ‖(w - Complex.I) / (w + Complex.I) - (p - Complex.I) / (p + Complex.I)‖ < ε → ‖w - p‖ < η

Push-back. Near a finite point p ≠ -i, closeness of Cayley transforms gives closeness of the points themselves. This is what converts the equicontinuity of the transformed family back into Euclidean information about the iterates.