7747
|
1 |
|
7917
|
2 |
\documentclass[11pt,a4paper,twoside]{article}
|
|
3 |
|
|
4 |
\usepackage{comment}
|
|
5 |
\usepackage{latexsym,theorem}
|
|
6 |
\usepackage{isabelle,pdfsetup} %last one!
|
7978
|
7 |
\usepackage{bbb}
|
7747
|
8 |
|
7808
|
9 |
\input{notation}
|
|
10 |
|
7747
|
11 |
\begin{document}
|
|
12 |
|
7917
|
13 |
\pagestyle{headings}
|
|
14 |
\pagenumbering{arabic}
|
|
15 |
|
7927
|
16 |
\title{The Hahn-Banach Theorem for Real Vector Spaces}
|
7978
|
17 |
|
|
18 |
\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
|
|
19 |
\maketitle
|
7747
|
20 |
\maketitle
|
|
21 |
|
7808
|
22 |
\begin{abstract}
|
7978
|
23 |
The Hahn-Banach Theorem is one of the most fundamental results in functional
|
7927
|
24 |
analysis. We present a fully formal proof of two versions of the theorem,
|
|
25 |
one for general linear spaces and another for normed spaces. This
|
|
26 |
development is based on simply-typed classical set-theory, as provided by
|
|
27 |
Isabelle/HOL.
|
7808
|
28 |
\end{abstract}
|
|
29 |
|
7927
|
30 |
|
7808
|
31 |
\tableofcontents
|
7927
|
32 |
\parindent 0pt \parskip 0.5ex
|
|
33 |
|
|
34 |
\clearpage
|
|
35 |
\section{Preface}
|
7808
|
36 |
|
7978
|
37 |
This is a fully formal proof of the Hahn-Banach Theorem. It closely follows
|
7927
|
38 |
the informal presentation given in the textbook \cite[\S 36]{Heuser:1986}.
|
|
39 |
Another formal proof of the same theorem has been done in Mizar
|
|
40 |
\cite{Nowak:1993}. A general overview of the relevance and history of the
|
7978
|
41 |
Hahn-Banach Theorem is given in \cite{Narici:1996}.
|
7927
|
42 |
|
|
43 |
\medskip The document is structured as follows. The first part contains
|
|
44 |
definitions of basic notions of linear algebra: vector spaces, subspaces,
|
|
45 |
normed spaces, continuous linearforms, norm of functions and an order on
|
|
46 |
functions by domain extension. The second part contains some lemmas about the
|
|
47 |
supremum (w.r.t.\ the function order) and extension of non-maximal functions.
|
|
48 |
With these preliminaries, the main proof of the theorem (in its two versions)
|
|
49 |
is conducted in the third part.
|
|
50 |
|
|
51 |
|
|
52 |
\clearpage
|
|
53 |
\part {Basic Notions}
|
7917
|
54 |
|
|
55 |
\input{Bounds.tex}
|
|
56 |
\input{Aux.tex}
|
|
57 |
\input{VectorSpace.tex}
|
|
58 |
\input{Subspace.tex}
|
|
59 |
\input{NormedSpace.tex}
|
|
60 |
\input{Linearform.tex}
|
|
61 |
\input{FunctionOrder.tex}
|
|
62 |
\input{FunctionNorm.tex}
|
|
63 |
\input{ZornLemma.tex}
|
|
64 |
|
7927
|
65 |
\clearpage
|
|
66 |
\part {Lemmas for the Proof}
|
7917
|
67 |
|
|
68 |
\input{HahnBanachSupLemmas.tex}
|
|
69 |
\input{HahnBanachExtLemmas.tex}
|
|
70 |
|
7927
|
71 |
\clearpage
|
|
72 |
\part {The Main Proof}
|
7917
|
73 |
|
|
74 |
\input{HahnBanach.tex}
|
|
75 |
\bibliographystyle{abbrv}
|
7927
|
76 |
\bibliography{root}
|
7747
|
77 |
|
|
78 |
\end{document}
|