Amenable groups

DefinitionAmenable group (Følner condition)#✓fully proved

A discrete group \(G\) is amenable if it satisfies the Følner condition: for every finite subset \(K \subseteq G\) and every real \(\varepsilon > 0\) there is a finite nonempty subset \(F \subseteq G\) such that \(|sF \mathbin{\triangle} F| / |F| < \varepsilon\) for every \(s \in K\). Here \(sF = \{sf : f \in F\}\) is the left translate of \(F\) by \(s\), \(\triangle\) is symmetric difference and \(|\cdot|\) is cardinality.

def IsAmenable (G : Type*) [Group G] : Prop :=
  ∀ (K : Finset G) (ε : ℝ), 0 < ε →
    ∃ F : Finset G, F.Nonempty ∧
      ∀ s ∈ K, (((s • F) ∆ F).card : ℝ) / (F.card : ℝ) < ε

Used by 6

Used byFinite groups are amenable · Trivial groups are amenable · Kourovka Problem 15.14(a): non-amenable branch groups · Kourovka Problem 15.14(b): non-amenable branch groups without free subgroups · Kourovka Problem 15.5 (statement): infinite finitely generated simple amenable groups · Kourovka Problem 15.4 (large growth rate implies non-amenability)

TheoremFinite groups are amenable#✓fully proved

Every finite group is amenable.

The whole group \(F = G\) is invariant under left translation, so it is a Følner set whose symmetric-difference ratio is \(0\).

theorem isAmenable_of_finite (G : Type*) [Group G] [Finite G] : IsAmenable G

Uses 1

Statement usesAmenable group (Følner condition)

TheoremTrivial groups are amenable#✓fully proved

Every group with at most one element is amenable; the set \(F = \{1\}\) witnesses the Følner condition.

theorem isAmenable_of_subsingleton (G : Type*) [Group G] [Subsingleton G] :
    IsAmenable G

Uses 1

Statement usesAmenable group (Følner condition)

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.