author wenzelm Mon Oct 25 19:24:43 1999 +0200 (1999-10-25) changeset 7927 b50446a33c16 parent 7926 9c20924de52c child 7928 06a11f8cf573
update by Gertrud Bauer;
     1.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Mon Oct 25 19:24:31 1999 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Mon Oct 25 19:24:43 1999 +0200
1.3 @@ -12,7 +12,7 @@
1.4  text{* A linearform $f$ on a normed vector space $(V, \norm{\cdot})$
1.5  is \emph{continous}, iff it is bounded, i.~e.
1.6  $\exists\ap c\in R.\ap \forall\ap x\in V.\ap 1.7 -|f\ap x| \leq c \cdot \norm x.$
1.8 +|f\ap x| \leq c \cdot \norm x\]
1.9  In our application no other functions than linearforms are considered,
1.10  so we can define continous linearforms as follows:
1.11  *};
1.12 @@ -48,15 +48,15 @@
1.13  is called the \emph{norm} of $f$.
1.14
1.15  For the non-trivial vector space $V$ the norm can be defined as
1.16 -$\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x}.$
1.17 +$\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x}$
1.18
1.19 -For the case that the vector space $V$ contains only the zero vector
1.20 -set, the set $B$ this supremum is taken from would be empty, and any
1.21 -real number is a supremum of $B$. So it must be guarateed that there
1.22 -is an element in $B$. This element must be greater or equal $0$ so
1.23 -that $\idt{function{\dsh}norm}$ has the norm properties. Furthermore
1.24 -it does not have to change the norm in all other cases, so it must be
1.25 -$0$, as all other elements of $B$ are greater or equal $0$.
1.26 +For the case that the vector space $V$ contains only the $\zero$
1.27 +vector, the set $B$ this supremum is taken from would be empty, and
1.28 +any real number is a supremum of $B$. So it must be guarateed that
1.29 +there is an element in $B$. This element must be ${} \ge 0$ so that
1.30 +$\idt{function{\dsh}norm}$ has the norm properties. Furthermore it
1.31 +does not have to change the norm in all other cases, so it must be
1.32 +$0$, as all other elements of $B$ are ${} \ge 0$.
1.33
1.34  Thus $B$ is defined as follows.
1.35  *};
1.36 @@ -250,7 +250,7 @@
1.37
1.38   txt{* The proof is by case analysis on $x$. *};
1.39
1.40 -  show "?thesis";
1.41 +  show ?thesis;
1.42    proof (rule case_split);
1.43
1.44      txt {* For the case $x = \zero$ the thesis follows

     2.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Mon Oct 25 19:24:31 1999 +0200
2.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Mon Oct 25 19:24:43 1999 +0200
2.3 @@ -12,11 +12,11 @@
2.4
2.5  text{* We define the \emph{graph} of a (real) function $f$ with the
2.6  domain $F$ as the set
2.7 -\begin{matharray}{l}
2.8 -\{(x, f\ap x). \ap x:F\}.
2.9 -\end{matharray}
2.10 +$2.11 +\{(x, f\ap x). \ap x:F\} 2.12 +$
2.13  So we are modelling partial functions by specifying the domain and
2.14 -the mapping function. We use the notion 'function' also for the graph
2.15 +the mapping function. We use the notion function'' also for the graph
2.16  of a function.
2.17  *};
2.18

     3.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Oct 25 19:24:31 1999 +0200
3.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Oct 25 19:24:43 1999 +0200
3.3 @@ -10,7 +10,7 @@
3.4
3.5  text {*
3.6    We present the proof of two different versions of the Hahn-Banach
3.7 -  Theorem, closely following \cite{Heuser:1986}.
3.8 +  Theorem, closely following \cite[\S36]{Heuser:1986}.
3.9  *};
3.10
3.11  subsection {* The case of general linear spaces *};
3.12 @@ -49,7 +49,7 @@
3.13    the union of all functions in the chain is again a norm preserving
3.14    function. (The union is an upper bound for all elements.
3.15    It is even the least upper bound, because every upper bound of $M$
3.16 -  is also an upper bound for $\cup\; c$.) *};
3.17 +  is also an upper bound for $\Union c$.) *};
3.18
3.19    have "!! c. [| c : chain M; EX x. x:c |] ==> Union c : M";
3.20    proof -;
3.21 @@ -91,7 +91,7 @@
3.22      qed;
3.23    qed;
3.24
3.25 -  txt {* According to Zorn's Lemma there exists
3.26 +  txt {* According to Zorn's Lemma there is
3.27    a maximal norm-preserving extension $g\in M$. *};
3.28
3.29    with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x";
3.30 @@ -283,7 +283,7 @@
3.31      thus ?thesis; ..;
3.32    qed;
3.33
3.34 -  txt {* We have shown, that $h$ can still be extended to
3.35 +  txt {* We have shown that $h$ can still be extended to
3.36    some $h_0$, in contradiction to the assumption that
3.37    $h$ is a maximal element. *};
3.38
3.39 @@ -293,7 +293,7 @@
3.41  qed;
3.42
3.43 -txt{* It follows $H = E$ and the thesis can be shown. *};
3.44 +txt{* It follows $H = E$, and the thesis can be shown. *};
3.45
3.46  show "is_linearform E h & (ALL x:F. h x = f x)
3.47       & (ALL x:E. h x <= p x)";
3.48 @@ -372,8 +372,8 @@
3.49
3.50    txt{* We define the function $p$ on $E$ as follows:
3.51    \begin{matharray}{l}
3.52 -  p\ap x = \fnorm f * \norm x\\
3.53 -  % p\ap x = \fnorm f * \fnorm x.\\
3.54 +  p\ap x = \fnorm f \cdot \norm x\\
3.55 +  % p\ap x = \fnorm f \cdot \fnorm x\\
3.56    \end{matharray}
3.57    *};
3.58
3.59 @@ -408,7 +408,7 @@
3.60        finally; show ?thesis; .;
3.61      qed;
3.62
3.63 -    txt{* Furthermore $p$ obeys the triangle inequation: *};
3.64 +    txt{* Furthermore, $p$ obeys the triangle inequation: *};
3.65
3.66      show "p (x + y) <= p x + p y";
3.67      proof -;
3.68 @@ -478,7 +478,7 @@
3.69          a solution
3.70          for the inequation
3.71          \begin{matharray}{l}
3.72 -        \forall\ap x\in E.\ap |g\ap x| \leq c * \norm x.
3.73 +        \forall\ap x\in E.\ap |g\ap x| \leq c \cdot \norm x
3.74          \end{matharray} *};
3.75
3.76          have "ALL x:E. rabs (g x) <= function_norm F norm f * norm x";

     4.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Mon Oct 25 19:24:31 1999 +0200
4.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Mon Oct 25 19:24:43 1999 +0200
4.3 @@ -3,7 +3,7 @@
4.4      Author:     Gertrud Bauer, TU Munich
4.5  *)
4.6
4.7 -header {* Extending a non-ma\-xi\-mal function *};
4.8 +header {* Extending a non-maximal function *};
4.9
4.10  theory HahnBanachExtLemmas = FunctionNorm:;
4.11
4.12 @@ -30,7 +30,7 @@
4.13  \end{matharray}
4.14  it suffices to show that
4.15  \begin{matharray}{l}
4.16 -\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v.
4.17 +\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v
4.18  \end{matharray}
4.19  *};
4.20
4.21 @@ -84,7 +84,7 @@
4.22      show ?thesis;
4.23      proof (intro exI conjI ballI);
4.24
4.25 -      txt {* For all $y\in F$ is $a\ap y \leq \xi$. *};
4.26 +      txt {* For all $y\in F$ holds $a\ap y \leq \xi$. *};
4.27
4.28        fix y; assume y: "y:F";
4.29        show "a y <= xi";
4.30 @@ -93,7 +93,7 @@
4.31        qed (force!);
4.32      next;
4.33
4.34 -      txt {* For all $y\in F$ is $\xi\leq b\ap y$. *};
4.35 +      txt {* For all $y\in F$ holds $\xi\leq b\ap y$. *};
4.36
4.37        fix y; assume "y:F";
4.38        show "xi <= b y";
4.39 @@ -115,8 +115,8 @@
4.40    qed;
4.41  qed;
4.42
4.43 -text{* The function $h_0$ is defined as a linear extension of $h$
4.44 -to $H_0$. $h_0$ is linear. *};
4.45 +text{* The function $h_0$ is defined as a canonical linear extension
4.46 +of $h$ to $H_0$. *};
4.47
4.48  lemma h0_lf:
4.49    "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
4.50 @@ -142,7 +142,7 @@
4.51      fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0";
4.52
4.53      txt{* We now have to show that $h_0$ is linear
4.56      $h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$
4.57      for $x_1, x_2\in H$. *};
4.58
4.59 @@ -192,8 +192,8 @@
4.60
4.61      txt{* We further have to show that $h_0$ is linear
4.62      w.~r.~t.~scalar multiplication,
4.63 -    i.~e.~ $c\in real$ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
4.64 -    for $x\in H$ and real $c$.
4.65 +    i.~e.\ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
4.66 +    for $x\in H$ and any real number $c$.
4.67      *};
4.68
4.69    next;
4.70 @@ -268,7 +268,7 @@
4.71        by (rule h0_definite);
4.72
4.73      txt{* Now we show
4.74 -    $h\ap y + a * xi\leq p\ap (y\plus a \mult x_0)$
4.75 +    $h\ap y + a \cdot xi\leq p\ap (y\plus a \mult x_0)$
4.76      by case analysis on $a$. *};
4.77
4.78      also; have "... <= p (y + a <*> x0)";
4.79 @@ -278,7 +278,7 @@
4.80        with vs y a; show ?thesis; by simp;
4.81
4.82      txt {* In the case $a < 0$ we use $a_1$ with $y$ taken as
4.83 -    $\frac{y}{a}$. *};
4.84 +    $y/a$. *};
4.85
4.86      next;
4.87        assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
4.88 @@ -308,7 +308,7 @@
4.89        thus ?thesis; by simp;
4.90
4.91        txt {* In the case $a > 0$ we use $a_2$ with $y$ taken
4.92 -      as $\frac{y}{a}$. *};
4.93 +      as $y/a$. *};
4.94      next;
4.95        assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
4.96        have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)";

     5.1 --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Mon Oct 25 19:24:31 1999 +0200
