The ongoing program of `proof mining' aims to extract new, quantitative information in the form of bounds and rates from prima facie noneffective proofs in mathematics. In doing so, proof mining and the thesis at hand draws a bridge between mathematics and logic, prompting a lively interaction between mathematical practice and logical theory. This thesis applies proof mining paradigms to several convergence results in fixed point theory and nonlinear optimization, resulting in new complexity information in the form of rates of convergence or rates of metastability.

A first -- yet from the proof mining perspective trivial -- example is Banach's famous fixed point theorem; The theorem itself asserts that any contraction mapping on a complete metric space possesses a unique fixed point, and that this fixed point may be approximated by means of the Picard iteration. The proof, on the other hand, exhibits the well known rate of convergence, which can be read off immediately from it. Moreover, the rate is uniform in the mapping, the underlying metric space and the starting point in that it only depends on a Lipschitz constant for the mapping in question and an upper bound on its initial displacement. In other words, for given contraction constant $q$ and positive real number $b$, the rate of convergence is valid for the class of all metric spaces, all mappings on this metric space with contraction constant $q$ and all starting points that are displaced by the operator by a distance of at most $b$.

The reason that Banach's fixed point theorem admits such a uniform rate of convergence and that its proof divulges the rate so easily has two reasons: It is constructive and convergence to the limit point is monotone. In general, however, neither is the case. It is precisely in these cases that proof mining, or rather the general logical theorems and tools behind the name, come into play.

Under vastly general conditions on the proof that admit non-constructive reasoning in the form of ideal principles and classical logic, so-called metatheorems guarantee the existence of uniform complexity information. For instance, a large part of classical analysis is covered by those metatheorems. Furthermore, the complexity information is not only guaranteed to exist, but can be extracted from the proof at hand.

The original proof is moreover transformed into a new proof of the new statement which exhibits the additional complexity information. The new proof then exhibits no trace of its proof-theoretic manipulation and is carried out without reference to any mathematical logic. This has the further advantage that the complexity bound is not only valid, but its proof is easily accessible to the experts of the respective mathematical field and can be published in the corresponding journals.