Closed forms for the hyperbolic distance on the unit disc

The hyperbolic (Poincaré) distance of Conformal/Hyperbolic/Distance.lean is defined as hyperbolicDist z w = Real.artanh (pseudoHyperbolicExpr z w), a reparametrisation of the pseudo-hyperbolic expression p = ‖(z - w) / (1 - conj w * z)‖. That definition is the one that makes the Schwarz--Pick contraction property and the triangle inequality easy, but it hides the quantity behind an inverse hyperbolic tangent. This file evaluates the elementary functions of hyperbolicDist in closed form, in terms of the three Euclidean quantities

• the numerator ‖z - w‖,
• the Moebius denominator ‖1 - conj w * z‖, and
• the product of hyperbolic defects (1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2).

Everything rests on the Poincaré defect identity ‖1 - conj w * z‖ ^ 2 - ‖z - w‖ ^ 2 = (1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2) (TauCeti.norm_sq_one_sub_conj_mul_sub_norm_sq_sub), which says exactly that 1 - p ^ 2 = (1 - ‖z‖ ^ 2) (1 - ‖w‖ ^ 2) / ‖1 - conj w * z‖ ^ 2. Feeding that into Mathlib's Real.sinh_artanh, Real.cosh_artanh and Real.artanh_eq_half_log turns the Moebius denominator into the common factor that the quotient p and the defect 1 - p ^ 2 share, and it cancels: what is left involves only ‖z - w‖, ‖1 - conj w * z‖ and the defect product.

Main results

• TauCeti.one_sub_pseudoHyperbolicExpr_sq and TauCeti.sqrt_one_sub_pseudoHyperbolicExpr_sq — the defect identity in the form the closed forms consume;
• TauCeti.sinh_hyperbolicDist, TauCeti.cosh_hyperbolicDist, TauCeti.tanh_hyperbolicDist, TauCeti.exp_hyperbolicDist — the four elementary functions of the hyperbolic distance;
• TauCeti.cosh_two_mul_hyperbolicDist — the double-angle form cosh (2 d) = 1 + 2 ‖z - w‖ ^ 2 / ((1 - ‖z‖ ^ 2)(1 - ‖w‖ ^ 2)), the identity usually quoted as the formula for the Poincaré distance;
• TauCeti.hyperbolicDist_eq_half_log and TauCeti.hyperbolicDist_zero_right_eq_half_log — the logarithmic form, in general and against the origin;
• TauCeti.hyperbolicDist_le_iff_le_sinh and TauCeti.hyperbolicDist_le_div_sqrt — the comparison with the Euclidean distance that the closed forms make available;
• TauCeti.exists_mem_ball_lt_hyperbolicDist — the disc has infinite hyperbolic diameter.

Normalisation

hyperbolicDist is normalised to the infinitesimal metric |dz| / (1 - |z| ^ 2), half the curvature -1 metric 2 |dz| / (1 - |z| ^ 2); this is the normalisation already fixed by Conformal/Hyperbolic/Distance.lean and used throughout Conformal/Poincare/. Under the Cayley transform it corresponds to half the distance that Mathlib's UpperHalfPlane.dist records on the upper half-plane, so the statements below are the disc analogues of Mathlib's UpperHalfPlane.sinh_half_dist, UpperHalfPlane.cosh_half_dist, UpperHalfPlane.tanh_half_dist, UpperHalfPlane.exp_half_dist and UpperHalfPlane.cosh_dist — the half-distance formulas there are the plain ones here. The Cayley transform itself is not used: the disc formulas are proved directly from the defect identity, which is shorter than transporting the half-plane ones and avoids the im-versus-defect bookkeeping.

This advances the conformal-mapping roadmap's L2 target "the hyperbolic / Poincaré metric on 𝔻" (see ConformalMapping/README.md), completing the basic API of hyperbolicDist with the closed forms that the geometric statements of Conformal/Poincare/ are usually quoted in. As with the rest of the L0--L3 conformal-mapping material it is coordinated with the upstream Mathlib RMT effort leanprover-community/mathlib4#33505, which contains no Poincaré metric on the disc: should a human-curated disc metric land in Mathlib, these formulas are to be refactored onto it.

