On the removal of weak compactness arguments in proof mining

TL;DR

This paper shows that certain weak compactness arguments in Hilbert space proofs can be replaced by stronger, though false, compactness principles that become trivial under bounded functional interpretation, enabling new proof mining techniques.

Contribution

It introduces the use of bounded functional interpretation in proof mining to replace weak compactness arguments with Heine/Borel compactness, facilitating extraction of computational bounds.

Findings

Weak compactness can be replaced by Heine/Borel compactness in proofs.

Bounded functional interpretation trivializes these compactness arguments.

Application to three case studies demonstrates the method's effectiveness.

Abstract

The main observation of this paper is that some sequential weak compactness arguments in Hilbert space theory can be replaced by Heine/Borel compactness arguments (for the strong topology). Even though the latter form of compactness fails in (infinite-dimensional) Hilbert spaces, it nevertheless trivializes under the so-called bounded functional interpretation. As a consequence, the proof mining programme of extracting computational bounds from ordinary proofs of mathematics can be applied to {\em modified proofs} which use these false Heine/Borel compactness arguments. Additionally, the bounded functional interpretation provides good logical guidance in formulating quantitative versions of analytical statements. We illustrate these claims with three minings. The bounded functional interpretation is here used for the first time in proof mining.