Garrido, Theorem 2.7 — amenability, an invariant mean, non-paradoxicality and the Invariant Extension Theorem are equivalent

For a group $G$ the following are equivalent: $G$ is amenable (IsAmenable G); there is a left-invariant mean on $G$ (HasInvariantMean G); $G$ is not paradoxical under left multiplication (¬ IsParadoxical G Set.univ); $G$ satisfies the Invariant Extension Theorem for every boolean algebra (SatisfiesInvariantExtensionTheorem G).

Garrido writes on p. 7: “Theorem 2.7. For a group $G$, the following are equivalent: 1. $G$ is amenable, that is, there is a finitely additive left-invariant probability measure on $\mathcal B(G)$; 2. there is a left-invariant mean on $G$; 3. $G$ is not paradoxical; 4. $G$ satisfies the Invariant Extension Theorem.” Item 4 is read at the generality of Theorem 2.6 (any boolean algebra, any subring, no extension supplied). The mission's milestone Garrido.isAmenable_tfae_four is the same equivalence with item 4 restricted to the algebras of all subsets of $G$-sets and an extension supplied. IsAmenable, HasInvariantMean and IsParadoxical are from the Garrido amenability and equidecomposability definitions.