5.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Mon Oct 25 19:24:43 1999 +0200
5.3 @@ -15,7 +15,7 @@
5.4  Let $E$ be a real vector space with a quasinorm $q$ on $E$.
5.5  $F$ is a subspace of $E$ and $f$ a linearform on $F$. We
5.6  consider a chain $c$ of norm preserving extensions of $f$, such that
5.7 -$\cup\; c = \idt{graph}\ap H\ap h$.
5.8 +$\Union c = \idt{graph}\ap H\ap h$.
5.9  We will show some properties about the limit function $h$,
5.10  i.~e.~the supremum of the chain $c$.
5.11  *};
5.12 @@ -348,8 +348,8 @@
5.13    thus ?thesis;
5.14    proof (elim UnionE chainE2);
5.15
5.16 -    txt{* Since both $(x, y) \in \cup\; c$ and $(x, z) \in cup c$
5.17 -    they are menbers of some graphs $G_1$ and $G_2$, resp.~, such that
5.18 +    txt{* Since both $(x, y) \in \Union c$ and $(x, z) \in \Union c$
5.19 +    they are members of some graphs $G_1$ and $G_2$, resp., such that
5.20      both $G_1$ and $G_2$ are members of $c$*};
5.21
5.22      fix G1 G2; assume
5.23 @@ -390,13 +390,11 @@
5.24    qed;
5.25  qed;
5.26
5.27 -text{* The limit function $h$ is linear: Every element $x$
5.28 -in the domain of $h$ is in the domain of
5.29 -a function $h'$ in the chain of norm preserving extensions.
5.30 -Futher $h$ is an extension of $h'$ so the value
5.31 -of $x$ are identical for $h'$ and $h$.
5.32 -Finally, the function $h'$ is linear by construction of $M$.
5.33 -*};
5.34 +text{* The limit function $h$ is linear: every element $x$ in the
5.35 +domain of $h$ is in the domain of a function $h'$ in the chain of norm
5.36 +preserving extensions.  Furthermore, $h$ is an extension of $h'$ so
5.37 +the value of $x$ are identical for $h'$ and $h$.  Finally, the
5.38 +function $h'$ is linear by construction of $M$.  *};
5.39
5.40  lemma sup_lf:
5.41    "[| M = norm_pres_extensions E p F f; c: chain M;
5.42 @@ -439,7 +437,7 @@
5.43        by (rule some_H'h');
5.44
5.45      txt{* We have to show that h is linear w.~r.~t.
5.46 -    skalar multiplication. *};
5.47 +    scalar multiplication. *};
5.48
5.49      thus "h (a <*> x) = a * h x";
5.50      proof (elim exE conjE);
5.51 @@ -494,10 +492,10 @@
5.52    qed;
5.53  qed;
5.54
5.55 -text{* The domain $H$ of the limit function is a superspace
5.56 -of $F$, since $F$ is a subset of $H$. The existence of
5.57 -the $\zero$ element in $F$ and the closeness properties
5.58 -follow from the fact that $F$ is a vectorspace. *};
5.59 +text{* The domain $H$ of the limit function is a superspace of $F$,
5.60 +since $F$ is a subset of $H$. The existence of the $\zero$ element in
5.61 +$F$ and the closure properties follow from the fact that $F$ is a
5.62 +vectorspace. *};
5.63
5.64  lemma sup_supF:
5.65    "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
5.66 @@ -528,7 +526,7 @@
5.67    qed;
5.68  qed;
5.69
5.70 -text{* The domain $H$ of the limt function is a subspace
5.71 +text{* The domain $H$ of the limit function is a subspace
5.72  of $E$. *};
5.73
5.74  lemma sup_subE:
5.75 @@ -588,7 +586,7 @@
5.76        qed;
5.77      qed;
5.78
5.79 -    txt{* $H$ is closed under skalar multiplication. *};
5.80 +    txt{* $H$ is closed under scalar multiplication. *};
5.81
5.82      show "ALL x:H. ALL a. a <*> x : H";
5.83      proof (intro ballI allI);
5.84 @@ -610,8 +608,8 @@
5.85    qed;
5.86  qed;
5.87
5.88 -text {* The limit functon is bounded by
5.89 -the norm $p$ as well, simce all elements in the chain are norm preserving.
5.90 +text {* The limit function is bounded by
5.91 +the norm $p$ as well, since all elements in the chain are norm preserving.
5.92  *};
5.93
5.94  lemma sup_norm_pres:

     6.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Oct 25 19:24:31 1999 +0200
6.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Oct 25 19:24:43 1999 +0200
6.3 @@ -72,7 +72,8 @@
6.4
6.5  subsection {* Norms *};
6.6
6.7 -text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only $\zero$ to $0$. *};
6.8 +text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only the
6.9 +$\zero$ vector to $0$. *};
6.10
6.11  constdefs
6.12    is_norm :: "['a::{minus, plus} set, 'a => real] => bool"

     7.1 --- a/src/HOL/Real/HahnBanach/README.html	Mon Oct 25 19:24:31 1999 +0200
7.2 +++ b/src/HOL/Real/HahnBanach/README.html	Mon Oct 25 19:24:43 1999 +0200
7.3 @@ -1,6 +1,6 @@
7.5
7.6 -<H3> The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).</H3>
7.7 +<H3> The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar).</H3>
7.8
7.9  Author:     Gertrud Bauer, Technische Universit&auml;t M&uuml;nchen<P>
7.10

     8.1 --- a/src/HOL/Real/HahnBanach/ROOT.ML	Mon Oct 25 19:24:31 1999 +0200
