Dirichlet domains

Let a group G act by isometries on a metric space X, and fix a centre p : X. The Dirichlet domain of p is the set of points at least as close to p as to every other point of its orbit, {x | ∀ g : G, dist x p ≤ dist x (g • p)}.

For a properly discontinuous action on a proper space, every orbit meets the Dirichlet domain: the orbit of p has only finitely many points in each closed ball, so the distance from a point to the orbit of p is attained. If two translates of the Dirichlet domain meet, every common point is equidistant from the two corresponding translates of p. Consequently, when the centre has trivial stabilizer and the equidistant set of any two distinct orbit points is null, the Dirichlet domain is a measurable fundamental domain. In the hyperbolic plane these equidistant sets are geodesics, which is how the Dirichlet polygon of a Fuchsian group arises.

Main declarations

• TauCeti.dirichletDomain G p: the Dirichlet domain of the centre p.
• TauCeti.isClosed_dirichletDomain: it is closed.
• TauCeti.smul_dirichletDomain: translating the Dirichlet domain translates its centre.
• TauCeti.finite_dirichletCompetitors: on a bounded set, only finitely many acting elements can move the centre to a point at least as close as the centre.
• TauCeti.exists_finset_dirichletDomain_inter_eq: on a bounded set, the Dirichlet domain is cut out by finitely many of its defining inequalities.
• TauCeti.mem_interior_dirichletDomain_of_forall_dist_lt: strict dominance over distinct orbit points implies interior membership.
• TauCeti.exists_smul_mem_dirichletDomain: for a properly discontinuous isometric action on a proper space, every orbit meets it.
• TauCeti.dirichletDomain_inter_dirichletDomain_smul_subset: the Dirichlet domains of two points of one orbit meet only in points equidistant from them.
• TauCeti.isFundamentalDomain_dirichletDomain: it is a fundamental domain when the centre has trivial stabilizer and equidistant sets of distinct orbit points are null.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §9.4.
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §3.2.

def TauCeti.dirichletDomain (G : Type u_1) {X : Type u_2} [PseudoMetricSpace X] [SMul G X] (p : X) : Set X

The Dirichlet domain of a centre p: the points at least as close to p as to every point g • p of its orbit.

Equations

• TauCeti.dirichletDomain G p = {x : X | ∀ (g : G), dist x p ≤ dist x (g • p)}

@[simp]

theorem TauCeti.mem_dirichletDomain {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] {p x : X} : x ∈ dirichletDomain G p ↔ ∀ (g : G), dist x p ≤ dist x (g • p)

Membership in a Dirichlet domain, unfolded.

theorem TauCeti.self_mem_dirichletDomain {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] (p : X) : p ∈ dirichletDomain G p

The centre lies in its Dirichlet domain.

theorem TauCeti.isClosed_dirichletDomain (G : Type u_1) {X : Type u_2} [PseudoMetricSpace X] [SMul G X] (p : X) : IsClosed (dirichletDomain G p)

A Dirichlet domain is closed, being an intersection of closed sets.

theorem TauCeti.measurableSet_dirichletDomain (G : Type u_1) {X : Type u_2} [PseudoMetricSpace X] [SMul G X] [MeasurableSpace X] [OpensMeasurableSpace X] (p : X) : MeasurableSet (dirichletDomain G p)

A Dirichlet domain is measurable.

def TauCeti.dirichletCompetitors (G : Type u_1) {X : Type u_2} [PseudoMetricSpace X] [SMul G X] (p : X) (K : Set X) : Set G

The acting elements whose images of p compete with p somewhere on K: for some x ∈ K, the point g • p is at least as close to x as p is. Equivalently, these are the g whose defining inequality of the Dirichlet domain does not hold strictly everywhere on K. Every constraint that cuts into K is indexed by a competitor, but a competitor's constraint may still be redundant.

Equations

• TauCeti.dirichletCompetitors G p K = {g : G | ∃ x ∈ K, dist x (g • p) ≤ dist x p}

@[simp]

theorem TauCeti.mem_dirichletCompetitors {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] {p : X} {K : Set X} {g : G} : g ∈ dirichletCompetitors G p K ↔ ∃ x ∈ K, dist x (g • p) ≤ dist x p

