summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 02 Nov 2015 11:43:02 +0100 | |

changeset 61541 | f92bf6674699 |

parent 61540 | a29295dac1ca |

child 61542 | 846c72206207 |

tuned document;

--- a/src/HOL/Hahn_Banach/Function_Norm.thy Mon Nov 02 11:10:28 2015 +0100 +++ b/src/HOL/Hahn_Banach/Function_Norm.thy Mon Nov 02 11:43:02 2015 +0100 @@ -11,14 +11,13 @@ subsection \<open>Continuous linear forms\<close> text \<open> - A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> - is \<^emph>\<open>continuous\<close>, iff it is bounded, i.e. + A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>, + iff it is bounded, i.e. \begin{center} \<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> \end{center} - In our application no other functions than linear forms are - considered, so we can define continuous linear forms as bounded - linear forms: + In our application no other functions than linear forms are considered, so + we can define continuous linear forms as bounded linear forms: \<close> locale continuous = linearform + @@ -48,28 +47,25 @@ \end{center} is called the \<^emph>\<open>norm\<close> of \<open>f\<close>. - For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be - defined as + For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be defined as \begin{center} \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> \end{center} - For the case \<open>V = {0}\<close> the supremum would be taken from an - empty set. Since \<open>\<real>\<close> is unbounded, there would be no supremum. - To avoid this situation it must be guaranteed that there is an - element in this set. This element must be \<open>{} \<ge> 0\<close> so that - \<open>fn_norm\<close> has the norm properties. Furthermore it does not - have to change the norm in all other cases, so it must be \<open>0\<close>, - as all other elements are \<open>{} \<ge> 0\<close>. + For the case \<open>V = {0}\<close> the supremum would be taken from an empty set. + Since \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this + situation it must be guaranteed that there is an element in this set. This + element must be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties. + Furthermore it does not have to change the norm in all other cases, so it + must be \<open>0\<close>, as all other elements are \<open>{} \<ge> 0\<close>. - Thus we define the set \<open>B\<close> where the supremum is taken from as - follows: + Thus we define the set \<open>B\<close> where the supremum is taken from as follows: \begin{center} \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close> \end{center} - \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the - supremum exists (otherwise it is undefined). + \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists + (otherwise it is undefined). \<close> locale fn_norm = @@ -84,8 +80,8 @@ by (simp add: B_def) text \<open> - The following lemma states that every continuous linear form on a - normed space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm. + The following lemma states that every continuous linear form on a normed + space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm. \<close> lemma (in normed_vectorspace_with_fn_norm) fn_norm_works: @@ -108,9 +104,9 @@ txt \<open>We know that \<open>f\<close> is bounded by some value \<open>c\<close>.\<close> from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. - txt \<open>To prove the thesis, we have to show that there is some - \<open>b\<close>, such that \<open>y \<le> b\<close> for all \<open>y \<in> - B\<close>. Due to the definition of \<open>B\<close> there are two cases.\<close> + txt \<open>To prove the thesis, we have to show that there is some \<open>b\<close>, such + that \<open>y \<le> b\<close> for all \<open>y \<in> B\<close>. Due to the definition of \<open>B\<close> there are + two cases.\<close> def b \<equiv> "max c 0" have "\<forall>y \<in> B V f. y \<le> b" @@ -237,8 +233,8 @@ text \<open> \<^medskip> - The function norm is the least positive real number for - which the following inequation holds: + The function norm is the least positive real number for which the + following inequality holds: \begin{center} \<open>\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> \end{center}