8.2 +++ b/src/HOL/Real/HahnBanach/ROOT.ML	Mon Oct 25 19:24:43 1999 +0200
8.3 @@ -2,7 +2,7 @@
8.4      ID:         $Id$
8.5      Author:     Gertrud Bauer, TU Munich
8.6
8.7 -The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
8.8 +The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
8.9  *)
8.10
8.11  time_use_thy "Bounds";

     9.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Mon Oct 25 19:24:31 1999 +0200
9.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Mon Oct 25 19:24:43 1999 +0200
9.3 @@ -213,9 +213,8 @@
9.4  instance set :: (plus) plus; by intro_classes;
9.5
9.6  defs vs_sum_def:
9.7 -  "U + V == {x. EX u:U. EX v:V. x = u + v}";
9.8 +  "U + V == {x. EX u:U. EX v:V. x = u + v}";(***
9.9
9.10 -(***
9.11  constdefs
9.12    vs_sum ::
9.13    "['a::{minus, plus} set, 'a set] => 'a set"         (infixl "+" 65)
9.14 @@ -318,7 +317,7 @@
9.15  text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero
9.16  element is the only common element of $U$ and $V$. For every element
9.17  $x$ of the direct sum of $U$ and $V$ the decomposition in
9.18 -$x = u + v$ with $u:U$ and $v:V$ is unique.*};
9.19 +$x = u + v$ with $u \in U$ and $v \in V$ is unique.*};
9.20
9.21  lemma decomp:
9.22    "[| is_vectorspace E; is_subspace U E; is_subspace V E;
9.23 @@ -352,7 +351,7 @@
9.24  text {* An application of the previous lemma will be used in the
9.25  proof of the Hahn-Banach theorem: for an element $y + a \mult x_0$
9.26  of the direct sum of a vectorspace $H$ and the linear closure of
9.27 -$x_0$ the components $y:H$ and $a$ are unique. *};
9.28 +$x_0$ the components $y \in H$ and $a$ are unique. *};
9.29
9.30  lemma decomp_H0:
9.31    "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H;
9.32 @@ -426,7 +425,7 @@
9.33
9.34  text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$
9.35  are unique, so the function $h_0$ defined by
9.36 -$h_0 (y \plus a \mult x_0) = h y + a * xi$ is definite. *};
9.37 +$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
9.38
9.39  lemma h0_definite:
9.40    "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)

    10.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Mon Oct 25 19:24:31 1999 +0200
