Strict side inequalities for convex hyperbolic polygons

Distinct sides of a convex polygon have distinct supporting geodesic lines. Every point on a side other than its finite endpoints lies strictly to the left of all the other supporting lines. This identifies regular edge points by strict inequalities and permits local tessellation arguments without assuming those inequalities separately. The results include ideal vertices: a side can be a segment, a ray, or a full line.

Main results

• ConvexPolygon.range_sideGeodesic_ne: distinct sides have distinct supporting lines.
• ConvexPolygon.mem_leftHalfPlane_of_mem_side: a nonendpoint side point satisfies every other side inequality strictly.

References

Walkden, Hyperbolic geometry (Manchester lecture notes, 2019), §14.2 (convex polygons as intersections of half-planes) and §§19–20 (local tessellation in Poincaré's theorem). Beardon, The Geometry of Discrete Groups, Chapter 9.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.range_sideGeodesic_ne {n : ℕ} [NeZero n] (P : ConvexPolygon n) {i j : Fin n} (hij : i ≠ j) : Set.range (geodesicLine (P.sideGeodesic i)) ≠ Set.range (geodesicLine (P.sideGeodesic j))

Distinct sides of a convex polygon have distinct supporting geodesic lines, including when one or both sides have ideal endpoints.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.mem_leftHalfPlane_of_mem_side {n : ℕ} [NeZero n] (P : ConvexPolygon n) {i j : Fin n} {z : UpperHalfPlane} (hz : z ∈ P.side i) (hzp : P.vertex i ≠ Sum.inl z) (hzq : P.vertex (i + 1) ≠ Sum.inl z) (hji : j ≠ i) : z ∈ leftHalfPlane (P.sideGeodesic j)

A point of a side other than its finite endpoints lies strictly to the left of every other side's supporting geodesic.