Amenable discrete groups have Følner sets

Let G be a discrete group. We prove that G is amenable, in the sense of a left-invariant mean on TauCeti.UCB G (which for discrete G consists of all bounded functions), exactly when it has Følner sets: for every finite K ⊆ G and ε > 0 there is a finite nonempty F ⊆ G with |gF △ F| < ε · |F| for all g ∈ K.

The implication from Følner sets to amenability is TauCeti.Amenable.of_hasFoelnerSets. For the converse we first establish Reiter's condition: for every finite K ⊆ G and ε > 0 there is a finitely supported probability density p : G → ℝ with

∑_{g ∈ K} ∑_x |p (g⁻¹ x) - p x| < ε.

The proof is by Hahn–Banach separation in the finite product K → ℓ¹(G). The vectors (p (g⁻¹ ·) - p)_{g ∈ K} for finitely supported probabilities p form the convex hull of the vectors (δ_{g x} - δ_x)_{g ∈ K}. If 0 were not in the closure of this convex set, a continuous functional Λ would separate them, so that Λ (δ_{g x} - δ_x)_{g ∈ K} ≥ u > 0 for every x. Writing f_g y = Λ (ι_g δ_y), these functions are bounded by ‖Λ‖, and the bounded function x ↦ ∑_{g ∈ K} (f_g (g x) - f_g x) is at least u everywhere; but a left-invariant mean assigns it the value 0. Reiter's condition then yields Følner sets among the superlevel sets of p, by TauCeti.hasFoelnerSets_of_forall_exists_sum_tsum_abs_sub_lt.

Main results

• TauCeti.Amenable.exists_sum_tsum_abs_sub_lt: an amenable discrete group satisfies Reiter's condition.
• TauCeti.amenable_iff_exists_sum_tsum_abs_sub_lt: a discrete group is amenable exactly when it satisfies Reiter's condition.
• TauCeti.Amenable.hasFoelnerSets: an amenable discrete group has Følner sets.
• TauCeti.amenable_iff_hasFoelnerSets: a discrete group is amenable exactly when it has Følner sets.
• TauCeti.amenable_iff_exists_finset: the same characterization in terms of finite sets.

References

• B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Theorem G.3.1 and Theorem G.5.1.
• A. Garrido, An introduction to amenable groups, Theorem 3.6.

theorem TauCeti.Amenable.exists_sum_tsum_abs_sub_lt {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] [Amenable G] (K : Finset G) {ε : ℝ} (hε : 0 < ε) : ∃ (p : G → ℝ), 0 ≤ p ∧ Function.HasFiniteSupport p ∧ ∑' (x : G), p x = 1 ∧ ∑ g ∈ K, ∑' (x : G), |p (g⁻¹ * x) - p x| < ε

Reiter's condition. In an amenable discrete group, for every finite K and ε > 0 there is a finitely supported probability density p with ∑_{g ∈ K} ∑_x |p (g⁻¹ x) - p x| < ε.

theorem TauCeti.amenable_iff_exists_sum_tsum_abs_sub_lt {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] : Amenable G ↔ ∀ (K : Finset G) (ε : ℝ), 0 < ε → ∃ (p : G → ℝ), 0 ≤ p ∧ Function.HasFiniteSupport p ∧ ∑' (x : G), p x = 1 ∧ ∑ g ∈ K, ∑' (x : G), |p (g⁻¹ * x) - p x| < ε

A discrete group is amenable exactly when it satisfies Reiter's condition: for every finite K and ε > 0 there is a finitely supported probability density p with ∑_{g ∈ K} ∑_x |p (g⁻¹ x) - p x| < ε.

theorem TauCeti.Amenable.hasFoelnerSets {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] [Amenable G] : HasFoelnerSets G

An amenable discrete group has Følner sets.

theorem TauCeti.amenable_iff_hasFoelnerSets {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] : Amenable G ↔ HasFoelnerSets G

A discrete group is amenable exactly when it has Følner sets.

theorem TauCeti.amenable_iff_exists_finset {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] [DecidableEq G] : Amenable G ↔ ∀ (K : Finset G) (ε : ℝ), 0 < ε → ∃ (F : Finset G), F.Nonempty ∧ ∀ g ∈ K, ↑(symmDiff (g • F) F).card < ε * ↑F.card

A discrete group is amenable exactly when for every finite K ⊆ G and every ε > 0 there is a finite nonempty F ⊆ G with |gF △ F| < ε · |F| for all g ∈ K.