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