Computing uniform (metastable) rates of convergence from the statement of the theorem alone
Penn State University
Consider a convergence theorem of the following form.
(T): If the property P holds, then the sequence (xn) converges.
For example, the monotone convergence principle states that any monotone, bounded sequence of reals converges.
This talk concerns the notion of metastable rates of convergence. The advantage of this notion is that metastable rates are often uniform and computable. Kohlenbach, using proof theory, showed that if the property P is of a certain form and the theorem (T) is provable in a certain formal type theory, then the rate of metastable convergence is both uniform and computable. Avigad and Iovino, using model theory, showed that if the theorem (T) is true and the property P is preserved by ultraproducts, then the rate of metastable convergence is uniform (no mention of computability). In this result, using computable analysis and computable continuous model theory, we show that if (T) is true and P is axiomatizable in continuous logic, then the corresponding metastable bounds are both uniform and computable from P. This generalizes both of the previous results.
Jason Rute received his doctorate in 2013 from Carnegie Mellon University, under the supervision of Jeremy Avigad. After a short stint at the University of Hawaii, he assumed a postdoctoral position at Penn State University. His work involves connections between computable mathematical structure and classical mathematical structure, including algorithmic randomness, reverse mathematics, effective mathematics, quantitative analysis, and metastability.