The Poincaré disc is a geodesic metric space

Poincare/MetricSpace.lean makes the complex open unit disc a metric space TauCeti.PoincareDisc for the hyperbolic distance TauCeti.hyperbolicDist, and Poincare/Topology.lean shows the resulting metric is proper. This file adds the remaining basic geometric fact about that metric: it is geodesic, the Euclidean diameters being unit-speed geodesic lines through the origin. (The converse classification — that every geodesic through the origin is a Euclidean diameter — is a uniqueness statement, and is not proved here.)

The computation behind everything is that along a fixed Euclidean diameter {u * a | a : ℝ} of the disc, with ‖u‖ = 1, the hyperbolic distance is the difference of the inverse hyperbolic tangents of the signed radii: hyperbolicDist (u * a) (u * b) = |artanh a - artanh b| (TauCeti.hyperbolicDist_mul_ofReal_of_norm_eq_one). Indeed the Moebius denominator 1 - conj (u * b) * (u * a) collapses to the real number 1 - a * b, so the pseudo-hyperbolic expression is |a - b| / |1 - a * b|, and the subtraction formula Real.artanh_sub of TauCeti/Analysis/SpecialFunctions/Artanh.lean, together with Real.artanh_abs, turns that into |artanh a - artanh b|. Reparametrising the diameter by a = Real.tanh t makes it a unit-speed line: TauCeti.PoincareDisc.radialGeodesic u is an isometric embedding of ℝ.

Every point of the disc lies on such a line through the origin, and the disc automorphisms act transitively by isometries, so transporting a radial line names the geodesic line through an arbitrary point: carrying the radial geodesic in direction u back by (unitDiscMoebiusIsometryEquiv (toUnitDisc a)).symm — the inverse of the Moebius isometry that sends a to the origin — gives TauCeti.PoincareDisc.geodesicLine a u, which starts at a and repeats the radial API (coe_geodesicLine, geodesicLine_zero, isometry_geodesicLine, dist_geodesicLine_self, geodesicLine_injective) at that base point. No hyperbolic computation is redone: each of those statements is its radial counterpart read through an isometry. Negating the direction of either line reverses its time parameter (radialGeodesic_neg, geodesicLine_neg), Real.tanh being odd, so the two halves of a line are one construction.

Those lines are what makes the disc a geodesic space: through any two prescribed points there passes one of them.

Main declarations

• TauCeti.hyperbolicDist_mul_ofReal_of_norm_eq_one — the hyperbolic distance along a Euclidean diameter, in terms of Real.artanh of the signed radii.
• TauCeti.PoincareDisc.radialGeodesic — the unit-speed geodesic line through the origin in direction u : Circle, namely t ↦ u * Real.tanh t, together with TauCeti.PoincareDisc.isometry_radialGeodesic saying it is an isometric embedding of ℝ.
• TauCeti.PoincareDisc.exists_radialGeodesic_eq — every point of the disc is reached by the radial geodesic in its own direction, at time its distance to the origin.
• TauCeti.PoincareDisc.geodesicLine — the same line based at an arbitrary point a instead of the origin, with TauCeti.PoincareDisc.isometry_geodesicLine, TauCeti.PoincareDisc.geodesicLine_zero, TauCeti.PoincareDisc.coe_geodesicLine (its value in the ambient plane) and TauCeti.PoincareDisc.geodesicLine_injective.
• TauCeti.PoincareDisc.radialGeodesic_neg, TauCeti.PoincareDisc.geodesicLine_neg — reversing the direction of a geodesic line reverses its time parameter.
• TauCeti.PoincareDisc.exists_isometry_apply_zero_apply_dist — the Poincaré disc is a geodesic space: through any two points there is a unit-speed geodesic line γ : ℝ → 𝔻, with γ 0 the first point and γ (dist z w) the second.
• TauCeti.PoincareDisc.exists_dist_eq_of_mem_Icc, TauCeti.PoincareDisc.exists_dist_eq_half_dist — the consequences usually packaged as Menger convexity: every intermediate distance, and in particular a midpoint, is realised.
• TauCeti.hyperbolicDist_zero_add_hyperbolicDist_ofReal_mul — the Euclidean radius from the origin to a disc point is a hyperbolic geodesic segment: the hyperbolic distance adds along it.