10.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Mon Oct 25 19:24:43 1999 +0200
10.3 @@ -9,9 +9,10 @@
10.4
10.5  subsection {* Signature *};
10.6
10.7 -text {* For the definition of real vector spaces a type $\alpha$ is
10.8 -considered, on which the operations addition and real scalar
10.9 -multiplication are defined, and which has an zero element.*};
10.10 +text {* For the definition of real vector spaces a type $\alpha$
10.11 +of the sort $\idt{plus}, \idt{minus}$ is considered, on which a
10.12 +real scalar multiplication $\mult$ is defined, and which has an zero
10.13 +element $\zero$.*};
10.14
10.15  consts
10.16  (***
10.17 @@ -24,8 +25,9 @@
10.18    prod  :: "[real, 'a] => 'a"                       (infixr "\<prod>" 70)
10.19    zero  :: 'a                                       ("\<zero>");
10.20
10.21 -text {* The unary and binary minus can be considered as
10.22 +(* text {* The unary and binary minus can be considered as
10.23  abbreviations: *};
10.24 +*)
10.25
10.26  (***
10.27  constdefs
10.28 @@ -37,15 +39,14 @@
10.29
10.30  subsection {* Vector space laws *};
10.31
10.32 -text {* A \emph{vector space} is a non-empty set $V$ of elements
10.33 -from $\alpha$ with the following vector space laws:
10.34 -The set $V$ is closed under addition and scalar multiplication,
10.35 -addition is associative and  commutative. $\minus x$ is the inverse
10.36 -of $x$ w.~r.~t.~addition and $\zero$ is the neutral element of
10.38 -Addition and multiplication are distributive.
10.39 -Scalar multiplication is associative and the real $1$ is the neutral
10.40 -element of scalar multiplication.
10.41 +text {* A \emph{vector space} is a non-empty set $V$ of elements from
10.42 +  $\alpha$ with the following vector space laws: The set $V$ is closed
10.44 +  and commutative; $\minus x$ is the inverse of $x$ w.~r.~t.~addition
10.45 +  and $\zero$ is the neutral element of addition.  Addition and
10.46 +  multiplication are distributive; scalar multiplication is
10.47 +  associative and the real $1$ is the neutral element of scalar
10.48 +  multiplication.
10.49  *};
10.50
10.51  constdefs

    11.1 --- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Mon Oct 25 19:24:31 1999 +0200
11.2 +++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Mon Oct 25 19:24:43 1999 +0200
11.3 @@ -13,8 +13,8 @@
11.4  In our application $S$ is a set of sets, ordered by set inclusion. Since
11.5  the union of a chain of sets is an upperbound for all elements of the
11.6  chain, the conditions of Zorn's lemma can be modified:
11.7 -If $S$ is non-empty, it suffices to show that for every non-empty
11.8 -chain $c$ in $S$ the union of $c$ also lies in $S$:
11.9 +if $S$ is non-empty, it suffices to show that for every non-empty
11.10 +chain $c$ in $S$ the union of $c$ also lies in $S$.
11.11  *};
11.12
11.13  theorem Zorn's_Lemma:
11.14 @@ -35,7 +35,7 @@
11.15        assume "c={}";
11.16        with aS; show ?thesis; by fast;
11.17
11.18 -      txt{* If $c$ is non-empty, then $\cup\; c$
11.19 +      txt{* If $c$ is non-empty, then $\Union c$
11.20        is an upperbound of $c$, that lies in $S$. *};
11.21
11.22      next;

    12.1 --- a/src/HOL/Real/HahnBanach/document/notation.tex	Mon Oct 25 19:24:31 1999 +0200
12.2 +++ b/src/HOL/Real/HahnBanach/document/notation.tex	Mon Oct 25 19:24:43 1999 +0200
12.3 @@ -2,7 +2,7 @@
12.5  \newcommand{\isasymbollambda}{${\mathtt{\lambda}}$}
12.6
12.7 -\parindent 0pt \parskip 0.5ex
12.8 +
12.9
12.10  \newcommand{\name}[1]{\textsf{#1}}
12.11
12.12 @@ -34,16 +34,17 @@
12.13  \newcommand{\Le}{\le}
12.14  \newcommand{\Lt}{\lt}
12.15  \newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
12.16 -\newcommand{\ap}{\mathbin{\!}}
12.17 +\newcommand{\ap}{\mathbin{}}
12.18 +\newcommand{\Union}{\bigcup}
12.19
12.20
12.21 -\newcommand{\norm}[1]{\|\, #1\,\|}
12.22 -\newcommand{\fnorm}[1]{\|\, #1\,\|}
12.23 -\newcommand{\zero}{{\mathord{\mathbf {0}}}}
12.24 -\newcommand{\plus}{{\mathbin{\;\mathtt {+}\;}}}
12.25 -\newcommand{\minus}{{\mathbin{\;\mathtt {-}\;}}}
12.26 -\newcommand{\mult}{{\mathbin{\;\mathbf {\odot}\;}}}
12.27 -\newcommand{\1}{{\mathord{\mathrm{1}}}}
12.28 +\newcommand{\norm}[1]{\left\|#1\right\|}
12.29 +\newcommand{\fnorm}[1]{\left\|#1\right\|}
12.30 +\newcommand{\zero}{\mathord{\mathbf 0}}
12.31 +\newcommand{\plus}{\mathbin{\mathbf +}}
12.32 +\newcommand{\minus}{\mathbin{\mathbf -}}
12.33 +\newcommand{\mult}{\mathbin{\mathbf\odot}}
12.34 +\newcommand{\1}{\mathord{\mathrm{1}}}
12.35  %\newcommand{\zero}{{\mathord{\small\sl\tt {<0>}}}}
12.36  %\newcommand{\plus}{{\mathbin{\;\small\sl\tt {[+]}\;}}}
12.37  %\newcommand{\minus}{{\mathbin{\;\small\sl\tt {[-]}\;}}}

    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/HOL/Real/HahnBanach/document/root.bib	Mon Oct 25 19:24:43 1999 +0200
13.3 @@ -0,0 +1,27 @@
13.4 +
13.5 +@Book{Heuser:1986,
13.6 +  author = 	 {H. Heuser},
13.7 +  title = 	 {Funktionalanalysis: Theorie und Anwendung},
13.8 +  publisher = 	 {Teubner},
13.9 +  year = 	 1986
13.10 +}
13.11 +
13.12 +@InCollection{Narici:1996,
13.13 +  author = 	 {L. Narici and E. Beckenstein},
13.14 +  title = 	 {The {Hahn-Banach Theorem}: The Life and Times},
13.15 +  booktitle = 	 {Topology Atlas},
13.16 +  publisher =	 {York University, Toronto, Ontario, Canada},
13.17 +  year =	 1996,
13.18 +  note =	 {\url{http://at.yorku.ca/topology/preprint.htm} and
13.19 +                  \url{http://at.yorku.ca/p/a/a/a/16.htm}}
13.20 +}
13.21 +
13.22 +@Article{Nowak:1993,
13.23 +  author =       {B. Nowak and A. Trybulec},
13.24 +  title =	 {{Hahn-Banach} Theorem},
13.25 +  journal =      {Journal of Formalized Mathematics},
13.26 +  year =         {1993},
13.27 +  volume =       {5},
13.28 +  institution =  {University of Bialystok},
13.29 +  note =         {\url{http://mizar.uwb.edu.pl/JFM/Vol5/hahnban.html}}
13.30 +}

    14.1 --- a/src/HOL/Real/HahnBanach/document/root.tex	Mon Oct 25 19:24:31 1999 +0200
14.2 +++ b/src/HOL/Real/HahnBanach/document/root.tex	Mon Oct 25 19:24:43 1999 +0200
14.3 @@ -12,32 +12,42 @@
14.5  \pagenumbering{arabic}
14.6
14.7 -\title{The Hahn-Banach Theorem for Real Vectorspaces}
14.8 +\title{The Hahn-Banach Theorem for Real Vector Spaces}
14.9  \author{Gertrud Bauer}
14.10  \maketitle
14.11
14.12  \begin{abstract}
14.13 -The Hahn-Banach theorem is one of the most important theorems
14.14 -of functional analysis. We present the fully formal proof of two versions of
14.15 -the theorem, one for general linear spaces and one for normed spaces
14.16 -as a corollary of the first.
14.17 -
14.18 -The first part contains the definition of basic notions of
14.19 -linear algebra, such as vector spaces, subspaces, normed spaces,
14.20 -continous linearforms, norm of functions and an order on
14.21 -functions by domain extension.
14.22 -
14.23 -The second part contains some lemmas about the supremum w.r.t. the
14.24 -function order and the extension of a non-maximal function,
14.25 -which are needed for the proof of the main theorem.
14.26 -
14.27 -The third part is the proof of the theorem in its two different versions.
14.28 -
14.29 +  The Hahn-Banach theorem is one of the most fundamental results in functional
14.30 +  analysis. We present a fully formal proof of two versions of the theorem,
14.31 +  one for general linear spaces and another for normed spaces.  This
14.32 +  development is based on simply-typed classical set-theory, as provided by
14.33 +  Isabelle/HOL.
14.34  \end{abstract}
14.35
14.36 +
14.37  \tableofcontents
14.38 +\parindent 0pt \parskip 0.5ex
14.39 +
14.40 +\clearpage
14.41 +\section{Preface}
14.42
14.43 -\part {Basic notions}
14.44 +This is a fully formal proof of the Hahn-Banach theorem. It closely follows
14.45 +the informal presentation given in the textbook \cite[\S 36]{Heuser:1986}.
14.46 +Another formal proof of the same theorem has been done in Mizar
14.47 +\cite{Nowak:1993}.  A general overview of the relevance and history of the
14.48 +Hahn-Banach theorem is given in \cite{Narici:1996}.
14.49 +
14.50 +\medskip The document is structured as follows.  The first part contains
14.51 +definitions of basic notions of linear algebra: vector spaces, subspaces,
14.52 +normed spaces, continuous linearforms, norm of functions and an order on
14.53 +functions by domain extension.  The second part contains some lemmas about the
14.54 +supremum (w.r.t.\ the function order) and extension of non-maximal functions.
14.55 +With these preliminaries, the main proof of the theorem (in its two versions)
14.56 +is conducted in the third part.
14.57 +
14.58 +
14.59 +\clearpage
14.60 +\part {Basic Notions}
14.61
14.62  \input{Bounds.tex}
14.63  \input{Aux.tex}
14.64 @@ -49,15 +59,17 @@
14.65  \input{FunctionNorm.tex}
14.66  \input{ZornLemma.tex}
14.67
14.68 -\part {Lemmas for the proof}
14.69 +\clearpage
14.70 +\part {Lemmas for the Proof}
14.71
14.72  \input{HahnBanachSupLemmas.tex}
14.73  \input{HahnBanachExtLemmas.tex}
14.74
14.75 -\part {The proof}
14.76 +\clearpage
14.77 +\part {The Main Proof}
14.78
14.79  \input{HahnBanach.tex}
14.80  \bibliographystyle{abbrv}
14.81 -\bibliography{bib}
14.82 +\bibliography{root}
14.83
14.84  \end{document}