Balls separated from their translates outside the stabilizer

For a properly discontinuous action on a locally compact metric space, every point x lies in a ball which meets none of its translates by group elements outside the stabilizer of x: a group element moving that ball to meet itself already fixes x.

This separation is one half of the localization of an orbit space near a point with nontrivial stabilizer. The other half, that the ball is itself invariant under the stabilizer, does not follow from the hypotheses here: under ContinuousConstSMul alone an element fixing x need not preserve a ball about x. Once that invariance is supplied — for an isometric action, say, whose elements fixing x preserve every ball about x — the orbit space of the whole group near x agrees with the orbit space of the single stabilizer, which for a properly discontinuous action is a finite group.

Main results

• TauCeti.eventually_smul_eq_self_of_image_smul_ball_inter_nonempty: for every small enough ball about a point, a scalar moving a point of the ball into the ball fixes the centre.
• TauCeti.exists_ball_disjoint_smul_of_notMem_stabilizer: a small enough ball about a point is disjoint from each of its translates by a group element not fixing that point.

theorem TauCeti.eventually_smul_eq_self_of_image_smul_ball_inter_nonempty (G : Type u_1) {X : Type u_2} [PseudoMetricSpace X] [T2Space X] [LocallyCompactSpace X] [SMul G X] [ContinuousConstSMul G X] [ProperlyDiscontinuousSMul G X] (x : X) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (g : G), ((fun (x : X) => g • x) '' Metric.ball x r ∩ Metric.ball x r).Nonempty → g • x = x

Small balls are separated from translates that move the centre. For a properly discontinuous scalar action on a locally compact Hausdorff pseudo-metric space, for every small enough r > 0, a scalar moving some point of the ball of radius r about x into that ball fixes x.

theorem TauCeti.exists_ball_disjoint_smul_of_notMem_stabilizer (G : Type u_1) {X : Type u_2} [PseudoMetricSpace X] [T2Space X] [LocallyCompactSpace X] [Group G] [MulAction G X] [ContinuousConstSMul G X] [ProperlyDiscontinuousSMul G X] (x : X) : ∃ r > 0, ∀ g ∉ MulAction.stabilizer G x, Disjoint (g • Metric.ball x r) (Metric.ball x r)

A small enough ball meets no translate of itself by an element outside the stabilizer. For a properly discontinuous action on a locally compact Hausdorff pseudo-metric space, some ball about x is moved to meet itself only by the elements fixing x.