The thick part of a Dirichlet domain

Let a group G act by isometries on a metric space X, and recall that the ε-thick part TauCeti.thickPart G ε is the set of points moved a distance at least ε by every nonidentity element of G. Suppose that G is countable and preserves a measure μ for which it has a fundamental domain of finite measure, and that the balls of radius ε / 2 have measure bounded below by a positive constant. Then the ε-thick part of every Dirichlet domain is bounded (TauCeti.isBounded_dirichletDomain_inter_thickPart). Indeed, a point of a Dirichlet domain is a point of its orbit closest to the centre, so if thick points x and y of the domain have distances from the centre differing by at least ε, then g • x and y are at distance at least ε for every g. Infinitely many such points would give infinitely many balls of radius ε / 2 whose translates are pairwise disjoint, and the measure of their union would be infinite yet at most the measure of a fundamental domain.

For a properly discontinuous action on a proper space every orbit meets the Dirichlet domain, so the image of the thick part in the orbit space is then compact (TauCeti.isCompact_image_thickPart). For a Fuchsian group of finite covolume this is the compactness of the thick part of the quotient surface, the starting point of its thick-thin decomposition.

Main declarations

• TauCeti.isBounded_dirichletDomain_inter_thickPart: for a lattice, the thick part of a Dirichlet domain is bounded.
• TauCeti.isCompact_image_thickPart: for a lattice acting properly discontinuously on a proper space, the thick part of the orbit space is compact.

References

• Riccardo Benedetti and Carlo Petronio, Lectures on Hyperbolic Geometry, Universitext, Springer, 1992, Chapter D (the thick part of a finite-volume hyperbolic manifold).
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §§3.2 and 4.1 (Dirichlet regions of groups of finite covolume).

theorem TauCeti.isBounded_dirichletDomain_inter_thickPart {G : Type u_1} {X : Type u_2} [Group G] [PseudoMetricSpace X] [MulAction G X] [IsIsometricSMul G X] [MeasurableSpace X] [OpensMeasurableSpace X] [Countable G] [MeasurableConstSMul G X] {μ : MeasureTheory.Measure X} [MeasureTheory.SMulInvariantMeasure G X μ] {s : Set X} (hs : MeasureTheory.IsFundamentalDomain G s μ) (hμs : μ s ≠ ⊤) {ε : ℝ} {c : ENNReal} (hc : c ≠ 0) (hball : ∀ (x : X), c ≤ μ (Metric.ball x (ε / 2))) (p : X) : Bornology.IsBounded (dirichletDomain G p ∩ thickPart G ε)

The thick part of a Dirichlet domain of a lattice is bounded. Let G act isometrically on X, preserving a measure μ with a fundamental domain s of finite measure. If the balls of radius ε / 2 have measure at least c ≠ 0, then the points of a Dirichlet domain moved at least ε by every nonidentity element form a bounded set.

theorem TauCeti.isCompact_image_thickPart {G : Type u_1} {X : Type u_2} [Group G] [PseudoMetricSpace X] [MulAction G X] [IsIsometricSMul G X] [MeasurableSpace X] [OpensMeasurableSpace X] [Countable G] [MeasurableConstSMul G X] {μ : MeasureTheory.Measure X} [MeasureTheory.SMulInvariantMeasure G X μ] {s : Set X} [ProperSpace X] [ProperlyDiscontinuousSMul G X] (hs : MeasureTheory.IsFundamentalDomain G s μ) (hμs : μ s ≠ ⊤) {ε : ℝ} {c : ENNReal} (hc : c ≠ 0) (hball : ∀ (x : X), c ≤ μ (Metric.ball x (ε / 2))) : IsCompact (Quotient.mk (MulAction.orbitRel G X) '' thickPart G ε)

The thick part of the orbit space of a lattice is compact. Let G act isometrically and properly discontinuously on a proper metric space X, preserving a measure μ with a fundamental domain s of finite measure. If the balls of radius ε / 2 have measure at least c ≠ 0, then the image in the orbit space of the points moved at least ε by every nonidentity element is compact.