Computability of Banach space principles
We investigate the computable content of certain theorems which are sometimes called the \principles" of the theory of Banach spaces. Among these the main theorems are the Open Mapping Theorem, the Closed Graph Theorem and the Uniform Boundedness Theorem. We also study closely related theorems, as Banach's Inverse Mapping The- orem, the Theorem on Condensation of Singularities and the Banach- Steinhaus Theorem. From the computational point of view these the- orems are interesting, since their classical proofs rely more or less on the Baire Category Theorem and therefore they count as \non-constructive". These theorems have already been studied in Bishop's constructive anal- ysis but the picture that we can draw in computable analysis di ers in several points. On the one hand, computable analysis is based on clas- sical logic and thus can apply stronger principles to prove that certain operations are computable. On the other hand, classical logic enables us to prove \semi-constructive" versions of theorems, which can hardly be expressed in constructive analysis. For instance, the computable ver- sion of Banach's Inverse Mapping Theorem states that the inverse T − 1 of a linear computable and bijective operator T from a computable Ba- nach space into a computable Banach space is computable too, whereas the mapping T 7! T − 1 itself is not computable. Thus, there is no gen- eral algorithmic procedure to transfer a program of T into a program of T − 1 , although a program for T − 1 always exists. In this way we can explore the border between computability and non-computability in the theory of Banach spaces. As applications we briefly discuss the e ective solvability of the initial value problem of ordinary linear dif- ferential equations and we prove the existence of computable functions with divergent Fourier series. The focus of our investigation is mainly on in nite-dimensional separable Banach spaces, but also the nite- dimensional case, as well as the non-separable case, will be discussed.
Nutzung und Vervielfältigung:
Alle Rechte vorbehalten