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 Γ be a computable amenable group, then there always exists a canonically computable tempered two-sided Følner sequence (Fn)n≥ 1 in Γ. For a computable, measure-preserving, ergodic action of Γ on a Cantor space { 0 , 1 } ℕ endowed with a computable probability measure μ, it is shown that for every bounded lower semicomputable function f on { 0 , 1 } ℕ and for every Martin-Löf random ω∈ { 0 , 1 } ℕ the equalitylimn→∞1|Fn|∑g∈Fnf(g⋅ω)=∫fdμholds, where the averages are taken with respect to a canonically computable tempered two-sided Følner sequence (Fn)n≥ 1. We also prove the same identity for all lower semicomputable f’s in the special case when Γ is a computable group of polynomial growth and Fn := B(n) is the Følner sequence of balls around the neutral Γ.
Analysis