# HG changeset patch # User wenzelm # Date 940872283 -7200 # Node ID b50446a33c160d805c6e4a3473978d4b39b067f4 # Parent 9c20924de52c2b60c7f67a6c28d8f439d534cbfe update by Gertrud Bauer; diff -r 9c20924de52c -r b50446a33c16 src/HOL/Real/HahnBanach/FunctionNorm.thy --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Mon Oct 25 19:24:31 1999 +0200 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Mon Oct 25 19:24:43 1999 +0200 @@ -12,7 +12,7 @@ text{* A linearform $f$ on a normed vector space $(V, \norm{\cdot})$ is \emph{continous}, iff it is bounded, i.~e. \[\exists\ap c\in R.\ap \forall\ap x\in V.\ap -|f\ap x| \leq c \cdot \norm x.\] +|f\ap x| \leq c \cdot \norm x\] In our application no other functions than linearforms are considered, so we can define continous linearforms as follows: *}; @@ -48,15 +48,15 @@ is called the \emph{norm} of $f$. For the non-trivial vector space $V$ the norm can be defined as -\[\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x}. \] +\[\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x} \] -For the case that the vector space $V$ contains only the zero vector -set, the set $B$ this supremum is taken from would be empty, and any -real number is a supremum of $B$. So it must be guarateed that there -is an element in $B$. This element must be greater or equal $0$ so -that $\idt{function{\dsh}norm}$ has the norm properties. Furthermore -it does not have to change the norm in all other cases, so it must be -$0$, as all other elements of $B$ are greater or equal $0$. +For the case that the vector space $V$ contains only the $\zero$ +vector, the set $B$ this supremum is taken from would be empty, and +any real number is a supremum of $B$. So it must be guarateed that +there is an element in $B$. This element must be ${} \ge 0$ so that +$\idt{function{\dsh}norm}$ has the norm properties. Furthermore it +does not have to change the norm in all other cases, so it must be +$0$, as all other elements of $B$ are ${} \ge 0$. Thus $B$ is defined as follows. *}; @@ -250,7 +250,7 @@ txt{* The proof is by case analysis on $x$. *}; - show "?thesis"; + show ?thesis; proof (rule case_split); txt {* For the case $x = \zero$ the thesis follows diff -r 9c20924de52c -r b50446a33c16 src/HOL/Real/HahnBanach/FunctionOrder.thy --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Mon Oct 25 19:24:31 1999 +0200 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy Mon Oct 25 19:24:43 1999 +0200 @@ -12,11 +12,11 @@ text{* We define the \emph{graph} of a (real) function $f$ with the domain $F$ as the set -\begin{matharray}{l} -\{(x, f\ap x). \ap x:F\}. -\end{matharray} +\[ +\{(x, f\ap x). \ap x:F\} +\] So we are modelling partial functions by specifying the domain and -the mapping function. We use the notion 'function' also for the graph +the mapping function. We use the notion ``function'' also for the graph of a function. *}; diff -r 9c20924de52c -r b50446a33c16 src/HOL/Real/HahnBanach/HahnBanach.thy --- a/src/HOL/Real/HahnBanach/HahnBanach.thy Mon Oct 25 19:24:31 1999 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Mon Oct 25 19:24:43 1999 +0200 @@ -10,7 +10,7 @@ text {* We present the proof of two different versions of the Hahn-Banach - Theorem, closely following \cite{Heuser:1986}. + Theorem, closely following \cite[\S36]{Heuser:1986}. *}; subsection {* The case of general linear spaces *}; @@ -49,7 +49,7 @@ the union of all functions in the chain is again a norm preserving function. (The union is an upper bound for all elements. It is even the least upper bound, because every upper bound of $M$ - is also an upper bound for $\cup\; c$.) *}; + is also an upper bound for $\Union c$.) *}; have "!! c. [| c : chain M; EX x. x:c |] ==> Union c : M"; proof -; @@ -91,7 +91,7 @@ qed; qed; - txt {* According to Zorn's Lemma there exists + txt {* According to Zorn's Lemma there is a maximal norm-preserving extension $g\in M$. *}; with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x"; @@ -283,7 +283,7 @@ thus ?thesis; ..; qed; - txt {* We have shown, that $h$ can still be extended to + txt {* We have shown that $h$ can still be extended to some $h_0$, in contradiction to the assumption that $h$ is a maximal element. *}; @@ -293,7 +293,7 @@ thus ?thesis; by contradiction; qed; -txt{* It follows $H = E$ and the thesis can be shown. *}; +txt{* It follows $H = E$, and the thesis can be shown. *}; show "is_linearform E h & (ALL x:F. h x = f x) & (ALL x:E. h x <= p x)"; @@ -372,8 +372,8 @@ txt{* We define the function $p$ on $E$ as follows: \begin{matharray}{l} - p\ap x = \fnorm f * \norm x\\ - % p\ap x = \fnorm f * \fnorm x.\\ + p\ap x = \fnorm f \cdot \norm x\\ + % p\ap x = \fnorm f \cdot \fnorm x\\ \end{matharray} *}; @@ -408,7 +408,7 @@ finally; show ?thesis; .; qed; - txt{* Furthermore $p$ obeys the triangle inequation: *}; + txt{* Furthermore, $p$ obeys the triangle inequation: *}; show "p (x + y) <= p x + p y"; proof -; @@ -478,7 +478,7 @@ a solution for the inequation \begin{matharray}{l} - \forall\ap x\in E.\ap |g\ap x| \leq c * \norm x. + \forall\ap x\in E.\ap |g\ap x| \leq c \cdot \norm x \end{matharray} *}; have "ALL x:E. rabs (g x) <= function_norm F norm f * norm x"; diff -r 9c20924de52c -r b50446a33c16 src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Mon Oct 25 19:24:31 1999 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Mon Oct 25 19:24:43 1999 +0200 @@ -3,7 +3,7 @@ Author: Gertrud Bauer, TU Munich *) -header {* Extending a non-ma\-xi\-mal function *}; +header {* Extending a non-maximal function *}; theory HahnBanachExtLemmas = FunctionNorm:; @@ -30,7 +30,7 @@ \end{matharray} it suffices to show that \begin{matharray}{l} -\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v. +\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v \end{matharray} *}; @@ -84,7 +84,7 @@ show ?thesis; proof (intro exI conjI ballI); - txt {* For all $y\in F$ is $a\ap y \leq \xi$. *}; + txt {* For all $y\in F$ holds $a\ap y \leq \xi$. *}; fix y; assume y: "y:F"; show "a y <= xi"; @@ -93,7 +93,7 @@ qed (force!); next; - txt {* For all $y\in F$ is $\xi\leq b\ap y$. *}; + txt {* For all $y\in F$ holds $\xi\leq b\ap y$. *}; fix y; assume "y:F"; show "xi <= b y"; @@ -115,8 +115,8 @@ qed; qed; -text{* The function $h_0$ is defined as a linear extension of $h$ -to $H_0$. $h_0$ is linear. *}; +text{* The function $h_0$ is defined as a canonical linear extension +of $h$ to $H_0$. *}; lemma h0_lf: "[| h0 = (\x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H @@ -142,7 +142,7 @@ fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0"; txt{* We now have to show that $h_0$ is linear - w.~r.~t.~addition, i.~e.~ + w.~r.~t.~addition, i.~e.\ $h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$ for $x_1, x_2\in H$. *}; @@ -192,8 +192,8 @@ txt{* We further have to show that $h_0$ is linear w.~r.~t.~scalar multiplication, - i.~e.~ $c\in real$ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$ - for $x\in H$ and real $c$. + i.~e.\ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$ + for $x\in H$ and any real number $c$. *}; next; @@ -268,7 +268,7 @@ by (rule h0_definite); txt{* Now we show - $h\ap y + a * xi\leq p\ap (y\plus a \mult x_0)$ + $h\ap y + a \cdot xi\leq p\ap (y\plus a \mult x_0)$ by case analysis on $a$. *}; also; have "... <= p (y + a <*> x0)"; @@ -278,7 +278,7 @@ with vs y a; show ?thesis; by simp; txt {* In the case $a < 0$ we use $a_1$ with $y$ taken as - $\frac{y}{a}$. *}; + $y/a$. *}; next; assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp; @@ -308,7 +308,7 @@ thus ?thesis; by simp; txt {* In the case $a > 0$ we use $a_2$ with $y$ taken - as $\frac{y}{a}$. *}; + as $y/a$. *}; next; assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp; have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)"; diff -r 9c20924de52c -r b50446a33c16 src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Mon Oct 25 19:24:31 1999 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Mon Oct 25 19:24:43 1999 +0200 @@ -15,7 +15,7 @@ Let $E$ be a real vector space with a quasinorm $q$ on $E$. $F$ is a subspace of $E$ and $f$ a linearform on $F$. We consider a chain $c$ of norm preserving extensions of $f$, such that -$\cup\; c = \idt{graph}\ap H\ap h$. +$\Union c = \idt{graph}\ap H\ap h$. We will show some properties about the limit function $h$, i.~e.~the supremum of the chain $c$. *}; @@ -348,8 +348,8 @@ thus ?thesis; proof (elim UnionE chainE2); - txt{* Since both $(x, y) \in \cup\; c$ and $(x, z) \in cup c$ - they are menbers of some graphs $G_1$ and $G_2$, resp.~, such that + txt{* Since both $(x, y) \in \Union c$ and $(x, z) \in \Union c$ + they are members of some graphs $G_1$ and $G_2$, resp., such that both $G_1$ and $G_2$ are members of $c$*}; fix G1 G2; assume @@ -390,13 +390,11 @@ qed; qed; -text{* The limit function $h$ is linear: Every element $x$ -in the domain of $h$ is in the domain of -a function $h'$ in the chain of norm preserving extensions. -Futher $h$ is an extension of $h'$ so the value -of $x$ are identical for $h'$ and $h$. -Finally, the function $h'$ is linear by construction of $M$. -*}; +text{* The limit function $h$ is linear: every element $x$ in the +domain of $h$ is in the domain of a function $h'$ in the chain of norm +preserving extensions. Furthermore, $h$ is an extension of $h'$ so +the value of $x$ are identical for $h'$ and $h$. Finally, the +function $h'$ is linear by construction of $M$. *}; lemma sup_lf: "[| M = norm_pres_extensions E p F f; c: chain M; @@ -439,7 +437,7 @@ by (rule some_H'h'); txt{* We have to show that h is linear w.~r.~t. - skalar multiplication. *}; + scalar multiplication. *}; thus "h (a <*> x) = a * h x"; proof (elim exE conjE); @@ -494,10 +492,10 @@ qed; qed; -text{* The domain $H$ of the limit function is a superspace -of $F$, since $F$ is a subset of $H$. The existence of -the $\zero$ element in $F$ and the closeness properties -follow from the fact that $F$ is a vectorspace. *}; +text{* The domain $H$ of the limit function is a superspace of $F$, +since $F$ is a subset of $H$. The existence of the $\zero$ element in +$F$ and the closure properties follow from the fact that $F$ is a +vectorspace. *}; lemma sup_supF: "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; @@ -528,7 +526,7 @@ qed; qed; -text{* The domain $H$ of the limt function is a subspace +text{* The domain $H$ of the limit function is a subspace of $E$. *}; lemma sup_subE: @@ -588,7 +586,7 @@ qed; qed; - txt{* $H$ is closed under skalar multiplication. *}; + txt{* $H$ is closed under scalar multiplication. *}; show "ALL x:H. ALL a. a <*> x : H"; proof (intro ballI allI); @@ -610,8 +608,8 @@ qed; qed; -text {* The limit functon is bounded by -the norm $p$ as well, simce all elements in the chain are norm preserving. +text {* The limit function is bounded by +the norm $p$ as well, since all elements in the chain are norm preserving. *}; lemma sup_norm_pres: diff -r 9c20924de52c -r b50446a33c16 src/HOL/Real/HahnBanach/NormedSpace.thy --- a/src/HOL/Real/HahnBanach/NormedSpace.thy Mon Oct 25 19:24:31 1999 +0200 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Mon Oct 25 19:24:43 1999 +0200 @@ -72,7 +72,8 @@ subsection {* Norms *}; -text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only $\zero$ to $0$. *}; +text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only the +$\zero$ vector to $0$. *}; constdefs is_norm :: "['a::{minus, plus} set, 'a => real] => bool" diff -r 9c20924de52c -r b50446a33c16 src/HOL/Real/HahnBanach/README.html --- a/src/HOL/Real/HahnBanach/README.html Mon Oct 25 19:24:31 1999 +0200 +++ b/src/HOL/Real/HahnBanach/README.html Mon Oct 25 19:24:43 1999 +0200 @@ -1,6 +1,6 @@ HOL/Real/HahnBanach/README -

