Spherical non-equicontinuity and non-normality

Iterates map the plane to the sphere. Two target values obstruct equicontinuity and locally uniform spherical subsequential limits.

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.

Spherical non-equicontinuity

The domain is ℂ with its usual Euclidean topology. The codomain is OnePoint ℂ with the canonical compact Hausdorff uniformity, identified below with the metric unit sphere by a uniform equivalence. Equicontinuity uses mathlib's standard EquicontinuousAt definition. The iterates remain defined only on the plane.

theorem ExponentialJuliaSetMisiurewicz.eventually_hits_one_and_two {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) : ∃ (N : ℕ), ∀ n ≥ N, (∃ z ∈ U, expIterate n z = 1) ∧ ∃ z ∈ U, expIterate n z = 2

Every sufficiently late iterate of a nonempty open set contains both 1 and 2.

theorem ExponentialJuliaSetMisiurewicz.not_equicontinuousAt_expIterate_comp {Y : Type u_1} [UniformSpace Y] [T0Space Y] {q : ℂ → Y} (hq : q 1 ≠ q 2) (z : ℂ) : ¬EquicontinuousAt (fun (n : ℕ) (w : ℂ) => q (expIterate n w)) z

The two-target obstruction to equicontinuity, for any separated uniform target and any target map distinguishing 1 and 2. The domain is the Euclidean plane.

@[reducible, inline]

abbrev ExponentialJuliaSetMisiurewicz.RiemannSphere : Type

The Riemann sphere, represented as the one-point compactification of ℂ.

Equations

• ExponentialJuliaSetMisiurewicz.RiemannSphere = OnePoint ℂ

@[instance_reducible]

noncomputable instance ExponentialJuliaSetMisiurewicz.riemannSphereUniformSpace : UniformSpace RiemannSphere

The canonical uniform structure on the compact Hausdorff Riemann sphere.

Equations

• ExponentialJuliaSetMisiurewicz.riemannSphereUniformSpace = uniformSpaceOfCompactR1

noncomputable def ExponentialJuliaSetMisiurewicz.riemannSphereUniformEquivUnitSphere : RiemannSphere ≃ᵤ ↑(Metric.sphere 0 1)

A checked identification with the ordinary metric unit sphere in ℝ³. Both directions are uniformly continuous by compactness.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ExponentialJuliaSetMisiurewicz.sphericalExpIterate (n : ℕ) (z : ℂ) : RiemannSphere

The exponential iterates from the Euclidean plane to the Riemann sphere.

Equations

• ExponentialJuliaSetMisiurewicz.sphericalExpIterate n z = ↑(ExponentialJuliaSetMisiurewicz.expIterate n z)

theorem ExponentialJuliaSetMisiurewicz.not_equicontinuousAt_sphericalExpIterate (z : ℂ) : ¬EquicontinuousAt sphericalExpIterate z

The exponential iterates fail to be spherically equicontinuous at every finite point.

theorem ExponentialJuliaSetMisiurewicz.not_equicontinuousAt_unitSphereExpIterate (z : ℂ) : ¬EquicontinuousAt (fun (n : ℕ) (w : ℂ) => riemannSphereUniformEquivUnitSphere (sphericalExpIterate n w)) z

The same non-equicontinuity statement with the ordinary metric sphere as codomain.

No locally uniform subsequential limits

For a continuous map into any separated uniform space distinguishing 1 and 2, the corresponding iterates have no locally uniform limit along an increasing subsequence on a nonempty open set. In particular, this applies to the spherical uniformity and allows arbitrary sphere-valued limit functions, including functions taking the value infinity.

theorem ExponentialJuliaSetMisiurewicz.not_tendstoLocallyUniformlyOn_expIterate_comp {Y : Type u_1} [UniformSpace Y] [T0Space Y] {q : ℂ → Y} (hqcont : Continuous q) (hq : q 1 ≠ q 2) {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) {φ : ℕ → ℕ} (hφ : StrictMono φ) (g : ℂ → Y) : ¬TendstoLocallyUniformlyOn (fun (n : ℕ) (z : ℂ) => q (expIterate (φ n) z)) g Filter.atTop U

Eventual point covering obstructs all locally uniform subsequential limits in any separated uniform target, provided the continuous target map distinguishes 1 and 2.

theorem ExponentialJuliaSetMisiurewicz.not_tendstoLocallyUniformly_expIterate_comp {Y : Type u_1} [UniformSpace Y] [T0Space Y] {q : ℂ → Y} (hqcont : Continuous q) (hq : q 1 ≠ q 2) {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) {φ : ℕ → ℕ} (hφ : StrictMono φ) (g : ↑U → Y) : ¬TendstoLocallyUniformly (fun (n : ℕ) (z : ↑U) => q (expIterate (φ n) ↑z)) g Filter.atTop

The two-target obstruction with the limit function defined only on its domain U. The auxiliary extension in the proof serves solely to use Mathlib's ambient-domain API.

theorem ExponentialJuliaSetMisiurewicz.not_tendstoLocallyUniformlyOn_sphericalExpIterate {U : Set ℂ} (hU : IsOpen U) (hUne : U.Nonempty) {φ : ℕ → ℕ} (hφ : StrictMono φ) (g : ℂ → RiemannSphere) : ¬TendstoLocallyUniformlyOn (fun (n : ℕ) => sphericalExpIterate (φ n)) g Filter.atTop U

No increasing subsequence of exponential iterates converges locally uniformly in the spherical uniformity on a nonempty open set, to any sphere-valued function.

def ExponentialJuliaSetMisiurewicz.HasSensitiveDependenceVia {Y : Type u_1} [MetricSpace Y] (q : ℂ → Y) : Prop

Sensitive dependence for maps from the plane to a metric target. The iterates themselves remain plane-valued; q changes only the metric used to compare their values.

Equations

• One or more equations did not get rendered due to their size.

theorem ExponentialJuliaSetMisiurewicz.spherical_sensitive_dependence_exp : HasSensitiveDependenceVia fun (w : ℂ) => riemannSphereUniformEquivUnitSphere ↑w

Corollary 4.4. The exponential map has sensitive dependence with respect to spherical distance, represented by the ordinary metric on the unit sphere in ℝ³.