A quantitative nonlinear strong ergodic theorem for Hilbert spaces

We give a quantitative version of a strong nonlinear ergodic theorem for (a class of possibly even discontinuous) selfmappings of an arbitrary subset of a Hilbert space due to R. Wittmann and outline how the existence of uniform bounds in such quantitative formulations of ergodic theorems can be proved by means of a general logical metatheorem. In particular these bounds depend neither on the operator nor on the initial point. Furthermore, we extract such uniform bounds in our quantitative formulation of Wittmannʼs theorem, implicitly using the proof-theoretic techniques on which the metatheorem is based. However, we present our result and its proof in analytic terms without any reference to logic as such. Our bounds turn out to involve nested iterations of relatively low computational complexity. While in theory these kind of iterations ought to be expected, so far this seems to be the first occurrence of such a nested use observed in practice.