Finite Dirichlet constraints near a cusp

For any Dirichlet centre and any normalized cusp datum of a discrete Fuchsian group, finitely many distance inequalities describe the Dirichlet domain on a sufficiently high horodisc. The centre need not lie in that horodisc, and the intersection is allowed to be empty. This controls the unbounded cusp ends when assembling a finite-sided Dirichlet polygon.

The two constraints from the positive cusp generator and its inverse restrict the horizontal coordinate to a strip of width equal to the cusp width. Low orbit points cannot compete high in this strip. The remaining orbit points have uniformly bounded height by Shimizu's lemma; translation by the cusp stabilizer reduces them to a compact rectangle, which meets the orbit in only finitely many acting elements.

The same comparison controls the translates of a high horodisc at the cusp. If g • y, with y high above the cusp, lies in the Dirichlet domain of p, then g⁻¹ • p cannot be much lower than p above the cusp, so g lies in finitely many cosets of the cusp stabilizer. Hence a Dirichlet domain meets only finitely many translates of a high horodisc, and its part in all translates of a lower horodisc consists of those finitely many horodiscs together with a bounded set. Combined with the description of the thin part of a cusp stabilizer as a horodisc (TauCeti.Subgroup.CuspDatum.mem_horodisc_iff_exists_dist_smul_lt), this confines the points of a Dirichlet domain moved a short distance by a parabolic element fixing a cusp Γ-equivalent to that of the datum to finitely many horodiscs and a bounded set.

Main results

In the following, all names are in the namespace TauCeti.Subgroup.

• CuspDatum.exists_finset_dirichletDomain_inter_horodisc_eq: finitely many distance constraints describe the Dirichlet domain on a high horodisc.
• CuspDatum.exists_finset_dirichletDomain_inter_iUnion_smul_horodisc_subset: only finitely many translates of a high horodisc meet a Dirichlet domain.
• CuspDatum.exists_finset_isBounded_dirichletDomain_inter_iUnion_smul_horodisc_diff: away from finitely many high horodiscs, the part of a Dirichlet domain in the translates of any horodisc is bounded.
• CuspDatum.exists_finset_isBounded_dirichletDomain_inter_setOf_dist_smul_lt_diff: away from finitely many high horodiscs, the points of a Dirichlet domain moved a short distance by a parabolic element fixing a cusp equivalent to that of the datum form a bounded set.

References

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

We use the orbit-height bound TauCeti.Subgroup.CuspDatum.exists_isOpen_mem_forall_im_scaling_smul_smul_le, the hyperbolic cosine distance formula, and Mathlib's proper-discontinuity finiteness theorem.

