Metric on the upper half-plane #
In this file we define a
MetricSpace structure on the
UpperHalfPlane. We use hyperbolic
(Poincaré) distance given by
dist z w = 2 * arsinh (dist (z : ℂ) w / (2 * Real.sqrt (z.im * w.im))) instead of the induced
Euclidean distance because the hyperbolic distance is invariant under holomorphic automorphisms of
the upper half-plane. However, we ensure that the projection to
definitionally equal to the induced topological space structure.
We also prove that a metric ball/closed ball/sphere in Poincaré metric is a Euclidean ball/closed ball/sphere with another center and radius.
For two points on the same vertical line, the distance is equal to the distance between the logarithms of their imaginary parts.
SL(2, ℝ) acts on the upper half plane as an isometry.