Classification of holomorphic automorphisms of the complex unit disc

This file completes the classification of the holomorphic automorphisms of the open unit disc. If f has a holomorphic two-sided inverse g, then on the disc

f z = u * (z - a) / (1 - conj a * z)

for a unique center a = g 0 and some u of modulus one. The proof conjugates f by the Moebius factor that sends a to the origin, then applies the origin-fixing rotation theorem exists_eqOn_const_mul_of_leftInvOn_ball_of_map_zero.

This discharges the conformal-mapping roadmap's L2 description of the disc automorphism group Aut(𝔻) = {e^{iθ}(z−a)/(1−āz)}. It builds on Mathlib's Schwarz lemma and on the standard disc-Moebius API developed in Tau Ceti. As with the other L0--L3 conformal-mapping material, this statement is coordinated with the upstream Mathlib Riemann-mapping effort leanprover-community/mathlib4#33505, whose preceding human-curated work is Analysis/Complex/RiemannMapping.lean and Analysis/Complex/BranchLogRoot.lean; none of it is duplicated here, and this statement should be replaced by human-curated upstream API if a disc-automorphism classification lands there.

theorem TauCeti.exists_forall_unitDisc_eq_unitDiscStandardAutomorphismEquiv {f g : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hg : DifferentiableOn ℂ g (Metric.ball 0 1)) (hfmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hgmaps : Set.MapsTo g (Metric.ball 0 1) (Metric.ball 0 1)) (hgf : Set.LeftInvOn g f (Metric.ball 0 1)) (hfg : Set.RightInvOn g f (Metric.ball 0 1)) : ∃ (u : Circle) (a : Complex.UnitDisc), ↑a = g 0 ∧ ∀ (z : Complex.UnitDisc), f ↑z = ↑((unitDiscStandardAutomorphismEquiv u a) z)

Classification of holomorphic disc automorphisms. A holomorphic self-map f of the open unit disc with a holomorphic two-sided inverse g has the standard form. Its center is g 0, and its rotation factor lies on the unit circle.