This mission formalizes A. Garrido, An introduction to amenable groups, lecture notes from four talks at the Oxford Advanced Class in Algebra, Michaelmas 2013 (archived PDF) — its Section 1.2, Section 2 and Section 3.

Motivation

A group is amenable when its subsets can be measured in a way that translation does not disturb. Von Neumann isolated the notion in 1929 to explain the Banach–Tarski paradox: a solid ball in $\mathbb{R}^3$ can be cut into finitely many pieces and reassembled into two balls of the original size, and the reason is group-theoretic rather than geometric — the rotation group $SO(3,\mathbb{R})$ contains a free group of rank two, while the isometry groups of $\mathbb{R}$ and $\mathbb{R}^2$ do not. No paradox is possible for a group carrying a translation-invariant finitely additive probability measure.

Mahlon Day proved in the 1950s that von Neumann's definition agrees with the existence of an invariant mean on bounded functions, moving the theory into functional analysis, and coined the word "amenable" as a pun on "mean"; the problem below was first stated in print, with von Neumann's name attached, in Day's 1957 paper. Følner gave a combinatorial criterion — a group is amenable exactly when it has finite subsets almost invariant under translation — now usually taken as the definition, and the link to growth.

The organizing question of the classical theory was the von Neumann–Day problem: writing $EG$ for the elementary amenable groups, $AG$ for the amenable groups and $NF$ for the groups with no free subgroup of rank two, one has $EG \subseteq AG \subseteq NF$, and both inclusions were asked to be equalities. Both are strict. Ol'shanskii (1980) showed $AG \neq NF$, and Grigorchuk (1985) showed $EG \neq AG$ with a group of intermediate growth. Chou (1980) supplied the structural facts about $EG$ that the separation rests on.

Amenability is now basic vocabulary in geometric group theory, ergodic theory and operator algebras.

Setting

Let $G$ be a discrete group. A measure on $G$, in von Neumann's sense, is a function $\mu$ assigning a value to every subset of $G$ — not merely to a distinguished $\sigma$-algebra — such that

$$\mu(G) = 1, \qquad \mu(A \sqcup B) = \mu(A) + \mu(B), \qquad \mu(gA) = \mu(A)$$

for all $g \in G$ and all disjoint $A, B \subseteq G$. Only finite additivity is required; countable additivity together with invariance is impossible for a countably infinite group. $G$ is amenable if such a $\mu$ exists.

Two reformulations matter. A left-invariant mean is a positive linear functional $m$ on the bounded real functions $\ell^\infty(G)$ with $m(\mathbf{1}) = 1$ and $m({}_g f) = m(f)$, where ${}_g f(h) = f(g^{-1}h)$. And $G$ satisfies the Følner condition if for every finite $A \subseteq G$ and every $\varepsilon > 0$ there is a finite nonempty $F \subseteq G$ with

$$\frac{|aF \,\triangle\, F|}{|F|} \le \varepsilon \qquad \text{for every } a \in A,$$

where $\triangle$ is symmetric difference. In the Cayley graph this says $F$ has small boundary relative to its size.

Against amenability stands paradoxicality. Two subsets $A, B$ of a $G$-set $X$ are $G$-equidecomposable, written $A \sim B$, if $A$ can be cut into finitely many pieces which, after each is moved by a single element of $G$, reassemble to $B$; and $E \subseteq X$ is $G$-paradoxical if it has two disjoint proper subsets each equidecomposable with $E$ itself. A group that is paradoxical under left translation admits no invariant measure.

Formalization targets

Goal — Theorem 3.6

$$G \text{ satisfies the Følner condition} \iff G \text{ is amenable}$$

This is the goal because it bridges the combinatorial and measure-theoretic sides of the subject, and every later application of amenability to growth uses it in one direction or the other.

Supporting equivalences — Theorems 1.15 and 2.7

For a group $G$, these four are equivalent: $G$ is amenable; there is a left-invariant mean on $\ell^\infty(G)$; $G$ is not paradoxical; and $G$ has the invariant extension property.

Closure properties — Proposition 2.2

Amenability passes to subgroups and quotients, is closed under extensions, and is closed under directed unions; hence all abelian and all virtually solvable groups are amenable, and $EG \subseteq AG$.

Significance

Each of the three equivalent pictures serves a different purpose: the measure gives non-paradoxicality, the mean gives access to functional analysis and fixed-point arguments, and the Følner condition is what one can verify for a concrete group. Theorem 3.8 is the typical consequence — a group of subexponential growth is amenable — proved by exhibiting the balls of the word metric as a Følner sequence, which only the equivalence licenses.

Mathlib has very little of this. It names no definition of amenability: FoelnerFilter.lean says one "has not yet been given" for want of "a general consensus" on the right generality, and writes the property out inline in the conclusion of IsFoelner.amenable, which is one direction of the goal. Equidecomp.lean has the equidecomposition machinery, with a TODO asking for the Schröder–Bernstein theorem for equidecomposability that is Theorem 1.2 here.

This mission supplies the missing definitions, that Schröder–Bernstein theorem, the closure properties, and the direction of the Følner equivalence that is genuinely open. Nothing here is a new mathematical result: all of it is classical, and the work is formalization.

Difficulty

The Følner-implies-amenable direction is the easier one, and the natural construction almost works: given a Følner sequence $F_n$, set $\mu(B) = \lim_n |B \cap F_n| / |F_n|$. That limit need not exist. It must be replaced by a limit along a non-principal ultrafilter, or the measure obtained by compactness in $[0,1]^{\mathcal{P}(G)}$.

