The infinitesimal density of the Poincaré metric #
Hyperbolic/Distance.lean defines the hyperbolic (Poincaré) distance on the complex open unit
disc in closed form, hyperbolicDist z w = Real.artanh (pseudoHyperbolicExpr z w), and its
docstring asserts that this normalisation "agrees with the infinitesimal Poincaré metric
|dz| / (1 - |z| ^ 2)". Nothing in the disc files proved that assertion: the closed form and
the conformal density were never connected. This file connects them, in the two ways the
statement is normally read.
Differentially. Along any approach to a point z of the disc, the ratio of hyperbolic to
Euclidean distance tends to (1 - ‖z‖ ^ 2)⁻¹
(TauCeti.tendsto_hyperbolicDist_div_norm_sub). The proof factors the ratio as
hyperbolicDist z w / ‖w - z‖ = (artanh p / p) * ‖1 - conj w * z‖⁻¹
for p = pseudoHyperbolicExpr z w, which is legitimate off the diagonal because p is
exactly ‖w - z‖ / ‖1 - conj w * z‖. As
w → z the first factor tends to 1 — this is Real.tendsto_artanh_div_nhdsNE_zero,
the derivative of Real.artanh at the origin read as a limit of slopes — while the Moebius
denominator tends to 1 - ‖z‖ ^ 2, which is where the density comes from.
Integrally. The hyperbolic distance from the origin along a radius is the integral of the
density over that radius, ∫ t in (0)..r, (1 - t ^ 2)⁻¹ = hyperbolicDist 0 (r * u) for a unit
vector u (TauCeti.integral_one_sub_sq_inv_eq_hyperbolicDist_zero): the hyperbolic distance
to a point is the length, in the density, of the radius joining it to the origin — and
Poincare/Geodesic.lean shows those radii to be the geodesics through the origin. Only radii
are treated here. Neither the density-weighted length of a general curve nor the infimum of
such lengths between two arbitrary points is defined anywhere in the tree, so nothing below
identifies hyperbolicDist as the length metric induced by the density; that identification
would need those definitions first.
Bounding the density between its values at the endpoints of a radius also gives the two-sided
comparison of the hyperbolic distance with the pseudo-hyperbolic expression,
p ≤ hyperbolicDist ≤ p / (1 - p ^ 2); the lower bound sharpens the crude Euclidean estimate
‖z - w‖ ≤ 2 * p of Poincare/Topology.lean into ‖z - w‖ / ‖1 - conj w * z‖ ≤ hyperbolicDist.
Main declarations #
TauCeti.pseudoHyperbolicExpr_le_hyperbolicDistandTauCeti.hyperbolicDist_le_pseudoHyperbolicExpr_div_one_sub_sq— the two-sided comparison of the hyperbolic distance with the pseudo-hyperbolic expression.TauCeti.tendsto_hyperbolicDist_div_norm_sub— the infinitesimal Poincaré density(1 - ‖z‖ ^ 2)⁻¹at a pointzof the disc.TauCeti.tendsto_hyperbolicDist_zero_div_norm— the density at the origin is1, so the hyperbolic and Euclidean metrics are infinitesimally equal there.TauCeti.integral_one_sub_sq_inv_eq_hyperbolicDist_zero— the radial form of the density.
This carries the conformal-mapping roadmap's L2 target "the hyperbolic / Poincaré metric on
𝔻" (see ConformalMapping/README.md) onto its infinitesimal side, and reuses Tau Ceti's
pseudo-hyperbolic and hyperbolic-distance API throughout. 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's preceding human-curated work in
Analysis/Complex/RiemannMapping.lean and Analysis/Complex/BranchLogRoot.lean is neither
duplicated nor extended here. Mathlib has the hyperbolic metric on the upper half-plane
(Analysis/Complex/UpperHalfPlane/Metric.lean), but records no density statement for it
either.
Comparison with the pseudo-hyperbolic expression #
The hyperbolic distance dominates the pseudo-hyperbolic expression: Real.artanh moves
[0, 1) upwards because the Poincaré density is at least 1.
All that is needed is that the pseudo-hyperbolic expression lies below 1; for two points of
the open unit disc that is TauCeti.pseudoHyperbolicExpr_lt_one_of_norm_lt_one.
The hyperbolic distance is bounded above by p / (1 - p ^ 2), where p is the
pseudo-hyperbolic expression: the Poincaré density on [0, p] is at most its value at p.
As for the lower bound, only p < 1 is needed, which holds for two points of the open unit
disc by TauCeti.pseudoHyperbolicExpr_lt_one_of_norm_lt_one.
The Euclidean distance divided by the Moebius denominator is a lower bound for the
hyperbolic distance, sharpening the crude estimate ‖z - w‖ ≤ 2 * pseudoHyperbolicExpr z w.
The infinitesimal density #
The infinitesimal Poincaré density. At a point z of the open unit disc the ratio of
the hyperbolic distance to the Euclidean distance tends to (1 - ‖z‖ ^ 2)⁻¹.
This is the precise sense in which TauCeti.hyperbolicDist has infinitesimal density
|dz| / (1 - |z| ^ 2): the closed form Real.artanh of the pseudo-hyperbolic expression is
only a reparametrisation, and the density it produces at z is read off from the Moebius
denominator 1 - conj z * z. It is a statement about the first order behaviour at z alone;
calling hyperbolicDist the distance induced by that density would need the density-weighted
length of a curve, which is defined nowhere in the tree (see the module docstring).
The Poincaré density at the origin is 1. The hyperbolic and Euclidean metrics of the
disc agree to first order at the centre.
The radial form of the density #
The hyperbolic distance along a radius is the integral of the density. For a unit
vector u and a radius r in [0, 1), the hyperbolic distance from the origin to r * u is
∫ t in (0)..r, (1 - t ^ 2)⁻¹.
This is the radial case of the agreement between TauCeti.hyperbolicDist and the density
|dz| / (1 - |z| ^ 2), and only that case: the radii through the origin are geodesics of the
Poincaré disc (TauCeti.PoincareDisc.isometry_radialGeodesic), but the density-weighted length
of a general curve is not defined here, so this does not identify hyperbolicDist with the
length metric of the density between arbitrary points.