--- a/src/HOL/Hahn_Banach/Function_Order.thy Mon Nov 02 11:10:28 2015 +0100 +++ b/src/HOL/Hahn_Banach/Function_Order.thy Mon Nov 02 11:43:02 2015 +0100 @@ -70,8 +70,8 @@ where "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))" text \<open> - The following lemma states that \<open>g\<close> is the graph of a function - if the relation induced by \<open>g\<close> is unique. + The following lemma states that \<open>g\<close> is the graph of a function if the + relation induced by \<open>g\<close> is unique. \<close> lemma graph_domain_funct: @@ -93,9 +93,9 @@ subsection \<open>Norm-preserving extensions of a function\<close> text \<open> - 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 of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are bounded by - \<open>p\<close>, is defined as follows. + 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 of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are + bounded by \<open>p\<close>, is defined as follows. \<close> definition

--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Mon Nov 02 11:10:28 2015 +0100 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Mon Nov 02 11:43:02 2015 +0100 @@ -9,37 +9,36 @@ begin text \<open> - We present the proof of two different versions of the Hahn-Banach - Theorem, closely following @{cite \<open>\S36\<close> "Heuser:1986"}. + We present the proof of two different versions of the Hahn-Banach Theorem, + closely following @{cite \<open>\S36\<close> "Heuser:1986"}. \<close> + subsection \<open>The Hahn-Banach Theorem for vector spaces\<close> paragraph \<open>Hahn-Banach Theorem.\<close> text \<open> - 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 - \<open>F\<close> such that \<open>f\<close> is bounded 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 form \<open>h\<close> - on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is - also bounded by \<open>p\<close>. -\<close> + 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 \<open>F\<close> such that \<open>f\<close> is bounded + 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 + form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded + by \<open>p\<close>. \<close> paragraph \<open>Proof Sketch.\<close> text \<open> - \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of - \<open>f\<close> to subspaces of \<open>E\<close>. The linear forms in \<open>M\<close> - are ordered by domain extension. + \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces + of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension. - \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper - bound in \<open>M\<close>. + \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper bound in \<open>M\<close>. - \<^enum> With Zorn's Lemma we conclude that there is a maximal function - \<open>g\<close> in \<open>M\<close>. + \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in + \<open>M\<close>. - \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical contradiction: + \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical + contradiction: - \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can - still be extended in a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>. + \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in + a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>. \<^item> Thus \<open>g\<close> can not be maximal. Contradiction! \<close> @@ -153,7 +152,7 @@ obtain xi where xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi \<and> xi \<le> p (y + x') - h y" - -- \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequations; this will\<close> + -- \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequality; this will\<close> -- \<open>be used to establish that \<open>h'\<close> is a norm-preserving extension of \<open>h\<close>. \label{ex-xi-use}\<^smallskip>\<close> proof - @@ -292,10 +291,10 @@ text \<open> The following alternative formulation of the Hahn-Banach - Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear - form \<open>f\<close> and a seminorm \<open>p\<close> the following inequations - are equivalent:\footnote{This was shown in lemma @{thm [source] - abs_ineq_iff} (see page \pageref{abs-ineq-iff}).} + Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form + \<open>f\<close> and a seminorm \<open>p\<close> the following inequality are + equivalent:\footnote{This was shown in lemma @{thm [source] abs_ineq_iff} + (see page \pageref{abs-ineq-iff}).} \begin{center} \begin{tabular}{lll} \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and & @@ -336,9 +335,9 @@ subsection \<open>The Hahn-Banach Theorem for normed spaces\<close> text \<open> - Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a - norm space \<open>E\<close>, can be extended to a continuous linear form - \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = \<parallel>g\<parallel>\<close>. + Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>, + can be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = + \<parallel>g\<parallel>\<close>. \<close> theorem norm_Hahn_Banach: @@ -420,10 +419,10 @@ OF F_norm, folded B_def fn_norm_def]) qed - txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded - by \<open>p\<close> we can apply the Hahn-Banach Theorem for real vector - spaces. So \<open>f\<close> can be extended in a norm-preserving way to - some function \<open>g\<close> on the whole vector space \<open>E\<close>.\<close> + txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we + can apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be + extended in a norm-preserving way to some function \<open>g\<close> on the whole + vector space \<open>E\<close>.\<close> with E FE linearform q obtain g where linearformE: "linearform E g" @@ -445,19 +444,20 @@ have "\<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F" proof (rule order_antisym) txt \<open> - 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 + 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 \begin{center} \begin{tabular}{l} \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close> \end{tabular} \end{center} - \noindent Furthermore holds + \<^noindent> Furthermore holds \begin{center} \begin{tabular}{l} \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close> \end{tabular} \end{center} -\<close> + \<close> from g_cont _ ge_zero show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"

