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

We introduce computable actions of computable groups and prove the following versions of effective Birkhoff’s ergodic theorem. Let $\mathrm{\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$\mathrm{.}Foracomputable,measure-preserving,ergodicactionof$\Gamma$onaCantorspace${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 $$\underset{n\to \mathrm{\infty }}{\lim }\frac{1}{\mathrm{\mid }{F}_n\mathrm{\mid }}\sum _{g\in F_n}f(g\cdot \omega )=\int fd\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}$\mathrm{.}Wealsoprovethesameidentityforalllowersemicomputable$f$'s in the special case when $\mathrm{\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 $\mathrm{\Gamma }$.