Følner sets of a group for counting measure

Mathlib's IsFoelner G μ l F and maxFoelner G μ describe Følner families and the maximal Følner filter for a group G acting on a measure space. For the left regular action of a group on itself with counting measure on all subsets, this file identifies nontriviality of the maximal Følner filter with the classical finite-set condition: for every finite K ⊆ G and ε > 0 there is a finite nonempty F ⊆ G with

|gF △ F| < ε · |F|        for all g ∈ K.

TauCeti.HasFoelnerSets G names nontriviality of the counting-measure Følner filter. It installs the discrete measurable space ⊤ locally, so every subset is measurable and the notion depends only on the group, with no topology or countability hypothesis.

The two directions go through explicit Følner families, which we treat for counting measure on any type X with measurable singletons acted on by G. A Følner family along a nontrivial filter passes all finite tests, because finitely many eventual conditions hold simultaneously. Conversely, if every finite test has a witness, there is a Følner family of finite nonempty sets indexed by pairs (K, n) of a finite test set and a natural number, along atTop, which is a nontrivial filter. The proof picks for (K, n) a witness for K with tolerance 1 / (n + 1).

Main definitions

• TauCeti.HasFoelnerSets G: the counting-measure Følner filter of G is nontrivial.

Main results

• IsFoelner.tendsto_card_smul_symmDiff_div_card: the real cardinality ratios of a counting-measure Følner family of finite sets tend to zero.
• IsFoelner.exists_finset_card_smul_symmDiff_lt: a nontrivial counting-measure Følner family passes every finite test.
• TauCeti.exists_isFoelner_atTop: if every finite test has a witness, there is a Følner family of finite nonempty sets indexed by Finset G × ℕ along atTop.
• TauCeti.hasFoelnerSets_iff: HasFoelnerSets G is equivalent to the finite-set condition.
• TauCeti.HasFoelnerSets.of_tendsto_card_smul_symmDiff_div_card: finite sets with vanishing relative translation boundaries along a nontrivial filter give Følner sets.
• MulEquiv.hasFoelnerSets_iff: having Følner sets is invariant under group isomorphisms.

References

• A. Garrido, An introduction to amenable groups, Definitions 3.1 and 3.3.
• B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Appendix G.5.

theorem MeasureTheory.Measure.count_smul_symmDiff_div_count_lt_ofReal_iff {X : Type u_2} [MeasurableSpace X] [MeasurableSingletonClass X] [DecidableEq X] {M : Type u_3} [SMul M X] {F : Finset X} (hF : F.Nonempty) (m : M) {ε : ℝ} (hε : 0 < ε) : count (symmDiff (m • ↑F) ↑F) / count ↑F < ENNReal.ofReal ε ↔ ↑(symmDiff (m • F) F).card < ε * ↑F.card

For a finite nonempty F, the counting-measure Følner ratio of F at m is below ENNReal.ofReal ε exactly when |mF △ F| < ε · |F|.

theorem IsFoelner.tendsto_card_smul_symmDiff_div_card {G : Type u_1} [Group G] {X : Type u_2} [MeasurableSpace X] [MeasurableSingletonClass X] [DecidableEq X] [MulAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Finset X} (hF : IsFoelner G MeasureTheory.Measure.count l fun (i : ι) => ↑(F i)) (g : G) : Filter.Tendsto (fun (i : ι) => ↑(symmDiff (g • F i) (F i)).card / ↑(F i).card) l (nhds 0)

The real cardinality ratios of a counting-measure Følner family of finite sets tend to zero for every group element.

theorem IsFoelner.exists_finset_card_smul_symmDiff_lt {G : Type u_1} [Group G] {X : Type u_2} [MeasurableSpace X] [MeasurableSingletonClass X] [DecidableEq X] [MulAction G X] {ι : Type u_3} {l : Filter ι} [l.NeBot] {F : ι → Set X} (hF : IsFoelner G MeasureTheory.Measure.count l F) (K : Finset G) {ε : ℝ} (hε : 0 < ε) : ∃ (F' : Finset X), F'.Nonempty ∧ ∀ g ∈ K, ↑(symmDiff (g • F') F').card < ε * ↑F'.card

A Følner family for counting measure along a nontrivial filter passes every finite test: for each finite K ⊆ G and ε > 0 there is a finite nonempty F ⊆ X with |gF △ F| < ε · |F| for all g ∈ K.

theorem TauCeti.exists_isFoelner_atTop {G : Type u_1} [Group G] {X : Type u_2} [MeasurableSpace X] [MeasurableSingletonClass X] [DecidableEq X] [MulAction G X] (h : ∀ (K : Finset G) (ε : ℝ), 0 < ε → ∃ (F : Finset X), F.Nonempty ∧ ∀ g ∈ K, ↑(symmDiff (g • F) F).card < ε * ↑F.card) : ∃ (F : Finset G × ℕ → Finset X), (∀ (i : Finset G × ℕ), (F i).Nonempty) ∧ IsFoelner G MeasureTheory.Measure.count Filter.atTop fun (i : Finset G × ℕ) => ↑(F i)

If every finite test has a witness, then there is a Følner family of finite nonempty sets for counting measure, indexed by Finset G × ℕ along atTop.

@[reducible, inline]

abbrev TauCeti.HasFoelnerSets (G : Type u_1) [Group G] : Prop

A group G has Følner sets when Mathlib's maximal Følner filter for the left regular action of G on itself with counting measure is nontrivial. The measurable space ⊤ is installed locally, so every subset of G is measurable and the notion depends only on the group.

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

A group has Følner sets 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.

theorem TauCeti.HasFoelnerSets.of_tendsto_card_smul_symmDiff_div_card {G : Type u_1} [Group G] [DecidableEq G] {ι : Type u_2} {l : Filter ι} [l.NeBot] {F : ι → Finset G} (hne : ∀ᶠ (i : ι) in l, (F i).Nonempty) (hF : ∀ (g : G), Filter.Tendsto (fun (i : ι) => ↑(symmDiff (g • F i) (F i)).card / ↑(F i).card) l (nhds 0)) : HasFoelnerSets G

A group has Følner sets if a family of eventually nonempty finite sets has vanishing relative translation boundaries along a nontrivial filter.

theorem MulEquiv.hasFoelnerSets_iff {G : Type u_1} [Group G] {H : Type u_2} [Group H] (e : G ≃* H) : TauCeti.HasFoelnerSets G ↔ TauCeti.HasFoelnerSets H

Having Følner sets is invariant under group isomorphisms.