Membership in the set of competitors of a Dirichlet centre on a set.

theorem TauCeti.finite_dirichletCompetitors {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] [ProperSpace X] [ProperlyDiscontinuousSMul G X] (p : X) {K : Set X} (hK : Bornology.IsBounded K) : (dirichletCompetitors G p K).Finite

Only finitely many acting elements compete with a Dirichlet centre on a bounded set. For a properly discontinuous action on a proper metric space, a bounded set K meets the region where g • p is at least as close as p for only finitely many g.

theorem TauCeti.exists_finset_dirichletDomain_inter_eq {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] [ProperSpace X] [ProperlyDiscontinuousSMul G X] (p : X) {K : Set X} (hK : Bornology.IsBounded K) : ∃ (s : Finset G), dirichletDomain G p ∩ K = (⋂ g ∈ s, {x : X | dist x p ≤ dist x (g • p)}) ∩ K

A Dirichlet domain has finitely many defining inequalities on every bounded set. For a bounded K, there is a finite set s of acting elements such that intersecting K with the full Dirichlet domain is the same as imposing only the inequalities indexed by s on K. This is the local-finiteness input for viewing Dirichlet domains as locally finite intersections of the distance-dominance regions {x | dist x p ≤ dist x (g • p)}.

theorem TauCeti.mem_interior_dirichletDomain_of_forall_dist_lt {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [SMul G X] [ProperSpace X] [ProperlyDiscontinuousSMul G X] {p x : X} (hx : ∀ (g : G), g • p ≠ p → dist x p < dist x (g • p)) : x ∈ interior (dirichletDomain G p)

Strict dominance over every distinct orbit point puts a point in the interior of the Dirichlet domain. Elements fixing the centre are allowed.

theorem TauCeti.dirichletDomain_inter_dirichletDomain_smul_subset {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [Group G] [MulAction G X] (p : X) (g : G) : dirichletDomain G p ∩ dirichletDomain G (g • p) ⊆ {x : X | dist x p = dist x (g • p)}

The Dirichlet domains of two points of one orbit meet only in points equidistant from them.

theorem TauCeti.mem_dirichletDomain_smul_iff {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [Group G] [MulAction G X] {p x : X} (hx : x ∈ dirichletDomain G p) (g : G) : x ∈ dirichletDomain G (g • p) ↔ dist x p = dist x (g • p)

On the Dirichlet domain, equal distance to p and g • p is equivalent to lying in the Dirichlet domain centred at g • p.

@[simp]

theorem TauCeti.smul_dirichletDomain {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] (g : G) (p : X) : g • dirichletDomain G p = dirichletDomain G (g • p)

Translating a Dirichlet domain by a group element gives the Dirichlet domain of the translated centre.

theorem TauCeti.exists_smul_mem_dirichletDomain {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] [ProperSpace X] [ProperlyDiscontinuousSMul G X] (p x : X) : ∃ (g : G), g • x ∈ dirichletDomain G p

Every orbit meets the Dirichlet domain. For a properly discontinuous isometric action on a proper space, each point has a translate in the Dirichlet domain of any centre: translate it by the inverse of an element g for which g • p is a closest point of the orbit of p.

theorem TauCeti.iUnion_smul_dirichletDomain {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] [ProperSpace X] [ProperlyDiscontinuousSMul G X] (p : X) : ⋃ (g : G), g • dirichletDomain G p = Set.univ

The translates of a Dirichlet domain cover the whole space.

theorem TauCeti.isFundamentalDomain_dirichletDomain {G : Type u_1} {X : Type u_2} [PseudoMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] [ProperSpace X] [ProperlyDiscontinuousSMul G X] [MeasurableSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) {p : X} (hp : MulAction.stabilizer G p = ⊥) (hμ : ∀ (g h : G), g • p ≠ h • p → μ {x : X | dist x (g • p) = dist x (h • p)} = 0) : MeasureTheory.IsFundamentalDomain G (dirichletDomain G p) μ

The Dirichlet domain is a fundamental domain. For a properly discontinuous isometric action on a proper space, the Dirichlet domain of a centre with trivial stabilizer is a fundamental domain for any measure in which the equidistant set of any two distinct points of the orbit of the centre is null.