Smooth cutoff functions for proper actions on manifolds

Let a group G act properly discontinuously on a Hausdorff σ-compact finite-dimensional real manifold M by C^n maps. Then M carries a C^n cutoff function for the action (TauCeti.MulAction.exists_isCutoff_contMDiff): a nonnegative C^n function c with ∑ᶠ g, c (g • x) = 1 for every x, whose support meets only finitely many translates of each compact set. No faithfulness or freeness is assumed: every group element is counted, including those acting trivially, so stabilizers and the ineffective kernel are retained.

For the action presentation G ⋉ M this is a cutoff function on the objects, summing to one over the targets of the arrows with each given source, with the source map proper on the support of c composed with the target (TauCeti.MulAction.IsCutoff.isProperMap_snd). Such functions turn averages over the orbits of a proper action with noncompact orbit space into locally finite sums.

Implementation notes

The construction first builds a nonnegative smooth function β whose support meets each orbit and has the finiteness property. Since the orbit space is Hausdorff, there is such a β whose support meets the preimage of each compact set of orbits in a compact set (TauCeti.exists_contMDiff_nonneg_isCompact_tsupport_inter_preimage), and proper discontinuity gives the finiteness property. Then c = β / ∑ᶠ g, β (g • ·) by TauCeti.MulAction.isCutoff_div_finsum.

References

• N. Bourbaki, Integration II, Chapter VII, §2, for Bruhat functions of proper actions.
• M. Crainic, Differentiable and algebroid cohomology, van Est isomorphisms, and characteristic classes, Comment. Math. Helv. 78 (2003), Section 2, for cutoff functions on proper groupoids.

theorem TauCeti.MulAction.exists_isCutoff_contMDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M] (G : Type u_4) [Group G] [MulAction G M] {n : ℕ∞} [ContMDiffConstSMul I (↑n) G M] [ProperlyDiscontinuousSMul G M] : ∃ (c : M → ℝ), IsCutoff G c ∧ ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑n) c

A group acting properly discontinuously by C^n maps on a Hausdorff σ-compact finite-dimensional real manifold has a C^n cutoff function.