The converse — amenable implies Følner — is where the content is, and no averaging argument reaches it. One has to produce, from a mean, finite sets that are almost invariant; the passage runs through a separation theorem in $\ell^1(G)$, the only step here needing a genuinely infinite-dimensional tool. The classical arguments provide no combinatorial route.

Two smaller obstructions are worth naming. Tarski's theorem — an invariant measure giving a set measure one exists precisely when that set is not paradoxical — is quoted without proof in the source and is the hardest single statement in the mission. And Theorem 2.6 rests on a finitely additive extension theorem for measures on a Boolean algebra, which is not the Carathéodory construction in Mathlib; Mathlib's is about outer measures and $\sigma$-additivity.

Formalization scope

Amenability is IsAmenable G: the existence of $m : \mathcal{P}(G) \to [0,\infty]$ with $m(G) = 1$, finitely additive on disjoint pairs, and invariant under left translation. The codomain is the extended nonnegative reals rather than $[0,1]$, to match the conclusion of Mathlib's IsFoelner.amenable — which at $X = G$ with every set measurable is exactly IsAmenable — so that theorem is directly usable; finite additivity and $m(G) = 1$ force $m(s) \le 1$ anyway, so nothing is added or lost.

Committed conventions. Means live on $\ell^\infty(G)$, realised as lp (fun _ : G => ℝ) ∞ — not on all of $G \to \mathbb{R}$, where invariance and normalisation are already contradictory (proved for $\mathbb{Z}$), so every statement about means would be vacuously unprovable. Normalisation is phrased via constantly-$1$ functions, to avoid depending on the ring structure of $\ell^\infty$. Cardinalities use Set.ncard, so no DecidableEq instance propagates into the statements. Paradoxicality is defined for an arbitrary subset, recovering the source's whole-space notion as a special case, because the source states it for the whole space but uses it for subsets throughout. Equidecomposability builds on Mathlib's Equidecomp, and growth on the published Chou_Growth bundle, rather than either being redefined.

One trivialising formalization is ruled out: amenability requiring only $m(G) = 1$ and additivity, without invariance, is satisfied by any normalised counting density and would make the mission vacuous. Left-invariance is part of every definition here, and IsAmenable is exhibited non-vacuously for finite groups.

A complete development needs finitely additive measures on a power set, invariant means on $\ell^\infty$, the Følner condition and sequences, paradoxical decompositions, and a finitely additive extension theorem on a Boolean algebra; the definitions and the last of these are reusable beyond this mission. Contributions are welcome on any milestone. Proposition 2.2's closure properties are the most self-contained entry points, and Theorem 1.2 is the one Mathlib has explicitly asked for.

What is left out

Two bodies of material from the source are deliberately out of scope, left for later missions in this series.

The geometric construction of the Banach–Tarski paradox — that $SO(3,\mathbb{R})$ contains a free group of rank two, the Hausdorff paradox, and the paradoxical decompositions of the sphere and the ball. This mission takes the measure-theoretic half of Section 1 and leaves the half about the $2$-sphere. Tarski's theorem and the Banach–Schröder–Bernstein theorem are in scope despite being printed alongside that material, because both are equidecomposability combinatorics and both are needed by results that are in scope.

The Grigorchuk group — its construction on the binary rooted tree, the proof that it is amenable but not elementary amenable, and its subexponential growth. Theorem 4.2 and Theorem 4.3 are the exceptions, and they enter as references rather than targets.

Also out of scope: the locally compact case. The source gives most definitions for both discrete and locally compact groups, then says it will "mostly focus on discrete groups"; only the discrete case is formalized. Følner nets for uncountable groups are likewise omitted, as is the extension of Example 3.5 to finitely generated abelian groups, which the source leaves as an exercise.

Selected references

• A. Garrido, An introduction to amenable groups, lecture notes, Oxford Advanced Class in Algebra, Michaelmas 2013. archived PDF
• S. Banach and A. Tarski, Sur la décomposition des ensembles de points en parties respectivement congruentes, Fund. Math. 6 (1924), 244–277. DOI
• J. von Neumann, Zur allgemeinen Theorie des Maßes, Fund. Math. 13 (1929), 73–116. DOI
• M. M. Day, Amenable semigroups, Illinois J. Math. 1 (1957), 509–544. DOI
• E. Følner, On groups with full Banach mean value, Math. Scand. 3 (1955), 243–254. DOI
• I. Namioka, Følner's conditions for amenable semi-groups, Math. Scand. 15 (1964), 18–28 — the source of the argument for the goal theorem. DOI
• J. M. Rosenblatt, Invariant measures and growth conditions, Trans. Amer. Math. Soc. 193 (1974), 33–53 — where supramenability is introduced. DOI
• A. Yu. Ol'shanskii, On the problem of the existence of an invariant mean on a group, Russian Math. Surveys 35 (1980), 180–181 — the paper Grigorchuk credits for $AG \neq NF$. DOI
• C. Chou, Elementary amenable groups, Illinois J. Math. 24 (1980), 396–407. DOI
• R. I. Grigorchuk, Degrees of growth of finitely generated groups, and the theory of invariant means, Math. USSR-Izvestiya 25 (1985), 259. DOI
• S. Wagon, The Banach–Tarski Paradox, Cambridge University Press, 1985. DOI