A constructive version of Birkhoffs ergodic theorem for Martin-Lof random points
We prove the effective version of Birkhoffs ergodic theorem for Martin-Lof random points and effectively open sets, improving the results previously obtained in this direction (in particular those of Vyugin, Nandakumar and Hoyrup, Rojas). The proof consists of two steps. First, we prove a generalization of Kucera's theorem, which is a particular case of effective ergodic theorem: a trajectory of a computable ergodic mapping that starts from a random point cannot remain inside an effectively open set of measure less than 1. Second, we show that the full statement of the effective ergodic theorem can be reduced to this special case. Both steps use the statement of classical ergodic theorem. but not its usual classical proof. Therefore, we get a new simple proof of the effective ergodic theorem (with weaker assumptions than before). This result was recently obtained independently by Franklin, Greenberg, Miller and Ng. (C) 2011 Elsevier Inc. All rights reserved.
birkhoffs ergodic theorem martin-lof randomness algorithmic randomness poincare recurrence theorem