theorem TauCeti.one_sub_pseudoHyperbolicExpr_sq {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : 1 - pseudoHyperbolicExpr z w ^ 2 = (1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2) / ‖1 - (starRingEnd ℂ) w * z‖ ^ 2

The defect identity, squared form. For two points of the open unit disc the deficiency 1 - p ^ 2 of the pseudo-hyperbolic expression p is the product of the two hyperbolic defects divided by the squared Moebius denominator.

theorem TauCeti.sqrt_one_sub_pseudoHyperbolicExpr_sq {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : √(1 - pseudoHyperbolicExpr z w ^ 2) = √((1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2)) / ‖1 - (starRingEnd ℂ) w * z‖

The defect identity, square-root form. The square root of 1 - p ^ 2 occurring in the closed forms of Real.sinh and Real.cosh at Real.artanh p.

theorem TauCeti.sinh_hyperbolicDist {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : Real.sinh (hyperbolicDist z w) = ‖z - w‖ / √((1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2))

The hyperbolic sine of the hyperbolic distance. The disc analogue of Mathlib's UpperHalfPlane.sinh_half_dist.

theorem TauCeti.cosh_hyperbolicDist {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : Real.cosh (hyperbolicDist z w) = ‖1 - (starRingEnd ℂ) w * z‖ / √((1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2))

The hyperbolic cosine of the hyperbolic distance. The disc analogue of Mathlib's UpperHalfPlane.cosh_half_dist.

theorem TauCeti.tanh_hyperbolicDist {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : Real.tanh (hyperbolicDist z w) = pseudoHyperbolicExpr z w

The hyperbolic tangent of the hyperbolic distance is the pseudo-hyperbolic expression: hyperbolicDist and pseudoHyperbolicExpr are two readings of the same geometry, the first unbounded and additive along geodesics, the second confined to [0, 1). The disc analogue of Mathlib's UpperHalfPlane.tanh_half_dist.

theorem TauCeti.exp_hyperbolicDist {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : Real.exp (hyperbolicDist z w) = (‖1 - (starRingEnd ℂ) w * z‖ + ‖z - w‖) / √((1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2))

The exponential of the hyperbolic distance. The disc analogue of Mathlib's UpperHalfPlane.exp_half_dist.

theorem TauCeti.cosh_two_mul_hyperbolicDist {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : Real.cosh (2 * hyperbolicDist z w) = 1 + 2 * ‖z - w‖ ^ 2 / ((1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2))

The double-angle closed form, the identity usually quoted as the formula for the Poincaré distance of the disc: cosh (2 d) = 1 + 2 ‖z - w‖ ^ 2 / ((1 - ‖z‖ ^ 2) (1 - ‖w‖ ^ 2)). Only Euclidean data appear on the right, and the Moebius denominator has disappeared. The disc analogue of Mathlib's UpperHalfPlane.cosh_dist (the factor 2 reflecting the normalisation: 2 * hyperbolicDist is the curvature -1 distance).

theorem TauCeti.hyperbolicDist_eq_half_log {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : hyperbolicDist z w = 1 / 2 * Real.log ((‖1 - (starRingEnd ℂ) w * z‖ + ‖z - w‖) / (‖1 - (starRingEnd ℂ) w * z‖ - ‖z - w‖))

The logarithmic closed form. Writing N = ‖z - w‖ for the numerator and D = ‖1 - conj w * z‖ for the Moebius denominator, the hyperbolic distance is (1 / 2) log ((D + N) / (D - N)); the denominator D - N is positive on the disc precisely because the defect identity makes D ^ 2 - N ^ 2 positive there.

theorem TauCeti.hyperbolicDist_zero_right_eq_half_log {z : ℂ} (hz : ‖z‖ < 1) : hyperbolicDist z 0 = 1 / 2 * Real.log ((1 + ‖z‖) / (1 - ‖z‖))

The logarithmic closed form against the origin, (1 / 2) log ((1 + ‖z‖) / (1 - ‖z‖)).

theorem TauCeti.sinh_hyperbolicDist_zero_right {z : ℂ} (hz : ‖z‖ < 1) : Real.sinh (hyperbolicDist z 0) = ‖z‖ / √(1 - ‖z‖ ^ 2)

The hyperbolic sine of the distance to the origin: the closed form sinh (hyperbolicDist z 0) = ‖z‖ / √(1 - ‖z‖ ^ 2).

theorem TauCeti.cosh_hyperbolicDist_zero_right {z : ℂ} (hz : ‖z‖ < 1) : Real.cosh (hyperbolicDist z 0) = 1 / √(1 - ‖z‖ ^ 2)

The hyperbolic cosine of the distance to the origin: the closed form cosh (hyperbolicDist z 0) = 1 / √(1 - ‖z‖ ^ 2).

theorem TauCeti.hyperbolicDist_le_iff_le_sinh {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) {r : ℝ} : hyperbolicDist z w ≤ r ↔ ‖z - w‖ ≤ Real.sinh r * √((1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2))

Hyperbolic balls in Euclidean terms. A bound on the hyperbolic distance is a bound on the Euclidean distance weighted by the hyperbolic defects. The disc analogue of Mathlib's UpperHalfPlane.dist_le_iff_le_sinh.

theorem TauCeti.hyperbolicDist_le_div_sqrt {z w : ℂ} (hz : ‖z‖ < 1) (hw : ‖w‖ < 1) : hyperbolicDist z w ≤ ‖z - w‖ / √((1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2))

The hyperbolic distance is at most the weighted Euclidean one. The disc analogue of Mathlib's UpperHalfPlane.dist_le_dist_coe_div_sqrt; in particular the hyperbolic distance of two points is small when they are Euclidean-close and both stay in a fixed smaller disc.

theorem TauCeti.exists_mem_ball_lt_hyperbolicDist (C : ℝ) : ∃ z ∈ Metric.ball 0 1, C < hyperbolicDist z 0

The unit disc has infinite hyperbolic diameter: no real number bounds the hyperbolic distance to the origin. The witnesses are supplied by hyperbolicDist_zero_right: for 0 ≤ t the point of Euclidean norm Real.tanh t lies in the disc and is at hyperbolic distance exactly t from the origin. So the Euclidean boundary is infinitely far away in the Poincaré metric.