PROOF MINING AND HIGH-LEVEL PROOF-THEORETIC REASONING: A CASE STUDY ON GREEDY APPROXIMATION SCHEMES

Abstract We carry out a logical analysis of a convergence proof for greedy approximation schemes in uniformly smooth Banach spaces. Though the proof is by contradiction, we are able to extract computable rates of convergence that depend on the corresponding modulus of uniform smoothness for the space. While our quantitative results represent a first proof-theoretic study of greedy approximation schemes, we use this case study more generally as an opportunity to make explicit some of the high-level proof-theoretic reasoning that enables us to transform a nonconstructive convergence proof to one where computable convergence rates are apparent, representing the proof using a series of formal derivations that are designed to capture core mathematical reasoning, as opposed to low-level proof-theoretic bureaucracy. In this way we exemplify an approach to representing the process of program extraction that might, in particular, inform efforts to formalise proof mining in proof assistants.