On the extraction of computational content from noneffective convergence proofs in analysis

Pavol Safarik

ISBN 978-3-8325-3765-4
160 pages, year of publication: 2014
price: 35.00 €
On the extraction of computational content from noneffective convergence proofs in analysis
The Fields medalist, Terence Tao, recently emphasized the importance of ''hard'' (or finitary) analysis and connected the finitisation to the methods we will employ in this thesis:

... The main advantage of working in a finitary setting ... is that the underlying dynamical system becomes extremely explicit. ... In proof theory, this finitisation is known as Gödel functional interpretation ...

For convergence theorems Tao calls the finitary formulation metastability and the corresponding explicit content its rate(s). In the case of the mean ergodic theorem such a rate can be used to obtain even an effective bound on the number of fluctuations.
We introduce effective learnability and three other natural kinds of such finitary information and analyze the corresponding proof-theoretic conditions.
Effective learnability not only provides means to know when to expect a bound on the number of fluctuations but also explains a very common pattern in the realizers for strong ergodic theorems. Moreover, we will see how a most natural example for a non-learnable convergence theorem closely relates to a notable exception to this pattern, the strong nonlinear ergodic theorem due to Wittmann.
Finally, we show how can computational content be extracted in the context of non-standard analysis.

P. Safarik, born and studied at grammar school Grösslingová in Bratislava, Diplom (ger.) and PhD in mathematics at TU Darmstadt.

cover cover cover cover cover cover cover cover cover
Table of contents (PDF)


  • Beweistheorie
  • Berechenbarkeit
  • Analysis
  • learnability
  • proof mining


35.00 €
in stock

34.00 €
45.00 €
49.00 €

(D) = Within Germany
(W) = Abroad

*You can purchase the eBook (PDF) alone or combined with the printed book (eBundle). In both cases we use the payment service of PayPal for charging you - nevertheless it is not necessary to have a PayPal-account. With purchasing the eBook or eBundle you accept our licence for eBooks.

For multi-user or campus licences (MyLibrary) please fill in the form or write an email to