A constructive Borel-Cantelli Lemma. Constructing orbits with required statistical properties

TL;DR

This paper proves a constructive version of the Borel-Cantelli lemma in computable metric spaces, enabling the construction of points with typical statistical properties in various dynamical systems.

Contribution

It introduces a constructive Borel-Cantelli lemma and applies it to show the existence of computable points with typical statistical behavior in complex dynamical systems.

Findings

Existence of computable points following Birkhoff's theorem in certain systems

Application to hyperbolic and interval maps with invariant measures

Construction of computable normal numbers in any base

Abstract

In the general context of computable metric spaces and computable measures we prove a kind of constructive Borel-Cantelli lemma: given a sequence (constructive in some way) of sets $A_{i}$ with effectively summable measures, there are computable points which are not contained in infinitely many $A_{i}$. As a consequence of this we obtain the existence of computable points which follow the \emph{typical statistical behavior} of a dynamical system (they satisfy the Birkhoff theorem) for a large class of systems, having computable invariant measure and a certain ``logarithmic'' speed of convergence of Birkhoff averages over Lipshitz observables. This is applied to uniformly hyperbolic systems, piecewise expanding maps, systems on the interval with an indifferent fixed point and it directly implies the existence of computable numbers which are normal with respect to any base.