--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Mon Nov 02 11:10:28 2015 +0100 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Mon Nov 02 11:43:02 2015 +0100 @@ -9,29 +9,27 @@ begin text \<open> - In this section the following context is presumed. Let \<open>E\<close> be - 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 - \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a - 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 - an element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct - sum \<open>H' = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close> - the decomposition of \<open>x = y + a \<cdot> x\<close> 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> for a certain \<open>\<xi>\<close>. + In this section the following context is presumed. Let \<open>E\<close> be 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 \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a + 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 an element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H' + = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close> + 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> + for a certain \<open>\<xi>\<close>. - Subsequently we show some properties of this extension \<open>h'\<close> of - \<open>h\<close>. + Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>. \<^medskip> - This lemma will be used to show the existence of a linear - extension of \<open>f\<close> (see page \pageref{ex-xi-use}). It is a - consequence of the completeness of \<open>\<real>\<close>. To show + This lemma will be used to show the existence of a linear extension of \<open>f\<close> + (see page \pageref{ex-xi-use}). It is a consequence of the completeness of + \<open>\<real>\<close>. To show \begin{center} \begin{tabular}{l} \<open>\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y\<close> \end{tabular} \end{center} - \noindent it suffices to show that + \<^noindent> it suffices to show that \begin{center} \begin{tabular}{l} \<open>\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v\<close> @@ -84,9 +82,8 @@ text \<open> \<^medskip> - 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> is a linear extension of - \<open>h\<close> to \<open>H'\<close>. + 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> is a linear extension of \<open>h\<close> to \<open>H'\<close>. \<close> lemma h'_lf: @@ -192,8 +189,8 @@ text \<open> \<^medskip> - The linear extension \<open>h'\<close> of \<open>h\<close> - is bounded by the seminorm \<open>p\<close>.\<close> + The linear extension \<open>h'\<close> of \<open>h\<close> is bounded by the seminorm \<open>p\<close>. +\<close> lemma h'_norm_pres: assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =

