tuned document;
authorwenzelm
Mon Nov 02 11:43:02 2015 +0100 (2015-11-02)
changeset 61540f92bf6674699
parent 61539 a29295dac1ca
child 61541 846c72206207
tuned document;
src/HOL/Hahn_Banach/Function_Norm.thy
src/HOL/Hahn_Banach/Function_Order.thy
src/HOL/Hahn_Banach/Hahn_Banach.thy
src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
src/HOL/Hahn_Banach/Linearform.thy
src/HOL/Hahn_Banach/Normed_Space.thy
src/HOL/Hahn_Banach/Subspace.thy
src/HOL/Hahn_Banach/Vector_Space.thy
src/HOL/Hahn_Banach/document/root.tex
     1.1 --- a/src/HOL/Hahn_Banach/Function_Norm.thy	Mon Nov 02 11:10:28 2015 +0100
     1.2 +++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Mon Nov 02 11:43:02 2015 +0100
     1.3 @@ -11,14 +11,13 @@
     1.4  subsection \<open>Continuous linear forms\<close>
     1.5  
     1.6  text \<open>
     1.7 -  A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close>
     1.8 -  is \<^emph>\<open>continuous\<close>, iff it is bounded, i.e.
     1.9 +  A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>,
    1.10 +  iff it is bounded, i.e.
    1.11    \begin{center}
    1.12    \<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
    1.13    \end{center}
    1.14 -  In our application no other functions than linear forms are
    1.15 -  considered, so we can define continuous linear forms as bounded
    1.16 -  linear forms:
    1.17 +  In our application no other functions than linear forms are considered, so
    1.18 +  we can define continuous linear forms as bounded linear forms:
    1.19  \<close>
    1.20  
    1.21  locale continuous = linearform +
    1.22 @@ -48,28 +47,25 @@
    1.23    \end{center}
    1.24    is called the \<^emph>\<open>norm\<close> of \<open>f\<close>.
    1.25  
    1.26 -  For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be
    1.27 -  defined as
    1.28 +  For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be defined as
    1.29    \begin{center}
    1.30    \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close>
    1.31    \end{center}
    1.32  
    1.33 -  For the case \<open>V = {0}\<close> the supremum would be taken from an
    1.34 -  empty set. Since \<open>\<real>\<close> is unbounded, there would be no supremum.
    1.35 -  To avoid this situation it must be guaranteed that there is an
    1.36 -  element in this set. This element must be \<open>{} \<ge> 0\<close> so that
    1.37 -  \<open>fn_norm\<close> has the norm properties. Furthermore it does not
    1.38 -  have to change the norm in all other cases, so it must be \<open>0\<close>,
    1.39 -  as all other elements are \<open>{} \<ge> 0\<close>.
    1.40 +  For the case \<open>V = {0}\<close> the supremum would be taken from an empty set.
    1.41 +  Since \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this
    1.42 +  situation it must be guaranteed that there is an element in this set. This
    1.43 +  element must be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties.
    1.44 +  Furthermore it does not have to change the norm in all other cases, so it
    1.45 +  must be \<open>0\<close>, as all other elements are \<open>{} \<ge> 0\<close>.
    1.46  
    1.47 -  Thus we define the set \<open>B\<close> where the supremum is taken from as
    1.48 -  follows:
    1.49 +  Thus we define the set \<open>B\<close> where the supremum is taken from as follows:
    1.50    \begin{center}
    1.51    \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close>
    1.52    \end{center}
    1.53  
    1.54 -  \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the
    1.55 -  supremum exists (otherwise it is undefined).
    1.56 +  \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists
    1.57 +  (otherwise it is undefined).
    1.58  \<close>
    1.59  
    1.60  locale fn_norm =
    1.61 @@ -84,8 +80,8 @@
    1.62    by (simp add: B_def)
    1.63  
    1.64  text \<open>
    1.65 -  The following lemma states that every continuous linear form on a
    1.66 -  normed space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm.
    1.67 +  The following lemma states that every continuous linear form on a normed
    1.68 +  space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm.
    1.69  \<close>
    1.70  
    1.71  lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
    1.72 @@ -108,9 +104,9 @@
    1.73        txt \<open>We know that \<open>f\<close> is bounded by some value \<open>c\<close>.\<close>
    1.74        from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
    1.75  
    1.76 -      txt \<open>To prove the thesis, we have to show that there is some
    1.77 -        \<open>b\<close>, such that \<open>y \<le> b\<close> for all \<open>y \<in>
    1.78 -        B\<close>. Due to the definition of \<open>B\<close> there are two cases.\<close>
    1.79 +      txt \<open>To prove the thesis, we have to show that there is some \<open>b\<close>, such
    1.80 +        that \<open>y \<le> b\<close> for all \<open>y \<in> B\<close>. Due to the definition of \<open>B\<close> there are
    1.81 +        two cases.\<close>
    1.82  
    1.83        def b \<equiv> "max c 0"
    1.84        have "\<forall>y \<in> B V f. y \<le> b"
    1.85 @@ -237,8 +233,8 @@
    1.86  
    1.87  text \<open>
    1.88    \<^medskip>
    1.89 -  The function norm is the least positive real number for
    1.90 -  which the following inequation holds:
    1.91 +  The function norm is the least positive real number for which the
    1.92 +  following inequality holds:
    1.93    \begin{center}
    1.94      \<open>\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
    1.95    \end{center}
     2.1 --- a/src/HOL/Hahn_Banach/Function_Order.thy	Mon Nov 02 11:10:28 2015 +0100
     2.2 +++ b/src/HOL/Hahn_Banach/Function_Order.thy	Mon Nov 02 11:43:02 2015 +0100
     2.3 @@ -70,8 +70,8 @@
     2.4    where "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
     2.5  
     2.6  text \<open>
     2.7 -  The following lemma states that \<open>g\<close> is the graph of a function
     2.8 -  if the relation induced by \<open>g\<close> is unique.
     2.9 +  The following lemma states that \<open>g\<close> is the graph of a function if the
    2.10 +  relation induced by \<open>g\<close> is unique.
    2.11  \<close>
    2.12  
    2.13  lemma graph_domain_funct:
    2.14 @@ -93,9 +93,9 @@
    2.15  subsection \<open>Norm-preserving extensions of a function\<close>
    2.16  
    2.17  text \<open>
    2.18 -  Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm
    2.19 -  \<open>p\<close> on \<open>E\<close>. The set of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are bounded by
    2.20 -  \<open>p\<close>, is defined as follows.
    2.21 +  Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm \<open>p\<close> on \<open>E\<close>. The
    2.22 +  set of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are
    2.23 +  bounded by \<open>p\<close>, is defined as follows.
    2.24  \<close>
    2.25  
    2.26  definition
     3.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Nov 02 11:10:28 2015 +0100
     3.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Nov 02 11:43:02 2015 +0100
     3.3 @@ -9,37 +9,36 @@
     3.4  begin
     3.5  
     3.6  text \<open>
     3.7 -  We present the proof of two different versions of the Hahn-Banach
     3.8 -  Theorem, closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
     3.9 +  We present the proof of two different versions of the Hahn-Banach Theorem,
    3.10 +  closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
    3.11  \<close>
    3.12  
    3.13 +
    3.14  subsection \<open>The Hahn-Banach Theorem for vector spaces\<close>
    3.15  
    3.16  paragraph \<open>Hahn-Banach Theorem.\<close>
    3.17  text \<open>
    3.18 -  Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm on \<open>E\<close>, and \<open>f\<close> be a linear form defined on
    3.19 -  \<open>F\<close> such that \<open>f\<close> is bounded by \<open>p\<close>, i.e. \<open>\<forall>x \<in>
    3.20 -  F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear form \<open>h\<close>
    3.21 -  on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is
    3.22 -  also bounded by \<open>p\<close>.
    3.23 -\<close>
    3.24 +  Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm
    3.25 +  on \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded
    3.26 +  by \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear
    3.27 +  form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded
    3.28 +  by \<open>p\<close>. \<close>
    3.29  
    3.30  paragraph \<open>Proof Sketch.\<close>
    3.31  text \<open>
    3.32 -  \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of
    3.33 -  \<open>f\<close> to subspaces of \<open>E\<close>. The linear forms in \<open>M\<close>
    3.34 -  are ordered by domain extension.
    3.35 +  \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces
    3.36 +  of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.
    3.37  
    3.38 -  \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper
    3.39 -  bound in \<open>M\<close>.
    3.40 +  \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper bound in \<open>M\<close>.
    3.41  
    3.42 -  \<^enum> With Zorn's Lemma we conclude that there is a maximal function
    3.43 -  \<open>g\<close> in \<open>M\<close>.
    3.44 +  \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in
    3.45 +  \<open>M\<close>.
    3.46  
    3.47 -  \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical contradiction:
    3.48 +  \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical
    3.49 +  contradiction:
    3.50  
    3.51 -    \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can
    3.52 -    still be extended in a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
    3.53 +    \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in
    3.54 +    a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
    3.55  
    3.56      \<^item> Thus \<open>g\<close> can not be maximal. Contradiction!
    3.57  \<close>
    3.58 @@ -153,7 +152,7 @@
    3.59        obtain xi where
    3.60          xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
    3.61            \<and> xi \<le> p (y + x') - h y"
    3.62 -        -- \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequations; this will\<close>
    3.63 +        -- \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequality; this will\<close>
    3.64          -- \<open>be used to establish that \<open>h'\<close> is a norm-preserving extension of \<open>h\<close>.
    3.65             \label{ex-xi-use}\<^smallskip>\<close>
    3.66        proof -
    3.67 @@ -292,10 +291,10 @@
    3.68  
    3.69  text \<open>
    3.70    The following alternative formulation of the Hahn-Banach
    3.71 -  Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear
    3.72 -  form \<open>f\<close> and a seminorm \<open>p\<close> the following inequations
    3.73 -  are equivalent:\footnote{This was shown in lemma @{thm [source]
    3.74 -  abs_ineq_iff} (see page \pageref{abs-ineq-iff}).}
    3.75 +  Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form
    3.76 +  \<open>f\<close> and a seminorm \<open>p\<close> the following inequality are
    3.77 +  equivalent:\footnote{This was shown in lemma @{thm [source] abs_ineq_iff}
    3.78 +  (see page \pageref{abs-ineq-iff}).}
    3.79    \begin{center}
    3.80    \begin{tabular}{lll}
    3.81    \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
    3.82 @@ -336,9 +335,9 @@
    3.83  subsection \<open>The Hahn-Banach Theorem for normed spaces\<close>
    3.84  
    3.85  text \<open>
    3.86 -  Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a
    3.87 -  norm space \<open>E\<close>, can be extended to a continuous linear form
    3.88 -  \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = \<parallel>g\<parallel>\<close>.
    3.89 +  Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>,
    3.90 +  can be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> =
    3.91 +  \<parallel>g\<parallel>\<close>.
    3.92  \<close>
    3.93  
    3.94  theorem norm_Hahn_Banach:
    3.95 @@ -420,10 +419,10 @@
    3.96           OF F_norm, folded B_def fn_norm_def])
    3.97    qed
    3.98  
    3.99 -  txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded
   3.100 -    by \<open>p\<close> we can apply the Hahn-Banach Theorem for real vector
   3.101 -    spaces. So \<open>f\<close> can be extended in a norm-preserving way to
   3.102 -    some function \<open>g\<close> on the whole vector space \<open>E\<close>.\<close>
   3.103 +  txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we
   3.104 +    can apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be
   3.105 +    extended in a norm-preserving way to some function \<open>g\<close> on the whole
   3.106 +    vector space \<open>E\<close>.\<close>
   3.107  
   3.108    with E FE linearform q obtain g where
   3.109        linearformE: "linearform E g"
   3.110 @@ -445,19 +444,20 @@
   3.111    have "\<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
   3.112    proof (rule order_antisym)
   3.113      txt \<open>
   3.114 -      First we show \<open>\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>\<close>.  The function norm \<open>\<parallel>g\<parallel>\<close> is defined as the smallest \<open>c \<in> \<real>\<close> such that
   3.115 +      First we show \<open>\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>\<close>. The function norm \<open>\<parallel>g\<parallel>\<close> is defined as the
   3.116 +      smallest \<open>c \<in> \<real>\<close> such that
   3.117        \begin{center}
   3.118        \begin{tabular}{l}
   3.119        \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
   3.120        \end{tabular}
   3.121        \end{center}
   3.122 -      \noindent Furthermore holds
   3.123 +      \<^noindent> Furthermore holds
   3.124        \begin{center}
   3.125        \begin{tabular}{l}
   3.126        \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>
   3.127        \end{tabular}
   3.128        \end{center}
   3.129 -\<close>
   3.130 +    \<close>
   3.131  
   3.132      from g_cont _ ge_zero
   3.133      show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
     4.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Mon Nov 02 11:10:28 2015 +0100
     4.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Mon Nov 02 11:43:02 2015 +0100
     4.3 @@ -9,29 +9,27 @@
     4.4  begin
     4.5  
     4.6  text \<open>
     4.7 -  In this section the following context is presumed.  Let \<open>E\<close> be
     4.8 -  a real vector space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close> a linear function on
     4.9 -  \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a
    4.10 -  superspace of \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close> and \<open>x\<^sub>0\<close> is
    4.11 -  an element in \<open>E - H\<close>.  \<open>H\<close> is extended to the direct
    4.12 -  sum \<open>H' = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close>
    4.13 -  the decomposition of \<open>x = y + a \<cdot> x\<close> with \<open>y \<in> H\<close> is
    4.14 -  unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y +
    4.15 -  a \<cdot> \<xi>\<close> for a certain \<open>\<xi>\<close>.
    4.16 +  In this section the following context is presumed. Let \<open>E\<close> be a real
    4.17 +  vector space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close>
    4.18 +  a linear function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a
    4.19 +  superspace of \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close>
    4.20 +  and \<open>x\<^sub>0\<close> is an element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H'
    4.21 +  = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close>
    4.22 +  with \<open>y \<in> H\<close> is unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close>
    4.23 +  for a certain \<open>\<xi>\<close>.
    4.24  
    4.25 -  Subsequently we show some properties of this extension \<open>h'\<close> of
    4.26 -  \<open>h\<close>.
    4.27 +  Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>.
    4.28  
    4.29    \<^medskip>
    4.30 -  This lemma will be used to show the existence of a linear
    4.31 -  extension of \<open>f\<close> (see page \pageref{ex-xi-use}). It is a
    4.32 -  consequence of the completeness of \<open>\<real>\<close>. To show
    4.33 +  This lemma will be used to show the existence of a linear extension of \<open>f\<close>
    4.34 +  (see page \pageref{ex-xi-use}). It is a consequence of the completeness of
    4.35 +  \<open>\<real>\<close>. To show
    4.36    \begin{center}
    4.37    \begin{tabular}{l}
    4.38    \<open>\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y\<close>
    4.39    \end{tabular}
    4.40    \end{center}
    4.41 -  \noindent it suffices to show that
    4.42 +  \<^noindent> it suffices to show that
    4.43    \begin{center}
    4.44    \begin{tabular}{l}
    4.45    \<open>\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v\<close>
    4.46 @@ -84,9 +82,8 @@
    4.47  
    4.48  text \<open>
    4.49    \<^medskip>
    4.50 -  The function \<open>h'\<close> is defined as a \<open>h' x = h y
    4.51 -  + a \<cdot> \<xi>\<close> where \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of
    4.52 -  \<open>h\<close> to \<open>H'\<close>.
    4.53 +  The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where
    4.54 +  \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of \<open>h\<close> to \<open>H'\<close>.
    4.55  \<close>
    4.56  
    4.57  lemma h'_lf:
    4.58 @@ -192,8 +189,8 @@
    4.59  
    4.60  text \<open>
    4.61    \<^medskip>
    4.62 -  The linear extension \<open>h'\<close> of \<open>h\<close>
    4.63 -  is bounded by the seminorm \<open>p\<close>.\<close>
    4.64 +  The linear extension \<open>h'\<close> of \<open>h\<close> is bounded by the seminorm \<open>p\<close>.
    4.65 +\<close>
    4.66  
    4.67  lemma h'_norm_pres:
    4.68    assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
     5.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Mon Nov 02 11:10:28 2015 +0100
     5.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Mon Nov 02 11:43:02 2015 +0100
     5.3 @@ -2,27 +2,25 @@
     5.4      Author:     Gertrud Bauer, TU Munich
     5.5  *)
     5.6  
     5.7 -section \<open>The supremum w.r.t.~the function order\<close>
     5.8 +section \<open>The supremum wrt.\ the function order\<close>
     5.9  
    5.10  theory Hahn_Banach_Sup_Lemmas
    5.11  imports Function_Norm Zorn_Lemma
    5.12  begin
    5.13  
    5.14  text \<open>
    5.15 -  This section contains some lemmas that will be used in the proof of
    5.16 -  the Hahn-Banach Theorem.  In this section the following context is
    5.17 -  presumed.  Let \<open>E\<close> be a real vector space with a seminorm
    5.18 -  \<open>p\<close> on \<open>E\<close>.  \<open>F\<close> is a subspace of \<open>E\<close> and
    5.19 -  \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close>
    5.20 -  of norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c =
    5.21 -  graph H h\<close>.  We will show some properties about the limit function
    5.22 -  \<open>h\<close>, i.e.\ the supremum of the chain \<open>c\<close>.
    5.23 +  This section contains some lemmas that will be used in the proof of the
    5.24 +  Hahn-Banach Theorem. In this section the following context is presumed.
    5.25 +  Let \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a
    5.26 +  subspace of \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of
    5.27 +  norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will
    5.28 +  show some properties about the limit function \<open>h\<close>, i.e.\ the supremum of
    5.29 +  the chain \<open>c\<close>.
    5.30  
    5.31    \<^medskip>
    5.32 -  Let \<open>c\<close> be a chain of norm-preserving extensions of
    5.33 -  the function \<open>f\<close> and let \<open>graph H h\<close> be the supremum
    5.34 -  of \<open>c\<close>.  Every element in \<open>H\<close> is member of one of the
    5.35 -  elements of the chain.
    5.36 +  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and
    5.37 +  let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of
    5.38 +  one of the elements of the chain.
    5.39  \<close>
    5.40  
    5.41  lemmas [dest?] = chainsD
    5.42 @@ -57,10 +55,10 @@
    5.43  
    5.44  text \<open>
    5.45    \<^medskip>
    5.46 -  Let \<open>c\<close> be a chain of norm-preserving extensions of
    5.47 -  the function \<open>f\<close> and let \<open>graph H h\<close> be the supremum
    5.48 -  of \<open>c\<close>.  Every element in the domain \<open>H\<close> of the supremum
    5.49 -  function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends \<open>h'\<close>.
    5.50 +  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and
    5.51 +  let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of
    5.52 +  the supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>,
    5.53 +  such that \<open>h\<close> extends \<open>h'\<close>.
    5.54  \<close>
    5.55  
    5.56  lemma some_H'h':
    5.57 @@ -85,10 +83,9 @@
    5.58  
    5.59  text \<open>
    5.60    \<^medskip>
    5.61 -  Any two elements \<open>x\<close> and \<open>y\<close> in the domain
    5.62 -  \<open>H\<close> of the supremum function \<open>h\<close> are both in the domain
    5.63 -  \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends
    5.64 -  \<open>h'\<close>.
    5.65 +  Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function
    5.66 +  \<open>h\<close> are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close>
    5.67 +  extends \<open>h'\<close>.
    5.68  \<close>
    5.69  
    5.70  lemma some_H'h'2:
    5.71 @@ -158,8 +155,8 @@
    5.72  
    5.73  text \<open>
    5.74    \<^medskip>
    5.75 -  The relation induced by the graph of the supremum of a
    5.76 -  chain \<open>c\<close> is definite, i.~e.~t is the graph of a function.
    5.77 +  The relation induced by the graph of the supremum of a chain \<open>c\<close> is
    5.78 +  definite, i.e.\ it is the graph of a function.
    5.79  \<close>
    5.80  
    5.81  lemma sup_definite:
    5.82 @@ -181,8 +178,8 @@
    5.83    then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
    5.84      unfolding M_def by blast
    5.85  
    5.86 -  txt \<open>\<open>G\<^sub>1\<close> is contained in \<open>G\<^sub>2\<close>
    5.87 -    or vice versa, since both \<open>G\<^sub>1\<close> and \<open>G\<^sub>2\<close> are members of \<open>c\<close>. \label{cases2}\<close>
    5.88 +  txt \<open>\<open>G\<^sub>1\<close> is contained in \<open>G\<^sub>2\<close> or vice versa, since both \<open>G\<^sub>1\<close> and \<open>G\<^sub>2\<close>
    5.89 +    are members of \<open>c\<close>. \label{cases2}\<close>
    5.90  
    5.91    from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1"
    5.92      by (blast dest: chainsD)
    5.93 @@ -208,12 +205,11 @@
    5.94  
    5.95  text \<open>
    5.96    \<^medskip>
    5.97 -  The limit function \<open>h\<close> is linear. Every element
    5.98 -  \<open>x\<close> in the domain of \<open>h\<close> is in the domain of a function
    5.99 -  \<open>h'\<close> in the chain of norm preserving extensions.  Furthermore,
   5.100 -  \<open>h\<close> is an extension of \<open>h'\<close> so the function values of
   5.101 -  \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>.  Finally, the
   5.102 -  function \<open>h'\<close> is linear by construction of \<open>M\<close>.
   5.103 +  The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close>
   5.104 +  is in the domain of a function \<open>h'\<close> in the chain of norm preserving
   5.105 +  extensions. Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function
   5.106 +  values of \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close>
   5.107 +  is linear by construction of \<open>M\<close>.
   5.108  \<close>
   5.109  
   5.110  lemma sup_lf:
   5.111 @@ -264,10 +260,9 @@
   5.112  
   5.113  text \<open>
   5.114    \<^medskip>
   5.115 -  The limit of a non-empty chain of norm preserving
   5.116 -  extensions of \<open>f\<close> is an extension of \<open>f\<close>, since every
   5.117 -  element of the chain is an extension of \<open>f\<close> and the supremum
   5.118 -  is an extension for every element of the chain.
   5.119 +  The limit of a non-empty chain of norm preserving extensions of \<open>f\<close> is an
   5.120 +  extension of \<open>f\<close>, since every element of the chain is an extension of \<open>f\<close>
   5.121 +  and the supremum is an extension for every element of the chain.
   5.122  \<close>
   5.123  
   5.124  lemma sup_ext:
   5.125 @@ -291,9 +286,8 @@
   5.126  
   5.127  text \<open>
   5.128    \<^medskip>
   5.129 -  The domain \<open>H\<close> of the limit function is a superspace
   5.130 -  of \<open>F\<close>, since \<open>F\<close> is a subset of \<open>H\<close>. The
   5.131 -  existence of the \<open>0\<close> element in \<open>F\<close> and the closure
   5.132 +  The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is
   5.133 +  a subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure
   5.134    properties follow from the fact that \<open>F\<close> is a vector space.
   5.135  \<close>
   5.136  
   5.137 @@ -317,8 +311,7 @@
   5.138  
   5.139  text \<open>
   5.140    \<^medskip>
   5.141 -  The domain \<open>H\<close> of the limit function is a subspace of
   5.142 -  \<open>E\<close>.
   5.143 +  The domain \<open>H\<close> of the limit function is a subspace of \<open>E\<close>.
   5.144  \<close>
   5.145  
   5.146  lemma sup_subE:
   5.147 @@ -374,8 +367,8 @@
   5.148  
   5.149  text \<open>
   5.150    \<^medskip>
   5.151 -  The limit function is bounded by the norm \<open>p\<close> as
   5.152 -  well, since all elements in the chain are bounded by \<open>p\<close>.
   5.153 +  The limit function is bounded by the norm \<open>p\<close> as well, since all elements
   5.154 +  in the chain are bounded by \<open>p\<close>.
   5.155  \<close>
   5.156  
   5.157  lemma sup_norm_pres:
   5.158 @@ -396,10 +389,10 @@
   5.159  
   5.160  text \<open>
   5.161    \<^medskip>
   5.162 -  The following lemma is a property of linear forms on real
   5.163 -  vector spaces. It will be used for the lemma \<open>abs_Hahn_Banach\<close>
   5.164 -  (see page \pageref{abs-Hahn_Banach}). \label{abs-ineq-iff} For real
   5.165 -  vector spaces the following inequations are equivalent:
   5.166 +  The following lemma is a property of linear forms on real vector spaces.
   5.167 +  It will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page
   5.168 +  \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces
   5.169 +  the following inequality are equivalent:
   5.170    \begin{center}
   5.171    \begin{tabular}{lll}
   5.172    \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
     6.1 --- a/src/HOL/Hahn_Banach/Linearform.thy	Mon Nov 02 11:10:28 2015 +0100
     6.2 +++ b/src/HOL/Hahn_Banach/Linearform.thy	Mon Nov 02 11:43:02 2015 +0100
     6.3 @@ -9,8 +9,8 @@
     6.4  begin
     6.5  
     6.6  text \<open>
     6.7 -  A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals
     6.8 -  that is additive and multiplicative.
     6.9 +  A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is
    6.10 +  additive and multiplicative.
    6.11  \<close>
    6.12  
    6.13  locale linearform =
     7.1 --- a/src/HOL/Hahn_Banach/Normed_Space.thy	Mon Nov 02 11:10:28 2015 +0100
     7.2 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Mon Nov 02 11:43:02 2015 +0100
     7.3 @@ -11,9 +11,9 @@
     7.4  subsection \<open>Quasinorms\<close>
     7.5  
     7.6  text \<open>
     7.7 -  A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space
     7.8 -  into the reals that has the following properties: it is positive
     7.9 -  definite, absolute homogeneous and subadditive.
    7.10 +  A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals
    7.11 +  that has the following properties: it is positive definite, absolute
    7.12 +  homogeneous and subadditive.
    7.13  \<close>
    7.14  
    7.15  locale seminorm =
     8.1 --- a/src/HOL/Hahn_Banach/Subspace.thy	Mon Nov 02 11:10:28 2015 +0100
     8.2 +++ b/src/HOL/Hahn_Banach/Subspace.thy	Mon Nov 02 11:43:02 2015 +0100
     8.3 @@ -11,9 +11,8 @@
     8.4  subsection \<open>Definition\<close>
     8.5  
     8.6  text \<open>
     8.7 -  A non-empty subset \<open>U\<close> of a vector space \<open>V\<close> is a
     8.8 -  \<^emph>\<open>subspace\<close> of \<open>V\<close>, iff \<open>U\<close> is closed under addition
     8.9 -  and scalar multiplication.
    8.10 +  A non-empty subset \<open>U\<close> of a vector space \<open>V\<close> is a \<^emph>\<open>subspace\<close> of \<open>V\<close>, iff
    8.11 +  \<open>U\<close> is closed under addition and scalar multiplication.
    8.12  \<close>
    8.13  
    8.14  locale subspace =
    8.15 @@ -51,9 +50,9 @@
    8.16  
    8.17  text \<open>
    8.18    \<^medskip>
    8.19 -  Similar as for linear spaces, the existence of the zero
    8.20 -  element in every subspace follows from the non-emptiness of the
    8.21 -  carrier set and by vector space laws.
    8.22 +  Similar as for linear spaces, the existence of the zero element in every
    8.23 +  subspace follows from the non-emptiness of the carrier set and by vector
    8.24 +  space laws.
    8.25  \<close>
    8.26  
    8.27  lemma (in subspace) zero [intro]:
    8.28 @@ -140,8 +139,8 @@
    8.29  subsection \<open>Linear closure\<close>
    8.30  
    8.31  text \<open>
    8.32 -  The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all
    8.33 -  scalar multiples of \<open>x\<close>.
    8.34 +  The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples
    8.35 +  of \<open>x\<close>.
    8.36  \<close>
    8.37  
    8.38  definition lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set"
    8.39 @@ -227,8 +226,8 @@
    8.40  subsection \<open>Sum of two vectorspaces\<close>
    8.41  
    8.42  text \<open>
    8.43 -  The \<^emph>\<open>sum\<close> of two vectorspaces \<open>U\<close> and \<open>V\<close> is the
    8.44 -  set of all sums of elements from \<open>U\<close> and \<open>V\<close>.
    8.45 +  The \<^emph>\<open>sum\<close> of two vectorspaces \<open>U\<close> and \<open>V\<close> is the set of all sums of
    8.46 +  elements from \<open>U\<close> and \<open>V\<close>.
    8.47  \<close>
    8.48  
    8.49  lemma sum_def: "U + V = {u + v | u v. u \<in> U \<and> v \<in> V}"
    8.50 @@ -329,10 +328,10 @@
    8.51  subsection \<open>Direct sums\<close>
    8.52  
    8.53  text \<open>
    8.54 -  The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the
    8.55 -  zero element is the only common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct sum of \<open>U\<close> and
    8.56 -  \<open>V\<close> the decomposition in \<open>x = u + v\<close> with
    8.57 -  \<open>u \<in> U\<close> and \<open>v \<in> V\<close> is unique.
    8.58 +  The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the
    8.59 +  only common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct
    8.60 +  sum of \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and
    8.61 +  \<open>v \<in> V\<close> is unique.
    8.62  \<close>
    8.63  
    8.64  lemma decomp:
    8.65 @@ -377,12 +376,10 @@
    8.66  qed
    8.67  
    8.68  text \<open>
    8.69 -  An application of the previous lemma will be used in the proof of
    8.70 -  the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
    8.71 -  element \<open>y + a \<cdot> x\<^sub>0\<close> of the direct sum of a
    8.72 -  vectorspace \<open>H\<close> and the linear closure of \<open>x\<^sub>0\<close>
    8.73 -  the components \<open>y \<in> H\<close> and \<open>a\<close> are uniquely
    8.74 -  determined.
    8.75 +  An application of the previous lemma will be used in the proof of the
    8.76 +  Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any element
    8.77 +  \<open>y + a \<cdot> x\<^sub>0\<close> of the direct sum of a vectorspace \<open>H\<close> and the linear closure
    8.78 +  of \<open>x\<^sub>0\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are uniquely determined.
    8.79  \<close>
    8.80  
    8.81  lemma decomp_H':
    8.82 @@ -436,10 +433,9 @@
    8.83  qed
    8.84  
    8.85  text \<open>
    8.86 -  Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a
    8.87 -  vectorspace \<open>H\<close> and the linear closure of \<open>x'\<close> the
    8.88 -  components \<open>y \<in> H\<close> and \<open>a\<close> are unique, it follows from
    8.89 -  \<open>y \<in> H\<close> that \<open>a = 0\<close>.
    8.90 +  Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a vectorspace \<open>H\<close>
    8.91 +  and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique,
    8.92 +  it follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>.
    8.93  \<close>
    8.94  
    8.95  lemma decomp_H'_H:
    8.96 @@ -464,9 +460,8 @@
    8.97  qed
    8.98  
    8.99  text \<open>
   8.100 -  The components \<open>y \<in> H\<close> and \<open>a\<close> in \<open>y + a \<cdot> x'\<close>
   8.101 -  are unique, so the function \<open>h'\<close> defined by
   8.102 -  \<open>h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>\<close> is definite.
   8.103 +  The components \<open>y \<in> H\<close> and \<open>a\<close> in \<open>y + a \<cdot> x'\<close> are unique, so the function
   8.104 +  \<open>h'\<close> defined by \<open>h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>\<close> is definite.
   8.105  \<close>
   8.106  
   8.107  lemma h'_definite:
     9.1 --- a/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Nov 02 11:10:28 2015 +0100
     9.2 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Nov 02 11:43:02 2015 +0100
     9.3 @@ -11,9 +11,9 @@
     9.4  subsection \<open>Signature\<close>
     9.5  
     9.6  text \<open>
     9.7 -  For the definition of real vector spaces a type @{typ 'a} of the
     9.8 -  sort \<open>{plus, minus, zero}\<close> is considered, on which a real
     9.9 -  scalar multiplication \<open>\<cdot>\<close> is declared.
    9.10 +  For the definition of real vector spaces a type @{typ 'a} of the sort
    9.11 +  \<open>{plus, minus, zero}\<close> is considered, on which a real scalar multiplication
    9.12 +  \<open>\<cdot>\<close> is declared.
    9.13  \<close>
    9.14  
    9.15  consts
    9.16 @@ -23,13 +23,13 @@
    9.17  subsection \<open>Vector space laws\<close>
    9.18  
    9.19  text \<open>
    9.20 -  A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from
    9.21 -  @{typ 'a} with the following vector space laws: The set \<open>V\<close> is
    9.22 -  closed under addition and scalar multiplication, addition is
    9.23 -  associative and commutative; \<open>- x\<close> is the inverse of \<open>x\<close> w.~r.~t.~addition and \<open>0\<close> is the neutral element of
    9.24 -  addition.  Addition and multiplication are distributive; scalar
    9.25 -  multiplication is associative and the real number \<open>1\<close> is
    9.26 -  the neutral element of scalar multiplication.
    9.27 +  A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with
    9.28 +  the following vector space laws: The set \<open>V\<close> is closed under addition and
    9.29 +  scalar multiplication, addition is associative and commutative; \<open>- x\<close> is
    9.30 +  the inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of
    9.31 +  addition. Addition and multiplication are distributive; scalar
    9.32 +  multiplication is associative and the real number \<open>1\<close> is the neutral
    9.33 +  element of scalar multiplication.
    9.34  \<close>
    9.35  
    9.36  locale vectorspace =
    9.37 @@ -64,7 +64,8 @@
    9.38  lemma neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V"
    9.39    by (simp add: negate_eq1)
    9.40  
    9.41 -lemma add_left_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
    9.42 +lemma add_left_commute:
    9.43 +  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
    9.44  proof -
    9.45    assume xyz: "x \<in> V"  "y \<in> V"  "z \<in> V"
    9.46    then have "x + (y + z) = (x + y) + z"
    9.47 @@ -77,8 +78,8 @@
    9.48  lemmas add_ac = add_assoc add_commute add_left_commute
    9.49  
    9.50  
    9.51 -text \<open>The existence of the zero element of a vector space
    9.52 -  follows from the non-emptiness of carrier set.\<close>
    9.53 +text \<open>The existence of the zero element of a vector space follows from the
    9.54 +  non-emptiness of carrier set.\<close>
    9.55  
    9.56  lemma zero [iff]: "0 \<in> V"
    9.57  proof -
    9.58 @@ -213,7 +214,8 @@
    9.59    then show "x + y = x + z" by (simp only:)
    9.60  qed
    9.61  
    9.62 -lemma add_right_cancel: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
    9.63 +lemma add_right_cancel:
    9.64 +    "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
    9.65    by (simp only: add_commute add_left_cancel)
    9.66  
    9.67  lemma add_assoc_cong:
    9.68 @@ -371,4 +373,3 @@
    9.69  end
    9.70  
    9.71  end
    9.72 -
    10.1 --- a/src/HOL/Hahn_Banach/document/root.tex	Mon Nov 02 11:10:28 2015 +0100
    10.2 +++ b/src/HOL/Hahn_Banach/document/root.tex	Mon Nov 02 11:43:02 2015 +0100
    10.3 @@ -16,7 +16,7 @@
    10.4  \pagenumbering{arabic}
    10.5  
    10.6  \title{The Hahn-Banach Theorem \\ for Real Vector Spaces}
    10.7 -\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
    10.8 +\author{Gertrud Bauer}
    10.9  \maketitle
   10.10  
   10.11  \begin{abstract}