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

## TL;DR

This paper establishes an effective version of Birkhoff's ergodic theorem for computable actions of amenable groups, showing convergence of averages for computable functions at Martin-Löf random points.

## Contribution

It introduces computable actions of amenable groups and proves an effective ergodic theorem with explicit computable F{
}lner sequences and convergence results.

## Key findings

- Existence of a computable tempered F{
}lner sequence in amenable groups.
- Convergence of averages for bounded lower semicomputable functions at Martin-Löf random points.
- Extension of the ergodic theorem to groups of polynomial growth with specific F{
}lner sequences.

## 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{\o}lner sequence $(F_n)_{n \geq 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\"of 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 \omega) = \int\limits f d \mu \] holds, where the averages are taken with respect to a canonically computable tempered two-sided F{\o}lner sequence $(F_n)_{n \geq 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{\o}lner sequence of balls around the neutral element of $\Gamma$.