Let T be a measure-preserving transformation of a space (X, B, mu), let f be a measurable function from X to the real numbers, and let x be any element of X. Think of x as denoting the state of a system, T x as denoting the state a unit of time later, and f as being some measurement that one can perform. Imagine now performing a sequence of measurements f x, f(T x), f(T^2 x), ..., f(T^n x) and taking their average. The pointwise ergodic theorem says that, in general, this sequence of averages will converge almost everywhere; the mean ergodic theorem says that, as a function of x, the averages converge in the L^2 norm.

In general, one cannot compute rates of convergence from the initial data, and, indeed, the limit may not be computable (given reasonable notions of computability for the relevant objects). In short, the ergodic theorems cannot be given a direct computational interpretation. I will explain how proof-theoretic methods yield classically equivalent formulations of the ergodic theorems, which are computably valid; and additional information besides.

Here are links to slides for both talks and the preprint.