Perpendicular bisectors and distance half-planes

For distinct p q : ℍ, perpBisector p q represents the oriented geodesic bisecting the segment from p to q. Its open left half-plane consists of the points closer to p, its closed left half-plane consists of the points at least as close to p, and its line consists of the points equidistant from the two centres. In particular, distance dominance regions are geodesically convex, the geometric ingredient in convexity of Dirichlet domains. The equidistant locus has zero invariant area (volume_setOf_dist_eq_dist), as every geodesic line does.

The construction moves the segment onto the imaginary axis, dilates to its midpoint, and rotates by π / 4 in SL(2, ℝ), which rotates the tangent by π / 2.

References

• Alan Beardon, The Geometry of Discrete Groups, §9.4.
• Svetlana Katok, Fuchsian Groups, §3.2.

noncomputable def TauCeti.UpperHalfPlane.perpBisector (p q : UpperHalfPlane) : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

The oriented perpendicular bisector of p and q, represented as a projective isometry. For distinct centres its left half-plane contains p. At coincident centres this is an arbitrary line through that point, not the equidistant locus.

Equations

• TauCeti.UpperHalfPlane.perpBisector p q = TauCeti.UpperHalfPlane.geodesicBetween p q * ↑(Matrix.SpecialLinearGroup.dilation (dist p q / 2)) * ↑(Matrix.SpecialLinearGroup.rotation (Real.pi / 4))

theorem TauCeti.UpperHalfPlane.perpBisector_def (p q : UpperHalfPlane) : perpBisector p q = geodesicBetween p q * ↑(Matrix.SpecialLinearGroup.dilation (dist p q / 2)) * ↑(Matrix.SpecialLinearGroup.rotation (Real.pi / 4))

The perpendicular bisector is obtained by moving to the midpoint of the oriented segment and rotating its tangent through a right angle.

theorem TauCeti.UpperHalfPlane.mem_leftHalfPlane_perpBisector_iff {p q : UpperHalfPlane} (hpq : p ≠ q) (z : UpperHalfPlane) : z ∈ leftHalfPlane (perpBisector p q) ↔ dist z p < dist z q

The points closer to p than to q form the open left half-plane of their perpendicular bisector.

theorem TauCeti.UpperHalfPlane.mem_rightHalfPlane_perpBisector_iff {p q : UpperHalfPlane} (hpq : p ≠ q) (z : UpperHalfPlane) : z ∈ rightHalfPlane (perpBisector p q) ↔ dist z q < dist z p

The points closer to q than to p form the open right half-plane of their perpendicular bisector.

theorem TauCeti.UpperHalfPlane.mem_range_geodesicLine_perpBisector_iff {p q : UpperHalfPlane} (hpq : p ≠ q) (z : UpperHalfPlane) : z ∈ Set.range (geodesicLine (perpBisector p q)) ↔ dist z p = dist z q

The perpendicular bisector is exactly the hyperbolic equidistant locus.

theorem TauCeti.UpperHalfPlane.volume_setOf_dist_eq_dist {p q : UpperHalfPlane} (hpq : p ≠ q) : MeasureTheory.volume {z : UpperHalfPlane | dist z p = dist z q} = 0

Hyperbolic perpendicular bisectors are null. The points of ℍ equidistant from two distinct points have zero invariant area.

theorem TauCeti.UpperHalfPlane.mem_closure_leftHalfPlane_perpBisector_iff {p q : UpperHalfPlane} (hpq : p ≠ q) (z : UpperHalfPlane) : z ∈ closure (leftHalfPlane (perpBisector p q)) ↔ dist z p ≤ dist z q

The points at least as close to p as to q form a closed geodesic half-plane.

theorem TauCeti.UpperHalfPlane.mem_closure_rightHalfPlane_perpBisector_iff {p q : UpperHalfPlane} (hpq : p ≠ q) (z : UpperHalfPlane) : z ∈ closure (rightHalfPlane (perpBisector p q)) ↔ dist z q ≤ dist z p

The points at least as close to q as to p form the opposite closed half-plane.

theorem TauCeti.UpperHalfPlane.geodesicSegment_subset_setOf_dist_le_dist {p q z w : UpperHalfPlane} (hz : dist z p ≤ dist z q) (hw : dist w p ≤ dist w q) : z.geodesicSegment w ⊆ {u : UpperHalfPlane | dist u p ≤ dist u q}

A hyperbolic distance dominance region contains the geodesic segment joining any two of its points. No distinctness assumption on the centres is needed.