Disc automorphisms are pseudo-hyperbolic isometries

The Schwarz--Pick contraction estimate pseudoHyperbolicExpr_map_le says a holomorphic self-map of the unit disc does not increase the pseudo-hyperbolic expression pseudoHyperbolicExpr z w = ‖(z - w) / (1 - conj w * z)‖. A holomorphic self-map that additionally has a holomorphic self-map inverse must then preserve the expression: applying the estimate to the map and to its inverse forces equality. This file records that equality and specializes it to the concrete disc automorphisms.

The results are:

• pseudoHyperbolicExpr_map_eq — the Schwarz--Pick equality for any holomorphic self-map of the disc with a holomorphic self-map left inverse;
• pseudoHyperbolicExpr_unitDiscMoebiusFormula_of_norm_lt_one / pseudoHyperbolicExpr_unitDiscMoebius — the Moebius factor z ↦ (z - a) / (1 - conj a * z) is a pseudo-hyperbolic isometry, in scalar and bundled Complex.UnitDisc form;
• pseudoHyperbolicExpr_unitDiscStandardAutomorphismEquiv — every standard disc automorphism z ↦ u * (z - a) / (1 - conj a * z) is a pseudo-hyperbolic isometry.

Together these say that the pseudo-hyperbolic expression is preserved by holomorphic self-maps of the disc with a holomorphic self-map left inverse, and by the standard automorphisms bundled as unitDiscStandardAutomorphismEquiv.

This advances the conformal-mapping roadmap's L2 Schwarz--Pick / disc-automorphism target, building directly on Tau Ceti's pseudoHyperbolicExpr_map_le (Mathlib's Schwarz lemma) and the unit-disc Moebius / automorphism API. As with the rest of the L0--L3 conformal-mapping material, it is coordinated with the upstream Mathlib RMT effort leanprover-community/mathlib4#33505 and should be refactored to upstream API if that work lands a human-curated Schwarz--Pick theorem.

theorem TauCeti.pseudoHyperbolicExpr_map_eq {f g : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hfmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hg : DifferentiableOn ℂ g (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)) {z w : ℂ} (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) : pseudoHyperbolicExpr (f z) (f w) = pseudoHyperbolicExpr z w

Schwarz--Pick equality. A holomorphic self-map of the unit disc that admits a holomorphic self-map left inverse preserves the pseudo-hyperbolic expression: the Schwarz--Pick contraction, applied to the map and to its inverse, forces equality.

@[simp]

theorem TauCeti.pseudoHyperbolicExpr_unitDiscMoebiusFormula_of_norm_lt_one {a : ℂ} (ha : ‖a‖ < 1) {z w : ℂ} (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) : pseudoHyperbolicExpr ((z - a) / (1 - (starRingEnd ℂ) a * z)) ((w - a) / (1 - (starRingEnd ℂ) a * w)) = pseudoHyperbolicExpr z w

Moebius invariance (scalar form). The Moebius factor z ↦ (z - a) / (1 - conj a * z) with ‖a‖ < 1 is a pseudo-hyperbolic isometry of the open unit disc.

@[simp]

theorem TauCeti.pseudoHyperbolicExpr_unitDiscMoebius (a z w : Complex.UnitDisc) : pseudoHyperbolicExpr ((↑z - ↑a) / (1 - (starRingEnd ℂ) ↑a * ↑z)) ((↑w - ↑a) / (1 - (starRingEnd ℂ) ↑a * ↑w)) = pseudoHyperbolicExpr ↑z ↑w

Moebius invariance (bundled form). The bundled unit-disc Moebius factor unitDiscMoebius a preserves the pseudo-hyperbolic expression.

theorem TauCeti.pseudoHyperbolicExpr_unitDiscStandardAutomorphismEquiv (u : Circle) (a z w : Complex.UnitDisc) : pseudoHyperbolicExpr ↑((unitDiscStandardAutomorphismEquiv u a) z) ↑((unitDiscStandardAutomorphismEquiv u a) w) = pseudoHyperbolicExpr ↑z ↑w

Standard automorphism invariance. Every standard disc automorphism bundled as unitDiscStandardAutomorphismEquiv u a preserves the pseudo-hyperbolic expression.