1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Hahn_Banach/document/root.tex	Wed Jun 24 21:46:54 2009 +0200
     1.3 @@ -0,0 +1,83 @@
     1.4 +\documentclass[10pt,a4paper,twoside]{article}
     1.5 +\usepackage{graphicx}
     1.6 +\usepackage{latexsym,theorem}
     1.7 +\usepackage{isabelle,isabellesym}
     1.8 +\usepackage{pdfsetup} %last one!
     1.9 +
    1.10 +\isabellestyle{it}
    1.11 +\urlstyle{rm}
    1.12 +
    1.13 +\newcommand{\isasymsup}{\isamath{\sup\,}}
    1.14 +\newcommand{\skp}{\smallskip}
    1.15 +
    1.16 +
    1.17 +\begin{document}
    1.18 +
    1.19 +\pagestyle{headings}
    1.20 +\pagenumbering{arabic}
    1.21 +
    1.22 +\title{The Hahn-Banach Theorem \\ for Real Vector Spaces}
    1.23 +\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
    1.24 +\maketitle
    1.25 +
    1.26 +\begin{abstract}
    1.27 +  The Hahn-Banach Theorem is one of the most fundamental results in functional
    1.28 +  analysis. We present a fully formal proof of two versions of the theorem,
    1.29 +  one for general linear spaces and another for normed spaces.  This
    1.30 +  development is based on simply-typed classical set-theory, as provided by
    1.31 +  Isabelle/HOL.
    1.32 +\end{abstract}
    1.33 +
    1.34 +
    1.35 +\tableofcontents
    1.36 +\parindent 0pt \parskip 0.5ex
    1.37 +
    1.38 +\clearpage
    1.39 +\section{Preface}
    1.40 +
    1.41 +This is a fully formal proof of the Hahn-Banach Theorem. It closely follows
    1.42 +the informal presentation given in Heuser's textbook \cite[{\S} 36]{Heuser:1986}.
    1.43 +Another formal proof of the same theorem has been done in Mizar
    1.44 +\cite{Nowak:1993}.  A general overview of the relevance and history of the
    1.45 +Hahn-Banach Theorem is given by Narici and Beckenstein \cite{Narici:1996}.
    1.46 +
    1.47 +\medskip The document is structured as follows.  The first part contains
    1.48 +definitions of basic notions of linear algebra: vector spaces, subspaces,
    1.49 +normed spaces, continuous linear-forms, norm of functions and an order on
    1.50 +functions by domain extension.  The second part contains some lemmas about the
    1.51 +supremum (w.r.t.\ the function order) and extension of non-maximal functions.
    1.52 +With these preliminaries, the main proof of the theorem (in its two versions)
    1.53 +is conducted in the third part.  The dependencies of individual theories are
    1.54 +as follows.
    1.55 +
    1.56 +\begin{center}
    1.57 +  \includegraphics[scale=0.5]{session_graph}  
    1.58 +\end{center}
    1.59 +
    1.60 +\clearpage
    1.61 +\part {Basic Notions}
    1.62 +
    1.63 +\input{Bounds}
    1.64 +\input{Vector_Space}
    1.65 +\input{Subspace}
    1.66 +\input{Normed_Space}
    1.67 +\input{Linearform}
    1.68 +\input{Function_Order}
    1.69 +\input{Function_Norm}
    1.70 +\input{Zorn_Lemma}
    1.71 +
    1.72 +\clearpage
    1.73 +\part {Lemmas for the Proof}
    1.74 +
    1.75 +\input{Hahn_Banach_Sup_Lemmas}
    1.76 +\input{Hahn_Banach_Ext_Lemmas}
    1.77 +\input{Hahn_Banach_Lemmas}
    1.78 +
    1.79 +\clearpage
    1.80 +\part {The Main Proof}
    1.81 +
    1.82 +\input{Hahn_Banach}
    1.83 +\bibliographystyle{abbrv}
    1.84 +\bibliography{root}
    1.85 +
    1.86 +\end{document}