Local finiteness of cuspidal polygon translates

The translates of a convex hyperbolic polygon by a discrete subgroup of PSL(2, ℝ) are locally finite whenever every ideal vertex is a cusp of the group. No side pairing or coverage of the upper half-plane is required.

Normalized cusp data supply a uniform bound on the heights of all translates of a neighbourhood of any point, by CuspDatum.exists_isOpen_mem_forall_im_scaling_smul_smul_le. Truncating the polygon at these heights leaves a compact core, by ConvexPolygon.isCompact_carrier_diff_iUnion. Every tile meeting the chosen neighbourhood meets a translate of that core; proper discontinuity then gives local finiteness. This accounts for the noncompact cusp tails when constructing fundamental polygons.

References

• Alan Beardon, The Geometry of Discrete Groups, Chapter 9.
• Svetlana Katok, Fuchsian Groups, Chapters 3–4.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.locallyFinite_smul_carrier_of_isCuspPoint {n : ℕ} [NeZero n] (P : ConvexPolygon n) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (hcusp : ∀ (i : Fin n) (c : OnePoint ℝ), P.vertex i = Sum.inr c → Γ.IsCuspPoint c) : LocallyFinite fun (γ : ↥Γ) => ↑γ • P.carrier

A discrete group's translates of a convex hyperbolic polygon are locally finite if every ideal vertex is a cusp of the group. The polygon need not meet every orbit or admit side pairings.