This advances the conformal-mapping roadmap's L2 target "the hyperbolic / Poincaré metric on 𝔻" (see ConformalMapping/README.md), which the preceding files carried as far as the metric-space instance and its topology; being geodesic is a further basic property of that metric, the one that makes hyperbolic lines and segments available in this model. (It is not by itself a characterisation of the hyperbolic plane: many unrelated metric spaces are geodesic.) It reuses Tau Ceti's pseudo-hyperbolic, hyperbolic-distance and disc-automorphism 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, whose preceding human-curated work in Analysis/Complex/RiemannMapping.lean and Analysis/Complex/BranchLogRoot.lean this file duplicates nothing of; should a human-curated Poincaré-disc metric land upstream, this material should be refactored onto it. Mathlib has the hyperbolic metric on the upper half-plane (Analysis/Complex/UpperHalfPlane), but no Poincaré metric on the disc and no geodesics for it.

The hyperbolic distance along a Euclidean diameter

theorem TauCeti.pseudoHyperbolicExpr_mul_ofReal_of_norm_eq_one {u : ℂ} (hu : ‖u‖ = 1) (a b : ℝ) : pseudoHyperbolicExpr (u * ↑a) (u * ↑b) = |a - b| / |1 - a * b|

The pseudo-hyperbolic expression of two points u * a, u * b of the same real line through the origin (‖u‖ = 1, a and b real) is |a - b| / |1 - a * b|: the rotation by u is invisible (TauCeti.pseudoHyperbolicExpr_const_mul), and on the real axis the Moebius denominator is the real number 1 - a * b.

Like TauCeti.pseudoHyperbolicExpr itself this is a total algebraic identity, needing no disc-membership hypothesis on a and b. For points of the disc the denominator is positive, so |1 - a * b| may be read as 1 - a * b.

theorem TauCeti.hyperbolicDist_mul_ofReal_of_norm_eq_one {u : ℂ} (hu : ‖u‖ = 1) {a b : ℝ} (ha : |a| < 1) (hb : |b| < 1) : hyperbolicDist (u * ↑a) (u * ↑b) = |Real.artanh a - Real.artanh b|

The hyperbolic distance along a Euclidean diameter. For ‖u‖ = 1 and real a, b of absolute value less than one, the hyperbolic distance between the disc points u * a and u * b is |artanh a - artanh b|: the map a ↦ u * a sends Real.artanh-arclength on (-1, 1) to hyperbolic distance.

theorem TauCeti.hyperbolicDist_mul_tanh_of_norm_eq_one {u : ℂ} (hu : ‖u‖ = 1) (s t : ℝ) : hyperbolicDist (u * ↑(Real.tanh s)) (u * ↑(Real.tanh t)) = |s - t|

Reparametrising a Euclidean diameter by Real.tanh makes it unit speed: the hyperbolic distance between u * Real.tanh s and u * Real.tanh t is |s - t|.

Geodesic lines through the origin

noncomputable def TauCeti.PoincareDisc.radialGeodesic (u : Circle) (t : ℝ) : PoincareDisc

The unit-speed geodesic line of the Poincaré disc through the origin in the direction u : Circle, that is, the Euclidean diameter in direction u parametrised by hyperbolic arclength: radialGeodesic u t is the disc point u * Real.tanh t.

Equations

• TauCeti.PoincareDisc.radialGeodesic u t = Complex.UnitDisc.toPoincare (u • Complex.UnitDisc.mk ↑(Real.tanh t) ⋯)

@[simp]

theorem TauCeti.PoincareDisc.coe_radialGeodesic (u : Circle) (t : ℝ) : ↑(toUnitDisc (radialGeodesic u t)) = ↑u * ↑(Real.tanh t)

The point radialGeodesic u t of the Poincaré disc is the complex number u * Real.tanh t.

@[simp]

theorem TauCeti.PoincareDisc.radialGeodesic_neg (u : Circle) (t : ℝ) : radialGeodesic (-u) t = radialGeodesic u (-t)

Reversing a radial geodesic. Negating the direction of a radial geodesic reverses its time parameter, Real.tanh being odd. So the backward half of radialGeodesic u is the forward half of radialGeodesic (-u).

