author | wenzelm |

Sun Dec 20 13:56:02 2015 +0100 (2015-12-20) | |

changeset 61879 | e4f9d8f094fe |

parent 61878 | fa4dbb82732f |

child 61880 | ff4d33058566 |

child 61883 | c0f34fe6aa61 |

tuned whitespace;

1.1 --- a/src/HOL/Hahn_Banach/Function_Norm.thy Sun Dec 20 13:11:47 2015 +0100 1.2 +++ b/src/HOL/Hahn_Banach/Function_Norm.thy Sun Dec 20 13:56:02 2015 +0100 1.3 @@ -11,8 +11,8 @@ 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> is \<^emph>\<open>continuous\<close>, 1.8 - 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>, iff 1.10 + 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 @@ -52,20 +52,20 @@ 1.15 \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> 1.16 \end{center} 1.17 1.18 - For the case \<open>V = {0}\<close> the supremum would be taken from an empty set. 1.19 - Since \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this 1.20 - situation it must be guaranteed that there is an element in this set. This 1.21 - element must be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties. 1.22 - Furthermore it does not have to change the norm in all other cases, so it 1.23 - must be \<open>0\<close>, as all other elements are \<open>{} \<ge> 0\<close>. 1.24 + For the case \<open>V = {0}\<close> the supremum would be taken from an empty set. Since 1.25 + \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this situation it 1.26 + must be guaranteed that there is an element in this set. This element must 1.27 + be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties. Furthermore it does 1.28 + not have to change the norm in all other cases, so it must be \<open>0\<close>, as all 1.29 + other elements are \<open>{} \<ge> 0\<close>. 1.30 1.31 Thus we define the set \<open>B\<close> where the supremum is taken from as follows: 1.32 \begin{center} 1.33 \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close> 1.34 \end{center} 1.35 1.36 - \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists 1.37 - (otherwise it is undefined). 1.38 + \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists (otherwise 1.39 + it is undefined). 1.40 \<close> 1.41 1.42 locale fn_norm =

2.1 --- a/src/HOL/Hahn_Banach/Function_Order.thy Sun Dec 20 13:11:47 2015 +0100 2.2 +++ b/src/HOL/Hahn_Banach/Function_Order.thy Sun Dec 20 13:56:02 2015 +0100 2.3 @@ -11,14 +11,12 @@ 2.4 subsection \<open>The graph of a function\<close> 2.5 2.6 text \<open> 2.7 - We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with 2.8 - domain \<open>F\<close> as the set 2.9 + We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with domain \<open>F\<close> as the set 2.10 \begin{center} 2.11 \<open>{(x, f x). x \<in> F}\<close> 2.12 \end{center} 2.13 - So we are modeling partial functions by specifying the domain and 2.14 - the mapping function. We use the term ``function'' also for its 2.15 - graph. 2.16 + So we are modeling partial functions by specifying the domain and the 2.17 + mapping function. We use the term ``function'' also for its graph. 2.18 \<close> 2.19 2.20 type_synonym 'a graph = "('a \<times> real) set" 2.21 @@ -41,8 +39,8 @@ 2.22 subsection \<open>Functions ordered by domain extension\<close> 2.23 2.24 text \<open> 2.25 - A function \<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of 2.26 - \<open>h\<close> is a subset of the graph of \<open>h'\<close>. 2.27 + A function \<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of \<open>h\<close> is a subset of 2.28 + the graph of \<open>h'\<close>. 2.29 \<close> 2.30 2.31 lemma graph_extI: 2.32 @@ -93,8 +91,8 @@ 2.33 subsection \<open>Norm-preserving extensions of a function\<close> 2.34 2.35 text \<open> 2.36 - 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.37 - set of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are 2.38 + Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm \<open>p\<close> on \<open>E\<close>. The set 2.39 + of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are 2.40 bounded by \<open>p\<close>, is defined as follows. 2.41 \<close> 2.42