theorem TauCeti.Subgroup.CuspDatum.abs_re_scaling_smul_sub_le {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {p z : UpperHalfPlane} (hz : z ∈ dirichletDomain (↥Γ) p) : |(D.scaling • z).re - (D.scaling • p).re| ≤ D.width / 2

The scaled image of the Dirichlet domain lies in the vertical strip of width D.width centred at (D.scaling • p).re.

theorem TauCeti.Subgroup.CuspDatum.isBounded_dirichletDomain_inter_horodisc_diff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (p : UpperHalfPlane) {A : ℝ} (hA : 0 < A) (B : ℝ) : Bornology.IsBounded ((dirichletDomain (↥Γ) p ∩ horodisc D A) \ horodisc D B)

The part of a Dirichlet domain between two cusp heights is bounded, provided the lower height is positive. The upper height is arbitrary, and the band may be empty.

theorem TauCeti.Subgroup.CuspDatum.isBounded_dirichletDomain_inter_iUnion_smul_horodisc_diff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (p : UpperHalfPlane) {A : ℝ} (hA : 0 < A) (B : ℝ) : Bornology.IsBounded (dirichletDomain (↥Γ) p ∩ ⋃ (g : ↥Γ), g • (horodisc D A \ horodisc D B))

The points of a Dirichlet domain lying in some Γ-translate of the band between two cusp heights form a bounded set, provided the lower height is positive.

theorem TauCeti.Subgroup.CuspDatum.exists_finset_dirichletDomain_inter_horodisc_eq {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) [DiscreteTopology ↥Γ] (p : UpperHalfPlane) : ∃ (s : Finset ↥Γ), ∀ (A : ℝ), (D.scaling • p).im + D.width / 2 ≤ A → dirichletDomain (↥Γ) p ∩ horodisc D A = (⋂ g ∈ s, {z : UpperHalfPlane | dist z p ≤ dist z (g • p)}) ∩ horodisc D A

A single finite family of distance constraints defines the Dirichlet domain on every horodisc of height at least (D.scaling • p).im + D.width / 2. This holds for every centre, without cofiniteness or a trivial-centre-stabilizer assumption.

theorem TauCeti.Subgroup.CuspDatum.exists_finset_dirichletDomain_inter_iUnion_smul_horodisc_subset {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) [DiscreteTopology ↥Γ] (p : UpperHalfPlane) : ∃ (s : Finset ↥Γ), ∀ (A : ℝ), (D.scaling • p).im + D.width / 2 ≤ A → dirichletDomain (↥Γ) p ∩ ⋃ (g : ↥Γ), g • horodisc D A ⊆ ⋃ g ∈ s, g • horodisc D A

Finitely many translates of a high horodisc meet a Dirichlet domain. For a discrete Γ, a cusp datum D and any centre p, there is a finite set s ⊆ Γ such that, at every height A ≥ (D.scaling • p).im + D.width / 2, every point of the Dirichlet domain lying in some Γ-translate of the horodisc of height A already lies in a translate by an element of s.

theorem TauCeti.Subgroup.CuspDatum.exists_finset_isBounded_dirichletDomain_inter_iUnion_smul_horodisc_diff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) [DiscreteTopology ↥Γ] (p : UpperHalfPlane) : ∃ (s : Finset ↥Γ), ∀ (A : ℝ), (D.scaling • p).im + D.width / 2 ≤ A → ∀ (B : ℝ), 0 < B → Bornology.IsBounded ((dirichletDomain (↥Γ) p ∩ ⋃ (g : ↥Γ), g • horodisc D B) \ ⋃ g ∈ s, g • horodisc D A)

The cusp ends of a Dirichlet domain. For a discrete Γ, a cusp datum D and any centre p, there is a finite set s ⊆ Γ such that, at every height A ≥ (D.scaling • p).im + D.width / 2 and every positive height B, the points of the Dirichlet domain lying in a Γ-translate of the horodisc of height B lie in the translates of the horodisc of height A by elements of s, apart from a bounded set.

By TauCeti.Subgroup.CuspDatum.horodisc_conj, each translate g • horodisc D A is the horodisc of height A of the conjugate cusp datum at g • D.cusp.

theorem TauCeti.Subgroup.CuspDatum.exists_finset_isBounded_dirichletDomain_inter_setOf_dist_smul_lt_diff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) [DiscreteTopology ↥Γ] (p : UpperHalfPlane) {ε : ℝ} (hε : 0 < ε) : ∃ (s : Finset ↥Γ), ∀ (A : ℝ), (D.scaling • p).im + D.width / 2 ≤ A → Bornology.IsBounded ((dirichletDomain (↥Γ) p ∩ {x : UpperHalfPlane | ∃ (γ : ↥Γ), ∃ g ∈ MulAction.stabilizer (↥Γ) (γ • D.cusp), g ≠ 1 ∧ dist (g • x) x < ε}) \ ⋃ g ∈ s, g • horodisc D A)

The parabolic thin part of a Dirichlet domain. For a discrete Γ, a cusp datum D, any centre p and ε > 0, there is a finite set s ⊆ Γ such that, at every height A ≥ (D.scaling • p).im + D.width / 2, the points of the Dirichlet domain moved less than ε by a nonidentity element of Γ fixing a cusp Γ-equivalent to that of D lie in the translates of the horodisc of height A by elements of s, apart from a bounded set.