The Poincaré disc carries the Euclidean topology and is a proper metric space

Poincare/MetricSpace.lean equips the type synonym TauCeti.PoincareDisc of Complex.UnitDisc with the hyperbolic (Poincaré) distance TauCeti.hyperbolicDist as a MetricSpace instance. That instance says nothing yet about how the resulting topology compares with the Euclidean subspace topology of the disc, nor whether the metric is complete. This file settles both.

The comparison rests on two elementary estimates for the pseudo-hyperbolic expression p = pseudoHyperbolicExpr z w = ‖(z - w) / (1 - conj w * z)‖, of which the hyperbolic distance is the reparametrisation Real.artanh p:

• the Moebius denominator has norm at most 2 on the disc, so ‖z - w‖ ≤ 2 * p, which makes the identity map from the Poincaré disc to the Euclidean disc Lipschitz-like near the diagonal;
• p depends continuously on (z, w) — that is TauCeti.continuousOn_pseudoHyperbolicExpr, from TauCeti/Analysis/Complex/Conformal/PseudoHyperbolic.lean — and Real.artanh is continuous on (-1, 1) — that is Real.continuousOn_artanh, from TauCeti/Analysis/SpecialFunctions/Artanh.lean — so the hyperbolic distance is jointly continuous for the Euclidean topology.

Properness comes from a compact exhaustion: a closed hyperbolic ball around x of radius r is contained in the closed Euclidean disc of radius Real.tanh (r + hyperbolicDist x 0), whose radius is strictly less than one, so it is a closed subset of a compact subset of the open disc.

Main declarations

• TauCeti.continuousOn_hyperbolicDist — the hyperbolic distance is jointly continuous on ball 0 1 ×ˢ ball 0 1.
• TauCeti.norm_sub_le_two_mul_pseudoHyperbolicExpr — the Euclidean distance of two disc points is at most twice their pseudo-hyperbolic expression.
• TauCeti.hyperbolicDist_zero_le_iff_norm_le_tanh — the closed hyperbolic ball about the origin of radius r is the closed Euclidean ball of radius Real.tanh r.
• TauCeti.PoincareDisc.toUnitDiscHomeomorph — the identification of the Poincaré disc with Complex.UnitDisc is a homeomorphism; the simp lemmas toUnitDiscHomeomorph_apply and toUnitDiscHomeomorph_symm_apply characterise both directions, so consumers never need to unfold the definition, whose body is deliberately not exposed.
• TauCeti.PoincareDisc.instProperSpace — the Poincaré disc is a proper metric space, hence complete and locally compact.

This carries the conformal-mapping roadmap's L2 target "the hyperbolic / Poincaré metric on 𝔻" (see ConformalMapping/README.md) onto its topological side: with the homeomorphism in hand, the hyperbolic metric may be used interchangeably with the Euclidean one for topological purposes, and completeness is what makes the Poincaré disc a usable model of the hyperbolic plane. It reuses Tau Ceti's pseudo-hyperbolic and hyperbolic-distance API. As with the rest of the L0--L3 conformal-mapping material, it is coordinated with the upstream Mathlib Riemann mapping effort leanprover-community/mathlib4#33505 and should be refactored to upstream API if that work lands a human-curated Poincaré metric. Mathlib already contains the preceding human-curated work in Analysis/Complex/RiemannMapping.lean and Analysis/Complex/BranchLogRoot.lean; this file duplicates none of their branch-logarithm and root API, adding only the topological side of the hyperbolic metric. Mathlib has the hyperbolic metric on the upper half-plane (Analysis/Complex/UpperHalfPlane), but no Poincaré metric on the disc.

Comparison of the Euclidean and pseudo-hyperbolic distances

