A Uniform Quantitative Form of Sequential Weak Compactness and Baillon's Nonlinear Ergodic Theorem

We apply proof-theoretic techniques of "proof mining" to obtain an effective uniform rate of metastability in the sense of Tao for Baillon's famous nonlinear ergodic theorem in Hilbert space. In fact, we analyze a proof due to Brézis and Browder of Baillon's theorem relative to the use of weak sequential compactness. Using previous results due to the author we show the existence of a bar recursive functional Ω* (using only lowest type bar recursion B 0, 1 ) providing a uniform quantitative version of weak compactness. Primitive recursively in this functional (and hence in T 0 + B 0, 1 ) we then construct an explicit bound φ on for the metastable version of Baillon's theorem. From the type level of φ and another result of the author it follows that φ is primitive recursive in the extended sense of Gödel's T. In a subsequent paper also Ω* will be explicitly constructed leading to the refined complexity estimate φ ∈ T 4 .