Gödel functional interpretation and weak compactness (Q450951)

This paper gives the construction of a bar-recursive functional \(\Omega^*\) which provides a uniform quantitative version of weak compactness. The existence of \(\Omega^*\) was established by the author in [Commun. Contemp. Math. 14, No. 1, 1250006, 20 p. (2012; Zbl 1245.03093)], where he analyzed a proof due to \textit{H. Brézis} and \textit{F. E. Browder} [Bull. Am. Math. Soc. 82, 959--961 (1976; Zbl 0339.47029)] of Baillon's nonlinear ergodic theorem and extracts an explicit bound for the metastable version of Baillon's theorem that is primitive recursive relative to \(\Omega^*\).