theorem TauCeti.norm_sub_le_two_mul_pseudoHyperbolicExpr {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : ‖z - w‖ ≤ 2 * pseudoHyperbolicExpr z w

The Euclidean distance between two points of the open unit disc is at most twice their pseudo-hyperbolic expression: the Moebius denominator 1 - conj w * z has norm at most 2.

Joint continuity of the hyperbolic distance

theorem TauCeti.continuousOn_hyperbolicDist : ContinuousOn (fun (p : ℂ × ℂ) => hyperbolicDist p.1 p.2) (Metric.ball 0 1 ×ˢ Metric.ball 0 1)

The hyperbolic distance is jointly continuous on the product of two copies of the open unit disc, for the Euclidean topology of ℂ.

theorem TauCeti.continuous_hyperbolicDist_unitDisc (w : Complex.UnitDisc) : Continuous fun (z : Complex.UnitDisc) => hyperbolicDist ↑z ↑w

For a fixed base point, the hyperbolic distance is a continuous function on Complex.UnitDisc with its Euclidean subspace topology.

Hyperbolic balls about the origin

theorem TauCeti.hyperbolicDist_zero_le_iff_norm_le_tanh {z : ℂ} (hz : ‖z‖ < 1) (r : ℝ) : hyperbolicDist z 0 ≤ r ↔ ‖z‖ ≤ Real.tanh r

A point of the open unit disc lies within hyperbolic distance r of the origin exactly when its Euclidean norm is at most Real.tanh r: the closed hyperbolic ball about the origin is the closed Euclidean ball of radius Real.tanh r.

The Poincaré disc is homeomorphic to the Euclidean disc

theorem TauCeti.PoincareDisc.continuous_toUnitDisc : Continuous ⇑toUnitDisc

The identity map from the Poincaré disc to Complex.UnitDisc is continuous: two points at small hyperbolic distance are at small Euclidean distance, since ‖z - w‖ ≤ 2 * p while the hyperbolic distance is the increasing reparametrisation Real.artanh p.

theorem Complex.UnitDisc.continuous_toPoincare : Continuous ⇑toPoincare

The identity map from Complex.UnitDisc to the Poincaré disc is continuous, because the hyperbolic distance to a fixed point is a continuous function for the Euclidean topology and vanishes at that point.

def TauCeti.PoincareDisc.toUnitDiscHomeomorph : PoincareDisc ≃ₜ Complex.UnitDisc

The Poincaré disc carries the Euclidean topology. The identification of the Poincaré disc with Complex.UnitDisc is a homeomorphism, so the hyperbolic metric may be used interchangeably with the Euclidean one for topological purposes.

The body is not exposed: the two simp lemmas below characterise both directions, so consumers never depend on how the homeomorphism is assembled.

Equations

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

@[simp]

theorem TauCeti.PoincareDisc.toUnitDiscHomeomorph_apply (z : PoincareDisc) : toUnitDiscHomeomorph z = toUnitDisc z

The homeomorphism acts as the identification PoincareDisc.toUnitDisc.

@[simp]

theorem TauCeti.PoincareDisc.toUnitDiscHomeomorph_symm_apply (z : Complex.UnitDisc) : toUnitDiscHomeomorph.symm z = Complex.UnitDisc.toPoincare z

The inverse homeomorphism acts as the identification Complex.UnitDisc.toPoincare.

Properness of the Poincaré metric

instance TauCeti.PoincareDisc.instProperSpace : ProperSpace PoincareDisc

The Poincaré disc is a proper metric space. A closed hyperbolic ball of radius r about x consists of points at hyperbolic distance at most r + hyperbolicDist x 0 from the origin, hence of Euclidean norm at most Real.tanh (r + hyperbolicDist x 0) < 1; it is therefore a closed subset of a compact subset of the open disc.

Concretely, every bounded hyperbolic ball is contained in a Euclidean subdisc of radius strictly less than one. Together with the instances Mathlib derives from ProperSpace, this makes the Poincaré disc a complete and locally compact metric space.

Completeness and local compactness

Mathlib derives CompleteSpace and LocallyCompactSpace from ProperSpace; we record that those instances are indeed found for the Poincaré disc.