@[simp]

theorem TauCeti.PoincareDisc.radialGeodesic_zero (u : Circle) : radialGeodesic u 0 = Complex.UnitDisc.toPoincare 0

Every radial geodesic starts at the origin.

theorem TauCeti.PoincareDisc.isometry_radialGeodesic (u : Circle) : Isometry (radialGeodesic u)

The radial geodesics are unit-speed geodesic lines: t ↦ u * Real.tanh t is an isometric embedding of the real line into the Poincaré disc.

theorem TauCeti.PoincareDisc.dist_radialGeodesic_zero (u : Circle) (t : ℝ) : dist (radialGeodesic u t) (Complex.UnitDisc.toPoincare 0) = |t|

The radial geodesic in direction u is at hyperbolic distance |t| from the origin at time t.

Not a simp lemma: dist_eq and coe_radialGeodesic already rewrite its left-hand side to a hyperbolicDist of complex numbers.

theorem TauCeti.PoincareDisc.radialGeodesic_injective : Function.Injective radialGeodesic

Distinct directions give distinct radial geodesics.

theorem TauCeti.PoincareDisc.exists_radialGeodesic_eq (z : PoincareDisc) : ∃ (u : Circle), radialGeodesic u (dist z (Complex.UnitDisc.toPoincare 0)) = z

Every point of the Poincaré disc lies on a geodesic through the origin, namely the Euclidean diameter through it, and it is reached at time its distance to the origin.

Geodesic lines through an arbitrary point

noncomputable def TauCeti.PoincareDisc.geodesicLine (a : PoincareDisc) (u : Circle) (t : ℝ) : PoincareDisc

The unit-speed geodesic line of the Poincaré disc through a in the direction u : Circle: the radial geodesic TauCeti.PoincareDisc.radialGeodesic u carried back to a by (unitDiscMoebiusIsometryEquiv (toUnitDisc a)).symm, the inverse of the Moebius isometry that sends a to the origin. Based at the origin it is radialGeodesic u itself (TauCeti.PoincareDisc.geodesicLine_toPoincare_zero).

Equations

• a.geodesicLine u t = (TauCeti.PoincareDisc.unitDiscMoebiusIsometryEquiv (TauCeti.PoincareDisc.toUnitDisc a)).symm (TauCeti.PoincareDisc.radialGeodesic u t)

theorem TauCeti.PoincareDisc.geodesicLine_def (a : PoincareDisc) (u : Circle) (t : ℝ) : a.geodesicLine u t = (unitDiscMoebiusIsometryEquiv (toUnitDisc a)).symm (radialGeodesic u t)

The defining formula for TauCeti.PoincareDisc.geodesicLine; its body is not @[expose]d, so this is how the definition is unfolded downstream.

theorem TauCeti.PoincareDisc.unitDiscMoebiusIsometryEquiv_geodesicLine (a : PoincareDisc) (u : Circle) (t : ℝ) : (unitDiscMoebiusIsometryEquiv (toUnitDisc a)) (a.geodesicLine u t) = radialGeodesic u t

The Moebius isometry that sends a to the origin straightens the geodesic line through a into the radial geodesic in the same direction. This is TauCeti.PoincareDisc.geodesicLine_def read forwards, and it is how a statement about geodesicLine is transported to the origin.

Not a simp lemma: unitDiscMoebiusIsometryEquiv_apply is itself simp, so the left-hand side here is not in simp-normal form — it rewrites to Complex.UnitDisc.toPoincare (unitDiscMoebius (toUnitDisc a) (toUnitDisc (geodesicLine a u t))), which the simpNF linter rejects.

@[simp]

theorem TauCeti.PoincareDisc.coe_geodesicLine (a : PoincareDisc) (u : Circle) (t : ℝ) : ↑(toUnitDisc (a.geodesicLine u t)) = (↑u * ↑(Real.tanh t) + ↑(toUnitDisc a)) / (1 + (starRingEnd ℂ) ↑(toUnitDisc a) * (↑u * ↑(Real.tanh t)))

The geodesic line through a in direction u, read in the ambient plane: it is the Moebius formula centred at -a evaluated at the radial point u * Real.tanh t. This is the base-point version of TauCeti.PoincareDisc.coe_radialGeodesic, and it is how geodesicLine is computed with on the underlying complex numbers.

