On effective Birkhoff's ergodic theorem for computable actions of amenable groups

Abstract

We introduce computable actions of computable groups and prove the following versions of effective Birkhoff's ergodic theorem. Let $\Gamma$ be a computable amenable group, then there always exists a canonically computable tempered two-sided Følner sequence $(F_n{)}_{n\ge 1}$ in $\Gamma$. For a computable, measure-preserving, ergodic action of $\Gamma$ on a Cantor space $\{0,1{\}}^{\mathbb{N}}$ endowed with a computable probability measure $\mu$, it is shown that for every bounded lower semicomputable function $f$ on $\{0,1{\}}^{\mathbb{N}}$ and for every Martin-Löf random $\omega \in \{0,1{\}}^{\mathbb{N}}$ the equality \[ \lim\limits_{n \to \infty} \frac{1}{|F_n|} \sum\limits_{g \in F_n} f(g \cdot ω) = \int\limits f d μ\] holds, where the averages are taken with respect to a canonically computable tempered two-sided Følner sequence $(F_n{)}_{n\ge 1}$. We also prove the same identity for all lower semicomputable $f$'s in the special case when $\Gamma$ is a computable group of polynomial growth and $F_n:=\mathrm{B}(n)$ is the Følner sequence of balls around the neutral element of $\Gamma$.

14 pages, comments are welcome