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 Γ be a computable amenable group, then there always exists a canonically computable tempered two-sided Følner sequence (F_n)_{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 (F_n)_{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 F_n := B(n) is the Følner sequence of balls around the neutral Γ.