--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Mon Nov 02 11:10:28 2015 +0100 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Mon Nov 02 11:43:02 2015 +0100 @@ -2,27 +2,25 @@ Author: Gertrud Bauer, TU Munich *) -section \<open>The supremum w.r.t.~the function order\<close> +section \<open>The supremum wrt.\ the function order\<close> theory Hahn_Banach_Sup_Lemmas imports Function_Norm Zorn_Lemma begin text \<open> - This section contains some lemmas that will be used in the proof of - the Hahn-Banach Theorem. In this section the following context is - presumed. Let \<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 \<open>E\<close> and - \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> - of norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c = - graph H h\<close>. We will show some properties about the limit function - \<open>h\<close>, i.e.\ the supremum of the chain \<open>c\<close>. + This section contains some lemmas that will be used in the proof of the + Hahn-Banach Theorem. In this section the following context is presumed. + Let \<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 \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of + norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will + show some properties about the limit function \<open>h\<close>, i.e.\ the supremum of + the chain \<open>c\<close>. \<^medskip> - Let \<open>c\<close> be a chain of norm-preserving extensions of - the function \<open>f\<close> and let \<open>graph H h\<close> be the supremum - of \<open>c\<close>. Every element in \<open>H\<close> is member of one of the - elements of the chain. + Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and + let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of + one of the elements of the chain. \<close> lemmas [dest?] = chainsD @@ -57,10 +55,10 @@ text \<open> \<^medskip> - Let \<open>c\<close> be a chain of norm-preserving extensions of - the function \<open>f\<close> and let \<open>graph H h\<close> be the supremum - of \<open>c\<close>. Every element in the domain \<open>H\<close> of the supremum - function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends \<open>h'\<close>. + Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and + let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of + the supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, + such that \<open>h\<close> extends \<open>h'\<close>. \<close> lemma some_H'h': @@ -85,10 +83,9 @@ text \<open> \<^medskip> - Any two elements \<open>x\<close> and \<open>y\<close> in the domain - \<open>H\<close> of the supremum function \<open>h\<close> are both in the domain - \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends - \<open>h'\<close>. + Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function + \<open>h\<close> are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> + extends \<open>h'\<close>. \<close> lemma some_H'h'2: @@ -158,8 +155,8 @@ text \<open> \<^medskip> - The relation induced by the graph of the supremum of a - chain \<open>c\<close> is definite, i.~e.~t is the graph of a function. + The relation induced by the graph of the supremum of a chain \<open>c\<close> is + definite, i.e.\ it is the graph of a function. \<close> lemma sup_definite: @@ -181,8 +178,8 @@ then obtain H2 h2 where G2_rep: "G2 = graph H2 h2" unfolding M_def by blast - 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> are members of \<open>c\<close>. \label{cases2}\<close> + 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> + are members of \<open>c\<close>. \label{cases2}\<close> from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1" by (blast dest: chainsD) @@ -208,12 +205,11 @@ text \<open> \<^medskip> - The limit function \<open>h\<close> is linear. Every element - \<open>x\<close> in the domain of \<open>h\<close> is in the domain of a function - \<open>h'\<close> in the chain of norm preserving extensions. Furthermore, - \<open>h\<close> is an extension of \<open>h'\<close> so the function values of - \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>. Finally, the - function \<open>h'\<close> is linear by construction of \<open>M\<close>. + The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close> + is in the domain of a function \<open>h'\<close> in the chain of norm preserving + extensions. Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function + values of \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close> + is linear by construction of \<open>M\<close>. \<close> lemma sup_lf: @@ -264,10 +260,9 @@ text \<open> \<^medskip> - The limit of a non-empty chain of norm preserving - extensions of \<open>f\<close> is an extension of \<open>f\<close>, since every - element of the chain is an extension of \<open>f\<close> and the supremum - is an extension for every element of the chain. + The limit of a non-empty chain of norm preserving extensions of \<open>f\<close> is an + extension of \<open>f\<close>, since every element of the chain is an extension of \<open>f\<close> + and the supremum is an extension for every element of the chain. \<close> lemma sup_ext: @@ -291,9 +286,8 @@ text \<open> \<^medskip> - The domain \<open>H\<close> of the limit function is a superspace - of \<open>F\<close>, since \<open>F\<close> is a subset of \<open>H\<close>. The - existence of the \<open>0\<close> element in \<open>F\<close> and the closure + The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is + a subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure properties follow from the fact that \<open>F\<close> is a vector space. \<close> @@ -317,8 +311,7 @@ text \<open> \<^medskip> - The domain \<open>H\<close> of the limit function is a subspace of - \<open>E\<close>. + The domain \<open>H\<close> of the limit function is a subspace of \<open>E\<close>. \<close> lemma sup_subE: @@ -374,8 +367,8 @@ text \<open> \<^medskip> - The limit function is bounded by the norm \<open>p\<close> as - well, since all elements in the chain are bounded by \<open>p\<close>. + The limit function is bounded by the norm \<open>p\<close> as well, since all elements + in the chain are bounded by \<open>p\<close>. \<close> lemma sup_norm_pres: @@ -396,10 +389,10 @@ text \<open> \<^medskip> - The following lemma is a property of linear forms on real - vector spaces. It will be used for the lemma \<open>abs_Hahn_Banach\<close> - (see page \pageref{abs-Hahn_Banach}). \label{abs-ineq-iff} For real - vector spaces the following inequations are equivalent: + The following lemma is a property of linear forms on real vector spaces. + It will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page + \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces + the following inequality are equivalent: \begin{center} \begin{tabular}{lll} \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &

--- a/src/HOL/Hahn_Banach/Linearform.thy Mon Nov 02 11:10:28 2015 +0100 +++ b/src/HOL/Hahn_Banach/Linearform.thy Mon Nov 02 11:43:02 2015 +0100 @@ -9,8 +9,8 @@ begin text \<open> - A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals - that is additive and multiplicative. + A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is + additive and multiplicative. \<close> locale linearform =

--- a/src/HOL/Hahn_Banach/Normed_Space.thy Mon Nov 02 11:10:28 2015 +0100 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy Mon Nov 02 11:43:02 2015 +0100 @@ -11,9 +11,9 @@ subsection \<open>Quasinorms\<close> text \<open> - A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space - into the reals that has the following properties: it is positive - definite, absolute homogeneous and subadditive. + A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals + that has the following properties: it is positive definite, absolute + homogeneous and subadditive. \<close> locale seminorm =

--- a/src/HOL/Hahn_Banach/Subspace.thy Mon Nov 02 11:10:28 2015 +0100 +++ b/src/HOL/Hahn_Banach/Subspace.thy Mon Nov 02 11:43:02 2015 +0100 @@ -11,9 +11,8 @@ subsection \<open>Definition\<close> text \<open> - 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 \<open>U\<close> is closed under addition - and scalar multiplication. + 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 + \<open>U\<close> is closed under addition and scalar multiplication. \<close> locale subspace = @@ -51,9 +50,9 @@ text \<open> \<^medskip> - Similar as for linear spaces, the existence of the zero - element in every subspace follows from the non-emptiness of the - carrier set and by vector space laws. + Similar as for linear spaces, the existence of the zero element in every + subspace follows from the non-emptiness of the carrier set and by vector + space laws. \<close> lemma (in subspace) zero [intro]: @@ -140,8 +139,8 @@ subsection \<open>Linear closure\<close> text \<open> - The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all - scalar multiples of \<open>x\<close>. + The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples + of \<open>x\<close>. \<close> definition lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set" @@ -227,8 +226,8 @@ subsection \<open>Sum of two vectorspaces\<close> text \<open> - The \<^emph>\<open>sum\<close> of two vectorspaces \<open>U\<close> and \<open>V\<close> is the - set of all sums of elements from \<open>U\<close> and \<open>V\<close>. + The \<^emph>\<open>sum\<close> of two vectorspaces \<open>U\<close> and \<open>V\<close> is the set of all sums of + elements from \<open>U\<close> and \<open>V\<close>. \<close> lemma sum_def: "U + V = {u + v | u v. u \<in> U \<and> v \<in> V}" @@ -329,10 +328,10 @@ subsection \<open>Direct sums\<close> text \<open> - The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the - 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 - \<open>V\<close> the decomposition in \<open>x = u + v\<close> with - \<open>u \<in> U\<close> and \<open>v \<in> V\<close> is unique. + The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the 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 \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and + \<open>v \<in> V\<close> is unique. \<close> lemma decomp: @@ -377,12 +376,10 @@ qed text \<open> - An application of the previous lemma will be used in the proof of - the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any - element \<open>y + a \<cdot> x\<^sub>0\<close> of the direct sum of a - vectorspace \<open>H\<close> and the linear closure of \<open>x\<^sub>0\<close> - the components \<open>y \<in> H\<close> and \<open>a\<close> are uniquely - determined. + An application of the previous lemma will be used in the proof of the + Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any element + \<open>y + a \<cdot> x\<^sub>0\<close> of the direct sum of a vectorspace \<open>H\<close> and the linear closure + of \<open>x\<^sub>0\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are uniquely determined. \<close> lemma decomp_H': @@ -436,10 +433,9 @@ qed text \<open> - Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a - vectorspace \<open>H\<close> and the linear closure of \<open>x'\<close> the - components \<open>y \<in> H\<close> and \<open>a\<close> are unique, it follows from - \<open>y \<in> H\<close> that \<open>a = 0\<close>. + Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a vectorspace \<open>H\<close> + and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique, + it follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>. \<close> lemma decomp_H'_H: @@ -464,9 +460,8 @@ qed text \<open> - The components \<open>y \<in> H\<close> and \<open>a\<close> in \<open>y + a \<cdot> x'\<close> - are unique, so the function \<open>h'\<close> defined by - \<open>h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>\<close> is definite. + The components \<open>y \<in> H\<close> and \<open>a\<close> in \<open>y + a \<cdot> x'\<close> are unique, so the function + \<open>h'\<close> defined by \<open>h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>\<close> is definite. \<close> lemma h'_definite:

