author | wenzelm |

Mon Nov 02 11:43:02 2015 +0100 (2015-11-02) | |

changeset 61540 | f92bf6674699 |

parent 61539 | a29295dac1ca |

child 61541 | 846c72206207 |

tuned document;

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}