The Poincaré metric space on the complex unit disc

The symmetry, nonnegativity, vanishing-on-the-diagonal and triangle-inequality lemmas already proved for the hyperbolic (Poincaré) distance hyperbolicDist on the open unit disc (HyperbolicDistance.lean, HyperbolicTriangle.lean) are exactly the metric-space axioms. This file records them as an actual MetricSpace instance.

The instance cannot be attached to Complex.UnitDisc, which already carries the Euclidean subspace metric. Following the standard Mathlib type-synonym idiom (as for OrderDual, Lex, …), we introduce

• PoincareDisc — a type synonym for Complex.UnitDisc, with the reinterpretation maps Complex.UnitDisc.toPoincare and PoincareDisc.toUnitDisc (mutually inverse identity equivalences);
• PoincareDisc.instMetricSpace — the Poincaré MetricSpace, with dist z w = hyperbolicDist z w on the underlying disc points (PoincareDisc.dist_eq).

The disc automorphisms are then recorded as genuine self-isometries of this metric space, validating that the Poincaré distance is the automorphism-invariant metric:

• PoincareDisc.isometry_of_hyperbolicDist_eq — a hyperbolic-distance-preserving self-map of the unit disc induces a self-isometry of the Poincaré disc;
• PoincareDisc.isometry_unitDiscMoebius, PoincareDisc.isometry_unitDiscStandardAutomorphismEquiv — the disc Moebius factors and the standard automorphisms as Poincaré isometries.

This completes the conformal-mapping roadmap's L2 target "the hyperbolic / Poincaré metric on 𝔻" (see ConformalMapping/README.md), discharging the MetricSpace-instance step that the docstrings of HyperbolicDistance.lean and HyperbolicTriangle.lean deferred as future work. It reuses Tau Ceti's hyperbolic-distance and disc-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 Poincaré metric. Mathlib has the hyperbolic metric on the upper half-plane (Analysis/Complex/UpperHalfPlane), but no Poincaré metric on the disc.

def TauCeti.PoincareDisc : Type

The complex open unit disc equipped with the hyperbolic (Poincaré) metric.

This is a type synonym for Complex.UnitDisc, introduced so that the Poincaré distance can be registered as a MetricSpace instance without clashing with the Euclidean subspace metric that Complex.UnitDisc already carries. Move between the two views with the identity equivalences Complex.UnitDisc.toPoincare and PoincareDisc.toUnitDisc.

Equations

• TauCeti.PoincareDisc = Complex.UnitDisc

def Complex.UnitDisc.toPoincare : UnitDisc ≃ TauCeti.PoincareDisc

Reinterpret a point of the unit disc as a point of the Poincaré disc (the identity map).

Equations

• Complex.UnitDisc.toPoincare = Equiv.refl Complex.UnitDisc

def TauCeti.PoincareDisc.toUnitDisc : PoincareDisc ≃ Complex.UnitDisc

Reinterpret a point of the Poincaré disc as a point of the unit disc (the identity map).

Equations

• TauCeti.PoincareDisc.toUnitDisc = Complex.UnitDisc.toPoincare.symm

@[simp]

theorem TauCeti.PoincareDisc.toUnitDisc_toPoincare (z : Complex.UnitDisc) : toUnitDisc (Complex.UnitDisc.toPoincare z) = z

@[simp]

theorem TauCeti.PoincareDisc.toPoincare_toUnitDisc (z : PoincareDisc) : Complex.UnitDisc.toPoincare (toUnitDisc z) = z

theorem TauCeti.PoincareDisc.coe_mem_ball (z : PoincareDisc) : ↑(toUnitDisc z) ∈ Metric.ball 0 1

Every point of the Poincaré disc lies in the open unit ball.

@[instance_reducible]

noncomputable instance TauCeti.PoincareDisc.instMetricSpace : MetricSpace PoincareDisc

The Poincaré (hyperbolic) metric space on the complex open unit disc. Its distance is the hyperbolic distance hyperbolicDist on the underlying disc points.

Equations

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

@[simp]

theorem TauCeti.PoincareDisc.dist_eq (z w : PoincareDisc) : dist z w = hyperbolicDist ↑(toUnitDisc z) ↑(toUnitDisc w)

The Poincaré distance between two disc points is their hyperbolic distance.

theorem TauCeti.PoincareDisc.dist_toPoincare_zero_right (z : PoincareDisc) : dist z (Complex.UnitDisc.toPoincare 0) = Real.artanh ‖↑(toUnitDisc z)‖

The Poincaré distance from a point to the origin has the closed form artanh ‖z‖.

theorem TauCeti.PoincareDisc.isometry_of_hyperbolicDist_eq {g : Complex.UnitDisc → Complex.UnitDisc} (hg : ∀ (z w : Complex.UnitDisc), hyperbolicDist ↑(g z) ↑(g w) = hyperbolicDist ↑z ↑w) : Isometry fun (z : PoincareDisc) => Complex.UnitDisc.toPoincare (g (toUnitDisc z))

A hyperbolic-distance-preserving self-map of the unit disc induces a self-isometry of the Poincaré disc (transported along the identification Complex.UnitDisc.toPoincare).

theorem TauCeti.PoincareDisc.isometry_unitDiscMoebius (a : Complex.UnitDisc) : Isometry fun (z : PoincareDisc) => Complex.UnitDisc.toPoincare (unitDiscMoebius a (toUnitDisc z))

The disc Moebius factor z ↦ (z - a) / (1 - conj a * z) is a Poincaré self-isometry.

theorem TauCeti.PoincareDisc.isometry_unitDiscStandardAutomorphismEquiv (u : Circle) (a : Complex.UnitDisc) : Isometry fun (z : PoincareDisc) => Complex.UnitDisc.toPoincare ((unitDiscStandardAutomorphismEquiv u a) (toUnitDisc z))

Every standard disc automorphism z ↦ u * (z - a) / (1 - conj a * z) is a Poincaré self-isometry.