Hyperbolic perpendicular bisectors and distance dominance

For two points p and q of the upper half-plane, the points equidistant from them in the hyperbolic metric are cut out by the equation q.im * |z - p|² = p.im * |z - q|² in the plane. For distinct centres, the perpendicular bisector has zero invariant area. This is proved in TauCeti.Analysis.Complex.UpperHalfPlane.Bisector.Geometry by identifying the equidistant locus with a geodesic line.

Likewise, the points at least as close to p as to q (the distance-dominance, or Voronoi, region of p relative to q) are cut out by the weak inequality q.im * |z - p|² ≤ p.im * |z - q|² in the plane. This is the planar form of the defining inequalities of a Dirichlet domain.

These planar characterizations describe the equality and dominance regions that occur in Dirichlet domains.

Main results

• TauCeti.UpperHalfPlane.dist_eq_dist_iff: the planar equation of the hyperbolic perpendicular bisector.
• TauCeti.UpperHalfPlane.dist_le_dist_iff: the planar inequality for the region of points at least as close to p as to q.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §9.4.
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §3.2.

theorem TauCeti.UpperHalfPlane.dist_eq_dist_iff {z p q : UpperHalfPlane} : dist z p = dist z q ↔ q.im * dist ↑z ↑p ^ 2 = p.im * dist ↑z ↑q ^ 2

A point is hyperbolically equidistant from p and q exactly when q.im * |z - p|² = p.im * |z - q|² in the plane.

theorem TauCeti.UpperHalfPlane.dist_le_dist_iff {z p q : UpperHalfPlane} : dist z p ≤ dist z q ↔ q.im * dist ↑z ↑p ^ 2 ≤ p.im * dist ↑z ↑q ^ 2

A point is hyperbolically at least as close to p as to q exactly when q.im * |z - p|² ≤ p.im * |z - q|² in the plane. This is the planar form of a defining inequality of a Dirichlet domain; compare Beardon, §9.4, and Katok, §3.2.