Garrido, Theorem 2.6 for power sets — an invariant measure on an invariant ring of sets extends to an invariant measure on all subsets

Let $G$ be amenable (Garrido.IsAmenable G) and act on a set $X$. Let $\mathcal R$ be a ring of sets in $X$ (Mathlib's IsSetRing: it contains $\emptyset$ and is closed under unions and differences) with $g s \in \mathcal R$ for every $g \in G$ and $s \in \mathcal R$, and let $\mu$ assign to subsets of $X$ values in $[0, \infty]$, with $\mu(\emptyset) = 0$, $\mu(s \cup t) = \mu(s) + \mu(t)$ for disjoint $s, t \in \mathcal R$, and $\mu(g s) = \mu(s)$ for $g \in G$ and $s \in \mathcal R$. Then there is a finitely additive $\bar\mu$ on all subsets of $X$ (IsFinitelyAdditiveMeasure) that agrees with $\mu$ on $\mathcal R$ and is $G$-invariant (IsInvariant G).

Garrido writes on p. 7: “Theorem 2.6 (Invariant Extension Theorem). Recall Carathéodory’s Extension Theorem: If $\mathcal R$ is a subring of the boolean algebra $\mathcal A$ and $\mu$ is a measure on $\mathcal R$, then $\mu$ can be extended to a measure $\bar\mu$ on $\mathcal A$. If $G$ is an amenable group of automorphisms of $\mathcal A$ and $\mathcal R$, $\mu$ are $G$-invariant, then $\bar\mu$ can be chosen to be $G$-invariant.” This is that theorem for the boolean algebra of all subsets of $X$, with no extension of $\mu$ supplied, a step between the mission's milestone Garrido.hasInvariantExtensionProperty_of_isAmenable, which takes an extension to all subsets as a hypothesis, and the statement for arbitrary boolean algebras. Its proof supplies that extension with FinitelyAdditive.exists_extension_of_isSetRing.