|
|
Computability of Banach Space Principles
Vasco Brattka, Informatik-Bericht 286, FernUniversität Hagen, 2001
Abstract
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 Theorem, the Theorem
on Condensation of Singularities and the
Banach-Steinhaus Theorem.
From the computational point of view these theorems 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 analysis but the picture that we can
draw in computable analysis differs in several points.
On the one hand, computable analysis is based on classical
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 version of Banach's Inverse Mapping
Theorem states that the inverse T -1 of a linear computable and
bijective operator T from a computable Banach space into a
computable Banach space is computable too, whereas the mapping
T-> T -1 itself is not computable.
Thus, there is no general 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 effective solvability of the
initial value problem of ordinary linear differential equations and
we prove the existence of computable functions with divergent Fourier series.
The focus of our investigation is mainly on infinite-dimensional separable
Banach spaces, but also the finite-dimensional case, as well as the
non-separable case, will be discussed.
Survey on some Results
1. Open Mapping Theorem
2. Banach's Inverse Mapping Theorem
3. Closed Graph Theorem
Electronical Versions
