The study of ergodic theorems from the viewpoint of computable analysis is a rich field of investigation. Interactions between algorithmic randomness, computability theory and ergodic theory have recently been examined by several authors. It has been observed that ergodic measures have better computability properties than non-ergodic ones. In a previous paper we studied the extent to which non-ergodic measures inherit the computability properties of ergodic ones, and introduced the notion of an effectively decomposable measure. We asked the following question: if (...) the ergodic decomposition of a stationary measure is finite, is this decomposition effective? In this paper we answer the question in the negative. (shrink)

This paper discusses what kind of quantitative information one can extract under which circumstances from proofs of convergence statements in analysis. We show that from proofs using only a limited amount of the law-of-excluded-middle, one can extract functionals , where L is a learning procedure for a rate of convergence which succeeds after at most B-many mind changes. This -learnability provides quantitative information strictly in between a full rate of convergence and a rate of metastability in the sense of Tao (...) . In fact, it corresponds to rates of metastability of a particular simple form. Moreover, if a certain gap condition is satisfied, then B and L yield a bound on the number of possible fluctuations. We explain recent applications of proof mining to ergodic theory in terms of these results. (shrink)

We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Gödel and Shoenfield can be used to rewrite proofs performed in these systems into standard ones. These functional interpretations show in particular that our nonstandard systems are conservative extensions of E-HAω and E-PAω, strengthening earlier results by Moerdijk and Palmgren, and Avigad and Helzner. We will also indicate how our rewriting algorithm can be used for term extraction purposes. To conclude the (...) paper, we will point out some open problems and directions for future research, including some initial results on saturation principles. (shrink)