@[simp]

theorem TauCeti.PoincareDisc.geodesicLine_neg (a : PoincareDisc) (u : Circle) (t : ℝ) : a.geodesicLine (-u) t = a.geodesicLine u (-t)

Reversing a geodesic line. The base-point version of TauCeti.PoincareDisc.radialGeodesic_neg: the line through a in direction -u is the line through a in direction u run backwards.

@[simp]

theorem TauCeti.PoincareDisc.geodesicLine_zero (a : PoincareDisc) (u : Circle) : a.geodesicLine u 0 = a

Every geodesic line through a starts at a: the generalisation of TauCeti.PoincareDisc.radialGeodesic_zero off the origin.

@[simp]

theorem TauCeti.PoincareDisc.geodesicLine_toPoincare_zero (u : Circle) : (Complex.UnitDisc.toPoincare 0).geodesicLine u = radialGeodesic u

Based at the origin, the geodesic lines are exactly the radial ones: the Moebius isometry centred at the origin is the identity.

theorem TauCeti.PoincareDisc.isometry_geodesicLine (a : PoincareDisc) (u : Circle) : Isometry (a.geodesicLine u)

The geodesic lines are unit-speed geodesic lines: geodesicLine a u is an isometric embedding of the real line into the Poincaré disc, being TauCeti.PoincareDisc.radialGeodesic u composed with an isometry.

theorem TauCeti.PoincareDisc.dist_geodesicLine_self (a : PoincareDisc) (u : Circle) (t : ℝ) : dist (a.geodesicLine u t) a = |t|

The geodesic line through a is at hyperbolic distance |t| from a at time t: the generalisation of TauCeti.PoincareDisc.dist_radialGeodesic_zero off the origin.

theorem TauCeti.PoincareDisc.geodesicLine_injective (a : PoincareDisc) : Function.Injective a.geodesicLine

Distinct directions give distinct geodesic lines through a common point: the generalisation of TauCeti.PoincareDisc.radialGeodesic_injective off the origin.

The Poincaré disc is a geodesic space

theorem TauCeti.PoincareDisc.exists_isometry_apply_zero_apply_dist (z w : PoincareDisc) : ∃ (γ : ℝ → PoincareDisc), Isometry γ ∧ γ 0 = z ∧ γ (dist z w) = w

The Poincaré disc is a geodesic metric space. Through any two of its points there is a unit-speed geodesic line γ : ℝ → PoincareDisc — an isometric embedding of the whole real line — that starts at z at time 0 and passes through w at time dist z w.

The line is TauCeti.PoincareDisc.geodesicLine z u, for u the direction in which the Moebius isometry sending z to the origin sees w (TauCeti.PoincareDisc.exists_radialGeodesic_eq).

theorem TauCeti.PoincareDisc.exists_dist_eq_of_mem_Icc (z w : PoincareDisc) {r : ℝ} (hr : r ∈ Set.Icc 0 (dist z w)) : ∃ (m : PoincareDisc), dist z m = r ∧ dist m w = dist z w - r

Every intermediate distance along a geodesic is realised: for 0 ≤ r ≤ dist z w there is a point at hyperbolic distance r from z and dist z w - r from w.

theorem TauCeti.PoincareDisc.exists_dist_eq_half_dist (z w : PoincareDisc) : ∃ (m : PoincareDisc), dist z m = dist z w / 2 ∧ dist m w = dist z w / 2

Midpoints exist in the Poincaré disc: any two points have a point halfway between them for the hyperbolic distance.

theorem TauCeti.hyperbolicDist_zero_add_hyperbolicDist_ofReal_mul {z : ℂ} (hz : ‖z‖ < 1) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : hyperbolicDist 0 (↑t * z) + hyperbolicDist (↑t * z) z = hyperbolicDist 0 z

The Euclidean radius is a hyperbolic geodesic segment. For z in the open unit disc and t ∈ [0, 1], the point t * z of the Euclidean segment from the origin to z splits the hyperbolic distance additively. Together with TauCeti.PoincareDisc.exists_radialGeodesic_eq this exhibits each Euclidean diameter as a hyperbolic geodesic through the origin, and every point of the disc as lying on one of them.