author | wenzelm |
Mon, 19 Oct 2015 17:45:36 +0200 | |
changeset 61486 | 3590367b0ce9 |
parent 31795 | be3e1cc5005c |
child 61540 | f92bf6674699 |
permissions | -rw-r--r-- |
9375 | 1 |
\documentclass[10pt,a4paper,twoside]{article} |
11851 | 2 |
\usepackage{graphicx} |
7917 | 3 |
\usepackage{latexsym,theorem} |
10687 | 4 |
\usepackage{isabelle,isabellesym} |
7984 | 5 |
\usepackage{pdfsetup} %last one! |
10687 | 6 |
|
7 |
\isabellestyle{it} |
|
9659 | 8 |
\urlstyle{rm} |
7747 | 9 |
|
10687 | 10 |
\newcommand{\isasymsup}{\isamath{\sup\,}} |
11 |
||
7808 | 12 |
|
7747 | 13 |
\begin{document} |
14 |
||
7917 | 15 |
\pagestyle{headings} |
16 |
\pagenumbering{arabic} |
|
17 |
||
11851 | 18 |
\title{The Hahn-Banach Theorem \\ for Real Vector Spaces} |
7978 | 19 |
\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}} |
20 |
\maketitle |
|
7747 | 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 |
15084 | 38 |
the informal presentation given in Heuser's textbook \cite[{\S} 36]{Heuser:1986}. |
7927 | 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 |
|
15084 | 41 |
Hahn-Banach Theorem is given by Narici and Beckenstein \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, |
|
11851 | 45 |
normed spaces, continuous linear-forms, norm of functions and an order on |
7927 | 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) |
|
11851 | 49 |
is conducted in the third part. The dependencies of individual theories are |
50 |
as follows. |
|
7927 | 51 |
|
11851 | 52 |
\begin{center} |
13548 | 53 |
\includegraphics[scale=0.5]{session_graph} |
11851 | 54 |
\end{center} |
7927 | 55 |
|
56 |
\clearpage |
|
57 |
\part {Basic Notions} |
|
7917 | 58 |
|
10687 | 59 |
\input{Bounds} |
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset
|
60 |
\input{Vector_Space} |
10687 | 61 |
\input{Subspace} |
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset
|
62 |
\input{Normed_Space} |
10687 | 63 |
\input{Linearform} |
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset
|
64 |
\input{Function_Order} |
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset
|
65 |
\input{Function_Norm} |
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset
|
66 |
\input{Zorn_Lemma} |
7917 | 67 |
|
7927 | 68 |
\clearpage |
69 |
\part {Lemmas for the Proof} |
|
7917 | 70 |
|
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset
|
71 |
\input{Hahn_Banach_Sup_Lemmas} |
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset
|
72 |
\input{Hahn_Banach_Ext_Lemmas} |
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset
|
73 |
\input{Hahn_Banach_Lemmas} |
7917 | 74 |
|
7927 | 75 |
\clearpage |
76 |
\part {The Main Proof} |
|
7917 | 77 |
|
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset
|
78 |
\input{Hahn_Banach} |
7917 | 79 |
\bibliographystyle{abbrv} |
7927 | 80 |
\bibliography{root} |
7747 | 81 |
|
82 |
\end{document} |