arXiv subjects
Publications and source records attributed to Henry Towsner.
Extending Gödel's \emph{Dialectica} interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.
Kreisel has observed that the termination proof for Hilbert's epsilon-substitution method bears a resemblance to the priority arguments used in recursion theory. We make this precise by proving the termination using a framework for priority arguments due to Lerman and Lempp.
The mean ergodic theorem is equivalent to the assertion that for every function K and every epsilon, there is an n with the property that the ergodic averages A_m f are stable to within epsilon on the interval [n,K(n)]. We show that even though it is not generally possible to compute a bound on the rate of convergence of a sequence of ergodic averages, one can give explicit bounds on n in terms of K and || f || / epsilon. This tells us how far one has to search to find an n so that the ergodic averages are "locally stable" on a large interval. We use these bounds to obtain a similarly explicit version of the pointwise ergodic theorem, and show that our bounds are qualitatively different from ones that can be obtained using upcrossing inequalities due to Bishop and Ivanov. Finally, we explain how our positive results can be viewed as an application of a body of general proof-theoretic methods falling under the heading of "proof mining."
Recent work has generalized the Furstenberg correspondence between sets of integers and dynamical systems to versions which involve sequences of finite graphs or sequences of $L^\infty$ functions. We give a unified version of the theorem subsuming all these generalizations.
Tao has recently proved that if $T_1,...,T_l$ are commuting, invertible, measure-preserving transformations on a dynamical system then for any $L^\infty$ functions $f_1,...,f_l$, the average $\frac{1}{N}\sum_{n=0}^{N-1}\prod_{i\leq l}f_i\circ T^n_i$ converges in the $L^2$ norm. Tao's proof is unusual in that it translates the problem into a more complicated statement about the combinatorics of finite spaces by using the Furstenberg correspondence "backwards". In this paper, we give an ergodic proof of this theorem, essentially a translation of Tao's argument to the ergodic setting. In order to do this, we develop two new variations on the usual Furstenberg correspondence, both of which take recurrence-type statements in one dynamical system and give equivalent statements in a different dynamical system with desirable properties.