--- a/src/HOL/Hahn_Banach/Vector_Space.thy Mon Nov 02 11:10:28 2015 +0100 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy Mon Nov 02 11:43:02 2015 +0100 @@ -11,9 +11,9 @@ subsection \<open>Signature\<close> text \<open> - For the definition of real vector spaces a type @{typ 'a} of the - sort \<open>{plus, minus, zero}\<close> is considered, on which a real - scalar multiplication \<open>\<cdot>\<close> is declared. + For the definition of real vector spaces a type @{typ 'a} of the sort + \<open>{plus, minus, zero}\<close> is considered, on which a real scalar multiplication + \<open>\<cdot>\<close> is declared. \<close> consts @@ -23,13 +23,13 @@ subsection \<open>Vector space laws\<close> text \<open> - A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from - @{typ 'a} with the following vector space laws: The set \<open>V\<close> is - closed under addition and scalar multiplication, addition is - 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 - addition. Addition and multiplication are distributive; scalar - multiplication is associative and the real number \<open>1\<close> is - the neutral element of scalar multiplication. + A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with + the following vector space laws: The set \<open>V\<close> is closed under addition and + scalar multiplication, addition is associative and commutative; \<open>- x\<close> is + the inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of + addition. Addition and multiplication are distributive; scalar + multiplication is associative and the real number \<open>1\<close> is the neutral + element of scalar multiplication. \<close> locale vectorspace = @@ -64,7 +64,8 @@ lemma neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V" by (simp add: negate_eq1) -lemma add_left_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)" +lemma add_left_commute: + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)" proof - assume xyz: "x \<in> V" "y \<in> V" "z \<in> V" then have "x + (y + z) = (x + y) + z" @@ -77,8 +78,8 @@ lemmas add_ac = add_assoc add_commute add_left_commute -text \<open>The existence of the zero element of a vector space - follows from the non-emptiness of carrier set.\<close> +text \<open>The existence of the zero element of a vector space follows from the + non-emptiness of carrier set.\<close> lemma zero [iff]: "0 \<in> V" proof - @@ -213,7 +214,8 @@ then show "x + y = x + z" by (simp only:) qed -lemma add_right_cancel: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)" +lemma add_right_cancel: + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)" by (simp only: add_commute add_left_cancel) lemma add_assoc_cong: @@ -371,4 +373,3 @@ end end -

--- a/src/HOL/Hahn_Banach/document/root.tex Mon Nov 02 11:10:28 2015 +0100 +++ b/src/HOL/Hahn_Banach/document/root.tex Mon Nov 02 11:43:02 2015 +0100 @@ -16,7 +16,7 @@ \pagenumbering{arabic} \title{The Hahn-Banach Theorem \\ for Real Vector Spaces} -\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}} +\author{Gertrud Bauer} \maketitle \begin{abstract}