Proof mining: a proof theoretic approach to numerical analysis

With the term `proof mining' we denote the activity of transforming a prima facie non-constructive proof into a new one from which certain computational information can be read off which was not visible beforehand.

Already in the 50's Georg Kreisel realized that logical techniques from proof theory -- originally developed for foundational purposes -- can be put to use here. In recent years, a more systematic proof theoretic approach to proof mining in numerical analysis emerged yielding new quantitative (and even qualitative) numerical results in approximation theory and fixed point theory and providing a bridge between mathematical numerical analysis and the area of computability (and complexity) in analysis which has mainly been developed by logicians (and complexity theorists).

Although proof mining has been applied also to e.g. number theory and combinatorics, the area of numerical (functional) analysis is of particular interest since here non-effectivity is at the core of many principles (like compactness arguments) which are used to ensure convergence. In mathematical terms this non-computability often is an obstacle to obtain a quantitative stability analysis and rates of convergence.

We will give a survey and discuss two recent applications concerning

(i) new uniform bounds for theorems of Ishikawa and Borwein-Reich-Shafrir on the asymptotic regularity of non-expansive mappings yielding even new qualitative results,

(ii) fully explicit description of the rate of strong unicity for best L_1-approximations of continuous functions by polynomials (joint work with Paulo Oliva).