Følner sets from almost invariant finitely supported functions

Let a group G act on a type X, and translate functions by (g • p) x = p (g⁻¹ • x). If a nonnegative finitely supported function p : X → ℝ is almost invariant under a finite set K ⊆ G in ℓ¹, in the sense that

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

then some finite nonempty set F ⊆ X satisfies

∑_{g ∈ K} |g • F ∆ F| < ε · |F|.

Such a set is found among the superlevel sets {x | t < p x}, t > 0.

This passes from Reiter's condition (almost invariant finitely supported probabilities) to Følner's condition (almost invariant finite sets). The proof is the layer-cake argument: for counting measure, the ℓ¹ distance between p and its translate is the integral over the levels t > 0 of |g • F_t ∆ F_t|, while the ℓ¹ norm of p is the integral of |F_t|; see MeasureTheory.Measure.exists_pos_sum_measure_symmDiff_lt_mul_measure.

Main results

• TauCeti.exists_finset_sum_card_smul_symmDiff_lt_of_sum_tsum_lt: a finite nonempty set whose total boundary ∑_{g ∈ K} |g • F ∆ F| is less than ε |F|.
• TauCeti.exists_finset_card_smul_symmDiff_lt_of_sum_tsum_lt: the same set satisfies |g • F ∆ F| < ε |F| for each g ∈ K.
• TauCeti.hasFoelnerSets_of_forall_exists_sum_tsum_abs_sub_lt: a group satisfying Reiter's condition, for its left regular action, has Følner sets.

References

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

theorem TauCeti.exists_finset_sum_card_smul_symmDiff_lt_of_sum_tsum_lt {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [DecidableEq X] {p : X → ℝ} (hp : 0 ≤ p) (hfin : Function.HasFiniteSupport p) {K : Finset G} {ε : ℝ} (h : ∑ g ∈ K, ∑' (x : X), |p (g⁻¹ • x) - p x| < ε * ∑' (x : X), p x) : ∃ (F : Finset X), F.Nonempty ∧ ∑ g ∈ K, ↑(symmDiff (g • F) F).card < ε * ↑F.card

Reiter implies Følner, summed form. If a nonnegative finitely supported function p on X satisfies ∑_{g ∈ K} ∑_x |p (g⁻¹ • x) - p x| < ε · ∑_x p x, then some finite nonempty set F ⊆ X has total boundary ∑_{g ∈ K} |g • F ∆ F| < ε |F|.

theorem TauCeti.exists_finset_card_smul_symmDiff_lt_of_sum_tsum_lt {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [DecidableEq X] {p : X → ℝ} (hp : 0 ≤ p) (hfin : Function.HasFiniteSupport p) {K : Finset G} {ε : ℝ} (h : ∑ g ∈ K, ∑' (x : X), |p (g⁻¹ • x) - p x| < ε * ∑' (x : X), p x) : ∃ (F : Finset X), F.Nonempty ∧ ∀ g ∈ K, ↑(symmDiff (g • F) F).card < ε * ↑F.card

Reiter implies Følner. If a nonnegative finitely supported function p on X satisfies ∑_{g ∈ K} ∑_x |p (g⁻¹ • x) - p x| < ε · ∑_x p x, then some finite nonempty set F ⊆ X satisfies |g • F ∆ F| < ε |F| for every g ∈ K.

theorem TauCeti.hasFoelnerSets_of_forall_exists_sum_tsum_abs_sub_lt {G : Type u_1} [Group G] (h : ∀ (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| < ε) : HasFoelnerSets G

A group satisfying Reiter's condition has Følner sets: if for every finite K and ε > 0 there is a finitely supported probability density p with ∑_{g ∈ K} ∑_x |p (g⁻¹ x) - p x| < ε, then G has Følner sets.