3.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Sun Dec 20 13:11:47 2015 +0100 3.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Sun Dec 20 13:56:02 2015 +0100 3.3 @@ -18,28 +18,26 @@ 3.4 3.5 paragraph \<open>Hahn-Banach Theorem.\<close> 3.6 text \<open> 3.7 - Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm 3.8 - 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.9 - 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.10 - 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.11 - by \<open>p\<close>. 3.12 + Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm on 3.13 + \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded by 3.14 + \<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 form \<open>h\<close> 3.15 + on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded by \<open>p\<close>. 3.16 \<close> 3.17 3.18 paragraph \<open>Proof Sketch.\<close> 3.19 text \<open> 3.20 - \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces 3.21 - of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension. 3.22 + \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces of 3.23 + \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension. 3.24 3.25 \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper bound in \<open>M\<close>. 3.26 3.27 - \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in 3.28 - \<open>M\<close>. 3.29 + \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in \<open>M\<close>. 3.30 3.31 \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical 3.32 contradiction: 3.33 3.34 - \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in 3.35 - a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>. 3.36 + \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in a 3.37 + norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>. 3.38 3.39 \<^item> Thus \<open>g\<close> can not be maximal. Contradiction! 3.40 \<close> 3.41 @@ -292,14 +290,13 @@ 3.42 3.43 text \<open> 3.44 The following alternative formulation of the Hahn-Banach 3.45 - Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form 3.46 - \<open>f\<close> and a seminorm \<open>p\<close> the following inequality are 3.47 - equivalent:\footnote{This was shown in lemma @{thm [source] abs_ineq_iff} 3.48 - (see page \pageref{abs-ineq-iff}).} 3.49 + Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form \<open>f\<close> 3.50 + and a seminorm \<open>p\<close> the following inequality are equivalent:\footnote{This 3.51 + was shown in lemma @{thm [source] abs_ineq_iff} (see page 3.52 + \pageref{abs-ineq-iff}).} 3.53 \begin{center} 3.54 \begin{tabular}{lll} 3.55 - \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and & 3.56 - \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\ 3.57 + \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and & \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\ 3.58 \end{tabular} 3.59 \end{center} 3.60 \<close> 3.61 @@ -336,9 +333,8 @@ 3.62 subsection \<open>The Hahn-Banach Theorem for normed spaces\<close> 3.63 3.64 text \<open> 3.65 - Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>, 3.66 - can be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = 3.67 - \<parallel>g\<parallel>\<close>. 3.68 + Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>, can 3.69 + be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = \<parallel>g\<parallel>\<close>. 3.70 \<close> 3.71 3.72 theorem norm_Hahn_Banach: 3.73 @@ -420,10 +416,10 @@ 3.74 OF F_norm, folded B_def fn_norm_def]) 3.75 qed 3.76 3.77 - txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we 3.78 - can apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be 3.79 - extended in a norm-preserving way to some function \<open>g\<close> on the whole 3.80 - vector space \<open>E\<close>.\<close> 3.81 + txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we can 3.82 + apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be 3.83 + extended in a norm-preserving way to some function \<open>g\<close> on the whole vector 3.84 + space \<open>E\<close>.\<close> 3.85 3.86 with E FE linearform q obtain g where 3.87 linearformE: "linearform E g"

4.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Sun Dec 20 13:11:47 2015 +0100 4.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Sun Dec 20 13:56:02 2015 +0100 4.3 @@ -9,14 +9,13 @@ 4.4 begin 4.5 4.6 text \<open> 4.7 - In this section the following context is presumed. Let \<open>E\<close> be a real 4.8 - 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.9 - a linear function on \<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> 4.11 - 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.12 - = 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.13 - 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.14 - for a certain \<open>\<xi>\<close>. 4.15 + In this section the following context is presumed. Let \<open>E\<close> be a real vector 4.16 + 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 4.17 + function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a superspace of 4.18 + \<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 an 4.19 + element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H' = H + lin x\<^sub>0\<close>, so 4.20 + for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close> with \<open>y \<in> H\<close> is 4.21 + unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close> for a certain \<open>\<xi>\<close>. 4.22 4.23 Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>. 4.24 4.25 @@ -82,8 +81,8 @@ 4.26 4.27 text \<open> 4.28 \<^medskip> 4.29 - The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where 4.30 - \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of \<open>h\<close> to \<open>H'\<close>. 4.31 + The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where \<open>x = y + a \<cdot> \<xi>\<close> 4.32 + is a linear extension of \<open>h\<close> to \<open>H'\<close>. 4.33 \<close> 4.34 4.35 lemma h'_lf:

5.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Sun Dec 20 13:11:47 2015 +0100 5.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Sun Dec 20 13:56:02 2015 +0100 5.3 @@ -10,17 +10,16 @@ 5.4 5.5 text \<open> 5.6 This section contains some lemmas that will be used in the proof of the 5.7 - Hahn-Banach Theorem. In this section the following context is presumed. 5.8 - 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.9 - 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.10 - norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will 5.11 - show some properties about the limit function \<open>h\<close>, i.e.\ the supremum of 5.12 - the chain \<open>c\<close>. 5.13 + Hahn-Banach Theorem. In this section the following context is presumed. Let 5.14 + \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of 5.15 + \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of norm-preserving 5.16 + extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will show some properties 5.17 + about the limit function \<open>h\<close>, i.e.\ the supremum of the chain \<open>c\<close>. 5.18 5.19 \<^medskip> 5.20 - Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and 5.21 - let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of 5.22 - one of the elements of the chain. 5.23 + Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let 5.24 + \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of one of 5.25 + the elements of the chain. 5.26 \<close> 5.27 5.28 lemmas [dest?] = chainsD 5.29 @@ -55,10 +54,10 @@ 5.30 5.31 text \<open> 5.32 \<^medskip> 5.33 - Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and 5.34 - let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of 5.35 - the supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, 5.36 - such that \<open>h\<close> extends \<open>h'\<close>. 5.37 + Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let 5.38 + \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of the 5.39 + supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, such 5.40 + that \<open>h\<close> extends \<open>h'\<close>. 5.41 \<close> 5.42 5.43 lemma some_H'h': 5.44 @@ -83,9 +82,9 @@ 5.45 5.46 text \<open> 5.47 \<^medskip> 5.48 - Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function 5.49 - \<open>h\<close> are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> 5.50 - extends \<open>h'\<close>. 5.51 + Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function \<open>h\<close> 5.52 + are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends 5.53 + \<open>h'\<close>. 5.54 \<close> 5.55 5.56 lemma some_H'h'2: 5.57 @@ -99,8 +98,8 @@ 5.58 \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H' 5.59 \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)" 5.60 proof - 5.61 - txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>, 5.62 - such that \<open>h\<close> extends \<open>h''\<close>.\<close> 5.63 + txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>, such that \<open>h\<close> 5.64 + extends \<open>h''\<close>.\<close> 5.65 5.66 from M cM u and y obtain H' h' where 5.67 y_hy: "(y, h y) \<in> graph H' h'" 5.68 @@ -121,10 +120,9 @@ 5.69 "graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x" 5.70 by (rule some_H'h't [elim_format]) blast 5.71 5.72 - txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain, 5.73 - \<open>h''\<close> is an extension of \<open>h'\<close> or vice versa. Thus both 5.74 - \<open>x\<close> and \<open>y\<close> are contained in the greater 5.75 - one. \label{cases1}\<close> 5.76 + txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain, \<open>h''\<close> is an 5.77 + extension of \<open>h'\<close> or vice versa. Thus both \<open>x\<close> and \<open>y\<close> are contained in 5.78 + the greater one. \label{cases1}\<close> 5.79 5.80 from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''" 5.81 by (blast dest: chainsD) 5.82 @@ -205,11 +203,11 @@ 5.83 5.84 text \<open> 5.85 \<^medskip> 5.86 - The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close> 5.87 - is in the domain of a function \<open>h'\<close> in the chain of norm preserving 5.88 - extensions. Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function 5.89 - values of \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close> 5.90 - is linear by construction of \<open>M\<close>. 5.91 + The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close> is 5.92 + in the domain of a function \<open>h'\<close> in the chain of norm preserving extensions. 5.93 + Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function values of \<open>x\<close> are 5.94 + identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close> is linear by 5.95 + construction of \<open>M\<close>. 5.96 \<close> 5.97 5.98 lemma sup_lf: 5.99 @@ -286,8 +284,8 @@ 5.100 5.101 text \<open> 5.102 \<^medskip> 5.103 - The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is 5.104 - a subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure 5.105 + The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is a 5.106 + subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure 5.107 properties follow from the fact that \<open>F\<close> is a vector space. 5.108 \<close> 5.109 5.110 @@ -367,8 +365,8 @@ 5.111 5.112 text \<open> 5.113 \<^medskip> 5.114 - The limit function is bounded by the norm \<open>p\<close> as well, since all elements 5.115 - in the chain are bounded by \<open>p\<close>. 5.116 + The limit function is bounded by the norm \<open>p\<close> as well, since all elements in 5.117 + the chain are bounded by \<open>p\<close>. 5.118 \<close> 5.119 5.120 lemma sup_norm_pres: 5.121 @@ -389,10 +387,10 @@ 5.122 5.123 text \<open> 5.124 \<^medskip> 5.125 - The following lemma is a property of linear forms on real vector spaces. 5.126 - It will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page 5.127 - \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces 5.128 - the following inequality are equivalent: 5.129 + The following lemma is a property of linear forms on real vector spaces. It 5.130 + will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page 5.131 + \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces the 5.132 + following inequality are equivalent: 5.133 \begin{center} 5.134 \begin{tabular}{lll} 5.135 \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &

6.1 --- a/src/HOL/Hahn_Banach/Normed_Space.thy Sun Dec 20 13:11:47 2015 +0100 6.2 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy Sun Dec 20 13:56:02 2015 +0100 6.3 @@ -11,9 +11,9 @@ 6.4 subsection \<open>Quasinorms\<close> 6.5 6.6 text \<open> 6.7 - A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals 6.8 - that has the following properties: it is positive definite, absolute 6.9 - homogeneous and subadditive. 6.10 + A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals that 6.11 + has the following properties: it is positive definite, absolute homogeneous 6.12 + and subadditive. 6.13 \<close> 6.14 6.15 locale seminorm = 6.16 @@ -57,8 +57,7 @@ 6.17 subsection \<open>Norms\<close> 6.18 6.19 text \<open> 6.20 - A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the 6.21 - \<open>0\<close> vector to \<open>0\<close>. 6.22 + A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the \<open>0\<close> vector to \<open>0\<close>. 6.23 \<close> 6.24 6.25 locale norm = seminorm + 6.26 @@ -68,8 +67,7 @@ 6.27 subsection \<open>Normed vector spaces\<close> 6.28 6.29 text \<open> 6.30 - A vector space together with a norm is called a \<^emph>\<open>normed 6.31 - space\<close>. 6.32 + A vector space together with a norm is called a \<^emph>\<open>normed space\<close>. 6.33 \<close> 6.34 6.35 locale normed_vectorspace = vectorspace + norm

7.1 --- a/src/HOL/Hahn_Banach/Subspace.thy Sun Dec 20 13:11:47 2015 +0100 7.2 +++ b/src/HOL/Hahn_Banach/Subspace.thy Sun Dec 20 13:56:02 2015 +0100 7.3 @@ -139,8 +139,8 @@ 7.4 subsection \<open>Linear closure\<close> 7.5 7.6 text \<open> 7.7 - The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples 7.8 - of \<open>x\<close>. 7.9 + The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples of 7.10 + \<open>x\<close>. 7.11 \<close> 7.12 7.13 definition lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set" 7.14 @@ -318,7 +318,7 @@ 7.15 qed 7.16 qed 7.17 7.18 -text\<open>The sum of two subspaces is a vectorspace.\<close> 7.19 +text \<open>The sum of two subspaces is a vectorspace.\<close> 7.20 7.21 lemma sum_vs [intro?]: 7.22 "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)" 7.23 @@ -328,10 +328,10 @@ 7.24 subsection \<open>Direct sums\<close> 7.25 7.26 text \<open> 7.27 - The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the 7.28 - only common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct 7.29 - sum of \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and 7.30 - \<open>v \<in> V\<close> is unique. 7.31 + The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the only 7.32 + common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct sum of 7.33 + \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and \<open>v \<in> V\<close> is 7.34 + unique. 7.35 \<close> 7.36 7.37 lemma decomp: 7.38 @@ -434,8 +434,8 @@ 7.39 7.40 text \<open> 7.41 Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a vectorspace \<open>H\<close> 7.42 - and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique, 7.43 - it follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>. 7.44 + and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique, it 7.45 + follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>. 7.46 \<close> 7.47 7.48 lemma decomp_H'_H:

8.1 --- a/src/HOL/Hahn_Banach/Vector_Space.thy Sun Dec 20 13:11:47 2015 +0100 8.2 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy Sun Dec 20 13:56:02 2015 +0100 8.3 @@ -23,13 +23,13 @@ 8.4 subsection \<open>Vector space laws\<close> 8.5 8.6 text \<open> 8.7 - A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with 8.8 - the following vector space laws: The set \<open>V\<close> is closed under addition and 8.9 - scalar multiplication, addition is associative and commutative; \<open>- x\<close> is 8.10 - the inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of 8.11 - addition. Addition and multiplication are distributive; scalar 8.12 - multiplication is associative and the real number \<open>1\<close> is the neutral 8.13 - element of scalar multiplication. 8.14 + A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with the 8.15 + following vector space laws: The set \<open>V\<close> is closed under addition and scalar 8.16 + multiplication, addition is associative and commutative; \<open>- x\<close> is the 8.17 + inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of addition. 8.18 + Addition and multiplication are distributive; scalar multiplication is 8.19 + associative and the real number \<open>1\<close> is the neutral element of scalar 8.20 + multiplication. 8.21 \<close> 8.22 8.23 locale vectorspace = 8.24 @@ -78,8 +78,10 @@ 8.25 lemmas add_ac = add_assoc add_commute add_left_commute 8.26 8.27 8.28 -text \<open>The existence of the zero element of a vector space follows from the 8.29 - non-emptiness of carrier set.\<close> 8.30 +text \<open> 8.31 + The existence of the zero element of a vector space follows from the 8.32 + non-emptiness of carrier set. 8.33 +\<close> 8.34 8.35 lemma zero [iff]: "0 \<in> V" 8.36 proof -

9.1 --- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy Sun Dec 20 13:11:47 2015 +0100 9.2 +++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy Sun Dec 20 13:56:02 2015 +0100 9.3 @@ -9,13 +9,13 @@ 9.4 begin 9.5 9.6 text \<open> 9.7 - Zorn's Lemmas states: if every linear ordered subset of an ordered 9.8 - set \<open>S\<close> has an upper bound in \<open>S\<close>, then there exists a 9.9 - maximal element in \<open>S\<close>. In our application, \<open>S\<close> is a 9.10 - set of sets ordered by set inclusion. Since the union of a chain of 9.11 - sets is an upper bound for all elements of the chain, the conditions 9.12 - of Zorn's lemma can be modified: if \<open>S\<close> is non-empty, it 9.13 - suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close> also lies in \<open>S\<close>. 9.14 + Zorn's Lemmas states: if every linear ordered subset of an ordered set \<open>S\<close> 9.15 + has an upper bound in \<open>S\<close>, then there exists a maximal element in \<open>S\<close>. In 9.16 + our application, \<open>S\<close> is a set of sets ordered by set inclusion. Since the 9.17 + union of a chain of sets is an upper bound for all elements of the chain, 9.18 + the conditions of Zorn's lemma can be modified: if \<open>S\<close> is non-empty, it 9.19 + suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close> 9.20 + also lies in \<open>S\<close>. 9.21 \<close> 9.22 9.23 theorem Zorn's_Lemma: 9.24 @@ -28,16 +28,14 @@ 9.25 fix c assume "c \<in> chains S" 9.26 show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" 9.27 proof cases 9.28 - 9.29 - txt \<open>If \<open>c\<close> is an empty chain, then every element in 9.30 - \<open>S\<close> is an upper bound of \<open>c\<close>.\<close> 9.31 + txt \<open>If \<open>c\<close> is an empty chain, then every element in \<open>S\<close> is an upper 9.32 + bound of \<open>c\<close>.\<close> 9.33 9.34 assume "c = {}" 9.35 with aS show ?thesis by fast 9.36 9.37 - txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper 9.38 - bound of \<open>c\<close>, lying in \<open>S\<close>.\<close> 9.39 - 9.40 + txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper bound of \<open>c\<close>, lying in 9.41 + \<open>S\<close>.\<close> 9.42 next 9.43 assume "c \<noteq> {}" 9.44 show ?thesis