The hyperbolic (Poincaré) distance on the unit disc

This file defines the hyperbolic (Poincaré) distance on the complex open unit disc, hyperbolicDist z w = Real.artanh p where p = pseudoHyperbolicExpr z w is the pseudo-hyperbolic expression ‖(z - w) / (1 - conj w * z)‖. The inverse hyperbolic tangent Real.artanh t = (1 / 2) * log ((1 + t) / (1 - t)) is the standard order isomorphism [0, 1) ≃ [0, ∞), so the hyperbolic distance is a strictly monotone reparametrisation of the pseudo-hyperbolic expression by which the two record the same geometry additively.

The normalisation matches the infinitesimal Poincaré metric |dz| / (1 - |z| ^ 2) already formalized in this area (SchwarzPickDerivative.lean): the geodesic distance from the origin to a point at radius r under that metric is ∫₀ʳ dt / (1 - t ^ 2) = artanh r, which is exactly hyperbolicDist z 0 for ‖z‖ = r.

The main API mirrors the pseudo-hyperbolic layer:

• hyperbolicDist_comm, hyperbolicDist_self, hyperbolicDist_nonneg, hyperbolicDist_eq_zero_iff_of_mem_ball — the basic pseudo-metric properties;
• hyperbolicDist_zero_right — the closed form artanh ‖z‖ from the origin;
• hyperbolicDist_map_le — the Schwarz--Pick theorem in its classical distance-decreasing form: a holomorphic self-map of the disc does not increase the hyperbolic distance;
• hyperbolicDist_unitDiscMoebius, hyperbolicDist_unitDiscStandardAutomorphismEquiv — the hyperbolic distance is invariant under the disc Moebius factors and the standard automorphisms, i.e. these are hyperbolic isometries.

The full metric-space structure (the triangle inequality, hence a MetricSpace instance on Complex.UnitDisc) is deferred; it rests on the strengthened pseudo-hyperbolic triangle inequality and is future work of the L2 layer.

This advances the conformal-mapping roadmap's L2 target "the hyperbolic / Poincaré metric on 𝔻" (see ConformalMapping/README.md). It reuses Tau Ceti's pseudo-hyperbolic and Schwarz--Pick 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. Mathlib already contains the preceding human-curated work in Analysis/Complex/RiemannMapping.lean and Analysis/Complex/BranchLogRoot.lean; none of it is duplicated here, and should that work land a human-curated Poincaré metric this file should be refactored onto it. Mathlib has the hyperbolic metric on the upper half-plane (Analysis/Complex/UpperHalfPlane), but no hyperbolic distance on the disc.

noncomputable def TauCeti.hyperbolicDist (z w : ℂ) : ℝ

The hyperbolic (Poincaré) distance on the complex unit disc, written as a total real-valued function Real.artanh p of the pseudo-hyperbolic expression p = pseudoHyperbolicExpr z w.

On the open unit disc this is the hyperbolic distance, normalised to agree with the infinitesimal Poincaré metric |dz| / (1 - |z| ^ 2). Outside the disc, where p may reach or exceed one, the formula remains a total Lean expression with no geometric meaning.

Equations

• TauCeti.hyperbolicDist z w = Real.artanh (TauCeti.pseudoHyperbolicExpr z w)

theorem TauCeti.hyperbolicDist_def (z w : ℂ) : hyperbolicDist z w = Real.artanh (pseudoHyperbolicExpr z w)

The defining formula for the hyperbolic distance.

theorem TauCeti.hyperbolicDist_comm (z w : ℂ) : hyperbolicDist z w = hyperbolicDist w z

The hyperbolic distance is symmetric.

@[simp]

theorem TauCeti.hyperbolicDist_conj (z w : ℂ) : hyperbolicDist ((starRingEnd ℂ) z) ((starRingEnd ℂ) w) = hyperbolicDist z w

Conjugation invariance. Conjugating both points leaves the hyperbolic distance unchanged, so conjugation is a hyperbolic isometry of the disc.

@[simp]

theorem TauCeti.hyperbolicDist_self (z : ℂ) : hyperbolicDist z z = 0

The hyperbolic distance from a point to itself is zero.

theorem TauCeti.hyperbolicDist_zero_right (z : ℂ) : hyperbolicDist z 0 = Real.artanh ‖z‖

The hyperbolic distance from a point of the disc to the origin has the closed form artanh ‖z‖.

theorem TauCeti.hyperbolicDist_nonneg (z w : ℂ) : 0 ≤ hyperbolicDist z w

The hyperbolic distance is nonnegative.

theorem TauCeti.hyperbolicDist_eq_zero_iff_of_mem_ball {z w : ℂ} (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) : hyperbolicDist z w = 0 ↔ z = w

On the open unit disc the hyperbolic distance vanishes exactly on the diagonal.

theorem TauCeti.pseudoHyperbolicExpr_eq_iff_hyperbolicDist_eq {z w z' w' : ℂ} (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) (hz' : z' ∈ Metric.ball 0 1) (hw' : w' ∈ Metric.ball 0 1) : pseudoHyperbolicExpr z w = pseudoHyperbolicExpr z' w' ↔ hyperbolicDist z w = hyperbolicDist z' w'

On the open unit disc the hyperbolic distance and the pseudo-hyperbolic expression carry the same information: Real.artanh is injective on (-1, 1), and the pseudo-hyperbolic expression of a pair of disc points lies in [0, 1).

theorem TauCeti.hyperbolicDist_map_le {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) {z w : ℂ} (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) : hyperbolicDist (f z) (f w) ≤ hyperbolicDist z w

Schwarz--Pick, distance form. A holomorphic self-map of the complex unit disc does not increase the hyperbolic distance.

theorem TauCeti.hyperbolicDist_map_le_unitDisc {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (z w : Complex.UnitDisc) : hyperbolicDist (f ↑z) (f ↑w) ≤ hyperbolicDist ↑z ↑w

Bundled unit-disc form of Schwarz--Pick in distance form.

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

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

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

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