The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).

+

The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar).

Author: Gertrud Bauer, Technische Universität München

diff -r 9c20924de52c -r b50446a33c16 src/HOL/Real/HahnBanach/ROOT.ML --- a/src/HOL/Real/HahnBanach/ROOT.ML Mon Oct 25 19:24:31 1999 +0200 +++ b/src/HOL/Real/HahnBanach/ROOT.ML Mon Oct 25 19:24:43 1999 +0200 @@ -2,7 +2,7 @@ ID: $Id$ Author: Gertrud Bauer, TU Munich -The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar). +The Hahn-Banach theorem for real vector spaces (Isabelle/Isar). *) time_use_thy "Bounds"; diff -r 9c20924de52c -r b50446a33c16 src/HOL/Real/HahnBanach/Subspace.thy --- a/src/HOL/Real/HahnBanach/Subspace.thy Mon Oct 25 19:24:31 1999 +0200 +++ b/src/HOL/Real/HahnBanach/Subspace.thy Mon Oct 25 19:24:43 1999 +0200 @@ -213,9 +213,8 @@ instance set :: (plus) plus; by intro_classes; defs vs_sum_def: - "U + V == {x. EX u:U. EX v:V. x = u + v}"; + "U + V == {x. EX u:U. EX v:V. x = u + v}";(*** -(*** constdefs vs_sum :: "['a::{minus, plus} set, 'a set] => 'a set" (infixl "+" 65) @@ -318,7 +317,7 @@ text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero element is the only common element of $U$ and $V$. For every element $x$ of the direct sum of $U$ and $V$ the decomposition in -$x = u + v$ with $u:U$ and $v:V$ is unique.*}; +$x = u + v$ with $u \in U$ and $v \in V$ is unique.*}; lemma decomp: "[| is_vectorspace E; is_subspace U E; is_subspace V E; @@ -352,7 +351,7 @@ text {* An application of the previous lemma will be used in the proof of the Hahn-Banach theorem: for an element $y + a \mult x_0$ of the direct sum of a vectorspace $H$ and the linear closure of -$x_0$ the components $y:H$ and $a$ are unique. *}; +$x_0$ the components $y \in H$ and $a$ are unique. *}; lemma decomp_H0: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; @@ -426,7 +425,7 @@ text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$ are unique, so the function $h_0$ defined by -$h_0 (y \plus a \mult x_0) = h y + a * xi$ is definite. *}; +$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *}; lemma h0_definite: "[| h0 = (\x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H) diff -r 9c20924de52c -r b50446a33c16 src/HOL/Real/HahnBanach/VectorSpace.thy --- a/src/HOL/Real/HahnBanach/VectorSpace.thy Mon Oct 25 19:24:31 1999 +0200 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Mon Oct 25 19:24:43 1999 +0200 @@ -9,9 +9,10 @@ subsection {* Signature *}; -text {* For the definition of real vector spaces a type $\alpha$ is -considered, on which the operations addition and real scalar -multiplication are defined, and which has an zero element.*}; +text {* For the definition of real vector spaces a type $\alpha$ +of the sort $\idt{plus}, \idt{minus}$ is considered, on which a +real scalar multiplication $\mult$ is defined, and which has an zero +element $\zero$.*}; consts (*** @@ -24,8 +25,9 @@ prod :: "[real, 'a] => 'a" (infixr "\" 70) zero :: 'a ("\"); -text {* The unary and binary minus can be considered as +(* text {* The unary and binary minus can be considered as abbreviations: *}; +*) (*** constdefs @@ -37,15 +39,14 @@ subsection {* Vector space laws *}; -text {* A \emph{vector space} is a non-empty set $V$ of elements -from $\alpha$ with the following vector space laws: -The set $V$ is closed under addition and scalar multiplication, -addition is associative and commutative. $\minus x$ is the inverse -of $x$ w.~r.~t.~addition and $\zero$ is the neutral element of -addition. -Addition and multiplication are distributive. -Scalar multiplication is associative and the real $1$ is the neutral -element of scalar multiplication. +text {* A \emph{vector space} is a non-empty set $V$ of elements from + $\alpha$ with the following vector space laws: The set $V$ is closed + under addition and scalar multiplication, addition is associative + and commutative; $\minus x$ is the inverse of $x$ w.~r.~t.~addition + and $\zero$ is the neutral element of addition. Addition and + multiplication are distributive; scalar multiplication is + associative and the real $1$ is the neutral element of scalar + multiplication. *}; constdefs diff -r 9c20924de52c -r b50446a33c16 src/HOL/Real/HahnBanach/ZornLemma.thy --- a/src/HOL/Real/HahnBanach/ZornLemma.thy Mon Oct 25 19:24:31 1999 +0200 +++ b/src/HOL/Real/HahnBanach/ZornLemma.thy Mon Oct 25 19:24:43 1999 +0200 @@ -13,8 +13,8 @@ In our application $S$ is a set of sets, ordered by set inclusion. Since the union of a chain of sets is an upperbound for all elements of the chain, the conditions of Zorn's lemma can be modified: -If $S$ is non-empty, it suffices to show that for every non-empty -chain $c$ in $S$ the union of $c$ also lies in $S$: +if $S$ is non-empty, it suffices to show that for every non-empty +chain $c$ in $S$ the union of $c$ also lies in $S$. *}; theorem Zorn's_Lemma: @@ -35,7 +35,7 @@ assume "c={}"; with aS; show ?thesis; by fast; - txt{* If $c$ is non-empty, then $\cup\; c$ + txt{* If $c$ is non-empty, then $\Union c$ is an upperbound of $c$, that lies in $S$. *}; next; diff -r 9c20924de52c -r b50446a33c16 src/HOL/Real/HahnBanach/document/notation.tex --- a/src/HOL/Real/HahnBanach/document/notation.tex Mon Oct 25 19:24:31 1999 +0200 +++ b/src/HOL/Real/HahnBanach/document/notation.tex Mon Oct 25 19:24:43 1999 +0200 @@ -2,7 +2,7 @@ \renewcommand{\isamarkupheader}[1]{\section{#1}} \newcommand{\isasymbollambda}{${\mathtt{\lambda}}$} -\parindent 0pt \parskip 0.5ex + \newcommand{\name}[1]{\textsf{#1}} @@ -34,16 +34,17 @@ \newcommand{\Le}{\le} \newcommand{\Lt}{\lt} \newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;} -\newcommand{\ap}{\mathbin{\!}} +\newcommand{\ap}{\mathbin{}} +\newcommand{\Union}{\bigcup} -\newcommand{\norm}[1]{\|\, #1\,\|} -\newcommand{\fnorm}[1]{\|\, #1\,\|} -\newcommand{\zero}{{\mathord{\mathbf {0}}}} -\newcommand{\plus}{{\mathbin{\;\mathtt {+}\;}}} -\newcommand{\minus}{{\mathbin{\;\mathtt {-}\;}}} -\newcommand{\mult}{{\mathbin{\;\mathbf {\odot}\;}}} -\newcommand{\1}{{\mathord{\mathrm{1}}}} +\newcommand{\norm}[1]{\left\|#1\right\|} +\newcommand{\fnorm}[1]{\left\|#1\right\|} +\newcommand{\zero}{\mathord{\mathbf 0}} +\newcommand{\plus}{\mathbin{\mathbf +}} +\newcommand{\minus}{\mathbin{\mathbf -}} +\newcommand{\mult}{\mathbin{\mathbf\odot}} +\newcommand{\1}{\mathord{\mathrm{1}}} %\newcommand{\zero}{{\mathord{\small\sl\tt {<0>}}}} %\newcommand{\plus}{{\mathbin{\;\small\sl\tt {[+]}\;}}} %\newcommand{\minus}{{\mathbin{\;\small\sl\tt {[-]}\;}}} diff -r 9c20924de52c -r b50446a33c16 src/HOL/Real/HahnBanach/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/HahnBanach/document/root.bib Mon Oct 25 19:24:43 1999 +0200 @@ -0,0 +1,27 @@ + +@Book{Heuser:1986, + author = {H. Heuser}, + title = {Funktionalanalysis: Theorie und Anwendung}, + publisher = {Teubner}, + year = 1986 +} + +@InCollection{Narici:1996, + author = {L. Narici and E. Beckenstein}, + title = {The {Hahn-Banach Theorem}: The Life and Times}, + booktitle = {Topology Atlas}, + publisher = {York University, Toronto, Ontario, Canada}, + year = 1996, + note = {\url{http://at.yorku.ca/topology/preprint.htm} and + \url{http://at.yorku.ca/p/a/a/a/16.htm}} +} + +@Article{Nowak:1993, + author = {B. Nowak and A. Trybulec}, + title = {{Hahn-Banach} Theorem}, + journal = {Journal of Formalized Mathematics}, + year = {1993}, + volume = {5}, + institution = {University of Bialystok}, + note = {\url{http://mizar.uwb.edu.pl/JFM/Vol5/hahnban.html}} +} diff -r 9c20924de52c -r b50446a33c16 src/HOL/Real/HahnBanach/document/root.tex --- a/src/HOL/Real/HahnBanach/document/root.tex Mon Oct 25 19:24:31 1999 +0200 +++ b/src/HOL/Real/HahnBanach/document/root.tex Mon Oct 25 19:24:43 1999 +0200 @@ -12,32 +12,42 @@ \pagestyle{headings} \pagenumbering{arabic} -\title{The Hahn-Banach Theorem for Real Vectorspaces} +\title{The Hahn-Banach Theorem for Real Vector Spaces} \author{Gertrud Bauer} \maketitle \begin{abstract} -The Hahn-Banach theorem is one of the most important theorems -of functional analysis. We present the fully formal proof of two versions of -the theorem, one for general linear spaces and one for normed spaces -as a corollary of the first. - -The first part contains the definition of basic notions of -linear algebra, such as vector spaces, subspaces, normed spaces, -continous linearforms, norm of functions and an order on -functions by domain extension. - -The second part contains some lemmas about the supremum w.r.t. the -function order and the extension of a non-maximal function, -which are needed for the proof of the main theorem. - -The third part is the proof of the theorem in its two different versions. - + The Hahn-Banach theorem is one of the most fundamental results in functional + analysis. We present a fully formal proof of two versions of the theorem, + one for general linear spaces and another for normed spaces. This + development is based on simply-typed classical set-theory, as provided by + Isabelle/HOL. \end{abstract} + \tableofcontents +\parindent 0pt \parskip 0.5ex + +\clearpage +\section{Preface} -\part {Basic notions} +This is a fully formal proof of the Hahn-Banach theorem. It closely follows +the informal presentation given in the textbook \cite[\S 36]{Heuser:1986}. +Another formal proof of the same theorem has been done in Mizar +\cite{Nowak:1993}. A general overview of the relevance and history of the +Hahn-Banach theorem is given in \cite{Narici:1996}. + +\medskip The document is structured as follows. The first part contains +definitions of basic notions of linear algebra: vector spaces, subspaces, +normed spaces, continuous linearforms, norm of functions and an order on +functions by domain extension. The second part contains some lemmas about the +supremum (w.r.t.\ the function order) and extension of non-maximal functions. +With these preliminaries, the main proof of the theorem (in its two versions) +is conducted in the third part. + + +\clearpage +\part {Basic Notions} \input{Bounds.tex} \input{Aux.tex} @@ -49,15 +59,17 @@ \input{FunctionNorm.tex} \input{ZornLemma.tex} -\part {Lemmas for the proof} +\clearpage +\part {Lemmas for the Proof} \input{HahnBanachSupLemmas.tex} \input{HahnBanachExtLemmas.tex} -\part {The proof} +\clearpage +\part {The Main Proof} \input{HahnBanach.tex} \bibliographystyle{abbrv} -\bibliography{bib} +\bibliography{root} \end{document}