Cutoff functions for group actions

A cutoff function for an action of a group G on a space X is a nonnegative function c : X → ℝ whose translates sum to one, ∑ᶠ g, c (g • x) = 1, and whose topological support meets the translates g • K of each compact set K for only finitely many g (TauCeti.MulAction.IsCutoff). The second condition makes every such sum finite (TauCeti.MulAction.IsCutoff.hasFiniteSupport), and locally finite in x (TauCeti.MulAction.IsCutoff.locallyFinite_support), so cutoff functions can be used to average data along the orbits of a proper action of a discrete group whose orbit space is not compact.

For the action presentation G ⋉ X of a discrete group, whose space of arrows is G × X (TauCeti.ActionGroupoid.arrowHomeomorph) with source (g, x) ↦ x and target (g, x) ↦ g • x, the sum ∑ᶠ g, c (g • x) is the sum of c over the targets of the arrows with source x. The finiteness condition is then the properness of the source map on the support of c composed with the target (TauCeti.MulAction.IsCutoff.isProperMap_snd).

Each sum ranges over the whole group, so elements acting trivially are counted. In particular, for a finite group the constant |G|⁻¹ is a cutoff function (TauCeti.MulAction.isCutoff_inv_card), whatever the kernel of the action.

Main results

• TauCeti.MulAction.isCutoff_div_finsum: dividing a nonnegative function by the sum of its translates gives a cutoff function, as soon as each orbit meets its support and each compact set has finitely many translates meeting its support.
• TauCeti.MulAction.locallyFinite_preimage_smul_tsupport, TauCeti.MulAction.locallyFinite_support_apply_smul: under this finiteness condition the translates of a function have locally finite topological supports, and so locally finite supports.
• TauCeti.MulAction.IsCutoff.isProperMap_snd: the source map of the action presentation is proper on the support of a cutoff function composed with the target.

The smooth cutoff functions of proper actions on manifolds are constructed in TauCeti.Geometry.Manifold.GroupAction.Cutoff.

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.

structure TauCeti.MulAction.IsCutoff (G : Type u_1) {X : Type u_2} [TopologicalSpace X] [SMul G X] (c : X → ℝ) : Prop

A cutoff function for an action of G on X: a nonnegative function whose translates sum to one at every point, and whose topological support meets the translates of each compact set by only finitely many group elements.

• nonneg (x : X) : 0 ≤ c x

  A cutoff function is nonnegative.

• finsum_smul_eq_one (x : X) : ∑ᶠ (g : G), c (g • x) = 1

  The translates of a cutoff function sum to one.

• finite_smul_inter_tsupport ⦃K : Set X⦄ (hK : IsCompact K) : {g : G | (g • K ∩ tsupport c).Nonempty}.Finite

  Only finitely many translates of a compact set meet the support of a cutoff function.

theorem TauCeti.MulAction.hasFiniteSupport_apply_smul {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul G X] {R : Type u_3} [Zero R] {f : X → R} (hf : ∀ ⦃K : Set X⦄, IsCompact K → {g : G | (g • K ∩ tsupport f).Nonempty}.Finite) (x : X) : Function.HasFiniteSupport fun (g : G) => f (g • x)

If only finitely many translates of each compact set meet the support of f, then each point has only finitely many translates at which f is nonzero.

theorem TauCeti.MulAction.locallyFinite_preimage_smul_tsupport {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul G X] {R : Type u_3} [Zero R] {f : X → R} [WeaklyLocallyCompactSpace X] (hf : ∀ ⦃K : Set X⦄, IsCompact K → {g : G | (g • K ∩ tsupport f).Nonempty}.Finite) : LocallyFinite fun (g : G) => (fun (x : X) => g • x) ⁻¹' tsupport f

If only finitely many translates of each compact set meet the support of f, then the preimages of the topological support of f under the maps x ↦ g • x form a locally finite family.

theorem TauCeti.MulAction.locallyFinite_support_apply_smul {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul G X] {R : Type u_3} [Zero R] {f : X → R} [WeaklyLocallyCompactSpace X] (hf : ∀ ⦃K : Set X⦄, IsCompact K → {g : G | (g • K ∩ tsupport f).Nonempty}.Finite) : LocallyFinite fun (g : G) => Function.support fun (x : X) => f (g • x)

If only finitely many translates of each compact set meet the support of f, then the supports of the translates x ↦ f (g • x) form a locally finite family.

theorem TauCeti.MulAction.finsum_apply_smul_pos {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul G X] {R : Type u_3} [AddCommMonoid R] [PartialOrder R] [IsOrderedCancelAddMonoid R] {f : X → R} (hf0 : ∀ (x : X), 0 ≤ f x) (hf : ∀ ⦃K : Set X⦄, IsCompact K → {g : G | (g • K ∩ tsupport f).Nonempty}.Finite) {x : X} (hx : ∃ (g : G), f (g • x) ≠ 0) : 0 < ∑ᶠ (g : G), f (g • x)

If f is nonnegative, nonzero somewhere on the orbit of x, and only finitely many translates of each compact set meet its support, then the sum of the translates of f at x is positive.

theorem TauCeti.MulAction.isCutoff_inv_card {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul G X] [Fintype G] [Nonempty G] : IsCutoff G fun (x : X) => (↑(Fintype.card G))⁻¹

For a finite nonempty G, such as a finite group, the constant function |G|⁻¹ is a cutoff function. Every element is counted, including those acting trivially.

theorem TauCeti.MulAction.IsCutoff.hasFiniteSupport {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul G X] {c : X → ℝ} (hc : IsCutoff G c) (x : X) : Function.HasFiniteSupport fun (g : G) => c (g • x)

The translates of a cutoff function at a point are nonzero for only finitely many group elements.

theorem TauCeti.MulAction.IsCutoff.locallyFinite_support {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul G X] {c : X → ℝ} [WeaklyLocallyCompactSpace X] (hc : IsCutoff G c) : LocallyFinite fun (g : G) => Function.support fun (x : X) => c (g • x)

The supports of the translates x ↦ c (g • x) of a cutoff function form a locally finite family.

theorem TauCeti.MulAction.IsCutoff.isProperMap_snd {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul G X] {c : X → ℝ} [TopologicalSpace G] [DiscreteTopology G] [ContinuousConstSMul G X] [T2Space X] [CompactlyCoherentSpace X] (hc : IsCutoff G c) : IsProperMap fun (p : ↑(tsupport fun (p : G × X) => c (p.1 • p.2))) => (↑p).2

The source map (g, x) ↦ x of the action presentation of a discrete group is proper on the support of a cutoff function composed with the target map (g, x) ↦ g • x.

theorem TauCeti.MulAction.isCutoff_div_finsum {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [Group G] [MulAction G X] {β : X → ℝ} (hβ : ∀ (x : X), 0 ≤ β x) (hfin : ∀ ⦃K : Set X⦄, IsCompact K → {g : G | (g • K ∩ tsupport β).Nonempty}.Finite) (hpos : ∀ (x : X), ∃ (g : G), β (g • x) ≠ 0) : IsCutoff G fun (x : X) => β x / ∑ᶠ (g : G), β (g • x)

Dividing a nonnegative function by the sum of its translates gives a cutoff function, provided every orbit meets the locus where the function is nonzero and only finitely many translates of each compact set meet its support.