# HG changeset patch # User wenzelm # Date 1245872814 -7200 # Node ID be3e1cc5005cd6a6bd31d9ab05e4e745a4f27ca2 # Parent 71af1fd6a5e4422b23ebe5b981cf29b68e424868 standard naming conventions for session and theories; diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/Bounds.thy --- a/src/HOL/HahnBanach/Bounds.thy Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,82 +0,0 @@ -(* Title: HOL/Real/HahnBanach/Bounds.thy - Author: Gertrud Bauer, TU Munich -*) - -header {* Bounds *} - -theory Bounds -imports Main ContNotDenum -begin - -locale lub = - fixes A and x - assumes least [intro?]: "(\a. a \ A \ a \ b) \ x \ b" - and upper [intro?]: "a \ A \ a \ x" - -lemmas [elim?] = lub.least lub.upper - -definition - the_lub :: "'a::order set \ 'a" where - "the_lub A = The (lub A)" - -notation (xsymbols) - the_lub ("\_" [90] 90) - -lemma the_lub_equality [elim?]: - assumes "lub A x" - shows "\A = (x::'a::order)" -proof - - interpret lub A x by fact - show ?thesis - proof (unfold the_lub_def) - from `lub A x` show "The (lub A) = x" - proof - fix x' assume lub': "lub A x'" - show "x' = x" - proof (rule order_antisym) - from lub' show "x' \ x" - proof - fix a assume "a \ A" - then show "a \ x" .. - qed - show "x \ x'" - proof - fix a assume "a \ A" - with lub' show "a \ x'" .. - qed - qed - qed - qed -qed - -lemma the_lubI_ex: - assumes ex: "\x. lub A x" - shows "lub A (\A)" -proof - - from ex obtain x where x: "lub A x" .. - also from x have [symmetric]: "\A = x" .. - finally show ?thesis . -qed - -lemma lub_compat: "lub A x = isLub UNIV A x" -proof - - have "isUb UNIV A = (\x. A *<= x \ x \ UNIV)" - by (rule ext) (simp only: isUb_def) - then show ?thesis - by (simp only: lub_def isLub_def leastP_def setge_def setle_def) blast -qed - -lemma real_complete: - fixes A :: "real set" - assumes nonempty: "\a. a \ A" - and ex_upper: "\y. \a \ A. a \ y" - shows "\x. lub A x" -proof - - from ex_upper have "\y. isUb UNIV A y" - unfolding isUb_def setle_def by blast - with nonempty have "\x. isLub UNIV A x" - by (rule reals_complete) - then show ?thesis by (simp only: lub_compat) -qed - -end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/FunctionNorm.thy --- a/src/HOL/HahnBanach/FunctionNorm.thy Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,278 +0,0 @@ -(* Title: HOL/Real/HahnBanach/FunctionNorm.thy - Author: Gertrud Bauer, TU Munich -*) - -header {* The norm of a function *} - -theory FunctionNorm -imports NormedSpace FunctionOrder -begin - -subsection {* Continuous linear forms*} - -text {* - A linear form @{text f} on a normed vector space @{text "(V, \\\)"} - is \emph{continuous}, iff it is bounded, i.e. - \begin{center} - @{text "\c \ R. \x \ V. \f x\ \ c \ \x\"} - \end{center} - In our application no other functions than linear forms are - considered, so we can define continuous linear forms as bounded - linear forms: -*} - -locale continuous = var_V + norm_syntax + linearform + - assumes bounded: "\c. \x \ V. \f x\ \ c * \x\" - -declare continuous.intro [intro?] continuous_axioms.intro [intro?] - -lemma continuousI [intro]: - fixes norm :: "_ \ real" ("\_\") - assumes "linearform V f" - assumes r: "\x. x \ V \ \f x\ \ c * \x\" - shows "continuous V norm f" -proof - show "linearform V f" by fact - from r have "\c. \x\V. \f x\ \ c * \x\" by blast - then show "continuous_axioms V norm f" .. -qed - - -subsection {* The norm of a linear form *} - -text {* - The least real number @{text c} for which holds - \begin{center} - @{text "\x \ V. \f x\ \ c \ \x\"} - \end{center} - is called the \emph{norm} of @{text f}. - - For non-trivial vector spaces @{text "V \ {0}"} the norm can be - defined as - \begin{center} - @{text "\f\ = \x \ 0. \f x\ / \x\"} - \end{center} - - For the case @{text "V = {0}"} the supremum would be taken from an - empty set. Since @{text \} 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 @{text "{} \ 0"} so that - @{text fn_norm} has the norm properties. Furthermore it does not - have to change the norm in all other cases, so it must be @{text 0}, - as all other elements are @{text "{} \ 0"}. - - Thus we define the set @{text B} where the supremum is taken from as - follows: - \begin{center} - @{text "{0} \ {\f x\ / \x\. x \ 0 \ x \ F}"} - \end{center} - - @{text fn_norm} is equal to the supremum of @{text B}, if the - supremum exists (otherwise it is undefined). -*} - -locale fn_norm = norm_syntax + - fixes B defines "B V f \ {0} \ {\f x\ / \x\ | x. x \ 0 \ x \ V}" - fixes fn_norm ("\_\\_" [0, 1000] 999) - defines "\f\\V \ \(B V f)" - -locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm - -lemma (in fn_norm) B_not_empty [intro]: "0 \ B V f" - by (simp add: B_def) - -text {* - The following lemma states that every continuous linear form on a - normed space @{text "(V, \\\)"} has a function norm. -*} - -lemma (in normed_vectorspace_with_fn_norm) fn_norm_works: - assumes "continuous V norm f" - shows "lub (B V f) (\f\\V)" -proof - - interpret continuous V norm f by fact - txt {* The existence of the supremum is shown using the - completeness of the reals. Completeness means, that every - non-empty bounded set of reals has a supremum. *} - have "\a. lub (B V f) a" - proof (rule real_complete) - txt {* First we have to show that @{text B} is non-empty: *} - have "0 \ B V f" .. - then show "\x. x \ B V f" .. - - txt {* Then we have to show that @{text B} is bounded: *} - show "\c. \y \ B V f. y \ c" - proof - - txt {* We know that @{text f} is bounded by some value @{text c}. *} - from bounded obtain c where c: "\x \ V. \f x\ \ c * \x\" .. - - txt {* To prove the thesis, we have to show that there is some - @{text b}, such that @{text "y \ b"} for all @{text "y \ - B"}. Due to the definition of @{text B} there are two cases. *} - - def b \ "max c 0" - have "\y \ B V f. y \ b" - proof - fix y assume y: "y \ B V f" - show "y \ b" - proof cases - assume "y = 0" - then show ?thesis unfolding b_def by arith - next - txt {* The second case is @{text "y = \f x\ / \x\"} for some - @{text "x \ V"} with @{text "x \ 0"}. *} - assume "y \ 0" - with y obtain x where y_rep: "y = \f x\ * inverse \x\" - and x: "x \ V" and neq: "x \ 0" - by (auto simp add: B_def real_divide_def) - from x neq have gt: "0 < \x\" .. - - txt {* The thesis follows by a short calculation using the - fact that @{text f} is bounded. *} - - note y_rep - also have "\f x\ * inverse \x\ \ (c * \x\) * inverse \x\" - proof (rule mult_right_mono) - from c x show "\f x\ \ c * \x\" .. - from gt have "0 < inverse \x\" - by (rule positive_imp_inverse_positive) - then show "0 \ inverse \x\" by (rule order_less_imp_le) - qed - also have "\ = c * (\x\ * inverse \x\)" - by (rule real_mult_assoc) - also - from gt have "\x\ \ 0" by simp - then have "\x\ * inverse \x\ = 1" by simp - also have "c * 1 \ b" by (simp add: b_def le_maxI1) - finally show "y \ b" . - qed - qed - then show ?thesis .. - qed - qed - then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex) -qed - -lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]: - assumes "continuous V norm f" - assumes b: "b \ B V f" - shows "b \ \f\\V" -proof - - interpret continuous V norm f by fact - have "lub (B V f) (\f\\V)" - using `continuous V norm f` by (rule fn_norm_works) - from this and b show ?thesis .. -qed - -lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB: - assumes "continuous V norm f" - assumes b: "\b. b \ B V f \ b \ y" - shows "\f\\V \ y" -proof - - interpret continuous V norm f by fact - have "lub (B V f) (\f\\V)" - using `continuous V norm f` by (rule fn_norm_works) - from this and b show ?thesis .. -qed - -text {* The norm of a continuous function is always @{text "\ 0"}. *} - -lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]: - assumes "continuous V norm f" - shows "0 \ \f\\V" -proof - - interpret continuous V norm f by fact - txt {* The function norm is defined as the supremum of @{text B}. - So it is @{text "\ 0"} if all elements in @{text B} are @{text "\ - 0"}, provided the supremum exists and @{text B} is not empty. *} - have "lub (B V f) (\f\\V)" - using `continuous V norm f` by (rule fn_norm_works) - moreover have "0 \ B V f" .. - ultimately show ?thesis .. -qed - -text {* - \medskip The fundamental property of function norms is: - \begin{center} - @{text "\f x\ \ \f\ \ \x\"} - \end{center} -*} - -lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong: - assumes "continuous V norm f" "linearform V f" - assumes x: "x \ V" - shows "\f x\ \ \f\\V * \x\" -proof - - interpret continuous V norm f by fact - interpret linearform V f by fact - show ?thesis - proof cases - assume "x = 0" - then have "\f x\ = \f 0\" by simp - also have "f 0 = 0" by rule unfold_locales - also have "\\\ = 0" by simp - also have a: "0 \ \f\\V" - using `continuous V norm f` by (rule fn_norm_ge_zero) - from x have "0 \ norm x" .. - with a have "0 \ \f\\V * \x\" by (simp add: zero_le_mult_iff) - finally show "\f x\ \ \f\\V * \x\" . - next - assume "x \ 0" - with x have neq: "\x\ \ 0" by simp - then have "\f x\ = (\f x\ * inverse \x\) * \x\" by simp - also have "\ \ \f\\V * \x\" - proof (rule mult_right_mono) - from x show "0 \ \x\" .. - from x and neq have "\f x\ * inverse \x\ \ B V f" - by (auto simp add: B_def real_divide_def) - with `continuous V norm f` show "\f x\ * inverse \x\ \ \f\\V" - by (rule fn_norm_ub) - qed - finally show ?thesis . - qed -qed - -text {* - \medskip The function norm is the least positive real number for - which the following inequation holds: - \begin{center} - @{text "\f x\ \ c \ \x\"} - \end{center} -*} - -lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]: - assumes "continuous V norm f" - assumes ineq: "\x \ V. \f x\ \ c * \x\" and ge: "0 \ c" - shows "\f\\V \ c" -proof - - interpret continuous V norm f by fact - show ?thesis - proof (rule fn_norm_leastB [folded B_def fn_norm_def]) - fix b assume b: "b \ B V f" - show "b \ c" - proof cases - assume "b = 0" - with ge show ?thesis by simp - next - assume "b \ 0" - with b obtain x where b_rep: "b = \f x\ * inverse \x\" - and x_neq: "x \ 0" and x: "x \ V" - by (auto simp add: B_def real_divide_def) - note b_rep - also have "\f x\ * inverse \x\ \ (c * \x\) * inverse \x\" - proof (rule mult_right_mono) - have "0 < \x\" using x x_neq .. - then show "0 \ inverse \x\" by simp - from ineq and x show "\f x\ \ c * \x\" .. - qed - also have "\ = c" - proof - - from x_neq and x have "\x\ \ 0" by simp - then show ?thesis by simp - qed - finally show ?thesis . - qed - qed (insert `continuous V norm f`, simp_all add: continuous_def) -qed - -end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/FunctionOrder.thy --- a/src/HOL/HahnBanach/FunctionOrder.thy Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,142 +0,0 @@ -(* Title: HOL/Real/HahnBanach/FunctionOrder.thy - ID: $Id$ - Author: Gertrud Bauer, TU Munich -*) - -header {* An order on functions *} - -theory FunctionOrder -imports Subspace Linearform -begin - -subsection {* The graph of a function *} - -text {* - We define the \emph{graph} of a (real) function @{text f} with - domain @{text F} as the set - \begin{center} - @{text "{(x, f x). x \ F}"} - \end{center} - So we are modeling partial functions by specifying the domain and - the mapping function. We use the term ``function'' also for its - graph. -*} - -types 'a graph = "('a \ real) set" - -definition - graph :: "'a set \ ('a \ real) \ 'a graph" where - "graph F f = {(x, f x) | x. x \ F}" - -lemma graphI [intro]: "x \ F \ (x, f x) \ graph F f" - unfolding graph_def by blast - -lemma graphI2 [intro?]: "x \ F \ \t \ graph F f. t = (x, f x)" - unfolding graph_def by blast - -lemma graphE [elim?]: - "(x, y) \ graph F f \ (x \ F \ y = f x \ C) \ C" - unfolding graph_def by blast - - -subsection {* Functions ordered by domain extension *} - -text {* - A function @{text h'} is an extension of @{text h}, iff the graph of - @{text h} is a subset of the graph of @{text h'}. -*} - -lemma graph_extI: - "(\x. x \ H \ h x = h' x) \ H \ H' - \ graph H h \ graph H' h'" - unfolding graph_def by blast - -lemma graph_extD1 [dest?]: - "graph H h \ graph H' h' \ x \ H \ h x = h' x" - unfolding graph_def by blast - -lemma graph_extD2 [dest?]: - "graph H h \ graph H' h' \ H \ H'" - unfolding graph_def by blast - - -subsection {* Domain and function of a graph *} - -text {* - The inverse functions to @{text graph} are @{text domain} and @{text - funct}. -*} - -definition - "domain" :: "'a graph \ 'a set" where - "domain g = {x. \y. (x, y) \ g}" - -definition - funct :: "'a graph \ ('a \ real)" where - "funct g = (\x. (SOME y. (x, y) \ g))" - -text {* - The following lemma states that @{text g} is the graph of a function - if the relation induced by @{text g} is unique. -*} - -lemma graph_domain_funct: - assumes uniq: "\x y z. (x, y) \ g \ (x, z) \ g \ z = y" - shows "graph (domain g) (funct g) = g" - unfolding domain_def funct_def graph_def -proof auto (* FIXME !? *) - fix a b assume g: "(a, b) \ g" - from g show "(a, SOME y. (a, y) \ g) \ g" by (rule someI2) - from g show "\y. (a, y) \ g" .. - from g show "b = (SOME y. (a, y) \ g)" - proof (rule some_equality [symmetric]) - fix y assume "(a, y) \ g" - with g show "y = b" by (rule uniq) - qed -qed - - -subsection {* Norm-preserving extensions of a function *} - -text {* - Given a linear form @{text f} on the space @{text F} and a seminorm - @{text p} on @{text E}. The set of all linear extensions of @{text - f}, to superspaces @{text H} of @{text F}, which are bounded by - @{text p}, is defined as follows. -*} - -definition - norm_pres_extensions :: - "'a::{plus, minus, uminus, zero} set \ ('a \ real) \ 'a set \ ('a \ real) - \ 'a graph set" where - "norm_pres_extensions E p F f - = {g. \H h. g = graph H h - \ linearform H h - \ H \ E - \ F \ H - \ graph F f \ graph H h - \ (\x \ H. h x \ p x)}" - -lemma norm_pres_extensionE [elim]: - "g \ norm_pres_extensions E p F f - \ (\H h. g = graph H h \ linearform H h - \ H \ E \ F \ H \ graph F f \ graph H h - \ \x \ H. h x \ p x \ C) \ C" - unfolding norm_pres_extensions_def by blast - -lemma norm_pres_extensionI2 [intro]: - "linearform H h \ H \ E \ F \ H - \ graph F f \ graph H h \ \x \ H. h x \ p x - \ graph H h \ norm_pres_extensions E p F f" - unfolding norm_pres_extensions_def by blast - -lemma norm_pres_extensionI: (* FIXME ? *) - "\H h. g = graph H h - \ linearform H h - \ H \ E - \ F \ H - \ graph F f \ graph H h - \ (\x \ H. h x \ p x) \ g \ norm_pres_extensions E p F f" - unfolding norm_pres_extensions_def by blast - -end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/HahnBanach.thy --- a/src/HOL/HahnBanach/HahnBanach.thy Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,509 +0,0 @@ -(* Title: HOL/Real/HahnBanach/HahnBanach.thy - Author: Gertrud Bauer, TU Munich -*) - -header {* The Hahn-Banach Theorem *} - -theory HahnBanach -imports HahnBanachLemmas -begin - -text {* - We present the proof of two different versions of the Hahn-Banach - Theorem, closely following \cite[\S36]{Heuser:1986}. -*} - -subsection {* The Hahn-Banach Theorem for vector spaces *} - -text {* - \textbf{Hahn-Banach Theorem.} Let @{text F} be a subspace of a real - vector space @{text E}, let @{text p} be a semi-norm on @{text E}, - and @{text f} be a linear form defined on @{text F} such that @{text - f} is bounded by @{text p}, i.e. @{text "\x \ F. f x \ p x"}. Then - @{text f} can be extended to a linear form @{text h} on @{text E} - such that @{text h} is norm-preserving, i.e. @{text h} is also - bounded by @{text p}. - - \bigskip - \textbf{Proof Sketch.} - \begin{enumerate} - - \item Define @{text M} as the set of norm-preserving extensions of - @{text f} to subspaces of @{text E}. The linear forms in @{text M} - are ordered by domain extension. - - \item We show that every non-empty chain in @{text M} has an upper - bound in @{text M}. - - \item With Zorn's Lemma we conclude that there is a maximal function - @{text g} in @{text M}. - - \item The domain @{text H} of @{text g} is the whole space @{text - E}, as shown by classical contradiction: - - \begin{itemize} - - \item Assuming @{text g} is not defined on whole @{text E}, it can - still be extended in a norm-preserving way to a super-space @{text - H'} of @{text H}. - - \item Thus @{text g} can not be maximal. Contradiction! - - \end{itemize} - \end{enumerate} -*} - -theorem HahnBanach: - assumes E: "vectorspace E" and "subspace F E" - and "seminorm E p" and "linearform F f" - assumes fp: "\x \ F. f x \ p x" - shows "\h. linearform E h \ (\x \ F. h x = f x) \ (\x \ E. h x \ p x)" - -- {* Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E}, *} - -- {* and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p}, *} - -- {* then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp *} -proof - - interpret vectorspace E by fact - interpret subspace F E by fact - interpret seminorm E p by fact - interpret linearform F f by fact - def M \ "norm_pres_extensions E p F f" - then have M: "M = \" by (simp only:) - from E have F: "vectorspace F" .. - note FE = `F \ E` - { - fix c assume cM: "c \ chain M" and ex: "\x. x \ c" - have "\c \ M" - -- {* Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}: *} - -- {* @{text "\c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\c \ M"}. *} - unfolding M_def - proof (rule norm_pres_extensionI) - let ?H = "domain (\c)" - let ?h = "funct (\c)" - - have a: "graph ?H ?h = \c" - proof (rule graph_domain_funct) - fix x y z assume "(x, y) \ \c" and "(x, z) \ \c" - with M_def cM show "z = y" by (rule sup_definite) - qed - moreover from M cM a have "linearform ?H ?h" - by (rule sup_lf) - moreover from a M cM ex FE E have "?H \ E" - by (rule sup_subE) - moreover from a M cM ex FE have "F \ ?H" - by (rule sup_supF) - moreover from a M cM ex have "graph F f \ graph ?H ?h" - by (rule sup_ext) - moreover from a M cM have "\x \ ?H. ?h x \ p x" - by (rule sup_norm_pres) - ultimately show "\H h. \c = graph H h - \ linearform H h - \ H \ E - \ F \ H - \ graph F f \ graph H h - \ (\x \ H. h x \ p x)" by blast - qed - } - then have "\g \ M. \x \ M. g \ x \ g = x" - -- {* With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp *} - proof (rule Zorn's_Lemma) - -- {* We show that @{text M} is non-empty: *} - show "graph F f \ M" - unfolding M_def - proof (rule norm_pres_extensionI2) - show "linearform F f" by fact - show "F \ E" by fact - from F show "F \ F" by (rule vectorspace.subspace_refl) - show "graph F f \ graph F f" .. - show "\x\F. f x \ p x" by fact - qed - qed - then obtain g where gM: "g \ M" and gx: "\x \ M. g \ x \ g = x" - by blast - from gM obtain H h where - g_rep: "g = graph H h" - and linearform: "linearform H h" - and HE: "H \ E" and FH: "F \ H" - and graphs: "graph F f \ graph H h" - and hp: "\x \ H. h x \ p x" unfolding M_def .. - -- {* @{text g} is a norm-preserving extension of @{text f}, in other words: *} - -- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *} - -- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *} - from HE E have H: "vectorspace H" - by (rule subspace.vectorspace) - - have HE_eq: "H = E" - -- {* We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp *} - proof (rule classical) - assume neq: "H \ E" - -- {* Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended *} - -- {* in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \skp *} - have "\g' \ M. g \ g' \ g \ g'" - proof - - from HE have "H \ E" .. - with neq obtain x' where x'E: "x' \ E" and "x' \ H" by blast - obtain x': "x' \ 0" - proof - show "x' \ 0" - proof - assume "x' = 0" - with H have "x' \ H" by (simp only: vectorspace.zero) - with `x' \ H` show False by contradiction - qed - qed - - def H' \ "H + lin x'" - -- {* Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp *} - have HH': "H \ H'" - proof (unfold H'_def) - from x'E have "vectorspace (lin x')" .. - with H show "H \ H + lin x'" .. - qed - - obtain xi where - xi: "\y \ H. - p (y + x') - h y \ xi - \ xi \ p (y + x') - h y" - -- {* Pick a real number @{text \} that fulfills certain inequations; this will *} - -- {* be used to establish that @{text h'} is a norm-preserving extension of @{text h}. - \label{ex-xi-use}\skp *} - proof - - from H have "\xi. \y \ H. - p (y + x') - h y \ xi - \ xi \ p (y + x') - h y" - proof (rule ex_xi) - fix u v assume u: "u \ H" and v: "v \ H" - with HE have uE: "u \ E" and vE: "v \ E" by auto - from H u v linearform have "h v - h u = h (v - u)" - by (simp add: linearform.diff) - also from hp and H u v have "\ \ p (v - u)" - by (simp only: vectorspace.diff_closed) - also from x'E uE vE have "v - u = x' + - x' + v + - u" - by (simp add: diff_eq1) - also from x'E uE vE have "\ = v + x' + - (u + x')" - by (simp add: add_ac) - also from x'E uE vE have "\ = (v + x') - (u + x')" - by (simp add: diff_eq1) - also from x'E uE vE E have "p \ \ p (v + x') + p (u + x')" - by (simp add: diff_subadditive) - finally have "h v - h u \ p (v + x') + p (u + x')" . - then show "- p (u + x') - h u \ p (v + x') - h v" by simp - qed - then show thesis by (blast intro: that) - qed - - def h' \ "\x. let (y, a) = - SOME (y, a). x = y + a \ x' \ y \ H in h y + a * xi" - -- {* Define the extension @{text h'} of @{text h} to @{text H'} using @{text \}. \skp *} - - have "g \ graph H' h' \ g \ graph H' h'" - -- {* @{text h'} is an extension of @{text h} \dots \skp *} - proof - show "g \ graph H' h'" - proof - - have "graph H h \ graph H' h'" - proof (rule graph_extI) - fix t assume t: "t \ H" - from E HE t have "(SOME (y, a). t = y + a \ x' \ y \ H) = (t, 0)" - using `x' \ H` `x' \ E` `x' \ 0` by (rule decomp_H'_H) - with h'_def show "h t = h' t" by (simp add: Let_def) - next - from HH' show "H \ H'" .. - qed - with g_rep show ?thesis by (simp only:) - qed - - show "g \ graph H' h'" - proof - - have "graph H h \ graph H' h'" - proof - assume eq: "graph H h = graph H' h'" - have "x' \ H'" - unfolding H'_def - proof - from H show "0 \ H" by (rule vectorspace.zero) - from x'E show "x' \ lin x'" by (rule x_lin_x) - from x'E show "x' = 0 + x'" by simp - qed - then have "(x', h' x') \ graph H' h'" .. - with eq have "(x', h' x') \ graph H h" by (simp only:) - then have "x' \ H" .. - with `x' \ H` show False by contradiction - qed - with g_rep show ?thesis by simp - qed - qed - moreover have "graph H' h' \ M" - -- {* and @{text h'} is norm-preserving. \skp *} - proof (unfold M_def) - show "graph H' h' \ norm_pres_extensions E p F f" - proof (rule norm_pres_extensionI2) - show "linearform H' h'" - using h'_def H'_def HE linearform `x' \ H` `x' \ E` `x' \ 0` E - by (rule h'_lf) - show "H' \ E" - unfolding H'_def - proof - show "H \ E" by fact - show "vectorspace E" by fact - from x'E show "lin x' \ E" .. - qed - from H `F \ H` HH' show FH': "F \ H'" - by (rule vectorspace.subspace_trans) - show "graph F f \ graph H' h'" - proof (rule graph_extI) - fix x assume x: "x \ F" - with graphs have "f x = h x" .. - also have "\ = h x + 0 * xi" by simp - also have "\ = (let (y, a) = (x, 0) in h y + a * xi)" - by (simp add: Let_def) - also have "(x, 0) = - (SOME (y, a). x = y + a \ x' \ y \ H)" - using E HE - proof (rule decomp_H'_H [symmetric]) - from FH x show "x \ H" .. - from x' show "x' \ 0" . - show "x' \ H" by fact - show "x' \ E" by fact - qed - also have - "(let (y, a) = (SOME (y, a). x = y + a \ x' \ y \ H) - in h y + a * xi) = h' x" by (simp only: h'_def) - finally show "f x = h' x" . - next - from FH' show "F \ H'" .. - qed - show "\x \ H'. h' x \ p x" - using h'_def H'_def `x' \ H` `x' \ E` `x' \ 0` E HE - `seminorm E p` linearform and hp xi - by (rule h'_norm_pres) - qed - qed - ultimately show ?thesis .. - qed - then have "\ (\x \ M. g \ x \ g = x)" by simp - -- {* So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp *} - with gx show "H = E" by contradiction - qed - - from HE_eq and linearform have "linearform E h" - by (simp only:) - moreover have "\x \ F. h x = f x" - proof - fix x assume "x \ F" - with graphs have "f x = h x" .. - then show "h x = f x" .. - qed - moreover from HE_eq and hp have "\x \ E. h x \ p x" - by (simp only:) - ultimately show ?thesis by blast -qed - - -subsection {* Alternative formulation *} - -text {* - The following alternative formulation of the Hahn-Banach - Theorem\label{abs-HahnBanach} uses the fact that for a real linear - form @{text f} and a seminorm @{text p} the following inequations - are equivalent:\footnote{This was shown in lemma @{thm [source] - abs_ineq_iff} (see page \pageref{abs-ineq-iff}).} - \begin{center} - \begin{tabular}{lll} - @{text "\x \ H. \h x\ \ p x"} & and & - @{text "\x \ H. h x \ p x"} \\ - \end{tabular} - \end{center} -*} - -theorem abs_HahnBanach: - assumes E: "vectorspace E" and FE: "subspace F E" - and lf: "linearform F f" and sn: "seminorm E p" - assumes fp: "\x \ F. \f x\ \ p x" - shows "\g. linearform E g - \ (\x \ F. g x = f x) - \ (\x \ E. \g x\ \ p x)" -proof - - interpret vectorspace E by fact - interpret subspace F E by fact - interpret linearform F f by fact - interpret seminorm E p by fact - have "\g. linearform E g \ (\x \ F. g x = f x) \ (\x \ E. g x \ p x)" - using E FE sn lf - proof (rule HahnBanach) - show "\x \ F. f x \ p x" - using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1]) - qed - then obtain g where lg: "linearform E g" and *: "\x \ F. g x = f x" - and **: "\x \ E. g x \ p x" by blast - have "\x \ E. \g x\ \ p x" - using _ E sn lg ** - proof (rule abs_ineq_iff [THEN iffD2]) - show "E \ E" .. - qed - with lg * show ?thesis by blast -qed - - -subsection {* The Hahn-Banach Theorem for normed spaces *} - -text {* - Every continuous linear form @{text f} on a subspace @{text F} of a - norm space @{text E}, can be extended to a continuous linear form - @{text g} on @{text E} such that @{text "\f\ = \g\"}. -*} - -theorem norm_HahnBanach: - fixes V and norm ("\_\") - fixes B defines "\V f. B V f \ {0} \ {\f x\ / \x\ | x. x \ 0 \ x \ V}" - fixes fn_norm ("\_\\_" [0, 1000] 999) - defines "\V f. \f\\V \ \(B V f)" - assumes E_norm: "normed_vectorspace E norm" and FE: "subspace F E" - and linearform: "linearform F f" and "continuous F norm f" - shows "\g. linearform E g - \ continuous E norm g - \ (\x \ F. g x = f x) - \ \g\\E = \f\\F" -proof - - interpret normed_vectorspace E norm by fact - interpret normed_vectorspace_with_fn_norm E norm B fn_norm - by (auto simp: B_def fn_norm_def) intro_locales - interpret subspace F E by fact - interpret linearform F f by fact - interpret continuous F norm f by fact - have E: "vectorspace E" by intro_locales - have F: "vectorspace F" by rule intro_locales - have F_norm: "normed_vectorspace F norm" - using FE E_norm by (rule subspace_normed_vs) - have ge_zero: "0 \ \f\\F" - by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero - [OF normed_vectorspace_with_fn_norm.intro, - OF F_norm `continuous F norm f` , folded B_def fn_norm_def]) - txt {* We define a function @{text p} on @{text E} as follows: - @{text "p x = \f\ \ \x\"} *} - def p \ "\x. \f\\F * \x\" - - txt {* @{text p} is a seminorm on @{text E}: *} - have q: "seminorm E p" - proof - fix x y a assume x: "x \ E" and y: "y \ E" - - txt {* @{text p} is positive definite: *} - have "0 \ \f\\F" by (rule ge_zero) - moreover from x have "0 \ \x\" .. - ultimately show "0 \ p x" - by (simp add: p_def zero_le_mult_iff) - - txt {* @{text p} is absolutely homogenous: *} - - show "p (a \ x) = \a\ * p x" - proof - - have "p (a \ x) = \f\\F * \a \ x\" by (simp only: p_def) - also from x have "\a \ x\ = \a\ * \x\" by (rule abs_homogenous) - also have "\f\\F * (\a\ * \x\) = \a\ * (\f\\F * \x\)" by simp - also have "\ = \a\ * p x" by (simp only: p_def) - finally show ?thesis . - qed - - txt {* Furthermore, @{text p} is subadditive: *} - - show "p (x + y) \ p x + p y" - proof - - have "p (x + y) = \f\\F * \x + y\" by (simp only: p_def) - also have a: "0 \ \f\\F" by (rule ge_zero) - from x y have "\x + y\ \ \x\ + \y\" .. - with a have " \f\\F * \x + y\ \ \f\\F * (\x\ + \y\)" - by (simp add: mult_left_mono) - also have "\ = \f\\F * \x\ + \f\\F * \y\" by (simp only: right_distrib) - also have "\ = p x + p y" by (simp only: p_def) - finally show ?thesis . - qed - qed - - txt {* @{text f} is bounded by @{text p}. *} - - have "\x \ F. \f x\ \ p x" - proof - fix x assume "x \ F" - with `continuous F norm f` and linearform - show "\f x\ \ p x" - unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong - [OF normed_vectorspace_with_fn_norm.intro, - OF F_norm, folded B_def fn_norm_def]) - qed - - txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded - by @{text p} we can apply the Hahn-Banach Theorem for real vector - spaces. So @{text f} can be extended in a norm-preserving way to - some function @{text g} on the whole vector space @{text E}. *} - - with E FE linearform q obtain g where - linearformE: "linearform E g" - and a: "\x \ F. g x = f x" - and b: "\x \ E. \g x\ \ p x" - by (rule abs_HahnBanach [elim_format]) iprover - - txt {* We furthermore have to show that @{text g} is also continuous: *} - - have g_cont: "continuous E norm g" using linearformE - proof - fix x assume "x \ E" - with b show "\g x\ \ \f\\F * \x\" - by (simp only: p_def) - qed - - txt {* To complete the proof, we show that @{text "\g\ = \f\"}. *} - - have "\g\\E = \f\\F" - proof (rule order_antisym) - txt {* - First we show @{text "\g\ \ \f\"}. The function norm @{text - "\g\"} is defined as the smallest @{text "c \ \"} such that - \begin{center} - \begin{tabular}{l} - @{text "\x \ E. \g x\ \ c \ \x\"} - \end{tabular} - \end{center} - \noindent Furthermore holds - \begin{center} - \begin{tabular}{l} - @{text "\x \ E. \g x\ \ \f\ \ \x\"} - \end{tabular} - \end{center} - *} - - have "\x \ E. \g x\ \ \f\\F * \x\" - proof - fix x assume "x \ E" - with b show "\g x\ \ \f\\F * \x\" - by (simp only: p_def) - qed - from g_cont this ge_zero - show "\g\\E \ \f\\F" - by (rule fn_norm_least [of g, folded B_def fn_norm_def]) - - txt {* The other direction is achieved by a similar argument. *} - - show "\f\\F \ \g\\E" - proof (rule normed_vectorspace_with_fn_norm.fn_norm_least - [OF normed_vectorspace_with_fn_norm.intro, - OF F_norm, folded B_def fn_norm_def]) - show "\x \ F. \f x\ \ \g\\E * \x\" - proof - fix x assume x: "x \ F" - from a x have "g x = f x" .. - then have "\f x\ = \g x\" by (simp only:) - also from g_cont - have "\ \ \g\\E * \x\" - proof (rule fn_norm_le_cong [OF _ linearformE, folded B_def fn_norm_def]) - from FE x show "x \ E" .. - qed - finally show "\f x\ \ \g\\E * \x\" . - qed - show "0 \ \g\\E" - using g_cont - by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def]) - show "continuous F norm f" by fact - qed - qed - with linearformE a g_cont show ?thesis by blast -qed - -end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/HahnBanachExtLemmas.thy --- a/src/HOL/HahnBanach/HahnBanachExtLemmas.thy Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,280 +0,0 @@ -(* Title: HOL/Real/HahnBanach/HahnBanachExtLemmas.thy - Author: Gertrud Bauer, TU Munich -*) - -header {* Extending non-maximal functions *} - -theory HahnBanachExtLemmas -imports FunctionNorm -begin - -text {* - In this section the following context is presumed. Let @{text E} be - a real vector space with a seminorm @{text q} on @{text E}. @{text - F} is a subspace of @{text E} and @{text f} a linear function on - @{text F}. We consider a subspace @{text H} of @{text E} that is a - superspace of @{text F} and a linear form @{text h} on @{text - H}. @{text H} is a not equal to @{text E} and @{text "x\<^sub>0"} is - an element in @{text "E - H"}. @{text H} is extended to the direct - sum @{text "H' = H + lin x\<^sub>0"}, so for any @{text "x \ H'"} - the decomposition of @{text "x = y + a \ x"} with @{text "y \ H"} is - unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y + - a \ \"} for a certain @{text \}. - - Subsequently we show some properties of this extension @{text h'} of - @{text h}. - - \medskip This lemma will be used to show the existence of a linear - extension of @{text f} (see page \pageref{ex-xi-use}). It is a - consequence of the completeness of @{text \}. To show - \begin{center} - \begin{tabular}{l} - @{text "\\. \y \ F. a y \ \ \ \ \ b y"} - \end{tabular} - \end{center} - \noindent it suffices to show that - \begin{center} - \begin{tabular}{l} - @{text "\u \ F. \v \ F. a u \ b v"} - \end{tabular} - \end{center} -*} - -lemma ex_xi: - assumes "vectorspace F" - assumes r: "\u v. u \ F \ v \ F \ a u \ b v" - shows "\xi::real. \y \ F. a y \ xi \ xi \ b y" -proof - - interpret vectorspace F by fact - txt {* From the completeness of the reals follows: - The set @{text "S = {a u. u \ F}"} has a supremum, if it is - non-empty and has an upper bound. *} - - let ?S = "{a u | u. u \ F}" - have "\xi. lub ?S xi" - proof (rule real_complete) - have "a 0 \ ?S" by blast - then show "\X. X \ ?S" .. - have "\y \ ?S. y \ b 0" - proof - fix y assume y: "y \ ?S" - then obtain u where u: "u \ F" and y: "y = a u" by blast - from u and zero have "a u \ b 0" by (rule r) - with y show "y \ b 0" by (simp only:) - qed - then show "\u. \y \ ?S. y \ u" .. - qed - then obtain xi where xi: "lub ?S xi" .. - { - fix y assume "y \ F" - then have "a y \ ?S" by blast - with xi have "a y \ xi" by (rule lub.upper) - } moreover { - fix y assume y: "y \ F" - from xi have "xi \ b y" - proof (rule lub.least) - fix au assume "au \ ?S" - then obtain u where u: "u \ F" and au: "au = a u" by blast - from u y have "a u \ b y" by (rule r) - with au show "au \ b y" by (simp only:) - qed - } ultimately show "\xi. \y \ F. a y \ xi \ xi \ b y" by blast -qed - -text {* - \medskip The function @{text h'} is defined as a @{text "h' x = h y - + a \ \"} where @{text "x = y + a \ \"} is a linear extension of - @{text h} to @{text H'}. -*} - -lemma h'_lf: - assumes h'_def: "h' \ \x. let (y, a) = - SOME (y, a). x = y + a \ x0 \ y \ H in h y + a * xi" - and H'_def: "H' \ H + lin x0" - and HE: "H \ E" - assumes "linearform H h" - assumes x0: "x0 \ H" "x0 \ E" "x0 \ 0" - assumes E: "vectorspace E" - shows "linearform H' h'" -proof - - interpret linearform H h by fact - interpret vectorspace E by fact - show ?thesis - proof - note E = `vectorspace E` - have H': "vectorspace H'" - proof (unfold H'_def) - from `x0 \ E` - have "lin x0 \ E" .. - with HE show "vectorspace (H + lin x0)" using E .. - qed - { - fix x1 x2 assume x1: "x1 \ H'" and x2: "x2 \ H'" - show "h' (x1 + x2) = h' x1 + h' x2" - proof - - from H' x1 x2 have "x1 + x2 \ H'" - by (rule vectorspace.add_closed) - with x1 x2 obtain y y1 y2 a a1 a2 where - x1x2: "x1 + x2 = y + a \ x0" and y: "y \ H" - and x1_rep: "x1 = y1 + a1 \ x0" and y1: "y1 \ H" - and x2_rep: "x2 = y2 + a2 \ x0" and y2: "y2 \ H" - unfolding H'_def sum_def lin_def by blast - - have ya: "y1 + y2 = y \ a1 + a2 = a" using E HE _ y x0 - proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *} - from HE y1 y2 show "y1 + y2 \ H" - by (rule subspace.add_closed) - from x0 and HE y y1 y2 - have "x0 \ E" "y \ E" "y1 \ E" "y2 \ E" by auto - with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \ x0 = x1 + x2" - by (simp add: add_ac add_mult_distrib2) - also note x1x2 - finally show "(y1 + y2) + (a1 + a2) \ x0 = y + a \ x0" . - qed - - from h'_def x1x2 E HE y x0 - have "h' (x1 + x2) = h y + a * xi" - by (rule h'_definite) - also have "\ = h (y1 + y2) + (a1 + a2) * xi" - by (simp only: ya) - also from y1 y2 have "h (y1 + y2) = h y1 + h y2" - by simp - also have "\ + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)" - by (simp add: left_distrib) - also from h'_def x1_rep E HE y1 x0 - have "h y1 + a1 * xi = h' x1" - by (rule h'_definite [symmetric]) - also from h'_def x2_rep E HE y2 x0 - have "h y2 + a2 * xi = h' x2" - by (rule h'_definite [symmetric]) - finally show ?thesis . - qed - next - fix x1 c assume x1: "x1 \ H'" - show "h' (c \ x1) = c * (h' x1)" - proof - - from H' x1 have ax1: "c \ x1 \ H'" - by (rule vectorspace.mult_closed) - with x1 obtain y a y1 a1 where - cx1_rep: "c \ x1 = y + a \ x0" and y: "y \ H" - and x1_rep: "x1 = y1 + a1 \ x0" and y1: "y1 \ H" - unfolding H'_def sum_def lin_def by blast - - have ya: "c \ y1 = y \ c * a1 = a" using E HE _ y x0 - proof (rule decomp_H') - from HE y1 show "c \ y1 \ H" - by (rule subspace.mult_closed) - from x0 and HE y y1 - have "x0 \ E" "y \ E" "y1 \ E" by auto - with x1_rep have "c \ y1 + (c * a1) \ x0 = c \ x1" - by (simp add: mult_assoc add_mult_distrib1) - also note cx1_rep - finally show "c \ y1 + (c * a1) \ x0 = y + a \ x0" . - qed - - from h'_def cx1_rep E HE y x0 have "h' (c \ x1) = h y + a * xi" - by (rule h'_definite) - also have "\ = h (c \ y1) + (c * a1) * xi" - by (simp only: ya) - also from y1 have "h (c \ y1) = c * h y1" - by simp - also have "\ + (c * a1) * xi = c * (h y1 + a1 * xi)" - by (simp only: right_distrib) - also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1" - by (rule h'_definite [symmetric]) - finally show ?thesis . - qed - } - qed -qed - -text {* \medskip The linear extension @{text h'} of @{text h} - is bounded by the seminorm @{text p}. *} - -lemma h'_norm_pres: - assumes h'_def: "h' \ \x. let (y, a) = - SOME (y, a). x = y + a \ x0 \ y \ H in h y + a * xi" - and H'_def: "H' \ H + lin x0" - and x0: "x0 \ H" "x0 \ E" "x0 \ 0" - assumes E: "vectorspace E" and HE: "subspace H E" - and "seminorm E p" and "linearform H h" - assumes a: "\y \ H. h y \ p y" - and a': "\y \ H. - p (y + x0) - h y \ xi \ xi \ p (y + x0) - h y" - shows "\x \ H'. h' x \ p x" -proof - - interpret vectorspace E by fact - interpret subspace H E by fact - interpret seminorm E p by fact - interpret linearform H h by fact - show ?thesis - proof - fix x assume x': "x \ H'" - show "h' x \ p x" - proof - - from a' have a1: "\ya \ H. - p (ya + x0) - h ya \ xi" - and a2: "\ya \ H. xi \ p (ya + x0) - h ya" by auto - from x' obtain y a where - x_rep: "x = y + a \ x0" and y: "y \ H" - unfolding H'_def sum_def lin_def by blast - from y have y': "y \ E" .. - from y have ay: "inverse a \ y \ H" by simp - - from h'_def x_rep E HE y x0 have "h' x = h y + a * xi" - by (rule h'_definite) - also have "\ \ p (y + a \ x0)" - proof (rule linorder_cases) - assume z: "a = 0" - then have "h y + a * xi = h y" by simp - also from a y have "\ \ p y" .. - also from x0 y' z have "p y = p (y + a \ x0)" by simp - finally show ?thesis . - next - txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"} - with @{text ya} taken as @{text "y / a"}: *} - assume lz: "a < 0" then have nz: "a \ 0" by simp - from a1 ay - have "- p (inverse a \ y + x0) - h (inverse a \ y) \ xi" .. - with lz have "a * xi \ - a * (- p (inverse a \ y + x0) - h (inverse a \ y))" - by (simp add: mult_left_mono_neg order_less_imp_le) - - also have "\ = - - a * (p (inverse a \ y + x0)) - a * (h (inverse a \ y))" - by (simp add: right_diff_distrib) - also from lz x0 y' have "- a * (p (inverse a \ y + x0)) = - p (a \ (inverse a \ y + x0))" - by (simp add: abs_homogenous) - also from nz x0 y' have "\ = p (y + a \ x0)" - by (simp add: add_mult_distrib1 mult_assoc [symmetric]) - also from nz y have "a * (h (inverse a \ y)) = h y" - by simp - finally have "a * xi \ p (y + a \ x0) - h y" . - then show ?thesis by simp - next - txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"} - with @{text ya} taken as @{text "y / a"}: *} - assume gz: "0 < a" then have nz: "a \ 0" by simp - from a2 ay - have "xi \ p (inverse a \ y + x0) - h (inverse a \ y)" .. - with gz have "a * xi \ - a * (p (inverse a \ y + x0) - h (inverse a \ y))" - by simp - also have "\ = a * p (inverse a \ y + x0) - a * h (inverse a \ y)" - by (simp add: right_diff_distrib) - also from gz x0 y' - have "a * p (inverse a \ y + x0) = p (a \ (inverse a \ y + x0))" - by (simp add: abs_homogenous) - also from nz x0 y' have "\ = p (y + a \ x0)" - by (simp add: add_mult_distrib1 mult_assoc [symmetric]) - also from nz y have "a * h (inverse a \ y) = h y" - by simp - finally have "a * xi \ p (y + a \ x0) - h y" . - then show ?thesis by simp - qed - also from x_rep have "\ = p x" by (simp only:) - finally show ?thesis . - qed - qed -qed - -end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/HahnBanachLemmas.thy --- a/src/HOL/HahnBanach/HahnBanachLemmas.thy Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -(*<*) -theory HahnBanachLemmas imports HahnBanachSupLemmas HahnBanachExtLemmas begin -end -(*>*) \ No newline at end of file diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/HahnBanachSupLemmas.thy --- a/src/HOL/HahnBanach/HahnBanachSupLemmas.thy Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,446 +0,0 @@ -(* Title: HOL/Real/HahnBanach/HahnBanachSupLemmas.thy - ID: $Id$ - Author: Gertrud Bauer, TU Munich -*) - -header {* The supremum w.r.t.~the function order *} - -theory HahnBanachSupLemmas -imports FunctionNorm ZornLemma -begin - -text {* - 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 @{text E} be a real vector space with a seminorm - @{text p} on @{text E}. @{text F} is a subspace of @{text E} and - @{text f} a linear form on @{text F}. We consider a chain @{text c} - of norm-preserving extensions of @{text f}, such that @{text "\c = - graph H h"}. We will show some properties about the limit function - @{text h}, i.e.\ the supremum of the chain @{text c}. - - \medskip Let @{text c} be a chain of norm-preserving extensions of - the function @{text f} and let @{text "graph H h"} be the supremum - of @{text c}. Every element in @{text H} is member of one of the - elements of the chain. -*} -lemmas [dest?] = chainD -lemmas chainE2 [elim?] = chainD2 [elim_format, standard] - -lemma some_H'h't: - assumes M: "M = norm_pres_extensions E p F f" - and cM: "c \ chain M" - and u: "graph H h = \c" - and x: "x \ H" - shows "\H' h'. graph H' h' \ c - \ (x, h x) \ graph H' h' - \ linearform H' h' \ H' \ E - \ F \ H' \ graph F f \ graph H' h' - \ (\x \ H'. h' x \ p x)" -proof - - from x have "(x, h x) \ graph H h" .. - also from u have "\ = \c" . - finally obtain g where gc: "g \ c" and gh: "(x, h x) \ g" by blast - - from cM have "c \ M" .. - with gc have "g \ M" .. - also from M have "\ = norm_pres_extensions E p F f" . - finally obtain H' and h' where g: "g = graph H' h'" - and * : "linearform H' h'" "H' \ E" "F \ H'" - "graph F f \ graph H' h'" "\x \ H'. h' x \ p x" .. - - from gc and g have "graph H' h' \ c" by (simp only:) - moreover from gh and g have "(x, h x) \ graph H' h'" by (simp only:) - ultimately show ?thesis using * by blast -qed - -text {* - \medskip Let @{text c} be a chain of norm-preserving extensions of - the function @{text f} and let @{text "graph H h"} be the supremum - of @{text c}. Every element in the domain @{text H} of the supremum - function is member of the domain @{text H'} of some function @{text - h'}, such that @{text h} extends @{text h'}. -*} - -lemma some_H'h': - assumes M: "M = norm_pres_extensions E p F f" - and cM: "c \ chain M" - and u: "graph H h = \c" - and x: "x \ H" - shows "\H' h'. x \ H' \ graph H' h' \ graph H h - \ linearform H' h' \ H' \ E \ F \ H' - \ graph F f \ graph H' h' \ (\x \ H'. h' x \ p x)" -proof - - from M cM u x obtain H' h' where - x_hx: "(x, h x) \ graph H' h'" - and c: "graph H' h' \ c" - and * : "linearform H' h'" "H' \ E" "F \ H'" - "graph F f \ graph H' h'" "\x \ H'. h' x \ p x" - by (rule some_H'h't [elim_format]) blast - from x_hx have "x \ H'" .. - moreover from cM u c have "graph H' h' \ graph H h" - by (simp only: chain_ball_Union_upper) - ultimately show ?thesis using * by blast -qed - -text {* - \medskip Any two elements @{text x} and @{text y} in the domain - @{text H} of the supremum function @{text h} are both in the domain - @{text H'} of some function @{text h'}, such that @{text h} extends - @{text h'}. -*} - -lemma some_H'h'2: - assumes M: "M = norm_pres_extensions E p F f" - and cM: "c \ chain M" - and u: "graph H h = \c" - and x: "x \ H" - and y: "y \ H" - shows "\H' h'. x \ H' \ y \ H' - \ graph H' h' \ graph H h - \ linearform H' h' \ H' \ E \ F \ H' - \ graph F f \ graph H' h' \ (\x \ H'. h' x \ p x)" -proof - - txt {* @{text y} is in the domain @{text H''} of some function @{text h''}, - such that @{text h} extends @{text h''}. *} - - from M cM u and y obtain H' h' where - y_hy: "(y, h y) \ graph H' h'" - and c': "graph H' h' \ c" - and * : - "linearform H' h'" "H' \ E" "F \ H'" - "graph F f \ graph H' h'" "\x \ H'. h' x \ p x" - by (rule some_H'h't [elim_format]) blast - - txt {* @{text x} is in the domain @{text H'} of some function @{text h'}, - such that @{text h} extends @{text h'}. *} - - from M cM u and x obtain H'' h'' where - x_hx: "(x, h x) \ graph H'' h''" - and c'': "graph H'' h'' \ c" - and ** : - "linearform H'' h''" "H'' \ E" "F \ H''" - "graph F f \ graph H'' h''" "\x \ H''. h'' x \ p x" - by (rule some_H'h't [elim_format]) blast - - txt {* Since both @{text h'} and @{text h''} are elements of the chain, - @{text h''} is an extension of @{text h'} or vice versa. Thus both - @{text x} and @{text y} are contained in the greater - one. \label{cases1}*} - - from cM c'' c' have "graph H'' h'' \ graph H' h' \ graph H' h' \ graph H'' h''" - (is "?case1 \ ?case2") .. - then show ?thesis - proof - assume ?case1 - have "(x, h x) \ graph H'' h''" by fact - also have "\ \ graph H' h'" by fact - finally have xh:"(x, h x) \ graph H' h'" . - then have "x \ H'" .. - moreover from y_hy have "y \ H'" .. - moreover from cM u and c' have "graph H' h' \ graph H h" - by (simp only: chain_ball_Union_upper) - ultimately show ?thesis using * by blast - next - assume ?case2 - from x_hx have "x \ H''" .. - moreover { - have "(y, h y) \ graph H' h'" by (rule y_hy) - also have "\ \ graph H'' h''" by fact - finally have "(y, h y) \ graph H'' h''" . - } then have "y \ H''" .. - moreover from cM u and c'' have "graph H'' h'' \ graph H h" - by (simp only: chain_ball_Union_upper) - ultimately show ?thesis using ** by blast - qed -qed - -text {* - \medskip The relation induced by the graph of the supremum of a - chain @{text c} is definite, i.~e.~t is the graph of a function. -*} - -lemma sup_definite: - assumes M_def: "M \ norm_pres_extensions E p F f" - and cM: "c \ chain M" - and xy: "(x, y) \ \c" - and xz: "(x, z) \ \c" - shows "z = y" -proof - - from cM have c: "c \ M" .. - from xy obtain G1 where xy': "(x, y) \ G1" and G1: "G1 \ c" .. - from xz obtain G2 where xz': "(x, z) \ G2" and G2: "G2 \ c" .. - - from G1 c have "G1 \ M" .. - then obtain H1 h1 where G1_rep: "G1 = graph H1 h1" - unfolding M_def by blast - - from G2 c have "G2 \ M" .. - then obtain H2 h2 where G2_rep: "G2 = graph H2 h2" - unfolding M_def by blast - - txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"} - or vice versa, since both @{text "G\<^sub>1"} and @{text - "G\<^sub>2"} are members of @{text c}. \label{cases2}*} - - from cM G1 G2 have "G1 \ G2 \ G2 \ G1" (is "?case1 \ ?case2") .. - then show ?thesis - proof - assume ?case1 - with xy' G2_rep have "(x, y) \ graph H2 h2" by blast - then have "y = h2 x" .. - also - from xz' G2_rep have "(x, z) \ graph H2 h2" by (simp only:) - then have "z = h2 x" .. - finally show ?thesis . - next - assume ?case2 - with xz' G1_rep have "(x, z) \ graph H1 h1" by blast - then have "z = h1 x" .. - also - from xy' G1_rep have "(x, y) \ graph H1 h1" by (simp only:) - then have "y = h1 x" .. - finally show ?thesis .. - qed -qed - -text {* - \medskip The limit function @{text h} is linear. Every element - @{text x} in the domain of @{text h} is in the domain of a function - @{text h'} in the chain of norm preserving extensions. Furthermore, - @{text h} is an extension of @{text h'} so the function values of - @{text x} are identical for @{text h'} and @{text h}. Finally, the - function @{text h'} is linear by construction of @{text M}. -*} - -lemma sup_lf: - assumes M: "M = norm_pres_extensions E p F f" - and cM: "c \ chain M" - and u: "graph H h = \c" - shows "linearform H h" -proof - fix x y assume x: "x \ H" and y: "y \ H" - with M cM u obtain H' h' where - x': "x \ H'" and y': "y \ H'" - and b: "graph H' h' \ graph H h" - and linearform: "linearform H' h'" - and subspace: "H' \ E" - by (rule some_H'h'2 [elim_format]) blast - - show "h (x + y) = h x + h y" - proof - - from linearform x' y' have "h' (x + y) = h' x + h' y" - by (rule linearform.add) - also from b x' have "h' x = h x" .. - also from b y' have "h' y = h y" .. - also from subspace x' y' have "x + y \ H'" - by (rule subspace.add_closed) - with b have "h' (x + y) = h (x + y)" .. - finally show ?thesis . - qed -next - fix x a assume x: "x \ H" - with M cM u obtain H' h' where - x': "x \ H'" - and b: "graph H' h' \ graph H h" - and linearform: "linearform H' h'" - and subspace: "H' \ E" - by (rule some_H'h' [elim_format]) blast - - show "h (a \ x) = a * h x" - proof - - from linearform x' have "h' (a \ x) = a * h' x" - by (rule linearform.mult) - also from b x' have "h' x = h x" .. - also from subspace x' have "a \ x \ H'" - by (rule subspace.mult_closed) - with b have "h' (a \ x) = h (a \ x)" .. - finally show ?thesis . - qed -qed - -text {* - \medskip The limit of a non-empty chain of norm preserving - extensions of @{text f} is an extension of @{text f}, since every - element of the chain is an extension of @{text f} and the supremum - is an extension for every element of the chain. -*} - -lemma sup_ext: - assumes graph: "graph H h = \c" - and M: "M = norm_pres_extensions E p F f" - and cM: "c \ chain M" - and ex: "\x. x \ c" - shows "graph F f \ graph H h" -proof - - from ex obtain x where xc: "x \ c" .. - from cM have "c \ M" .. - with xc have "x \ M" .. - with M have "x \ norm_pres_extensions E p F f" - by (simp only:) - then obtain G g where "x = graph G g" and "graph F f \ graph G g" .. - then have "graph F f \ x" by (simp only:) - also from xc have "\ \ \c" by blast - also from graph have "\ = graph H h" .. - finally show ?thesis . -qed - -text {* - \medskip The domain @{text H} of the limit function is a superspace - of @{text F}, since @{text F} is a subset of @{text H}. The - existence of the @{text 0} element in @{text F} and the closure - properties follow from the fact that @{text F} is a vector space. -*} - -lemma sup_supF: - assumes graph: "graph H h = \c" - and M: "M = norm_pres_extensions E p F f" - and cM: "c \ chain M" - and ex: "\x. x \ c" - and FE: "F \ E" - shows "F \ H" -proof - from FE show "F \ {}" by (rule subspace.non_empty) - from graph M cM ex have "graph F f \ graph H h" by (rule sup_ext) - then show "F \ H" .. - fix x y assume "x \ F" and "y \ F" - with FE show "x + y \ F" by (rule subspace.add_closed) -next - fix x a assume "x \ F" - with FE show "a \ x \ F" by (rule subspace.mult_closed) -qed - -text {* - \medskip The domain @{text H} of the limit function is a subspace of - @{text E}. -*} - -lemma sup_subE: - assumes graph: "graph H h = \c" - and M: "M = norm_pres_extensions E p F f" - and cM: "c \ chain M" - and ex: "\x. x \ c" - and FE: "F \ E" - and E: "vectorspace E" - shows "H \ E" -proof - show "H \ {}" - proof - - from FE E have "0 \ F" by (rule subspace.zero) - also from graph M cM ex FE have "F \ H" by (rule sup_supF) - then have "F \ H" .. - finally show ?thesis by blast - qed - show "H \ E" - proof - fix x assume "x \ H" - with M cM graph - obtain H' h' where x: "x \ H'" and H'E: "H' \ E" - by (rule some_H'h' [elim_format]) blast - from H'E have "H' \ E" .. - with x show "x \ E" .. - qed - fix x y assume x: "x \ H" and y: "y \ H" - show "x + y \ H" - proof - - from M cM graph x y obtain H' h' where - x': "x \ H'" and y': "y \ H'" and H'E: "H' \ E" - and graphs: "graph H' h' \ graph H h" - by (rule some_H'h'2 [elim_format]) blast - from H'E x' y' have "x + y \ H'" - by (rule subspace.add_closed) - also from graphs have "H' \ H" .. - finally show ?thesis . - qed -next - fix x a assume x: "x \ H" - show "a \ x \ H" - proof - - from M cM graph x - obtain H' h' where x': "x \ H'" and H'E: "H' \ E" - and graphs: "graph H' h' \ graph H h" - by (rule some_H'h' [elim_format]) blast - from H'E x' have "a \ x \ H'" by (rule subspace.mult_closed) - also from graphs have "H' \ H" .. - finally show ?thesis . - qed -qed - -text {* - \medskip The limit function is bounded by the norm @{text p} as - well, since all elements in the chain are bounded by @{text p}. -*} - -lemma sup_norm_pres: - assumes graph: "graph H h = \c" - and M: "M = norm_pres_extensions E p F f" - and cM: "c \ chain M" - shows "\x \ H. h x \ p x" -proof - fix x assume "x \ H" - with M cM graph obtain H' h' where x': "x \ H'" - and graphs: "graph H' h' \ graph H h" - and a: "\x \ H'. h' x \ p x" - by (rule some_H'h' [elim_format]) blast - from graphs x' have [symmetric]: "h' x = h x" .. - also from a x' have "h' x \ p x " .. - finally show "h x \ p x" . -qed - -text {* - \medskip The following lemma is a property of linear forms on real - vector spaces. It will be used for the lemma @{text abs_HahnBanach} - (see page \pageref{abs-HahnBanach}). \label{abs-ineq-iff} For real - vector spaces the following inequations are equivalent: - \begin{center} - \begin{tabular}{lll} - @{text "\x \ H. \h x\ \ p x"} & and & - @{text "\x \ H. h x \ p x"} \\ - \end{tabular} - \end{center} -*} - -lemma abs_ineq_iff: - assumes "subspace H E" and "vectorspace E" and "seminorm E p" - and "linearform H h" - shows "(\x \ H. \h x\ \ p x) = (\x \ H. h x \ p x)" (is "?L = ?R") -proof - interpret subspace H E by fact - interpret vectorspace E by fact - interpret seminorm E p by fact - interpret linearform H h by fact - have H: "vectorspace H" using `vectorspace E` .. - { - assume l: ?L - show ?R - proof - fix x assume x: "x \ H" - have "h x \ \h x\" by arith - also from l x have "\ \ p x" .. - finally show "h x \ p x" . - qed - next - assume r: ?R - show ?L - proof - fix x assume x: "x \ H" - show "\a b :: real. - a \ b \ b \ a \ \b\ \ a" - by arith - from `linearform H h` and H x - have "- h x = h (- x)" by (rule linearform.neg [symmetric]) - also - from H x have "- x \ H" by (rule vectorspace.neg_closed) - with r have "h (- x) \ p (- x)" .. - also have "\ = p x" - using `seminorm E p` `vectorspace E` - proof (rule seminorm.minus) - from x show "x \ E" .. - qed - finally have "- h x \ p x" . - then show "- p x \ h x" by simp - from r x show "h x \ p x" .. - qed - } -qed - -end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/Linearform.thy --- a/src/HOL/HahnBanach/Linearform.thy Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,60 +0,0 @@ -(* Title: HOL/Real/HahnBanach/Linearform.thy - Author: Gertrud Bauer, TU Munich -*) - -header {* Linearforms *} - -theory Linearform -imports VectorSpace -begin - -text {* - A \emph{linear form} is a function on a vector space into the reals - that is additive and multiplicative. -*} - -locale linearform = - fixes V :: "'a\{minus, plus, zero, uminus} set" and f - assumes add [iff]: "x \ V \ y \ V \ f (x + y) = f x + f y" - and mult [iff]: "x \ V \ f (a \ x) = a * f x" - -declare linearform.intro [intro?] - -lemma (in linearform) neg [iff]: - assumes "vectorspace V" - shows "x \ V \ f (- x) = - f x" -proof - - interpret vectorspace V by fact - assume x: "x \ V" - then have "f (- x) = f ((- 1) \ x)" by (simp add: negate_eq1) - also from x have "\ = (- 1) * (f x)" by (rule mult) - also from x have "\ = - (f x)" by simp - finally show ?thesis . -qed - -lemma (in linearform) diff [iff]: - assumes "vectorspace V" - shows "x \ V \ y \ V \ f (x - y) = f x - f y" -proof - - interpret vectorspace V by fact - assume x: "x \ V" and y: "y \ V" - then have "x - y = x + - y" by (rule diff_eq1) - also have "f \ = f x + f (- y)" by (rule add) (simp_all add: x y) - also have "f (- y) = - f y" using `vectorspace V` y by (rule neg) - finally show ?thesis by simp -qed - -text {* Every linear form yields @{text 0} for the @{text 0} vector. *} - -lemma (in linearform) zero [iff]: - assumes "vectorspace V" - shows "f 0 = 0" -proof - - interpret vectorspace V by fact - have "f 0 = f (0 - 0)" by simp - also have "\ = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all - also have "\ = 0" by simp - finally show ?thesis . -qed - -end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/NormedSpace.thy --- a/src/HOL/HahnBanach/NormedSpace.thy Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,117 +0,0 @@ -(* Title: HOL/Real/HahnBanach/NormedSpace.thy - Author: Gertrud Bauer, TU Munich -*) - -header {* Normed vector spaces *} - -theory NormedSpace -imports Subspace -begin - -subsection {* Quasinorms *} - -text {* - A \emph{seminorm} @{text "\\\"} is a function on a real vector space - into the reals that has the following properties: it is positive - definite, absolute homogenous and subadditive. -*} - -locale norm_syntax = - fixes norm :: "'a \ real" ("\_\") - -locale seminorm = var_V + norm_syntax + - constrains V :: "'a\{minus, plus, zero, uminus} set" - assumes ge_zero [iff?]: "x \ V \ 0 \ \x\" - and abs_homogenous [iff?]: "x \ V \ \a \ x\ = \a\ * \x\" - and subadditive [iff?]: "x \ V \ y \ V \ \x + y\ \ \x\ + \y\" - -declare seminorm.intro [intro?] - -lemma (in seminorm) diff_subadditive: - assumes "vectorspace V" - shows "x \ V \ y \ V \ \x - y\ \ \x\ + \y\" -proof - - interpret vectorspace V by fact - assume x: "x \ V" and y: "y \ V" - then have "x - y = x + - 1 \ y" - by (simp add: diff_eq2 negate_eq2a) - also from x y have "\\\ \ \x\ + \- 1 \ y\" - by (simp add: subadditive) - also from y have "\- 1 \ y\ = \- 1\ * \y\" - by (rule abs_homogenous) - also have "\ = \y\" by simp - finally show ?thesis . -qed - -lemma (in seminorm) minus: - assumes "vectorspace V" - shows "x \ V \ \- x\ = \x\" -proof - - interpret vectorspace V by fact - assume x: "x \ V" - then have "- x = - 1 \ x" by (simp only: negate_eq1) - also from x have "\\\ = \- 1\ * \x\" - by (rule abs_homogenous) - also have "\ = \x\" by simp - finally show ?thesis . -qed - - -subsection {* Norms *} - -text {* - A \emph{norm} @{text "\\\"} is a seminorm that maps only the - @{text 0} vector to @{text 0}. -*} - -locale norm = seminorm + - assumes zero_iff [iff]: "x \ V \ (\x\ = 0) = (x = 0)" - - -subsection {* Normed vector spaces *} - -text {* - A vector space together with a norm is called a \emph{normed - space}. -*} - -locale normed_vectorspace = vectorspace + norm - -declare normed_vectorspace.intro [intro?] - -lemma (in normed_vectorspace) gt_zero [intro?]: - "x \ V \ x \ 0 \ 0 < \x\" -proof - - assume x: "x \ V" and neq: "x \ 0" - from x have "0 \ \x\" .. - also have [symmetric]: "\ \ 0" - proof - assume "\x\ = 0" - with x have "x = 0" by simp - with neq show False by contradiction - qed - finally show ?thesis . -qed - -text {* - Any subspace of a normed vector space is again a normed vectorspace. -*} - -lemma subspace_normed_vs [intro?]: - fixes F E norm - assumes "subspace F E" "normed_vectorspace E norm" - shows "normed_vectorspace F norm" -proof - - interpret subspace F E by fact - interpret normed_vectorspace E norm by fact - show ?thesis - proof - show "vectorspace F" by (rule vectorspace) unfold_locales - next - have "NormedSpace.norm E norm" .. - with subset show "NormedSpace.norm F norm" - by (simp add: norm_def seminorm_def norm_axioms_def) - qed -qed - -end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/README.html --- a/src/HOL/HahnBanach/README.html Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,38 +0,0 @@ - - - - - - - - - HOL/Real/HahnBanach/README - - - - -

The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)

- -Author: Gertrud Bauer, Technische Universität München

- -This directory contains the proof of the Hahn-Banach theorem for real vectorspaces, -following H. Heuser, Funktionalanalysis, p. 228 -232. -The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis. -It is a conclusion of Zorn's lemma.

- -Two different formaulations of the theorem are presented, one for general real vectorspaces -and its application to normed vectorspaces.

- -The theorem says, that every continous linearform, defined on arbitrary subspaces -(not only one-dimensional subspaces), can be extended to a continous linearform on -the whole vectorspace. - - -


- -
-bauerg@in.tum.de -
- - - diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/ROOT.ML --- a/src/HOL/HahnBanach/ROOT.ML Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title: HOL/Real/HahnBanach/ROOT.ML - ID: $Id$ - Author: Gertrud Bauer, TU Munich - -The Hahn-Banach theorem for real vector spaces (Isabelle/Isar). -*) - -time_use_thy "HahnBanach"; diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/Subspace.thy --- a/src/HOL/HahnBanach/Subspace.thy Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,513 +0,0 @@ -(* Title: HOL/Real/HahnBanach/Subspace.thy - Author: Gertrud Bauer, TU Munich -*) - -header {* Subspaces *} - -theory Subspace -imports VectorSpace -begin - -subsection {* Definition *} - -text {* - A non-empty subset @{text U} of a vector space @{text V} is a - \emph{subspace} of @{text V}, iff @{text U} is closed under addition - and scalar multiplication. -*} - -locale subspace = - fixes U :: "'a\{minus, plus, zero, uminus} set" and V - assumes non_empty [iff, intro]: "U \ {}" - and subset [iff]: "U \ V" - and add_closed [iff]: "x \ U \ y \ U \ x + y \ U" - and mult_closed [iff]: "x \ U \ a \ x \ U" - -notation (symbols) - subspace (infix "\" 50) - -declare vectorspace.intro [intro?] subspace.intro [intro?] - -lemma subspace_subset [elim]: "U \ V \ U \ V" - by (rule subspace.subset) - -lemma (in subspace) subsetD [iff]: "x \ U \ x \ V" - using subset by blast - -lemma subspaceD [elim]: "U \ V \ x \ U \ x \ V" - by (rule subspace.subsetD) - -lemma rev_subspaceD [elim?]: "x \ U \ U \ V \ x \ V" - by (rule subspace.subsetD) - -lemma (in subspace) diff_closed [iff]: - assumes "vectorspace V" - assumes x: "x \ U" and y: "y \ U" - shows "x - y \ U" -proof - - interpret vectorspace V by fact - from x y show ?thesis by (simp add: diff_eq1 negate_eq1) -qed - -text {* - \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. -*} - -lemma (in subspace) zero [intro]: - assumes "vectorspace V" - shows "0 \ U" -proof - - interpret V: vectorspace V by fact - have "U \ {}" by (rule non_empty) - then obtain x where x: "x \ U" by blast - then have "x \ V" .. then have "0 = x - x" by simp - also from `vectorspace V` x x have "\ \ U" by (rule diff_closed) - finally show ?thesis . -qed - -lemma (in subspace) neg_closed [iff]: - assumes "vectorspace V" - assumes x: "x \ U" - shows "- x \ U" -proof - - interpret vectorspace V by fact - from x show ?thesis by (simp add: negate_eq1) -qed - -text {* \medskip Further derived laws: every subspace is a vector space. *} - -lemma (in subspace) vectorspace [iff]: - assumes "vectorspace V" - shows "vectorspace U" -proof - - interpret vectorspace V by fact - show ?thesis - proof - show "U \ {}" .. - fix x y z assume x: "x \ U" and y: "y \ U" and z: "z \ U" - fix a b :: real - from x y show "x + y \ U" by simp - from x show "a \ x \ U" by simp - from x y z show "(x + y) + z = x + (y + z)" by (simp add: add_ac) - from x y show "x + y = y + x" by (simp add: add_ac) - from x show "x - x = 0" by simp - from x show "0 + x = x" by simp - from x y show "a \ (x + y) = a \ x + a \ y" by (simp add: distrib) - from x show "(a + b) \ x = a \ x + b \ x" by (simp add: distrib) - from x show "(a * b) \ x = a \ b \ x" by (simp add: mult_assoc) - from x show "1 \ x = x" by simp - from x show "- x = - 1 \ x" by (simp add: negate_eq1) - from x y show "x - y = x + - y" by (simp add: diff_eq1) - qed -qed - - -text {* The subspace relation is reflexive. *} - -lemma (in vectorspace) subspace_refl [intro]: "V \ V" -proof - show "V \ {}" .. - show "V \ V" .. - fix x y assume x: "x \ V" and y: "y \ V" - fix a :: real - from x y show "x + y \ V" by simp - from x show "a \ x \ V" by simp -qed - -text {* The subspace relation is transitive. *} - -lemma (in vectorspace) subspace_trans [trans]: - "U \ V \ V \ W \ U \ W" -proof - assume uv: "U \ V" and vw: "V \ W" - from uv show "U \ {}" by (rule subspace.non_empty) - show "U \ W" - proof - - from uv have "U \ V" by (rule subspace.subset) - also from vw have "V \ W" by (rule subspace.subset) - finally show ?thesis . - qed - fix x y assume x: "x \ U" and y: "y \ U" - from uv and x y show "x + y \ U" by (rule subspace.add_closed) - from uv and x show "\a. a \ x \ U" by (rule subspace.mult_closed) -qed - - -subsection {* Linear closure *} - -text {* - The \emph{linear closure} of a vector @{text x} is the set of all - scalar multiples of @{text x}. -*} - -definition - lin :: "('a::{minus, plus, zero}) \ 'a set" where - "lin x = {a \ x | a. True}" - -lemma linI [intro]: "y = a \ x \ y \ lin x" - unfolding lin_def by blast - -lemma linI' [iff]: "a \ x \ lin x" - unfolding lin_def by blast - -lemma linE [elim]: "x \ lin v \ (\a::real. x = a \ v \ C) \ C" - unfolding lin_def by blast - - -text {* Every vector is contained in its linear closure. *} - -lemma (in vectorspace) x_lin_x [iff]: "x \ V \ x \ lin x" -proof - - assume "x \ V" - then have "x = 1 \ x" by simp - also have "\ \ lin x" .. - finally show ?thesis . -qed - -lemma (in vectorspace) "0_lin_x" [iff]: "x \ V \ 0 \ lin x" -proof - assume "x \ V" - then show "0 = 0 \ x" by simp -qed - -text {* Any linear closure is a subspace. *} - -lemma (in vectorspace) lin_subspace [intro]: - "x \ V \ lin x \ V" -proof - assume x: "x \ V" - then show "lin x \ {}" by (auto simp add: x_lin_x) - show "lin x \ V" - proof - fix x' assume "x' \ lin x" - then obtain a where "x' = a \ x" .. - with x show "x' \ V" by simp - qed - fix x' x'' assume x': "x' \ lin x" and x'': "x'' \ lin x" - show "x' + x'' \ lin x" - proof - - from x' obtain a' where "x' = a' \ x" .. - moreover from x'' obtain a'' where "x'' = a'' \ x" .. - ultimately have "x' + x'' = (a' + a'') \ x" - using x by (simp add: distrib) - also have "\ \ lin x" .. - finally show ?thesis . - qed - fix a :: real - show "a \ x' \ lin x" - proof - - from x' obtain a' where "x' = a' \ x" .. - with x have "a \ x' = (a * a') \ x" by (simp add: mult_assoc) - also have "\ \ lin x" .. - finally show ?thesis . - qed -qed - - -text {* Any linear closure is a vector space. *} - -lemma (in vectorspace) lin_vectorspace [intro]: - assumes "x \ V" - shows "vectorspace (lin x)" -proof - - from `x \ V` have "subspace (lin x) V" - by (rule lin_subspace) - from this and vectorspace_axioms show ?thesis - by (rule subspace.vectorspace) -qed - - -subsection {* Sum of two vectorspaces *} - -text {* - The \emph{sum} of two vectorspaces @{text U} and @{text V} is the - set of all sums of elements from @{text U} and @{text V}. -*} - -instantiation "fun" :: (type, type) plus -begin - -definition - sum_def: "plus_fun U V = {u + v | u v. u \ U \ v \ V}" (* FIXME not fully general!? *) - -instance .. - -end - -lemma sumE [elim]: - "x \ U + V \ (\u v. x = u + v \ u \ U \ v \ V \ C) \ C" - unfolding sum_def by blast - -lemma sumI [intro]: - "u \ U \ v \ V \ x = u + v \ x \ U + V" - unfolding sum_def by blast - -lemma sumI' [intro]: - "u \ U \ v \ V \ u + v \ U + V" - unfolding sum_def by blast - -text {* @{text U} is a subspace of @{text "U + V"}. *} - -lemma subspace_sum1 [iff]: - assumes "vectorspace U" "vectorspace V" - shows "U \ U + V" -proof - - interpret vectorspace U by fact - interpret vectorspace V by fact - show ?thesis - proof - show "U \ {}" .. - show "U \ U + V" - proof - fix x assume x: "x \ U" - moreover have "0 \ V" .. - ultimately have "x + 0 \ U + V" .. - with x show "x \ U + V" by simp - qed - fix x y assume x: "x \ U" and "y \ U" - then show "x + y \ U" by simp - from x show "\a. a \ x \ U" by simp - qed -qed - -text {* The sum of two subspaces is again a subspace. *} - -lemma sum_subspace [intro?]: - assumes "subspace U E" "vectorspace E" "subspace V E" - shows "U + V \ E" -proof - - interpret subspace U E by fact - interpret vectorspace E by fact - interpret subspace V E by fact - show ?thesis - proof - have "0 \ U + V" - proof - show "0 \ U" using `vectorspace E` .. - show "0 \ V" using `vectorspace E` .. - show "(0::'a) = 0 + 0" by simp - qed - then show "U + V \ {}" by blast - show "U + V \ E" - proof - fix x assume "x \ U + V" - then obtain u v where "x = u + v" and - "u \ U" and "v \ V" .. - then show "x \ E" by simp - qed - fix x y assume x: "x \ U + V" and y: "y \ U + V" - show "x + y \ U + V" - proof - - from x obtain ux vx where "x = ux + vx" and "ux \ U" and "vx \ V" .. - moreover - from y obtain uy vy where "y = uy + vy" and "uy \ U" and "vy \ V" .. - ultimately - have "ux + uy \ U" - and "vx + vy \ V" - and "x + y = (ux + uy) + (vx + vy)" - using x y by (simp_all add: add_ac) - then show ?thesis .. - qed - fix a show "a \ x \ U + V" - proof - - from x obtain u v where "x = u + v" and "u \ U" and "v \ V" .. - then have "a \ u \ U" and "a \ v \ V" - and "a \ x = (a \ u) + (a \ v)" by (simp_all add: distrib) - then show ?thesis .. - qed - qed -qed - -text{* The sum of two subspaces is a vectorspace. *} - -lemma sum_vs [intro?]: - "U \ E \ V \ E \ vectorspace E \ vectorspace (U + V)" - by (rule subspace.vectorspace) (rule sum_subspace) - - -subsection {* Direct sums *} - -text {* - The sum of @{text U} and @{text V} is called \emph{direct}, iff the - zero element is the only common element of @{text U} and @{text - V}. For every element @{text x} of the direct sum of @{text U} and - @{text V} the decomposition in @{text "x = u + v"} with - @{text "u \ U"} and @{text "v \ V"} is unique. -*} - -lemma decomp: - assumes "vectorspace E" "subspace U E" "subspace V E" - assumes direct: "U \ V = {0}" - and u1: "u1 \ U" and u2: "u2 \ U" - and v1: "v1 \ V" and v2: "v2 \ V" - and sum: "u1 + v1 = u2 + v2" - shows "u1 = u2 \ v1 = v2" -proof - - interpret vectorspace E by fact - interpret subspace U E by fact - interpret subspace V E by fact - show ?thesis - proof - have U: "vectorspace U" (* FIXME: use interpret *) - using `subspace U E` `vectorspace E` by (rule subspace.vectorspace) - have V: "vectorspace V" - using `subspace V E` `vectorspace E` by (rule subspace.vectorspace) - from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1" - by (simp add: add_diff_swap) - from u1 u2 have u: "u1 - u2 \ U" - by (rule vectorspace.diff_closed [OF U]) - with eq have v': "v2 - v1 \ U" by (simp only:) - from v2 v1 have v: "v2 - v1 \ V" - by (rule vectorspace.diff_closed [OF V]) - with eq have u': " u1 - u2 \ V" by (simp only:) - - show "u1 = u2" - proof (rule add_minus_eq) - from u1 show "u1 \ E" .. - from u2 show "u2 \ E" .. - from u u' and direct show "u1 - u2 = 0" by blast - qed - show "v1 = v2" - proof (rule add_minus_eq [symmetric]) - from v1 show "v1 \ E" .. - from v2 show "v2 \ E" .. - from v v' and direct show "v2 - v1 = 0" by blast - qed - qed -qed - -text {* - 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 @{text "y + a \ x\<^sub>0"} of the direct sum of a - vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"} - the components @{text "y \ H"} and @{text a} are uniquely - determined. -*} - -lemma decomp_H': - assumes "vectorspace E" "subspace H E" - assumes y1: "y1 \ H" and y2: "y2 \ H" - and x': "x' \ H" "x' \ E" "x' \ 0" - and eq: "y1 + a1 \ x' = y2 + a2 \ x'" - shows "y1 = y2 \ a1 = a2" -proof - - interpret vectorspace E by fact - interpret subspace H E by fact - show ?thesis - proof - have c: "y1 = y2 \ a1 \ x' = a2 \ x'" - proof (rule decomp) - show "a1 \ x' \ lin x'" .. - show "a2 \ x' \ lin x'" .. - show "H \ lin x' = {0}" - proof - show "H \ lin x' \ {0}" - proof - fix x assume x: "x \ H \ lin x'" - then obtain a where xx': "x = a \ x'" - by blast - have "x = 0" - proof cases - assume "a = 0" - with xx' and x' show ?thesis by simp - next - assume a: "a \ 0" - from x have "x \ H" .. - with xx' have "inverse a \ a \ x' \ H" by simp - with a and x' have "x' \ H" by (simp add: mult_assoc2) - with `x' \ H` show ?thesis by contradiction - qed - then show "x \ {0}" .. - qed - show "{0} \ H \ lin x'" - proof - - have "0 \ H" using `vectorspace E` .. - moreover have "0 \ lin x'" using `x' \ E` .. - ultimately show ?thesis by blast - qed - qed - show "lin x' \ E" using `x' \ E` .. - qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq) - then show "y1 = y2" .. - from c have "a1 \ x' = a2 \ x'" .. - with x' show "a1 = a2" by (simp add: mult_right_cancel) - qed -qed - -text {* - Since for any element @{text "y + a \ x'"} of the direct sum of a - vectorspace @{text H} and the linear closure of @{text x'} the - components @{text "y \ H"} and @{text a} are unique, it follows from - @{text "y \ H"} that @{text "a = 0"}. -*} - -lemma decomp_H'_H: - assumes "vectorspace E" "subspace H E" - assumes t: "t \ H" - and x': "x' \ H" "x' \ E" "x' \ 0" - shows "(SOME (y, a). t = y + a \ x' \ y \ H) = (t, 0)" -proof - - interpret vectorspace E by fact - interpret subspace H E by fact - show ?thesis - proof (rule, simp_all only: split_paired_all split_conv) - from t x' show "t = t + 0 \ x' \ t \ H" by simp - fix y and a assume ya: "t = y + a \ x' \ y \ H" - have "y = t \ a = 0" - proof (rule decomp_H') - from ya x' show "y + a \ x' = t + 0 \ x'" by simp - from ya show "y \ H" .. - qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+) - with t x' show "(y, a) = (y + a \ x', 0)" by simp - qed -qed - -text {* - The components @{text "y \ H"} and @{text a} in @{text "y + a \ x'"} - are unique, so the function @{text h'} defined by - @{text "h' (y + a \ x') = h y + a \ \"} is definite. -*} - -lemma h'_definite: - fixes H - assumes h'_def: - "h' \ (\x. let (y, a) = SOME (y, a). (x = y + a \ x' \ y \ H) - in (h y) + a * xi)" - and x: "x = y + a \ x'" - assumes "vectorspace E" "subspace H E" - assumes y: "y \ H" - and x': "x' \ H" "x' \ E" "x' \ 0" - shows "h' x = h y + a * xi" -proof - - interpret vectorspace E by fact - interpret subspace H E by fact - from x y x' have "x \ H + lin x'" by auto - have "\!p. (\(y, a). x = y + a \ x' \ y \ H) p" (is "\!p. ?P p") - proof (rule ex_ex1I) - from x y show "\p. ?P p" by blast - fix p q assume p: "?P p" and q: "?P q" - show "p = q" - proof - - from p have xp: "x = fst p + snd p \ x' \ fst p \ H" - by (cases p) simp - from q have xq: "x = fst q + snd q \ x' \ fst q \ H" - by (cases q) simp - have "fst p = fst q \ snd p = snd q" - proof (rule decomp_H') - from xp show "fst p \ H" .. - from xq show "fst q \ H" .. - from xp and xq show "fst p + snd p \ x' = fst q + snd q \ x'" - by simp - qed (rule `vectorspace E`, rule `subspace H E`, (rule x')+) - then show ?thesis by (cases p, cases q) simp - qed - qed - then have eq: "(SOME (y, a). x = y + a \ x' \ y \ H) = (y, a)" - by (rule some1_equality) (simp add: x y) - with h'_def show "h' x = h y + a * xi" by (simp add: Let_def) -qed - -end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/VectorSpace.thy --- a/src/HOL/HahnBanach/VectorSpace.thy Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,419 +0,0 @@ -(* Title: HOL/Real/HahnBanach/VectorSpace.thy - ID: $Id$ - Author: Gertrud Bauer, TU Munich -*) - -header {* Vector spaces *} - -theory VectorSpace -imports Real Bounds Zorn -begin - -subsection {* Signature *} - -text {* - For the definition of real vector spaces a type @{typ 'a} of the - sort @{text "{plus, minus, zero}"} is considered, on which a real - scalar multiplication @{text \} is declared. -*} - -consts - prod :: "real \ 'a::{plus, minus, zero} \ 'a" (infixr "'(*')" 70) - -notation (xsymbols) - prod (infixr "\" 70) -notation (HTML output) - prod (infixr "\" 70) - - -subsection {* Vector space laws *} - -text {* - A \emph{vector space} is a non-empty set @{text V} of elements from - @{typ 'a} with the following vector space laws: The set @{text V} is - closed under addition and scalar multiplication, addition is - associative and commutative; @{text "- x"} is the inverse of @{text - x} w.~r.~t.~addition and @{text 0} is the neutral element of - addition. Addition and multiplication are distributive; scalar - multiplication is associative and the real number @{text "1"} is - the neutral element of scalar multiplication. -*} - -locale var_V = fixes V - -locale vectorspace = var_V + - assumes non_empty [iff, intro?]: "V \ {}" - and add_closed [iff]: "x \ V \ y \ V \ x + y \ V" - and mult_closed [iff]: "x \ V \ a \ x \ V" - and add_assoc: "x \ V \ y \ V \ z \ V \ (x + y) + z = x + (y + z)" - and add_commute: "x \ V \ y \ V \ x + y = y + x" - and diff_self [simp]: "x \ V \ x - x = 0" - and add_zero_left [simp]: "x \ V \ 0 + x = x" - and add_mult_distrib1: "x \ V \ y \ V \ a \ (x + y) = a \ x + a \ y" - and add_mult_distrib2: "x \ V \ (a + b) \ x = a \ x + b \ x" - and mult_assoc: "x \ V \ (a * b) \ x = a \ (b \ x)" - and mult_1 [simp]: "x \ V \ 1 \ x = x" - and negate_eq1: "x \ V \ - x = (- 1) \ x" - and diff_eq1: "x \ V \ y \ V \ x - y = x + - y" - -lemma (in vectorspace) negate_eq2: "x \ V \ (- 1) \ x = - x" - by (rule negate_eq1 [symmetric]) - -lemma (in vectorspace) negate_eq2a: "x \ V \ -1 \ x = - x" - by (simp add: negate_eq1) - -lemma (in vectorspace) diff_eq2: "x \ V \ y \ V \ x + - y = x - y" - by (rule diff_eq1 [symmetric]) - -lemma (in vectorspace) diff_closed [iff]: "x \ V \ y \ V \ x - y \ V" - by (simp add: diff_eq1 negate_eq1) - -lemma (in vectorspace) neg_closed [iff]: "x \ V \ - x \ V" - by (simp add: negate_eq1) - -lemma (in vectorspace) add_left_commute: - "x \ V \ y \ V \ z \ V \ x + (y + z) = y + (x + z)" -proof - - assume xyz: "x \ V" "y \ V" "z \ V" - then have "x + (y + z) = (x + y) + z" - by (simp only: add_assoc) - also from xyz have "\ = (y + x) + z" by (simp only: add_commute) - also from xyz have "\ = y + (x + z)" by (simp only: add_assoc) - finally show ?thesis . -qed - -theorems (in vectorspace) add_ac = - add_assoc add_commute add_left_commute - - -text {* The existence of the zero element of a vector space - follows from the non-emptiness of carrier set. *} - -lemma (in vectorspace) zero [iff]: "0 \ V" -proof - - from non_empty obtain x where x: "x \ V" by blast - then have "0 = x - x" by (rule diff_self [symmetric]) - also from x x have "\ \ V" by (rule diff_closed) - finally show ?thesis . -qed - -lemma (in vectorspace) add_zero_right [simp]: - "x \ V \ x + 0 = x" -proof - - assume x: "x \ V" - from this and zero have "x + 0 = 0 + x" by (rule add_commute) - also from x have "\ = x" by (rule add_zero_left) - finally show ?thesis . -qed - -lemma (in vectorspace) mult_assoc2: - "x \ V \ a \ b \ x = (a * b) \ x" - by (simp only: mult_assoc) - -lemma (in vectorspace) diff_mult_distrib1: - "x \ V \ y \ V \ a \ (x - y) = a \ x - a \ y" - by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2) - -lemma (in vectorspace) diff_mult_distrib2: - "x \ V \ (a - b) \ x = a \ x - (b \ x)" -proof - - assume x: "x \ V" - have " (a - b) \ x = (a + - b) \ x" - by (simp add: real_diff_def) - also from x have "\ = a \ x + (- b) \ x" - by (rule add_mult_distrib2) - also from x have "\ = a \ x + - (b \ x)" - by (simp add: negate_eq1 mult_assoc2) - also from x have "\ = a \ x - (b \ x)" - by (simp add: diff_eq1) - finally show ?thesis . -qed - -lemmas (in vectorspace) distrib = - add_mult_distrib1 add_mult_distrib2 - diff_mult_distrib1 diff_mult_distrib2 - - -text {* \medskip Further derived laws: *} - -lemma (in vectorspace) mult_zero_left [simp]: - "x \ V \ 0 \ x = 0" -proof - - assume x: "x \ V" - have "0 \ x = (1 - 1) \ x" by simp - also have "\ = (1 + - 1) \ x" by simp - also from x have "\ = 1 \ x + (- 1) \ x" - by (rule add_mult_distrib2) - also from x have "\ = x + (- 1) \ x" by simp - also from x have "\ = x + - x" by (simp add: negate_eq2a) - also from x have "\ = x - x" by (simp add: diff_eq2) - also from x have "\ = 0" by simp - finally show ?thesis . -qed - -lemma (in vectorspace) mult_zero_right [simp]: - "a \ 0 = (0::'a)" -proof - - have "a \ 0 = a \ (0 - (0::'a))" by simp - also have "\ = a \ 0 - a \ 0" - by (rule diff_mult_distrib1) simp_all - also have "\ = 0" by simp - finally show ?thesis . -qed - -lemma (in vectorspace) minus_mult_cancel [simp]: - "x \ V \ (- a) \ - x = a \ x" - by (simp add: negate_eq1 mult_assoc2) - -lemma (in vectorspace) add_minus_left_eq_diff: - "x \ V \ y \ V \ - x + y = y - x" -proof - - assume xy: "x \ V" "y \ V" - then have "- x + y = y + - x" by (simp add: add_commute) - also from xy have "\ = y - x" by (simp add: diff_eq1) - finally show ?thesis . -qed - -lemma (in vectorspace) add_minus [simp]: - "x \ V \ x + - x = 0" - by (simp add: diff_eq2) - -lemma (in vectorspace) add_minus_left [simp]: - "x \ V \ - x + x = 0" - by (simp add: diff_eq2 add_commute) - -lemma (in vectorspace) minus_minus [simp]: - "x \ V \ - (- x) = x" - by (simp add: negate_eq1 mult_assoc2) - -lemma (in vectorspace) minus_zero [simp]: - "- (0::'a) = 0" - by (simp add: negate_eq1) - -lemma (in vectorspace) minus_zero_iff [simp]: - "x \ V \ (- x = 0) = (x = 0)" -proof - assume x: "x \ V" - { - from x have "x = - (- x)" by (simp add: minus_minus) - also assume "- x = 0" - also have "- \ = 0" by (rule minus_zero) - finally show "x = 0" . - next - assume "x = 0" - then show "- x = 0" by simp - } -qed - -lemma (in vectorspace) add_minus_cancel [simp]: - "x \ V \ y \ V \ x + (- x + y) = y" - by (simp add: add_assoc [symmetric] del: add_commute) - -lemma (in vectorspace) minus_add_cancel [simp]: - "x \ V \ y \ V \ - x + (x + y) = y" - by (simp add: add_assoc [symmetric] del: add_commute) - -lemma (in vectorspace) minus_add_distrib [simp]: - "x \ V \ y \ V \ - (x + y) = - x + - y" - by (simp add: negate_eq1 add_mult_distrib1) - -lemma (in vectorspace) diff_zero [simp]: - "x \ V \ x - 0 = x" - by (simp add: diff_eq1) - -lemma (in vectorspace) diff_zero_right [simp]: - "x \ V \ 0 - x = - x" - by (simp add: diff_eq1) - -lemma (in vectorspace) add_left_cancel: - "x \ V \ y \ V \ z \ V \ (x + y = x + z) = (y = z)" -proof - assume x: "x \ V" and y: "y \ V" and z: "z \ V" - { - from y have "y = 0 + y" by simp - also from x y have "\ = (- x + x) + y" by simp - also from x y have "\ = - x + (x + y)" - by (simp add: add_assoc neg_closed) - also assume "x + y = x + z" - also from x z have "- x + (x + z) = - x + x + z" - by (simp add: add_assoc [symmetric] neg_closed) - also from x z have "\ = z" by simp - finally show "y = z" . - next - assume "y = z" - then show "x + y = x + z" by (simp only:) - } -qed - -lemma (in vectorspace) add_right_cancel: - "x \ V \ y \ V \ z \ V \ (y + x = z + x) = (y = z)" - by (simp only: add_commute add_left_cancel) - -lemma (in vectorspace) add_assoc_cong: - "x \ V \ y \ V \ x' \ V \ y' \ V \ z \ V - \ x + y = x' + y' \ x + (y + z) = x' + (y' + z)" - by (simp only: add_assoc [symmetric]) - -lemma (in vectorspace) mult_left_commute: - "x \ V \ a \ b \ x = b \ a \ x" - by (simp add: real_mult_commute mult_assoc2) - -lemma (in vectorspace) mult_zero_uniq: - "x \ V \ x \ 0 \ a \ x = 0 \ a = 0" -proof (rule classical) - assume a: "a \ 0" - assume x: "x \ V" "x \ 0" and ax: "a \ x = 0" - from x a have "x = (inverse a * a) \ x" by simp - also from `x \ V` have "\ = inverse a \ (a \ x)" by (rule mult_assoc) - also from ax have "\ = inverse a \ 0" by simp - also have "\ = 0" by simp - finally have "x = 0" . - with `x \ 0` show "a = 0" by contradiction -qed - -lemma (in vectorspace) mult_left_cancel: - "x \ V \ y \ V \ a \ 0 \ (a \ x = a \ y) = (x = y)" -proof - assume x: "x \ V" and y: "y \ V" and a: "a \ 0" - from x have "x = 1 \ x" by simp - also from a have "\ = (inverse a * a) \ x" by simp - also from x have "\ = inverse a \ (a \ x)" - by (simp only: mult_assoc) - also assume "a \ x = a \ y" - also from a y have "inverse a \ \ = y" - by (simp add: mult_assoc2) - finally show "x = y" . -next - assume "x = y" - then show "a \ x = a \ y" by (simp only:) -qed - -lemma (in vectorspace) mult_right_cancel: - "x \ V \ x \ 0 \ (a \ x = b \ x) = (a = b)" -proof - assume x: "x \ V" and neq: "x \ 0" - { - from x have "(a - b) \ x = a \ x - b \ x" - by (simp add: diff_mult_distrib2) - also assume "a \ x = b \ x" - with x have "a \ x - b \ x = 0" by simp - finally have "(a - b) \ x = 0" . - with x neq have "a - b = 0" by (rule mult_zero_uniq) - then show "a = b" by simp - next - assume "a = b" - then show "a \ x = b \ x" by (simp only:) - } -qed - -lemma (in vectorspace) eq_diff_eq: - "x \ V \ y \ V \ z \ V \ (x = z - y) = (x + y = z)" -proof - assume x: "x \ V" and y: "y \ V" and z: "z \ V" - { - assume "x = z - y" - then have "x + y = z - y + y" by simp - also from y z have "\ = z + - y + y" - by (simp add: diff_eq1) - also have "\ = z + (- y + y)" - by (rule add_assoc) (simp_all add: y z) - also from y z have "\ = z + 0" - by (simp only: add_minus_left) - also from z have "\ = z" - by (simp only: add_zero_right) - finally show "x + y = z" . - next - assume "x + y = z" - then have "z - y = (x + y) - y" by simp - also from x y have "\ = x + y + - y" - by (simp add: diff_eq1) - also have "\ = x + (y + - y)" - by (rule add_assoc) (simp_all add: x y) - also from x y have "\ = x" by simp - finally show "x = z - y" .. - } -qed - -lemma (in vectorspace) add_minus_eq_minus: - "x \ V \ y \ V \ x + y = 0 \ x = - y" -proof - - assume x: "x \ V" and y: "y \ V" - from x y have "x = (- y + y) + x" by simp - also from x y have "\ = - y + (x + y)" by (simp add: add_ac) - also assume "x + y = 0" - also from y have "- y + 0 = - y" by simp - finally show "x = - y" . -qed - -lemma (in vectorspace) add_minus_eq: - "x \ V \ y \ V \ x - y = 0 \ x = y" -proof - - assume x: "x \ V" and y: "y \ V" - assume "x - y = 0" - with x y have eq: "x + - y = 0" by (simp add: diff_eq1) - with _ _ have "x = - (- y)" - by (rule add_minus_eq_minus) (simp_all add: x y) - with x y show "x = y" by simp -qed - -lemma (in vectorspace) add_diff_swap: - "a \ V \ b \ V \ c \ V \ d \ V \ a + b = c + d - \ a - c = d - b" -proof - - assume vs: "a \ V" "b \ V" "c \ V" "d \ V" - and eq: "a + b = c + d" - then have "- c + (a + b) = - c + (c + d)" - by (simp add: add_left_cancel) - also have "\ = d" using `c \ V` `d \ V` by (rule minus_add_cancel) - finally have eq: "- c + (a + b) = d" . - from vs have "a - c = (- c + (a + b)) + - b" - by (simp add: add_ac diff_eq1) - also from vs eq have "\ = d + - b" - by (simp add: add_right_cancel) - also from vs have "\ = d - b" by (simp add: diff_eq2) - finally show "a - c = d - b" . -qed - -lemma (in vectorspace) vs_add_cancel_21: - "x \ V \ y \ V \ z \ V \ u \ V - \ (x + (y + z) = y + u) = (x + z = u)" -proof - assume vs: "x \ V" "y \ V" "z \ V" "u \ V" - { - from vs have "x + z = - y + y + (x + z)" by simp - also have "\ = - y + (y + (x + z))" - by (rule add_assoc) (simp_all add: vs) - also from vs have "y + (x + z) = x + (y + z)" - by (simp add: add_ac) - also assume "x + (y + z) = y + u" - also from vs have "- y + (y + u) = u" by simp - finally show "x + z = u" . - next - assume "x + z = u" - with vs show "x + (y + z) = y + u" - by (simp only: add_left_commute [of x]) - } -qed - -lemma (in vectorspace) add_cancel_end: - "x \ V \ y \ V \ z \ V \ (x + (y + z) = y) = (x = - z)" -proof - assume vs: "x \ V" "y \ V" "z \ V" - { - assume "x + (y + z) = y" - with vs have "(x + z) + y = 0 + y" - by (simp add: add_ac) - with vs have "x + z = 0" - by (simp only: add_right_cancel add_closed zero) - with vs show "x = - z" by (simp add: add_minus_eq_minus) - next - assume eq: "x = - z" - then have "x + (y + z) = - z + (y + z)" by simp - also have "\ = y + (- z + z)" - by (rule add_left_commute) (simp_all add: vs) - also from vs have "\ = y" by simp - finally show "x + (y + z) = y" . - } -qed - -end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/ZornLemma.thy --- a/src/HOL/HahnBanach/ZornLemma.thy Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,57 +0,0 @@ -(* Title: HOL/Real/HahnBanach/ZornLemma.thy - Author: Gertrud Bauer, TU Munich -*) - -header {* Zorn's Lemma *} - -theory ZornLemma -imports Zorn -begin - -text {* - Zorn's Lemmas states: if every linear ordered subset of an ordered - set @{text S} has an upper bound in @{text S}, then there exists a - maximal element in @{text S}. In our application, @{text S} is a - set of sets ordered by set inclusion. Since the union of a chain of - sets is an upper bound for all elements of the chain, the conditions - of Zorn's lemma can be modified: if @{text S} is non-empty, it - suffices to show that for every non-empty chain @{text c} in @{text - S} the union of @{text c} also lies in @{text S}. -*} - -theorem Zorn's_Lemma: - assumes r: "\c. c \ chain S \ \x. x \ c \ \c \ S" - and aS: "a \ S" - shows "\y \ S. \z \ S. y \ z \ y = z" -proof (rule Zorn_Lemma2) - show "\c \ chain S. \y \ S. \z \ c. z \ y" - proof - fix c assume "c \ chain S" - show "\y \ S. \z \ c. z \ y" - proof cases - - txt {* If @{text c} is an empty chain, then every element in - @{text S} is an upper bound of @{text c}. *} - - assume "c = {}" - with aS show ?thesis by fast - - txt {* If @{text c} is non-empty, then @{text "\c"} is an upper - bound of @{text c}, lying in @{text S}. *} - - next - assume "c \ {}" - show ?thesis - proof - show "\z \ c. z \ \c" by fast - show "\c \ S" - proof (rule r) - from `c \ {}` show "\x. x \ c" by fast - show "c \ chain S" by fact - qed - qed - qed - qed -qed - -end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/document/root.bib --- a/src/HOL/HahnBanach/document/root.bib Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,27 +0,0 @@ - -@Book{Heuser:1986, - author = {H. Heuser}, - title = {Funktionalanalysis: Theorie und Anwendung}, - publisher = {Teubner}, - year = 1986 -} - -@InCollection{Narici:1996, - author = {L. Narici and E. Beckenstein}, - title = {The {Hahn-Banach Theorem}: The Life and Times}, - booktitle = {Topology Atlas}, - publisher = {York University, Toronto, Ontario, Canada}, - year = 1996, - note = {\url{http://at.yorku.ca/topology/preprint.htm} and - \url{http://at.yorku.ca/p/a/a/a/16.htm}} -} - -@Article{Nowak:1993, - author = {B. Nowak and A. Trybulec}, - title = {{Hahn-Banach} Theorem}, - journal = {Journal of Formalized Mathematics}, - year = {1993}, - volume = {5}, - institution = {University of Bialystok}, - note = {\url{http://mizar.uwb.edu.pl/JFM/Vol5/hahnban.html}} -} diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/HahnBanach/document/root.tex --- a/src/HOL/HahnBanach/document/root.tex Wed Jun 24 21:28:02 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,83 +0,0 @@ -\documentclass[10pt,a4paper,twoside]{article} -\usepackage{graphicx} -\usepackage{latexsym,theorem} -\usepackage{isabelle,isabellesym} -\usepackage{pdfsetup} %last one! - -\isabellestyle{it} -\urlstyle{rm} - -\newcommand{\isasymsup}{\isamath{\sup\,}} -\newcommand{\skp}{\smallskip} - - -\begin{document} - -\pagestyle{headings} -\pagenumbering{arabic} - -\title{The Hahn-Banach Theorem \\ for Real Vector Spaces} -\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}} -\maketitle - -\begin{abstract} - The Hahn-Banach Theorem is one of the most fundamental results in functional - analysis. We present a fully formal proof of two versions of the theorem, - one for general linear spaces and another for normed spaces. This - development is based on simply-typed classical set-theory, as provided by - Isabelle/HOL. -\end{abstract} - - -\tableofcontents -\parindent 0pt \parskip 0.5ex - -\clearpage -\section{Preface} - -This is a fully formal proof of the Hahn-Banach Theorem. It closely follows -the informal presentation given in Heuser's textbook \cite[{\S} 36]{Heuser:1986}. -Another formal proof of the same theorem has been done in Mizar -\cite{Nowak:1993}. A general overview of the relevance and history of the -Hahn-Banach Theorem is given by Narici and Beckenstein \cite{Narici:1996}. - -\medskip The document is structured as follows. The first part contains -definitions of basic notions of linear algebra: vector spaces, subspaces, -normed spaces, continuous linear-forms, norm of functions and an order on -functions by domain extension. The second part contains some lemmas about the -supremum (w.r.t.\ the function order) and extension of non-maximal functions. -With these preliminaries, the main proof of the theorem (in its two versions) -is conducted in the third part. The dependencies of individual theories are -as follows. - -\begin{center} - \includegraphics[scale=0.5]{session_graph} -\end{center} - -\clearpage -\part {Basic Notions} - -\input{Bounds} -\input{VectorSpace} -\input{Subspace} -\input{NormedSpace} -\input{Linearform} -\input{FunctionOrder} -\input{FunctionNorm} -\input{ZornLemma} - -\clearpage -\part {Lemmas for the Proof} - -\input{HahnBanachSupLemmas} -\input{HahnBanachExtLemmas} -\input{HahnBanachLemmas} - -\clearpage -\part {The Main Proof} - -\input{HahnBanach} -\bibliographystyle{abbrv} -\bibliography{root} - -\end{document} diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/Bounds.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/Bounds.thy Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,82 @@ +(* Title: HOL/Hahn_Banach/Bounds.thy + Author: Gertrud Bauer, TU Munich +*) + +header {* Bounds *} + +theory Bounds +imports Main ContNotDenum +begin + +locale lub = + fixes A and x + assumes least [intro?]: "(\a. a \ A \ a \ b) \ x \ b" + and upper [intro?]: "a \ A \ a \ x" + +lemmas [elim?] = lub.least lub.upper + +definition + the_lub :: "'a::order set \ 'a" where + "the_lub A = The (lub A)" + +notation (xsymbols) + the_lub ("\_" [90] 90) + +lemma the_lub_equality [elim?]: + assumes "lub A x" + shows "\A = (x::'a::order)" +proof - + interpret lub A x by fact + show ?thesis + proof (unfold the_lub_def) + from `lub A x` show "The (lub A) = x" + proof + fix x' assume lub': "lub A x'" + show "x' = x" + proof (rule order_antisym) + from lub' show "x' \ x" + proof + fix a assume "a \ A" + then show "a \ x" .. + qed + show "x \ x'" + proof + fix a assume "a \ A" + with lub' show "a \ x'" .. + qed + qed + qed + qed +qed + +lemma the_lubI_ex: + assumes ex: "\x. lub A x" + shows "lub A (\A)" +proof - + from ex obtain x where x: "lub A x" .. + also from x have [symmetric]: "\A = x" .. + finally show ?thesis . +qed + +lemma lub_compat: "lub A x = isLub UNIV A x" +proof - + have "isUb UNIV A = (\x. A *<= x \ x \ UNIV)" + by (rule ext) (simp only: isUb_def) + then show ?thesis + by (simp only: lub_def isLub_def leastP_def setge_def setle_def) blast +qed + +lemma real_complete: + fixes A :: "real set" + assumes nonempty: "\a. a \ A" + and ex_upper: "\y. \a \ A. a \ y" + shows "\x. lub A x" +proof - + from ex_upper have "\y. isUb UNIV A y" + unfolding isUb_def setle_def by blast + with nonempty have "\x. isLub UNIV A x" + by (rule reals_complete) + then show ?thesis by (simp only: lub_compat) +qed + +end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/Function_Norm.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/Function_Norm.thy Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,278 @@ +(* Title: HOL/Hahn_Banach/Function_Norm.thy + Author: Gertrud Bauer, TU Munich +*) + +header {* The norm of a function *} + +theory Function_Norm +imports Normed_Space Function_Order +begin + +subsection {* Continuous linear forms*} + +text {* + A linear form @{text f} on a normed vector space @{text "(V, \\\)"} + is \emph{continuous}, iff it is bounded, i.e. + \begin{center} + @{text "\c \ R. \x \ V. \f x\ \ c \ \x\"} + \end{center} + In our application no other functions than linear forms are + considered, so we can define continuous linear forms as bounded + linear forms: +*} + +locale continuous = var_V + norm_syntax + linearform + + assumes bounded: "\c. \x \ V. \f x\ \ c * \x\" + +declare continuous.intro [intro?] continuous_axioms.intro [intro?] + +lemma continuousI [intro]: + fixes norm :: "_ \ real" ("\_\") + assumes "linearform V f" + assumes r: "\x. x \ V \ \f x\ \ c * \x\" + shows "continuous V norm f" +proof + show "linearform V f" by fact + from r have "\c. \x\V. \f x\ \ c * \x\" by blast + then show "continuous_axioms V norm f" .. +qed + + +subsection {* The norm of a linear form *} + +text {* + The least real number @{text c} for which holds + \begin{center} + @{text "\x \ V. \f x\ \ c \ \x\"} + \end{center} + is called the \emph{norm} of @{text f}. + + For non-trivial vector spaces @{text "V \ {0}"} the norm can be + defined as + \begin{center} + @{text "\f\ = \x \ 0. \f x\ / \x\"} + \end{center} + + For the case @{text "V = {0}"} the supremum would be taken from an + empty set. Since @{text \} 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 @{text "{} \ 0"} so that + @{text fn_norm} has the norm properties. Furthermore it does not + have to change the norm in all other cases, so it must be @{text 0}, + as all other elements are @{text "{} \ 0"}. + + Thus we define the set @{text B} where the supremum is taken from as + follows: + \begin{center} + @{text "{0} \ {\f x\ / \x\. x \ 0 \ x \ F}"} + \end{center} + + @{text fn_norm} is equal to the supremum of @{text B}, if the + supremum exists (otherwise it is undefined). +*} + +locale fn_norm = norm_syntax + + fixes B defines "B V f \ {0} \ {\f x\ / \x\ | x. x \ 0 \ x \ V}" + fixes fn_norm ("\_\\_" [0, 1000] 999) + defines "\f\\V \ \(B V f)" + +locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm + +lemma (in fn_norm) B_not_empty [intro]: "0 \ B V f" + by (simp add: B_def) + +text {* + The following lemma states that every continuous linear form on a + normed space @{text "(V, \\\)"} has a function norm. +*} + +lemma (in normed_vectorspace_with_fn_norm) fn_norm_works: + assumes "continuous V norm f" + shows "lub (B V f) (\f\\V)" +proof - + interpret continuous V norm f by fact + txt {* The existence of the supremum is shown using the + completeness of the reals. Completeness means, that every + non-empty bounded set of reals has a supremum. *} + have "\a. lub (B V f) a" + proof (rule real_complete) + txt {* First we have to show that @{text B} is non-empty: *} + have "0 \ B V f" .. + then show "\x. x \ B V f" .. + + txt {* Then we have to show that @{text B} is bounded: *} + show "\c. \y \ B V f. y \ c" + proof - + txt {* We know that @{text f} is bounded by some value @{text c}. *} + from bounded obtain c where c: "\x \ V. \f x\ \ c * \x\" .. + + txt {* To prove the thesis, we have to show that there is some + @{text b}, such that @{text "y \ b"} for all @{text "y \ + B"}. Due to the definition of @{text B} there are two cases. *} + + def b \ "max c 0" + have "\y \ B V f. y \ b" + proof + fix y assume y: "y \ B V f" + show "y \ b" + proof cases + assume "y = 0" + then show ?thesis unfolding b_def by arith + next + txt {* The second case is @{text "y = \f x\ / \x\"} for some + @{text "x \ V"} with @{text "x \ 0"}. *} + assume "y \ 0" + with y obtain x where y_rep: "y = \f x\ * inverse \x\" + and x: "x \ V" and neq: "x \ 0" + by (auto simp add: B_def real_divide_def) + from x neq have gt: "0 < \x\" .. + + txt {* The thesis follows by a short calculation using the + fact that @{text f} is bounded. *} + + note y_rep + also have "\f x\ * inverse \x\ \ (c * \x\) * inverse \x\" + proof (rule mult_right_mono) + from c x show "\f x\ \ c * \x\" .. + from gt have "0 < inverse \x\" + by (rule positive_imp_inverse_positive) + then show "0 \ inverse \x\" by (rule order_less_imp_le) + qed + also have "\ = c * (\x\ * inverse \x\)" + by (rule real_mult_assoc) + also + from gt have "\x\ \ 0" by simp + then have "\x\ * inverse \x\ = 1" by simp + also have "c * 1 \ b" by (simp add: b_def le_maxI1) + finally show "y \ b" . + qed + qed + then show ?thesis .. + qed + qed + then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex) +qed + +lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]: + assumes "continuous V norm f" + assumes b: "b \ B V f" + shows "b \ \f\\V" +proof - + interpret continuous V norm f by fact + have "lub (B V f) (\f\\V)" + using `continuous V norm f` by (rule fn_norm_works) + from this and b show ?thesis .. +qed + +lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB: + assumes "continuous V norm f" + assumes b: "\b. b \ B V f \ b \ y" + shows "\f\\V \ y" +proof - + interpret continuous V norm f by fact + have "lub (B V f) (\f\\V)" + using `continuous V norm f` by (rule fn_norm_works) + from this and b show ?thesis .. +qed + +text {* The norm of a continuous function is always @{text "\ 0"}. *} + +lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]: + assumes "continuous V norm f" + shows "0 \ \f\\V" +proof - + interpret continuous V norm f by fact + txt {* The function norm is defined as the supremum of @{text B}. + So it is @{text "\ 0"} if all elements in @{text B} are @{text "\ + 0"}, provided the supremum exists and @{text B} is not empty. *} + have "lub (B V f) (\f\\V)" + using `continuous V norm f` by (rule fn_norm_works) + moreover have "0 \ B V f" .. + ultimately show ?thesis .. +qed + +text {* + \medskip The fundamental property of function norms is: + \begin{center} + @{text "\f x\ \ \f\ \ \x\"} + \end{center} +*} + +lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong: + assumes "continuous V norm f" "linearform V f" + assumes x: "x \ V" + shows "\f x\ \ \f\\V * \x\" +proof - + interpret continuous V norm f by fact + interpret linearform V f by fact + show ?thesis + proof cases + assume "x = 0" + then have "\f x\ = \f 0\" by simp + also have "f 0 = 0" by rule unfold_locales + also have "\\\ = 0" by simp + also have a: "0 \ \f\\V" + using `continuous V norm f` by (rule fn_norm_ge_zero) + from x have "0 \ norm x" .. + with a have "0 \ \f\\V * \x\" by (simp add: zero_le_mult_iff) + finally show "\f x\ \ \f\\V * \x\" . + next + assume "x \ 0" + with x have neq: "\x\ \ 0" by simp + then have "\f x\ = (\f x\ * inverse \x\) * \x\" by simp + also have "\ \ \f\\V * \x\" + proof (rule mult_right_mono) + from x show "0 \ \x\" .. + from x and neq have "\f x\ * inverse \x\ \ B V f" + by (auto simp add: B_def real_divide_def) + with `continuous V norm f` show "\f x\ * inverse \x\ \ \f\\V" + by (rule fn_norm_ub) + qed + finally show ?thesis . + qed +qed + +text {* + \medskip The function norm is the least positive real number for + which the following inequation holds: + \begin{center} + @{text "\f x\ \ c \ \x\"} + \end{center} +*} + +lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]: + assumes "continuous V norm f" + assumes ineq: "\x \ V. \f x\ \ c * \x\" and ge: "0 \ c" + shows "\f\\V \ c" +proof - + interpret continuous V norm f by fact + show ?thesis + proof (rule fn_norm_leastB [folded B_def fn_norm_def]) + fix b assume b: "b \ B V f" + show "b \ c" + proof cases + assume "b = 0" + with ge show ?thesis by simp + next + assume "b \ 0" + with b obtain x where b_rep: "b = \f x\ * inverse \x\" + and x_neq: "x \ 0" and x: "x \ V" + by (auto simp add: B_def real_divide_def) + note b_rep + also have "\f x\ * inverse \x\ \ (c * \x\) * inverse \x\" + proof (rule mult_right_mono) + have "0 < \x\" using x x_neq .. + then show "0 \ inverse \x\" by simp + from ineq and x show "\f x\ \ c * \x\" .. + qed + also have "\ = c" + proof - + from x_neq and x have "\x\ \ 0" by simp + then show ?thesis by simp + qed + finally show ?thesis . + qed + qed (insert `continuous V norm f`, simp_all add: continuous_def) +qed + +end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/Function_Order.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/Function_Order.thy Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,141 @@ +(* Title: HOL/Hahn_Banach/Function_Order.thy + Author: Gertrud Bauer, TU Munich +*) + +header {* An order on functions *} + +theory Function_Order +imports Subspace Linearform +begin + +subsection {* The graph of a function *} + +text {* + We define the \emph{graph} of a (real) function @{text f} with + domain @{text F} as the set + \begin{center} + @{text "{(x, f x). x \ F}"} + \end{center} + So we are modeling partial functions by specifying the domain and + the mapping function. We use the term ``function'' also for its + graph. +*} + +types 'a graph = "('a \ real) set" + +definition + graph :: "'a set \ ('a \ real) \ 'a graph" where + "graph F f = {(x, f x) | x. x \ F}" + +lemma graphI [intro]: "x \ F \ (x, f x) \ graph F f" + unfolding graph_def by blast + +lemma graphI2 [intro?]: "x \ F \ \t \ graph F f. t = (x, f x)" + unfolding graph_def by blast + +lemma graphE [elim?]: + "(x, y) \ graph F f \ (x \ F \ y = f x \ C) \ C" + unfolding graph_def by blast + + +subsection {* Functions ordered by domain extension *} + +text {* + A function @{text h'} is an extension of @{text h}, iff the graph of + @{text h} is a subset of the graph of @{text h'}. +*} + +lemma graph_extI: + "(\x. x \ H \ h x = h' x) \ H \ H' + \ graph H h \ graph H' h'" + unfolding graph_def by blast + +lemma graph_extD1 [dest?]: + "graph H h \ graph H' h' \ x \ H \ h x = h' x" + unfolding graph_def by blast + +lemma graph_extD2 [dest?]: + "graph H h \ graph H' h' \ H \ H'" + unfolding graph_def by blast + + +subsection {* Domain and function of a graph *} + +text {* + The inverse functions to @{text graph} are @{text domain} and @{text + funct}. +*} + +definition + "domain" :: "'a graph \ 'a set" where + "domain g = {x. \y. (x, y) \ g}" + +definition + funct :: "'a graph \ ('a \ real)" where + "funct g = (\x. (SOME y. (x, y) \ g))" + +text {* + The following lemma states that @{text g} is the graph of a function + if the relation induced by @{text g} is unique. +*} + +lemma graph_domain_funct: + assumes uniq: "\x y z. (x, y) \ g \ (x, z) \ g \ z = y" + shows "graph (domain g) (funct g) = g" + unfolding domain_def funct_def graph_def +proof auto (* FIXME !? *) + fix a b assume g: "(a, b) \ g" + from g show "(a, SOME y. (a, y) \ g) \ g" by (rule someI2) + from g show "\y. (a, y) \ g" .. + from g show "b = (SOME y. (a, y) \ g)" + proof (rule some_equality [symmetric]) + fix y assume "(a, y) \ g" + with g show "y = b" by (rule uniq) + qed +qed + + +subsection {* Norm-preserving extensions of a function *} + +text {* + Given a linear form @{text f} on the space @{text F} and a seminorm + @{text p} on @{text E}. The set of all linear extensions of @{text + f}, to superspaces @{text H} of @{text F}, which are bounded by + @{text p}, is defined as follows. +*} + +definition + norm_pres_extensions :: + "'a::{plus, minus, uminus, zero} set \ ('a \ real) \ 'a set \ ('a \ real) + \ 'a graph set" where + "norm_pres_extensions E p F f + = {g. \H h. g = graph H h + \ linearform H h + \ H \ E + \ F \ H + \ graph F f \ graph H h + \ (\x \ H. h x \ p x)}" + +lemma norm_pres_extensionE [elim]: + "g \ norm_pres_extensions E p F f + \ (\H h. g = graph H h \ linearform H h + \ H \ E \ F \ H \ graph F f \ graph H h + \ \x \ H. h x \ p x \ C) \ C" + unfolding norm_pres_extensions_def by blast + +lemma norm_pres_extensionI2 [intro]: + "linearform H h \ H \ E \ F \ H + \ graph F f \ graph H h \ \x \ H. h x \ p x + \ graph H h \ norm_pres_extensions E p F f" + unfolding norm_pres_extensions_def by blast + +lemma norm_pres_extensionI: (* FIXME ? *) + "\H h. g = graph H h + \ linearform H h + \ H \ E + \ F \ H + \ graph F f \ graph H h + \ (\x \ H. h x \ p x) \ g \ norm_pres_extensions E p F f" + unfolding norm_pres_extensions_def by blast + +end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/Hahn_Banach.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,509 @@ +(* Title: HOL/Hahn_Banach/Hahn_Banach.thy + Author: Gertrud Bauer, TU Munich +*) + +header {* The Hahn-Banach Theorem *} + +theory Hahn_Banach +imports Hahn_Banach_Lemmas +begin + +text {* + We present the proof of two different versions of the Hahn-Banach + Theorem, closely following \cite[\S36]{Heuser:1986}. +*} + +subsection {* The Hahn-Banach Theorem for vector spaces *} + +text {* + \textbf{Hahn-Banach Theorem.} Let @{text F} be a subspace of a real + vector space @{text E}, let @{text p} be a semi-norm on @{text E}, + and @{text f} be a linear form defined on @{text F} such that @{text + f} is bounded by @{text p}, i.e. @{text "\x \ F. f x \ p x"}. Then + @{text f} can be extended to a linear form @{text h} on @{text E} + such that @{text h} is norm-preserving, i.e. @{text h} is also + bounded by @{text p}. + + \bigskip + \textbf{Proof Sketch.} + \begin{enumerate} + + \item Define @{text M} as the set of norm-preserving extensions of + @{text f} to subspaces of @{text E}. The linear forms in @{text M} + are ordered by domain extension. + + \item We show that every non-empty chain in @{text M} has an upper + bound in @{text M}. + + \item With Zorn's Lemma we conclude that there is a maximal function + @{text g} in @{text M}. + + \item The domain @{text H} of @{text g} is the whole space @{text + E}, as shown by classical contradiction: + + \begin{itemize} + + \item Assuming @{text g} is not defined on whole @{text E}, it can + still be extended in a norm-preserving way to a super-space @{text + H'} of @{text H}. + + \item Thus @{text g} can not be maximal. Contradiction! + + \end{itemize} + \end{enumerate} +*} + +theorem Hahn_Banach: + assumes E: "vectorspace E" and "subspace F E" + and "seminorm E p" and "linearform F f" + assumes fp: "\x \ F. f x \ p x" + shows "\h. linearform E h \ (\x \ F. h x = f x) \ (\x \ E. h x \ p x)" + -- {* Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E}, *} + -- {* and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p}, *} + -- {* then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp *} +proof - + interpret vectorspace E by fact + interpret subspace F E by fact + interpret seminorm E p by fact + interpret linearform F f by fact + def M \ "norm_pres_extensions E p F f" + then have M: "M = \" by (simp only:) + from E have F: "vectorspace F" .. + note FE = `F \ E` + { + fix c assume cM: "c \ chain M" and ex: "\x. x \ c" + have "\c \ M" + -- {* Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}: *} + -- {* @{text "\c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\c \ M"}. *} + unfolding M_def + proof (rule norm_pres_extensionI) + let ?H = "domain (\c)" + let ?h = "funct (\c)" + + have a: "graph ?H ?h = \c" + proof (rule graph_domain_funct) + fix x y z assume "(x, y) \ \c" and "(x, z) \ \c" + with M_def cM show "z = y" by (rule sup_definite) + qed + moreover from M cM a have "linearform ?H ?h" + by (rule sup_lf) + moreover from a M cM ex FE E have "?H \ E" + by (rule sup_subE) + moreover from a M cM ex FE have "F \ ?H" + by (rule sup_supF) + moreover from a M cM ex have "graph F f \ graph ?H ?h" + by (rule sup_ext) + moreover from a M cM have "\x \ ?H. ?h x \ p x" + by (rule sup_norm_pres) + ultimately show "\H h. \c = graph H h + \ linearform H h + \ H \ E + \ F \ H + \ graph F f \ graph H h + \ (\x \ H. h x \ p x)" by blast + qed + } + then have "\g \ M. \x \ M. g \ x \ g = x" + -- {* With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp *} + proof (rule Zorn's_Lemma) + -- {* We show that @{text M} is non-empty: *} + show "graph F f \ M" + unfolding M_def + proof (rule norm_pres_extensionI2) + show "linearform F f" by fact + show "F \ E" by fact + from F show "F \ F" by (rule vectorspace.subspace_refl) + show "graph F f \ graph F f" .. + show "\x\F. f x \ p x" by fact + qed + qed + then obtain g where gM: "g \ M" and gx: "\x \ M. g \ x \ g = x" + by blast + from gM obtain H h where + g_rep: "g = graph H h" + and linearform: "linearform H h" + and HE: "H \ E" and FH: "F \ H" + and graphs: "graph F f \ graph H h" + and hp: "\x \ H. h x \ p x" unfolding M_def .. + -- {* @{text g} is a norm-preserving extension of @{text f}, in other words: *} + -- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *} + -- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *} + from HE E have H: "vectorspace H" + by (rule subspace.vectorspace) + + have HE_eq: "H = E" + -- {* We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp *} + proof (rule classical) + assume neq: "H \ E" + -- {* Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended *} + -- {* in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \skp *} + have "\g' \ M. g \ g' \ g \ g'" + proof - + from HE have "H \ E" .. + with neq obtain x' where x'E: "x' \ E" and "x' \ H" by blast + obtain x': "x' \ 0" + proof + show "x' \ 0" + proof + assume "x' = 0" + with H have "x' \ H" by (simp only: vectorspace.zero) + with `x' \ H` show False by contradiction + qed + qed + + def H' \ "H + lin x'" + -- {* Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp *} + have HH': "H \ H'" + proof (unfold H'_def) + from x'E have "vectorspace (lin x')" .. + with H show "H \ H + lin x'" .. + qed + + obtain xi where + xi: "\y \ H. - p (y + x') - h y \ xi + \ xi \ p (y + x') - h y" + -- {* Pick a real number @{text \} that fulfills certain inequations; this will *} + -- {* be used to establish that @{text h'} is a norm-preserving extension of @{text h}. + \label{ex-xi-use}\skp *} + proof - + from H have "\xi. \y \ H. - p (y + x') - h y \ xi + \ xi \ p (y + x') - h y" + proof (rule ex_xi) + fix u v assume u: "u \ H" and v: "v \ H" + with HE have uE: "u \ E" and vE: "v \ E" by auto + from H u v linearform have "h v - h u = h (v - u)" + by (simp add: linearform.diff) + also from hp and H u v have "\ \ p (v - u)" + by (simp only: vectorspace.diff_closed) + also from x'E uE vE have "v - u = x' + - x' + v + - u" + by (simp add: diff_eq1) + also from x'E uE vE have "\ = v + x' + - (u + x')" + by (simp add: add_ac) + also from x'E uE vE have "\ = (v + x') - (u + x')" + by (simp add: diff_eq1) + also from x'E uE vE E have "p \ \ p (v + x') + p (u + x')" + by (simp add: diff_subadditive) + finally have "h v - h u \ p (v + x') + p (u + x')" . + then show "- p (u + x') - h u \ p (v + x') - h v" by simp + qed + then show thesis by (blast intro: that) + qed + + def h' \ "\x. let (y, a) = + SOME (y, a). x = y + a \ x' \ y \ H in h y + a * xi" + -- {* Define the extension @{text h'} of @{text h} to @{text H'} using @{text \}. \skp *} + + have "g \ graph H' h' \ g \ graph H' h'" + -- {* @{text h'} is an extension of @{text h} \dots \skp *} + proof + show "g \ graph H' h'" + proof - + have "graph H h \ graph H' h'" + proof (rule graph_extI) + fix t assume t: "t \ H" + from E HE t have "(SOME (y, a). t = y + a \ x' \ y \ H) = (t, 0)" + using `x' \ H` `x' \ E` `x' \ 0` by (rule decomp_H'_H) + with h'_def show "h t = h' t" by (simp add: Let_def) + next + from HH' show "H \ H'" .. + qed + with g_rep show ?thesis by (simp only:) + qed + + show "g \ graph H' h'" + proof - + have "graph H h \ graph H' h'" + proof + assume eq: "graph H h = graph H' h'" + have "x' \ H'" + unfolding H'_def + proof + from H show "0 \ H" by (rule vectorspace.zero) + from x'E show "x' \ lin x'" by (rule x_lin_x) + from x'E show "x' = 0 + x'" by simp + qed + then have "(x', h' x') \ graph H' h'" .. + with eq have "(x', h' x') \ graph H h" by (simp only:) + then have "x' \ H" .. + with `x' \ H` show False by contradiction + qed + with g_rep show ?thesis by simp + qed + qed + moreover have "graph H' h' \ M" + -- {* and @{text h'} is norm-preserving. \skp *} + proof (unfold M_def) + show "graph H' h' \ norm_pres_extensions E p F f" + proof (rule norm_pres_extensionI2) + show "linearform H' h'" + using h'_def H'_def HE linearform `x' \ H` `x' \ E` `x' \ 0` E + by (rule h'_lf) + show "H' \ E" + unfolding H'_def + proof + show "H \ E" by fact + show "vectorspace E" by fact + from x'E show "lin x' \ E" .. + qed + from H `F \ H` HH' show FH': "F \ H'" + by (rule vectorspace.subspace_trans) + show "graph F f \ graph H' h'" + proof (rule graph_extI) + fix x assume x: "x \ F" + with graphs have "f x = h x" .. + also have "\ = h x + 0 * xi" by simp + also have "\ = (let (y, a) = (x, 0) in h y + a * xi)" + by (simp add: Let_def) + also have "(x, 0) = + (SOME (y, a). x = y + a \ x' \ y \ H)" + using E HE + proof (rule decomp_H'_H [symmetric]) + from FH x show "x \ H" .. + from x' show "x' \ 0" . + show "x' \ H" by fact + show "x' \ E" by fact + qed + also have + "(let (y, a) = (SOME (y, a). x = y + a \ x' \ y \ H) + in h y + a * xi) = h' x" by (simp only: h'_def) + finally show "f x = h' x" . + next + from FH' show "F \ H'" .. + qed + show "\x \ H'. h' x \ p x" + using h'_def H'_def `x' \ H` `x' \ E` `x' \ 0` E HE + `seminorm E p` linearform and hp xi + by (rule h'_norm_pres) + qed + qed + ultimately show ?thesis .. + qed + then have "\ (\x \ M. g \ x \ g = x)" by simp + -- {* So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp *} + with gx show "H = E" by contradiction + qed + + from HE_eq and linearform have "linearform E h" + by (simp only:) + moreover have "\x \ F. h x = f x" + proof + fix x assume "x \ F" + with graphs have "f x = h x" .. + then show "h x = f x" .. + qed + moreover from HE_eq and hp have "\x \ E. h x \ p x" + by (simp only:) + ultimately show ?thesis by blast +qed + + +subsection {* Alternative formulation *} + +text {* + The following alternative formulation of the Hahn-Banach + Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear + form @{text f} and a seminorm @{text p} the following inequations + are equivalent:\footnote{This was shown in lemma @{thm [source] + abs_ineq_iff} (see page \pageref{abs-ineq-iff}).} + \begin{center} + \begin{tabular}{lll} + @{text "\x \ H. \h x\ \ p x"} & and & + @{text "\x \ H. h x \ p x"} \\ + \end{tabular} + \end{center} +*} + +theorem abs_Hahn_Banach: + assumes E: "vectorspace E" and FE: "subspace F E" + and lf: "linearform F f" and sn: "seminorm E p" + assumes fp: "\x \ F. \f x\ \ p x" + shows "\g. linearform E g + \ (\x \ F. g x = f x) + \ (\x \ E. \g x\ \ p x)" +proof - + interpret vectorspace E by fact + interpret subspace F E by fact + interpret linearform F f by fact + interpret seminorm E p by fact + have "\g. linearform E g \ (\x \ F. g x = f x) \ (\x \ E. g x \ p x)" + using E FE sn lf + proof (rule Hahn_Banach) + show "\x \ F. f x \ p x" + using FE E sn lf and fp by (rule abs_ineq_iff [THEN iffD1]) + qed + then obtain g where lg: "linearform E g" and *: "\x \ F. g x = f x" + and **: "\x \ E. g x \ p x" by blast + have "\x \ E. \g x\ \ p x" + using _ E sn lg ** + proof (rule abs_ineq_iff [THEN iffD2]) + show "E \ E" .. + qed + with lg * show ?thesis by blast +qed + + +subsection {* The Hahn-Banach Theorem for normed spaces *} + +text {* + Every continuous linear form @{text f} on a subspace @{text F} of a + norm space @{text E}, can be extended to a continuous linear form + @{text g} on @{text E} such that @{text "\f\ = \g\"}. +*} + +theorem norm_Hahn_Banach: + fixes V and norm ("\_\") + fixes B defines "\V f. B V f \ {0} \ {\f x\ / \x\ | x. x \ 0 \ x \ V}" + fixes fn_norm ("\_\\_" [0, 1000] 999) + defines "\V f. \f\\V \ \(B V f)" + assumes E_norm: "normed_vectorspace E norm" and FE: "subspace F E" + and linearform: "linearform F f" and "continuous F norm f" + shows "\g. linearform E g + \ continuous E norm g + \ (\x \ F. g x = f x) + \ \g\\E = \f\\F" +proof - + interpret normed_vectorspace E norm by fact + interpret normed_vectorspace_with_fn_norm E norm B fn_norm + by (auto simp: B_def fn_norm_def) intro_locales + interpret subspace F E by fact + interpret linearform F f by fact + interpret continuous F norm f by fact + have E: "vectorspace E" by intro_locales + have F: "vectorspace F" by rule intro_locales + have F_norm: "normed_vectorspace F norm" + using FE E_norm by (rule subspace_normed_vs) + have ge_zero: "0 \ \f\\F" + by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero + [OF normed_vectorspace_with_fn_norm.intro, + OF F_norm `continuous F norm f` , folded B_def fn_norm_def]) + txt {* We define a function @{text p} on @{text E} as follows: + @{text "p x = \f\ \ \x\"} *} + def p \ "\x. \f\\F * \x\" + + txt {* @{text p} is a seminorm on @{text E}: *} + have q: "seminorm E p" + proof + fix x y a assume x: "x \ E" and y: "y \ E" + + txt {* @{text p} is positive definite: *} + have "0 \ \f\\F" by (rule ge_zero) + moreover from x have "0 \ \x\" .. + ultimately show "0 \ p x" + by (simp add: p_def zero_le_mult_iff) + + txt {* @{text p} is absolutely homogenous: *} + + show "p (a \ x) = \a\ * p x" + proof - + have "p (a \ x) = \f\\F * \a \ x\" by (simp only: p_def) + also from x have "\a \ x\ = \a\ * \x\" by (rule abs_homogenous) + also have "\f\\F * (\a\ * \x\) = \a\ * (\f\\F * \x\)" by simp + also have "\ = \a\ * p x" by (simp only: p_def) + finally show ?thesis . + qed + + txt {* Furthermore, @{text p} is subadditive: *} + + show "p (x + y) \ p x + p y" + proof - + have "p (x + y) = \f\\F * \x + y\" by (simp only: p_def) + also have a: "0 \ \f\\F" by (rule ge_zero) + from x y have "\x + y\ \ \x\ + \y\" .. + with a have " \f\\F * \x + y\ \ \f\\F * (\x\ + \y\)" + by (simp add: mult_left_mono) + also have "\ = \f\\F * \x\ + \f\\F * \y\" by (simp only: right_distrib) + also have "\ = p x + p y" by (simp only: p_def) + finally show ?thesis . + qed + qed + + txt {* @{text f} is bounded by @{text p}. *} + + have "\x \ F. \f x\ \ p x" + proof + fix x assume "x \ F" + with `continuous F norm f` and linearform + show "\f x\ \ p x" + unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong + [OF normed_vectorspace_with_fn_norm.intro, + OF F_norm, folded B_def fn_norm_def]) + qed + + txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded + by @{text p} we can apply the Hahn-Banach Theorem for real vector + spaces. So @{text f} can be extended in a norm-preserving way to + some function @{text g} on the whole vector space @{text E}. *} + + with E FE linearform q obtain g where + linearformE: "linearform E g" + and a: "\x \ F. g x = f x" + and b: "\x \ E. \g x\ \ p x" + by (rule abs_Hahn_Banach [elim_format]) iprover + + txt {* We furthermore have to show that @{text g} is also continuous: *} + + have g_cont: "continuous E norm g" using linearformE + proof + fix x assume "x \ E" + with b show "\g x\ \ \f\\F * \x\" + by (simp only: p_def) + qed + + txt {* To complete the proof, we show that @{text "\g\ = \f\"}. *} + + have "\g\\E = \f\\F" + proof (rule order_antisym) + txt {* + First we show @{text "\g\ \ \f\"}. The function norm @{text + "\g\"} is defined as the smallest @{text "c \ \"} such that + \begin{center} + \begin{tabular}{l} + @{text "\x \ E. \g x\ \ c \ \x\"} + \end{tabular} + \end{center} + \noindent Furthermore holds + \begin{center} + \begin{tabular}{l} + @{text "\x \ E. \g x\ \ \f\ \ \x\"} + \end{tabular} + \end{center} + *} + + have "\x \ E. \g x\ \ \f\\F * \x\" + proof + fix x assume "x \ E" + with b show "\g x\ \ \f\\F * \x\" + by (simp only: p_def) + qed + from g_cont this ge_zero + show "\g\\E \ \f\\F" + by (rule fn_norm_least [of g, folded B_def fn_norm_def]) + + txt {* The other direction is achieved by a similar argument. *} + + show "\f\\F \ \g\\E" + proof (rule normed_vectorspace_with_fn_norm.fn_norm_least + [OF normed_vectorspace_with_fn_norm.intro, + OF F_norm, folded B_def fn_norm_def]) + show "\x \ F. \f x\ \ \g\\E * \x\" + proof + fix x assume x: "x \ F" + from a x have "g x = f x" .. + then have "\f x\ = \g x\" by (simp only:) + also from g_cont + have "\ \ \g\\E * \x\" + proof (rule fn_norm_le_cong [OF _ linearformE, folded B_def fn_norm_def]) + from FE x show "x \ E" .. + qed + finally show "\f x\ \ \g\\E * \x\" . + qed + show "0 \ \g\\E" + using g_cont + by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def]) + show "continuous F norm f" by fact + qed + qed + with linearformE a g_cont show ?thesis by blast +qed + +end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,280 @@ +(* Title: HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy + Author: Gertrud Bauer, TU Munich +*) + +header {* Extending non-maximal functions *} + +theory Hahn_Banach_Ext_Lemmas +imports Function_Norm +begin + +text {* + In this section the following context is presumed. Let @{text E} be + a real vector space with a seminorm @{text q} on @{text E}. @{text + F} is a subspace of @{text E} and @{text f} a linear function on + @{text F}. We consider a subspace @{text H} of @{text E} that is a + superspace of @{text F} and a linear form @{text h} on @{text + H}. @{text H} is a not equal to @{text E} and @{text "x\<^sub>0"} is + an element in @{text "E - H"}. @{text H} is extended to the direct + sum @{text "H' = H + lin x\<^sub>0"}, so for any @{text "x \ H'"} + the decomposition of @{text "x = y + a \ x"} with @{text "y \ H"} is + unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y + + a \ \"} for a certain @{text \}. + + Subsequently we show some properties of this extension @{text h'} of + @{text h}. + + \medskip This lemma will be used to show the existence of a linear + extension of @{text f} (see page \pageref{ex-xi-use}). It is a + consequence of the completeness of @{text \}. To show + \begin{center} + \begin{tabular}{l} + @{text "\\. \y \ F. a y \ \ \ \ \ b y"} + \end{tabular} + \end{center} + \noindent it suffices to show that + \begin{center} + \begin{tabular}{l} + @{text "\u \ F. \v \ F. a u \ b v"} + \end{tabular} + \end{center} +*} + +lemma ex_xi: + assumes "vectorspace F" + assumes r: "\u v. u \ F \ v \ F \ a u \ b v" + shows "\xi::real. \y \ F. a y \ xi \ xi \ b y" +proof - + interpret vectorspace F by fact + txt {* From the completeness of the reals follows: + The set @{text "S = {a u. u \ F}"} has a supremum, if it is + non-empty and has an upper bound. *} + + let ?S = "{a u | u. u \ F}" + have "\xi. lub ?S xi" + proof (rule real_complete) + have "a 0 \ ?S" by blast + then show "\X. X \ ?S" .. + have "\y \ ?S. y \ b 0" + proof + fix y assume y: "y \ ?S" + then obtain u where u: "u \ F" and y: "y = a u" by blast + from u and zero have "a u \ b 0" by (rule r) + with y show "y \ b 0" by (simp only:) + qed + then show "\u. \y \ ?S. y \ u" .. + qed + then obtain xi where xi: "lub ?S xi" .. + { + fix y assume "y \ F" + then have "a y \ ?S" by blast + with xi have "a y \ xi" by (rule lub.upper) + } moreover { + fix y assume y: "y \ F" + from xi have "xi \ b y" + proof (rule lub.least) + fix au assume "au \ ?S" + then obtain u where u: "u \ F" and au: "au = a u" by blast + from u y have "a u \ b y" by (rule r) + with au show "au \ b y" by (simp only:) + qed + } ultimately show "\xi. \y \ F. a y \ xi \ xi \ b y" by blast +qed + +text {* + \medskip The function @{text h'} is defined as a @{text "h' x = h y + + a \ \"} where @{text "x = y + a \ \"} is a linear extension of + @{text h} to @{text H'}. +*} + +lemma h'_lf: + assumes h'_def: "h' \ \x. let (y, a) = + SOME (y, a). x = y + a \ x0 \ y \ H in h y + a * xi" + and H'_def: "H' \ H + lin x0" + and HE: "H \ E" + assumes "linearform H h" + assumes x0: "x0 \ H" "x0 \ E" "x0 \ 0" + assumes E: "vectorspace E" + shows "linearform H' h'" +proof - + interpret linearform H h by fact + interpret vectorspace E by fact + show ?thesis + proof + note E = `vectorspace E` + have H': "vectorspace H'" + proof (unfold H'_def) + from `x0 \ E` + have "lin x0 \ E" .. + with HE show "vectorspace (H + lin x0)" using E .. + qed + { + fix x1 x2 assume x1: "x1 \ H'" and x2: "x2 \ H'" + show "h' (x1 + x2) = h' x1 + h' x2" + proof - + from H' x1 x2 have "x1 + x2 \ H'" + by (rule vectorspace.add_closed) + with x1 x2 obtain y y1 y2 a a1 a2 where + x1x2: "x1 + x2 = y + a \ x0" and y: "y \ H" + and x1_rep: "x1 = y1 + a1 \ x0" and y1: "y1 \ H" + and x2_rep: "x2 = y2 + a2 \ x0" and y2: "y2 \ H" + unfolding H'_def sum_def lin_def by blast + + have ya: "y1 + y2 = y \ a1 + a2 = a" using E HE _ y x0 + proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *} + from HE y1 y2 show "y1 + y2 \ H" + by (rule subspace.add_closed) + from x0 and HE y y1 y2 + have "x0 \ E" "y \ E" "y1 \ E" "y2 \ E" by auto + with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \ x0 = x1 + x2" + by (simp add: add_ac add_mult_distrib2) + also note x1x2 + finally show "(y1 + y2) + (a1 + a2) \ x0 = y + a \ x0" . + qed + + from h'_def x1x2 E HE y x0 + have "h' (x1 + x2) = h y + a * xi" + by (rule h'_definite) + also have "\ = h (y1 + y2) + (a1 + a2) * xi" + by (simp only: ya) + also from y1 y2 have "h (y1 + y2) = h y1 + h y2" + by simp + also have "\ + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)" + by (simp add: left_distrib) + also from h'_def x1_rep E HE y1 x0 + have "h y1 + a1 * xi = h' x1" + by (rule h'_definite [symmetric]) + also from h'_def x2_rep E HE y2 x0 + have "h y2 + a2 * xi = h' x2" + by (rule h'_definite [symmetric]) + finally show ?thesis . + qed + next + fix x1 c assume x1: "x1 \ H'" + show "h' (c \ x1) = c * (h' x1)" + proof - + from H' x1 have ax1: "c \ x1 \ H'" + by (rule vectorspace.mult_closed) + with x1 obtain y a y1 a1 where + cx1_rep: "c \ x1 = y + a \ x0" and y: "y \ H" + and x1_rep: "x1 = y1 + a1 \ x0" and y1: "y1 \ H" + unfolding H'_def sum_def lin_def by blast + + have ya: "c \ y1 = y \ c * a1 = a" using E HE _ y x0 + proof (rule decomp_H') + from HE y1 show "c \ y1 \ H" + by (rule subspace.mult_closed) + from x0 and HE y y1 + have "x0 \ E" "y \ E" "y1 \ E" by auto + with x1_rep have "c \ y1 + (c * a1) \ x0 = c \ x1" + by (simp add: mult_assoc add_mult_distrib1) + also note cx1_rep + finally show "c \ y1 + (c * a1) \ x0 = y + a \ x0" . + qed + + from h'_def cx1_rep E HE y x0 have "h' (c \ x1) = h y + a * xi" + by (rule h'_definite) + also have "\ = h (c \ y1) + (c * a1) * xi" + by (simp only: ya) + also from y1 have "h (c \ y1) = c * h y1" + by simp + also have "\ + (c * a1) * xi = c * (h y1 + a1 * xi)" + by (simp only: right_distrib) + also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1" + by (rule h'_definite [symmetric]) + finally show ?thesis . + qed + } + qed +qed + +text {* \medskip The linear extension @{text h'} of @{text h} + is bounded by the seminorm @{text p}. *} + +lemma h'_norm_pres: + assumes h'_def: "h' \ \x. let (y, a) = + SOME (y, a). x = y + a \ x0 \ y \ H in h y + a * xi" + and H'_def: "H' \ H + lin x0" + and x0: "x0 \ H" "x0 \ E" "x0 \ 0" + assumes E: "vectorspace E" and HE: "subspace H E" + and "seminorm E p" and "linearform H h" + assumes a: "\y \ H. h y \ p y" + and a': "\y \ H. - p (y + x0) - h y \ xi \ xi \ p (y + x0) - h y" + shows "\x \ H'. h' x \ p x" +proof - + interpret vectorspace E by fact + interpret subspace H E by fact + interpret seminorm E p by fact + interpret linearform H h by fact + show ?thesis + proof + fix x assume x': "x \ H'" + show "h' x \ p x" + proof - + from a' have a1: "\ya \ H. - p (ya + x0) - h ya \ xi" + and a2: "\ya \ H. xi \ p (ya + x0) - h ya" by auto + from x' obtain y a where + x_rep: "x = y + a \ x0" and y: "y \ H" + unfolding H'_def sum_def lin_def by blast + from y have y': "y \ E" .. + from y have ay: "inverse a \ y \ H" by simp + + from h'_def x_rep E HE y x0 have "h' x = h y + a * xi" + by (rule h'_definite) + also have "\ \ p (y + a \ x0)" + proof (rule linorder_cases) + assume z: "a = 0" + then have "h y + a * xi = h y" by simp + also from a y have "\ \ p y" .. + also from x0 y' z have "p y = p (y + a \ x0)" by simp + finally show ?thesis . + next + txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"} + with @{text ya} taken as @{text "y / a"}: *} + assume lz: "a < 0" then have nz: "a \ 0" by simp + from a1 ay + have "- p (inverse a \ y + x0) - h (inverse a \ y) \ xi" .. + with lz have "a * xi \ + a * (- p (inverse a \ y + x0) - h (inverse a \ y))" + by (simp add: mult_left_mono_neg order_less_imp_le) + + also have "\ = + - a * (p (inverse a \ y + x0)) - a * (h (inverse a \ y))" + by (simp add: right_diff_distrib) + also from lz x0 y' have "- a * (p (inverse a \ y + x0)) = + p (a \ (inverse a \ y + x0))" + by (simp add: abs_homogenous) + also from nz x0 y' have "\ = p (y + a \ x0)" + by (simp add: add_mult_distrib1 mult_assoc [symmetric]) + also from nz y have "a * (h (inverse a \ y)) = h y" + by simp + finally have "a * xi \ p (y + a \ x0) - h y" . + then show ?thesis by simp + next + txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"} + with @{text ya} taken as @{text "y / a"}: *} + assume gz: "0 < a" then have nz: "a \ 0" by simp + from a2 ay + have "xi \ p (inverse a \ y + x0) - h (inverse a \ y)" .. + with gz have "a * xi \ + a * (p (inverse a \ y + x0) - h (inverse a \ y))" + by simp + also have "\ = a * p (inverse a \ y + x0) - a * h (inverse a \ y)" + by (simp add: right_diff_distrib) + also from gz x0 y' + have "a * p (inverse a \ y + x0) = p (a \ (inverse a \ y + x0))" + by (simp add: abs_homogenous) + also from nz x0 y' have "\ = p (y + a \ x0)" + by (simp add: add_mult_distrib1 mult_assoc [symmetric]) + also from nz y have "a * h (inverse a \ y) = h y" + by simp + finally have "a * xi \ p (y + a \ x0) - h y" . + then show ?thesis by simp + qed + also from x_rep have "\ = p x" by (simp only:) + finally show ?thesis . + qed + qed +qed + +end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/Hahn_Banach_Lemmas.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Lemmas.thy Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,4 @@ +(*<*) +theory Hahn_Banach_Lemmas imports Hahn_Banach_Sup_Lemmas Hahn_Banach_Ext_Lemmas begin +end +(*>*) \ No newline at end of file diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,445 @@ +(* Title: HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy + Author: Gertrud Bauer, TU Munich +*) + +header {* The supremum w.r.t.~the function order *} + +theory Hahn_Banach_Sup_Lemmas +imports Function_Norm Zorn_Lemma +begin + +text {* + 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 @{text E} be a real vector space with a seminorm + @{text p} on @{text E}. @{text F} is a subspace of @{text E} and + @{text f} a linear form on @{text F}. We consider a chain @{text c} + of norm-preserving extensions of @{text f}, such that @{text "\c = + graph H h"}. We will show some properties about the limit function + @{text h}, i.e.\ the supremum of the chain @{text c}. + + \medskip Let @{text c} be a chain of norm-preserving extensions of + the function @{text f} and let @{text "graph H h"} be the supremum + of @{text c}. Every element in @{text H} is member of one of the + elements of the chain. +*} +lemmas [dest?] = chainD +lemmas chainE2 [elim?] = chainD2 [elim_format, standard] + +lemma some_H'h't: + assumes M: "M = norm_pres_extensions E p F f" + and cM: "c \ chain M" + and u: "graph H h = \c" + and x: "x \ H" + shows "\H' h'. graph H' h' \ c + \ (x, h x) \ graph H' h' + \ linearform H' h' \ H' \ E + \ F \ H' \ graph F f \ graph H' h' + \ (\x \ H'. h' x \ p x)" +proof - + from x have "(x, h x) \ graph H h" .. + also from u have "\ = \c" . + finally obtain g where gc: "g \ c" and gh: "(x, h x) \ g" by blast + + from cM have "c \ M" .. + with gc have "g \ M" .. + also from M have "\ = norm_pres_extensions E p F f" . + finally obtain H' and h' where g: "g = graph H' h'" + and * : "linearform H' h'" "H' \ E" "F \ H'" + "graph F f \ graph H' h'" "\x \ H'. h' x \ p x" .. + + from gc and g have "graph H' h' \ c" by (simp only:) + moreover from gh and g have "(x, h x) \ graph H' h'" by (simp only:) + ultimately show ?thesis using * by blast +qed + +text {* + \medskip Let @{text c} be a chain of norm-preserving extensions of + the function @{text f} and let @{text "graph H h"} be the supremum + of @{text c}. Every element in the domain @{text H} of the supremum + function is member of the domain @{text H'} of some function @{text + h'}, such that @{text h} extends @{text h'}. +*} + +lemma some_H'h': + assumes M: "M = norm_pres_extensions E p F f" + and cM: "c \ chain M" + and u: "graph H h = \c" + and x: "x \ H" + shows "\H' h'. x \ H' \ graph H' h' \ graph H h + \ linearform H' h' \ H' \ E \ F \ H' + \ graph F f \ graph H' h' \ (\x \ H'. h' x \ p x)" +proof - + from M cM u x obtain H' h' where + x_hx: "(x, h x) \ graph H' h'" + and c: "graph H' h' \ c" + and * : "linearform H' h'" "H' \ E" "F \ H'" + "graph F f \ graph H' h'" "\x \ H'. h' x \ p x" + by (rule some_H'h't [elim_format]) blast + from x_hx have "x \ H'" .. + moreover from cM u c have "graph H' h' \ graph H h" + by (simp only: chain_ball_Union_upper) + ultimately show ?thesis using * by blast +qed + +text {* + \medskip Any two elements @{text x} and @{text y} in the domain + @{text H} of the supremum function @{text h} are both in the domain + @{text H'} of some function @{text h'}, such that @{text h} extends + @{text h'}. +*} + +lemma some_H'h'2: + assumes M: "M = norm_pres_extensions E p F f" + and cM: "c \ chain M" + and u: "graph H h = \c" + and x: "x \ H" + and y: "y \ H" + shows "\H' h'. x \ H' \ y \ H' + \ graph H' h' \ graph H h + \ linearform H' h' \ H' \ E \ F \ H' + \ graph F f \ graph H' h' \ (\x \ H'. h' x \ p x)" +proof - + txt {* @{text y} is in the domain @{text H''} of some function @{text h''}, + such that @{text h} extends @{text h''}. *} + + from M cM u and y obtain H' h' where + y_hy: "(y, h y) \ graph H' h'" + and c': "graph H' h' \ c" + and * : + "linearform H' h'" "H' \ E" "F \ H'" + "graph F f \ graph H' h'" "\x \ H'. h' x \ p x" + by (rule some_H'h't [elim_format]) blast + + txt {* @{text x} is in the domain @{text H'} of some function @{text h'}, + such that @{text h} extends @{text h'}. *} + + from M cM u and x obtain H'' h'' where + x_hx: "(x, h x) \ graph H'' h''" + and c'': "graph H'' h'' \ c" + and ** : + "linearform H'' h''" "H'' \ E" "F \ H''" + "graph F f \ graph H'' h''" "\x \ H''. h'' x \ p x" + by (rule some_H'h't [elim_format]) blast + + txt {* Since both @{text h'} and @{text h''} are elements of the chain, + @{text h''} is an extension of @{text h'} or vice versa. Thus both + @{text x} and @{text y} are contained in the greater + one. \label{cases1}*} + + from cM c'' c' have "graph H'' h'' \ graph H' h' \ graph H' h' \ graph H'' h''" + (is "?case1 \ ?case2") .. + then show ?thesis + proof + assume ?case1 + have "(x, h x) \ graph H'' h''" by fact + also have "\ \ graph H' h'" by fact + finally have xh:"(x, h x) \ graph H' h'" . + then have "x \ H'" .. + moreover from y_hy have "y \ H'" .. + moreover from cM u and c' have "graph H' h' \ graph H h" + by (simp only: chain_ball_Union_upper) + ultimately show ?thesis using * by blast + next + assume ?case2 + from x_hx have "x \ H''" .. + moreover { + have "(y, h y) \ graph H' h'" by (rule y_hy) + also have "\ \ graph H'' h''" by fact + finally have "(y, h y) \ graph H'' h''" . + } then have "y \ H''" .. + moreover from cM u and c'' have "graph H'' h'' \ graph H h" + by (simp only: chain_ball_Union_upper) + ultimately show ?thesis using ** by blast + qed +qed + +text {* + \medskip The relation induced by the graph of the supremum of a + chain @{text c} is definite, i.~e.~t is the graph of a function. +*} + +lemma sup_definite: + assumes M_def: "M \ norm_pres_extensions E p F f" + and cM: "c \ chain M" + and xy: "(x, y) \ \c" + and xz: "(x, z) \ \c" + shows "z = y" +proof - + from cM have c: "c \ M" .. + from xy obtain G1 where xy': "(x, y) \ G1" and G1: "G1 \ c" .. + from xz obtain G2 where xz': "(x, z) \ G2" and G2: "G2 \ c" .. + + from G1 c have "G1 \ M" .. + then obtain H1 h1 where G1_rep: "G1 = graph H1 h1" + unfolding M_def by blast + + from G2 c have "G2 \ M" .. + then obtain H2 h2 where G2_rep: "G2 = graph H2 h2" + unfolding M_def by blast + + txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"} + or vice versa, since both @{text "G\<^sub>1"} and @{text + "G\<^sub>2"} are members of @{text c}. \label{cases2}*} + + from cM G1 G2 have "G1 \ G2 \ G2 \ G1" (is "?case1 \ ?case2") .. + then show ?thesis + proof + assume ?case1 + with xy' G2_rep have "(x, y) \ graph H2 h2" by blast + then have "y = h2 x" .. + also + from xz' G2_rep have "(x, z) \ graph H2 h2" by (simp only:) + then have "z = h2 x" .. + finally show ?thesis . + next + assume ?case2 + with xz' G1_rep have "(x, z) \ graph H1 h1" by blast + then have "z = h1 x" .. + also + from xy' G1_rep have "(x, y) \ graph H1 h1" by (simp only:) + then have "y = h1 x" .. + finally show ?thesis .. + qed +qed + +text {* + \medskip The limit function @{text h} is linear. Every element + @{text x} in the domain of @{text h} is in the domain of a function + @{text h'} in the chain of norm preserving extensions. Furthermore, + @{text h} is an extension of @{text h'} so the function values of + @{text x} are identical for @{text h'} and @{text h}. Finally, the + function @{text h'} is linear by construction of @{text M}. +*} + +lemma sup_lf: + assumes M: "M = norm_pres_extensions E p F f" + and cM: "c \ chain M" + and u: "graph H h = \c" + shows "linearform H h" +proof + fix x y assume x: "x \ H" and y: "y \ H" + with M cM u obtain H' h' where + x': "x \ H'" and y': "y \ H'" + and b: "graph H' h' \ graph H h" + and linearform: "linearform H' h'" + and subspace: "H' \ E" + by (rule some_H'h'2 [elim_format]) blast + + show "h (x + y) = h x + h y" + proof - + from linearform x' y' have "h' (x + y) = h' x + h' y" + by (rule linearform.add) + also from b x' have "h' x = h x" .. + also from b y' have "h' y = h y" .. + also from subspace x' y' have "x + y \ H'" + by (rule subspace.add_closed) + with b have "h' (x + y) = h (x + y)" .. + finally show ?thesis . + qed +next + fix x a assume x: "x \ H" + with M cM u obtain H' h' where + x': "x \ H'" + and b: "graph H' h' \ graph H h" + and linearform: "linearform H' h'" + and subspace: "H' \ E" + by (rule some_H'h' [elim_format]) blast + + show "h (a \ x) = a * h x" + proof - + from linearform x' have "h' (a \ x) = a * h' x" + by (rule linearform.mult) + also from b x' have "h' x = h x" .. + also from subspace x' have "a \ x \ H'" + by (rule subspace.mult_closed) + with b have "h' (a \ x) = h (a \ x)" .. + finally show ?thesis . + qed +qed + +text {* + \medskip The limit of a non-empty chain of norm preserving + extensions of @{text f} is an extension of @{text f}, since every + element of the chain is an extension of @{text f} and the supremum + is an extension for every element of the chain. +*} + +lemma sup_ext: + assumes graph: "graph H h = \c" + and M: "M = norm_pres_extensions E p F f" + and cM: "c \ chain M" + and ex: "\x. x \ c" + shows "graph F f \ graph H h" +proof - + from ex obtain x where xc: "x \ c" .. + from cM have "c \ M" .. + with xc have "x \ M" .. + with M have "x \ norm_pres_extensions E p F f" + by (simp only:) + then obtain G g where "x = graph G g" and "graph F f \ graph G g" .. + then have "graph F f \ x" by (simp only:) + also from xc have "\ \ \c" by blast + also from graph have "\ = graph H h" .. + finally show ?thesis . +qed + +text {* + \medskip The domain @{text H} of the limit function is a superspace + of @{text F}, since @{text F} is a subset of @{text H}. The + existence of the @{text 0} element in @{text F} and the closure + properties follow from the fact that @{text F} is a vector space. +*} + +lemma sup_supF: + assumes graph: "graph H h = \c" + and M: "M = norm_pres_extensions E p F f" + and cM: "c \ chain M" + and ex: "\x. x \ c" + and FE: "F \ E" + shows "F \ H" +proof + from FE show "F \ {}" by (rule subspace.non_empty) + from graph M cM ex have "graph F f \ graph H h" by (rule sup_ext) + then show "F \ H" .. + fix x y assume "x \ F" and "y \ F" + with FE show "x + y \ F" by (rule subspace.add_closed) +next + fix x a assume "x \ F" + with FE show "a \ x \ F" by (rule subspace.mult_closed) +qed + +text {* + \medskip The domain @{text H} of the limit function is a subspace of + @{text E}. +*} + +lemma sup_subE: + assumes graph: "graph H h = \c" + and M: "M = norm_pres_extensions E p F f" + and cM: "c \ chain M" + and ex: "\x. x \ c" + and FE: "F \ E" + and E: "vectorspace E" + shows "H \ E" +proof + show "H \ {}" + proof - + from FE E have "0 \ F" by (rule subspace.zero) + also from graph M cM ex FE have "F \ H" by (rule sup_supF) + then have "F \ H" .. + finally show ?thesis by blast + qed + show "H \ E" + proof + fix x assume "x \ H" + with M cM graph + obtain H' h' where x: "x \ H'" and H'E: "H' \ E" + by (rule some_H'h' [elim_format]) blast + from H'E have "H' \ E" .. + with x show "x \ E" .. + qed + fix x y assume x: "x \ H" and y: "y \ H" + show "x + y \ H" + proof - + from M cM graph x y obtain H' h' where + x': "x \ H'" and y': "y \ H'" and H'E: "H' \ E" + and graphs: "graph H' h' \ graph H h" + by (rule some_H'h'2 [elim_format]) blast + from H'E x' y' have "x + y \ H'" + by (rule subspace.add_closed) + also from graphs have "H' \ H" .. + finally show ?thesis . + qed +next + fix x a assume x: "x \ H" + show "a \ x \ H" + proof - + from M cM graph x + obtain H' h' where x': "x \ H'" and H'E: "H' \ E" + and graphs: "graph H' h' \ graph H h" + by (rule some_H'h' [elim_format]) blast + from H'E x' have "a \ x \ H'" by (rule subspace.mult_closed) + also from graphs have "H' \ H" .. + finally show ?thesis . + qed +qed + +text {* + \medskip The limit function is bounded by the norm @{text p} as + well, since all elements in the chain are bounded by @{text p}. +*} + +lemma sup_norm_pres: + assumes graph: "graph H h = \c" + and M: "M = norm_pres_extensions E p F f" + and cM: "c \ chain M" + shows "\x \ H. h x \ p x" +proof + fix x assume "x \ H" + with M cM graph obtain H' h' where x': "x \ H'" + and graphs: "graph H' h' \ graph H h" + and a: "\x \ H'. h' x \ p x" + by (rule some_H'h' [elim_format]) blast + from graphs x' have [symmetric]: "h' x = h x" .. + also from a x' have "h' x \ p x " .. + finally show "h x \ p x" . +qed + +text {* + \medskip The following lemma is a property of linear forms on real + vector spaces. It will be used for the lemma @{text abs_Hahn_Banach} + (see page \pageref{abs-Hahn_Banach}). \label{abs-ineq-iff} For real + vector spaces the following inequations are equivalent: + \begin{center} + \begin{tabular}{lll} + @{text "\x \ H. \h x\ \ p x"} & and & + @{text "\x \ H. h x \ p x"} \\ + \end{tabular} + \end{center} +*} + +lemma abs_ineq_iff: + assumes "subspace H E" and "vectorspace E" and "seminorm E p" + and "linearform H h" + shows "(\x \ H. \h x\ \ p x) = (\x \ H. h x \ p x)" (is "?L = ?R") +proof + interpret subspace H E by fact + interpret vectorspace E by fact + interpret seminorm E p by fact + interpret linearform H h by fact + have H: "vectorspace H" using `vectorspace E` .. + { + assume l: ?L + show ?R + proof + fix x assume x: "x \ H" + have "h x \ \h x\" by arith + also from l x have "\ \ p x" .. + finally show "h x \ p x" . + qed + next + assume r: ?R + show ?L + proof + fix x assume x: "x \ H" + show "\a b :: real. - a \ b \ b \ a \ \b\ \ a" + by arith + from `linearform H h` and H x + have "- h x = h (- x)" by (rule linearform.neg [symmetric]) + also + from H x have "- x \ H" by (rule vectorspace.neg_closed) + with r have "h (- x) \ p (- x)" .. + also have "\ = p x" + using `seminorm E p` `vectorspace E` + proof (rule seminorm.minus) + from x show "x \ E" .. + qed + finally have "- h x \ p x" . + then show "- p x \ h x" by simp + from r x show "h x \ p x" .. + qed + } +qed + +end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/Linearform.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/Linearform.thy Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,60 @@ +(* Title: HOL/Hahn_Banach/Linearform.thy + Author: Gertrud Bauer, TU Munich +*) + +header {* Linearforms *} + +theory Linearform +imports Vector_Space +begin + +text {* + A \emph{linear form} is a function on a vector space into the reals + that is additive and multiplicative. +*} + +locale linearform = + fixes V :: "'a\{minus, plus, zero, uminus} set" and f + assumes add [iff]: "x \ V \ y \ V \ f (x + y) = f x + f y" + and mult [iff]: "x \ V \ f (a \ x) = a * f x" + +declare linearform.intro [intro?] + +lemma (in linearform) neg [iff]: + assumes "vectorspace V" + shows "x \ V \ f (- x) = - f x" +proof - + interpret vectorspace V by fact + assume x: "x \ V" + then have "f (- x) = f ((- 1) \ x)" by (simp add: negate_eq1) + also from x have "\ = (- 1) * (f x)" by (rule mult) + also from x have "\ = - (f x)" by simp + finally show ?thesis . +qed + +lemma (in linearform) diff [iff]: + assumes "vectorspace V" + shows "x \ V \ y \ V \ f (x - y) = f x - f y" +proof - + interpret vectorspace V by fact + assume x: "x \ V" and y: "y \ V" + then have "x - y = x + - y" by (rule diff_eq1) + also have "f \ = f x + f (- y)" by (rule add) (simp_all add: x y) + also have "f (- y) = - f y" using `vectorspace V` y by (rule neg) + finally show ?thesis by simp +qed + +text {* Every linear form yields @{text 0} for the @{text 0} vector. *} + +lemma (in linearform) zero [iff]: + assumes "vectorspace V" + shows "f 0 = 0" +proof - + interpret vectorspace V by fact + have "f 0 = f (0 - 0)" by simp + also have "\ = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all + also have "\ = 0" by simp + finally show ?thesis . +qed + +end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/Normed_Space.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,117 @@ +(* Title: HOL/Hahn_Banach/Normed_Space.thy + Author: Gertrud Bauer, TU Munich +*) + +header {* Normed vector spaces *} + +theory Normed_Space +imports Subspace +begin + +subsection {* Quasinorms *} + +text {* + A \emph{seminorm} @{text "\\\"} is a function on a real vector space + into the reals that has the following properties: it is positive + definite, absolute homogenous and subadditive. +*} + +locale norm_syntax = + fixes norm :: "'a \ real" ("\_\") + +locale seminorm = var_V + norm_syntax + + constrains V :: "'a\{minus, plus, zero, uminus} set" + assumes ge_zero [iff?]: "x \ V \ 0 \ \x\" + and abs_homogenous [iff?]: "x \ V \ \a \ x\ = \a\ * \x\" + and subadditive [iff?]: "x \ V \ y \ V \ \x + y\ \ \x\ + \y\" + +declare seminorm.intro [intro?] + +lemma (in seminorm) diff_subadditive: + assumes "vectorspace V" + shows "x \ V \ y \ V \ \x - y\ \ \x\ + \y\" +proof - + interpret vectorspace V by fact + assume x: "x \ V" and y: "y \ V" + then have "x - y = x + - 1 \ y" + by (simp add: diff_eq2 negate_eq2a) + also from x y have "\\\ \ \x\ + \- 1 \ y\" + by (simp add: subadditive) + also from y have "\- 1 \ y\ = \- 1\ * \y\" + by (rule abs_homogenous) + also have "\ = \y\" by simp + finally show ?thesis . +qed + +lemma (in seminorm) minus: + assumes "vectorspace V" + shows "x \ V \ \- x\ = \x\" +proof - + interpret vectorspace V by fact + assume x: "x \ V" + then have "- x = - 1 \ x" by (simp only: negate_eq1) + also from x have "\\\ = \- 1\ * \x\" + by (rule abs_homogenous) + also have "\ = \x\" by simp + finally show ?thesis . +qed + + +subsection {* Norms *} + +text {* + A \emph{norm} @{text "\\\"} is a seminorm that maps only the + @{text 0} vector to @{text 0}. +*} + +locale norm = seminorm + + assumes zero_iff [iff]: "x \ V \ (\x\ = 0) = (x = 0)" + + +subsection {* Normed vector spaces *} + +text {* + A vector space together with a norm is called a \emph{normed + space}. +*} + +locale normed_vectorspace = vectorspace + norm + +declare normed_vectorspace.intro [intro?] + +lemma (in normed_vectorspace) gt_zero [intro?]: + "x \ V \ x \ 0 \ 0 < \x\" +proof - + assume x: "x \ V" and neq: "x \ 0" + from x have "0 \ \x\" .. + also have [symmetric]: "\ \ 0" + proof + assume "\x\ = 0" + with x have "x = 0" by simp + with neq show False by contradiction + qed + finally show ?thesis . +qed + +text {* + Any subspace of a normed vector space is again a normed vectorspace. +*} + +lemma subspace_normed_vs [intro?]: + fixes F E norm + assumes "subspace F E" "normed_vectorspace E norm" + shows "normed_vectorspace F norm" +proof - + interpret subspace F E by fact + interpret normed_vectorspace E norm by fact + show ?thesis + proof + show "vectorspace F" by (rule vectorspace) unfold_locales + next + have "Normed_Space.norm E norm" .. + with subset show "Normed_Space.norm F norm" + by (simp add: norm_def seminorm_def norm_axioms_def) + qed +qed + +end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/README.html Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,38 @@ + + + + + + + + + HOL/Hahn_Banach/README + + + + +

The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)

+ +Author: Gertrud Bauer, Technische Universität München

+ +This directory contains the proof of the Hahn-Banach theorem for real vectorspaces, +following H. Heuser, Funktionalanalysis, p. 228 -232. +The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis. +It is a conclusion of Zorn's lemma.

+ +Two different formaulations of the theorem are presented, one for general real vectorspaces +and its application to normed vectorspaces.

+ +The theorem says, that every continous linearform, defined on arbitrary subspaces +(not only one-dimensional subspaces), can be extended to a continous linearform on +the whole vectorspace. + + +


+ +
+bauerg@in.tum.de +
+ + + diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/ROOT.ML Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,7 @@ +(* Title: HOL/Hahn_Banach/ROOT.ML + Author: Gertrud Bauer, TU Munich + +The Hahn-Banach theorem for real vector spaces (Isabelle/Isar). +*) + +use_thy "Hahn_Banach"; diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/Subspace.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/Subspace.thy Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,513 @@ +(* Title: HOL/Hahn_Banach/Subspace.thy + Author: Gertrud Bauer, TU Munich +*) + +header {* Subspaces *} + +theory Subspace +imports Vector_Space +begin + +subsection {* Definition *} + +text {* + A non-empty subset @{text U} of a vector space @{text V} is a + \emph{subspace} of @{text V}, iff @{text U} is closed under addition + and scalar multiplication. +*} + +locale subspace = + fixes U :: "'a\{minus, plus, zero, uminus} set" and V + assumes non_empty [iff, intro]: "U \ {}" + and subset [iff]: "U \ V" + and add_closed [iff]: "x \ U \ y \ U \ x + y \ U" + and mult_closed [iff]: "x \ U \ a \ x \ U" + +notation (symbols) + subspace (infix "\" 50) + +declare vectorspace.intro [intro?] subspace.intro [intro?] + +lemma subspace_subset [elim]: "U \ V \ U \ V" + by (rule subspace.subset) + +lemma (in subspace) subsetD [iff]: "x \ U \ x \ V" + using subset by blast + +lemma subspaceD [elim]: "U \ V \ x \ U \ x \ V" + by (rule subspace.subsetD) + +lemma rev_subspaceD [elim?]: "x \ U \ U \ V \ x \ V" + by (rule subspace.subsetD) + +lemma (in subspace) diff_closed [iff]: + assumes "vectorspace V" + assumes x: "x \ U" and y: "y \ U" + shows "x - y \ U" +proof - + interpret vectorspace V by fact + from x y show ?thesis by (simp add: diff_eq1 negate_eq1) +qed + +text {* + \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. +*} + +lemma (in subspace) zero [intro]: + assumes "vectorspace V" + shows "0 \ U" +proof - + interpret V: vectorspace V by fact + have "U \ {}" by (rule non_empty) + then obtain x where x: "x \ U" by blast + then have "x \ V" .. then have "0 = x - x" by simp + also from `vectorspace V` x x have "\ \ U" by (rule diff_closed) + finally show ?thesis . +qed + +lemma (in subspace) neg_closed [iff]: + assumes "vectorspace V" + assumes x: "x \ U" + shows "- x \ U" +proof - + interpret vectorspace V by fact + from x show ?thesis by (simp add: negate_eq1) +qed + +text {* \medskip Further derived laws: every subspace is a vector space. *} + +lemma (in subspace) vectorspace [iff]: + assumes "vectorspace V" + shows "vectorspace U" +proof - + interpret vectorspace V by fact + show ?thesis + proof + show "U \ {}" .. + fix x y z assume x: "x \ U" and y: "y \ U" and z: "z \ U" + fix a b :: real + from x y show "x + y \ U" by simp + from x show "a \ x \ U" by simp + from x y z show "(x + y) + z = x + (y + z)" by (simp add: add_ac) + from x y show "x + y = y + x" by (simp add: add_ac) + from x show "x - x = 0" by simp + from x show "0 + x = x" by simp + from x y show "a \ (x + y) = a \ x + a \ y" by (simp add: distrib) + from x show "(a + b) \ x = a \ x + b \ x" by (simp add: distrib) + from x show "(a * b) \ x = a \ b \ x" by (simp add: mult_assoc) + from x show "1 \ x = x" by simp + from x show "- x = - 1 \ x" by (simp add: negate_eq1) + from x y show "x - y = x + - y" by (simp add: diff_eq1) + qed +qed + + +text {* The subspace relation is reflexive. *} + +lemma (in vectorspace) subspace_refl [intro]: "V \ V" +proof + show "V \ {}" .. + show "V \ V" .. + fix x y assume x: "x \ V" and y: "y \ V" + fix a :: real + from x y show "x + y \ V" by simp + from x show "a \ x \ V" by simp +qed + +text {* The subspace relation is transitive. *} + +lemma (in vectorspace) subspace_trans [trans]: + "U \ V \ V \ W \ U \ W" +proof + assume uv: "U \ V" and vw: "V \ W" + from uv show "U \ {}" by (rule subspace.non_empty) + show "U \ W" + proof - + from uv have "U \ V" by (rule subspace.subset) + also from vw have "V \ W" by (rule subspace.subset) + finally show ?thesis . + qed + fix x y assume x: "x \ U" and y: "y \ U" + from uv and x y show "x + y \ U" by (rule subspace.add_closed) + from uv and x show "\a. a \ x \ U" by (rule subspace.mult_closed) +qed + + +subsection {* Linear closure *} + +text {* + The \emph{linear closure} of a vector @{text x} is the set of all + scalar multiples of @{text x}. +*} + +definition + lin :: "('a::{minus, plus, zero}) \ 'a set" where + "lin x = {a \ x | a. True}" + +lemma linI [intro]: "y = a \ x \ y \ lin x" + unfolding lin_def by blast + +lemma linI' [iff]: "a \ x \ lin x" + unfolding lin_def by blast + +lemma linE [elim]: "x \ lin v \ (\a::real. x = a \ v \ C) \ C" + unfolding lin_def by blast + + +text {* Every vector is contained in its linear closure. *} + +lemma (in vectorspace) x_lin_x [iff]: "x \ V \ x \ lin x" +proof - + assume "x \ V" + then have "x = 1 \ x" by simp + also have "\ \ lin x" .. + finally show ?thesis . +qed + +lemma (in vectorspace) "0_lin_x" [iff]: "x \ V \ 0 \ lin x" +proof + assume "x \ V" + then show "0 = 0 \ x" by simp +qed + +text {* Any linear closure is a subspace. *} + +lemma (in vectorspace) lin_subspace [intro]: + "x \ V \ lin x \ V" +proof + assume x: "x \ V" + then show "lin x \ {}" by (auto simp add: x_lin_x) + show "lin x \ V" + proof + fix x' assume "x' \ lin x" + then obtain a where "x' = a \ x" .. + with x show "x' \ V" by simp + qed + fix x' x'' assume x': "x' \ lin x" and x'': "x'' \ lin x" + show "x' + x'' \ lin x" + proof - + from x' obtain a' where "x' = a' \ x" .. + moreover from x'' obtain a'' where "x'' = a'' \ x" .. + ultimately have "x' + x'' = (a' + a'') \ x" + using x by (simp add: distrib) + also have "\ \ lin x" .. + finally show ?thesis . + qed + fix a :: real + show "a \ x' \ lin x" + proof - + from x' obtain a' where "x' = a' \ x" .. + with x have "a \ x' = (a * a') \ x" by (simp add: mult_assoc) + also have "\ \ lin x" .. + finally show ?thesis . + qed +qed + + +text {* Any linear closure is a vector space. *} + +lemma (in vectorspace) lin_vectorspace [intro]: + assumes "x \ V" + shows "vectorspace (lin x)" +proof - + from `x \ V` have "subspace (lin x) V" + by (rule lin_subspace) + from this and vectorspace_axioms show ?thesis + by (rule subspace.vectorspace) +qed + + +subsection {* Sum of two vectorspaces *} + +text {* + The \emph{sum} of two vectorspaces @{text U} and @{text V} is the + set of all sums of elements from @{text U} and @{text V}. +*} + +instantiation "fun" :: (type, type) plus +begin + +definition + sum_def: "plus_fun U V = {u + v | u v. u \ U \ v \ V}" (* FIXME not fully general!? *) + +instance .. + +end + +lemma sumE [elim]: + "x \ U + V \ (\u v. x = u + v \ u \ U \ v \ V \ C) \ C" + unfolding sum_def by blast + +lemma sumI [intro]: + "u \ U \ v \ V \ x = u + v \ x \ U + V" + unfolding sum_def by blast + +lemma sumI' [intro]: + "u \ U \ v \ V \ u + v \ U + V" + unfolding sum_def by blast + +text {* @{text U} is a subspace of @{text "U + V"}. *} + +lemma subspace_sum1 [iff]: + assumes "vectorspace U" "vectorspace V" + shows "U \ U + V" +proof - + interpret vectorspace U by fact + interpret vectorspace V by fact + show ?thesis + proof + show "U \ {}" .. + show "U \ U + V" + proof + fix x assume x: "x \ U" + moreover have "0 \ V" .. + ultimately have "x + 0 \ U + V" .. + with x show "x \ U + V" by simp + qed + fix x y assume x: "x \ U" and "y \ U" + then show "x + y \ U" by simp + from x show "\a. a \ x \ U" by simp + qed +qed + +text {* The sum of two subspaces is again a subspace. *} + +lemma sum_subspace [intro?]: + assumes "subspace U E" "vectorspace E" "subspace V E" + shows "U + V \ E" +proof - + interpret subspace U E by fact + interpret vectorspace E by fact + interpret subspace V E by fact + show ?thesis + proof + have "0 \ U + V" + proof + show "0 \ U" using `vectorspace E` .. + show "0 \ V" using `vectorspace E` .. + show "(0::'a) = 0 + 0" by simp + qed + then show "U + V \ {}" by blast + show "U + V \ E" + proof + fix x assume "x \ U + V" + then obtain u v where "x = u + v" and + "u \ U" and "v \ V" .. + then show "x \ E" by simp + qed + fix x y assume x: "x \ U + V" and y: "y \ U + V" + show "x + y \ U + V" + proof - + from x obtain ux vx where "x = ux + vx" and "ux \ U" and "vx \ V" .. + moreover + from y obtain uy vy where "y = uy + vy" and "uy \ U" and "vy \ V" .. + ultimately + have "ux + uy \ U" + and "vx + vy \ V" + and "x + y = (ux + uy) + (vx + vy)" + using x y by (simp_all add: add_ac) + then show ?thesis .. + qed + fix a show "a \ x \ U + V" + proof - + from x obtain u v where "x = u + v" and "u \ U" and "v \ V" .. + then have "a \ u \ U" and "a \ v \ V" + and "a \ x = (a \ u) + (a \ v)" by (simp_all add: distrib) + then show ?thesis .. + qed + qed +qed + +text{* The sum of two subspaces is a vectorspace. *} + +lemma sum_vs [intro?]: + "U \ E \ V \ E \ vectorspace E \ vectorspace (U + V)" + by (rule subspace.vectorspace) (rule sum_subspace) + + +subsection {* Direct sums *} + +text {* + The sum of @{text U} and @{text V} is called \emph{direct}, iff the + zero element is the only common element of @{text U} and @{text + V}. For every element @{text x} of the direct sum of @{text U} and + @{text V} the decomposition in @{text "x = u + v"} with + @{text "u \ U"} and @{text "v \ V"} is unique. +*} + +lemma decomp: + assumes "vectorspace E" "subspace U E" "subspace V E" + assumes direct: "U \ V = {0}" + and u1: "u1 \ U" and u2: "u2 \ U" + and v1: "v1 \ V" and v2: "v2 \ V" + and sum: "u1 + v1 = u2 + v2" + shows "u1 = u2 \ v1 = v2" +proof - + interpret vectorspace E by fact + interpret subspace U E by fact + interpret subspace V E by fact + show ?thesis + proof + have U: "vectorspace U" (* FIXME: use interpret *) + using `subspace U E` `vectorspace E` by (rule subspace.vectorspace) + have V: "vectorspace V" + using `subspace V E` `vectorspace E` by (rule subspace.vectorspace) + from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1" + by (simp add: add_diff_swap) + from u1 u2 have u: "u1 - u2 \ U" + by (rule vectorspace.diff_closed [OF U]) + with eq have v': "v2 - v1 \ U" by (simp only:) + from v2 v1 have v: "v2 - v1 \ V" + by (rule vectorspace.diff_closed [OF V]) + with eq have u': " u1 - u2 \ V" by (simp only:) + + show "u1 = u2" + proof (rule add_minus_eq) + from u1 show "u1 \ E" .. + from u2 show "u2 \ E" .. + from u u' and direct show "u1 - u2 = 0" by blast + qed + show "v1 = v2" + proof (rule add_minus_eq [symmetric]) + from v1 show "v1 \ E" .. + from v2 show "v2 \ E" .. + from v v' and direct show "v2 - v1 = 0" by blast + qed + qed +qed + +text {* + 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 @{text "y + a \ x\<^sub>0"} of the direct sum of a + vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"} + the components @{text "y \ H"} and @{text a} are uniquely + determined. +*} + +lemma decomp_H': + assumes "vectorspace E" "subspace H E" + assumes y1: "y1 \ H" and y2: "y2 \ H" + and x': "x' \ H" "x' \ E" "x' \ 0" + and eq: "y1 + a1 \ x' = y2 + a2 \ x'" + shows "y1 = y2 \ a1 = a2" +proof - + interpret vectorspace E by fact + interpret subspace H E by fact + show ?thesis + proof + have c: "y1 = y2 \ a1 \ x' = a2 \ x'" + proof (rule decomp) + show "a1 \ x' \ lin x'" .. + show "a2 \ x' \ lin x'" .. + show "H \ lin x' = {0}" + proof + show "H \ lin x' \ {0}" + proof + fix x assume x: "x \ H \ lin x'" + then obtain a where xx': "x = a \ x'" + by blast + have "x = 0" + proof cases + assume "a = 0" + with xx' and x' show ?thesis by simp + next + assume a: "a \ 0" + from x have "x \ H" .. + with xx' have "inverse a \ a \ x' \ H" by simp + with a and x' have "x' \ H" by (simp add: mult_assoc2) + with `x' \ H` show ?thesis by contradiction + qed + then show "x \ {0}" .. + qed + show "{0} \ H \ lin x'" + proof - + have "0 \ H" using `vectorspace E` .. + moreover have "0 \ lin x'" using `x' \ E` .. + ultimately show ?thesis by blast + qed + qed + show "lin x' \ E" using `x' \ E` .. + qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq) + then show "y1 = y2" .. + from c have "a1 \ x' = a2 \ x'" .. + with x' show "a1 = a2" by (simp add: mult_right_cancel) + qed +qed + +text {* + Since for any element @{text "y + a \ x'"} of the direct sum of a + vectorspace @{text H} and the linear closure of @{text x'} the + components @{text "y \ H"} and @{text a} are unique, it follows from + @{text "y \ H"} that @{text "a = 0"}. +*} + +lemma decomp_H'_H: + assumes "vectorspace E" "subspace H E" + assumes t: "t \ H" + and x': "x' \ H" "x' \ E" "x' \ 0" + shows "(SOME (y, a). t = y + a \ x' \ y \ H) = (t, 0)" +proof - + interpret vectorspace E by fact + interpret subspace H E by fact + show ?thesis + proof (rule, simp_all only: split_paired_all split_conv) + from t x' show "t = t + 0 \ x' \ t \ H" by simp + fix y and a assume ya: "t = y + a \ x' \ y \ H" + have "y = t \ a = 0" + proof (rule decomp_H') + from ya x' show "y + a \ x' = t + 0 \ x'" by simp + from ya show "y \ H" .. + qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+) + with t x' show "(y, a) = (y + a \ x', 0)" by simp + qed +qed + +text {* + The components @{text "y \ H"} and @{text a} in @{text "y + a \ x'"} + are unique, so the function @{text h'} defined by + @{text "h' (y + a \ x') = h y + a \ \"} is definite. +*} + +lemma h'_definite: + fixes H + assumes h'_def: + "h' \ (\x. let (y, a) = SOME (y, a). (x = y + a \ x' \ y \ H) + in (h y) + a * xi)" + and x: "x = y + a \ x'" + assumes "vectorspace E" "subspace H E" + assumes y: "y \ H" + and x': "x' \ H" "x' \ E" "x' \ 0" + shows "h' x = h y + a * xi" +proof - + interpret vectorspace E by fact + interpret subspace H E by fact + from x y x' have "x \ H + lin x'" by auto + have "\!p. (\(y, a). x = y + a \ x' \ y \ H) p" (is "\!p. ?P p") + proof (rule ex_ex1I) + from x y show "\p. ?P p" by blast + fix p q assume p: "?P p" and q: "?P q" + show "p = q" + proof - + from p have xp: "x = fst p + snd p \ x' \ fst p \ H" + by (cases p) simp + from q have xq: "x = fst q + snd q \ x' \ fst q \ H" + by (cases q) simp + have "fst p = fst q \ snd p = snd q" + proof (rule decomp_H') + from xp show "fst p \ H" .. + from xq show "fst q \ H" .. + from xp and xq show "fst p + snd p \ x' = fst q + snd q \ x'" + by simp + qed (rule `vectorspace E`, rule `subspace H E`, (rule x')+) + then show ?thesis by (cases p, cases q) simp + qed + qed + then have eq: "(SOME (y, a). x = y + a \ x' \ y \ H) = (y, a)" + by (rule some1_equality) (simp add: x y) + with h'_def show "h' x = h y + a * xi" by (simp add: Let_def) +qed + +end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/Vector_Space.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,418 @@ +(* Title: HOL/Hahn_Banach/Vector_Space.thy + Author: Gertrud Bauer, TU Munich +*) + +header {* Vector spaces *} + +theory Vector_Space +imports Real Bounds Zorn +begin + +subsection {* Signature *} + +text {* + For the definition of real vector spaces a type @{typ 'a} of the + sort @{text "{plus, minus, zero}"} is considered, on which a real + scalar multiplication @{text \} is declared. +*} + +consts + prod :: "real \ 'a::{plus, minus, zero} \ 'a" (infixr "'(*')" 70) + +notation (xsymbols) + prod (infixr "\" 70) +notation (HTML output) + prod (infixr "\" 70) + + +subsection {* Vector space laws *} + +text {* + A \emph{vector space} is a non-empty set @{text V} of elements from + @{typ 'a} with the following vector space laws: The set @{text V} is + closed under addition and scalar multiplication, addition is + associative and commutative; @{text "- x"} is the inverse of @{text + x} w.~r.~t.~addition and @{text 0} is the neutral element of + addition. Addition and multiplication are distributive; scalar + multiplication is associative and the real number @{text "1"} is + the neutral element of scalar multiplication. +*} + +locale var_V = fixes V + +locale vectorspace = var_V + + assumes non_empty [iff, intro?]: "V \ {}" + and add_closed [iff]: "x \ V \ y \ V \ x + y \ V" + and mult_closed [iff]: "x \ V \ a \ x \ V" + and add_assoc: "x \ V \ y \ V \ z \ V \ (x + y) + z = x + (y + z)" + and add_commute: "x \ V \ y \ V \ x + y = y + x" + and diff_self [simp]: "x \ V \ x - x = 0" + and add_zero_left [simp]: "x \ V \ 0 + x = x" + and add_mult_distrib1: "x \ V \ y \ V \ a \ (x + y) = a \ x + a \ y" + and add_mult_distrib2: "x \ V \ (a + b) \ x = a \ x + b \ x" + and mult_assoc: "x \ V \ (a * b) \ x = a \ (b \ x)" + and mult_1 [simp]: "x \ V \ 1 \ x = x" + and negate_eq1: "x \ V \ - x = (- 1) \ x" + and diff_eq1: "x \ V \ y \ V \ x - y = x + - y" + +lemma (in vectorspace) negate_eq2: "x \ V \ (- 1) \ x = - x" + by (rule negate_eq1 [symmetric]) + +lemma (in vectorspace) negate_eq2a: "x \ V \ -1 \ x = - x" + by (simp add: negate_eq1) + +lemma (in vectorspace) diff_eq2: "x \ V \ y \ V \ x + - y = x - y" + by (rule diff_eq1 [symmetric]) + +lemma (in vectorspace) diff_closed [iff]: "x \ V \ y \ V \ x - y \ V" + by (simp add: diff_eq1 negate_eq1) + +lemma (in vectorspace) neg_closed [iff]: "x \ V \ - x \ V" + by (simp add: negate_eq1) + +lemma (in vectorspace) add_left_commute: + "x \ V \ y \ V \ z \ V \ x + (y + z) = y + (x + z)" +proof - + assume xyz: "x \ V" "y \ V" "z \ V" + then have "x + (y + z) = (x + y) + z" + by (simp only: add_assoc) + also from xyz have "\ = (y + x) + z" by (simp only: add_commute) + also from xyz have "\ = y + (x + z)" by (simp only: add_assoc) + finally show ?thesis . +qed + +theorems (in vectorspace) add_ac = + add_assoc add_commute add_left_commute + + +text {* The existence of the zero element of a vector space + follows from the non-emptiness of carrier set. *} + +lemma (in vectorspace) zero [iff]: "0 \ V" +proof - + from non_empty obtain x where x: "x \ V" by blast + then have "0 = x - x" by (rule diff_self [symmetric]) + also from x x have "\ \ V" by (rule diff_closed) + finally show ?thesis . +qed + +lemma (in vectorspace) add_zero_right [simp]: + "x \ V \ x + 0 = x" +proof - + assume x: "x \ V" + from this and zero have "x + 0 = 0 + x" by (rule add_commute) + also from x have "\ = x" by (rule add_zero_left) + finally show ?thesis . +qed + +lemma (in vectorspace) mult_assoc2: + "x \ V \ a \ b \ x = (a * b) \ x" + by (simp only: mult_assoc) + +lemma (in vectorspace) diff_mult_distrib1: + "x \ V \ y \ V \ a \ (x - y) = a \ x - a \ y" + by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2) + +lemma (in vectorspace) diff_mult_distrib2: + "x \ V \ (a - b) \ x = a \ x - (b \ x)" +proof - + assume x: "x \ V" + have " (a - b) \ x = (a + - b) \ x" + by (simp add: real_diff_def) + also from x have "\ = a \ x + (- b) \ x" + by (rule add_mult_distrib2) + also from x have "\ = a \ x + - (b \ x)" + by (simp add: negate_eq1 mult_assoc2) + also from x have "\ = a \ x - (b \ x)" + by (simp add: diff_eq1) + finally show ?thesis . +qed + +lemmas (in vectorspace) distrib = + add_mult_distrib1 add_mult_distrib2 + diff_mult_distrib1 diff_mult_distrib2 + + +text {* \medskip Further derived laws: *} + +lemma (in vectorspace) mult_zero_left [simp]: + "x \ V \ 0 \ x = 0" +proof - + assume x: "x \ V" + have "0 \ x = (1 - 1) \ x" by simp + also have "\ = (1 + - 1) \ x" by simp + also from x have "\ = 1 \ x + (- 1) \ x" + by (rule add_mult_distrib2) + also from x have "\ = x + (- 1) \ x" by simp + also from x have "\ = x + - x" by (simp add: negate_eq2a) + also from x have "\ = x - x" by (simp add: diff_eq2) + also from x have "\ = 0" by simp + finally show ?thesis . +qed + +lemma (in vectorspace) mult_zero_right [simp]: + "a \ 0 = (0::'a)" +proof - + have "a \ 0 = a \ (0 - (0::'a))" by simp + also have "\ = a \ 0 - a \ 0" + by (rule diff_mult_distrib1) simp_all + also have "\ = 0" by simp + finally show ?thesis . +qed + +lemma (in vectorspace) minus_mult_cancel [simp]: + "x \ V \ (- a) \ - x = a \ x" + by (simp add: negate_eq1 mult_assoc2) + +lemma (in vectorspace) add_minus_left_eq_diff: + "x \ V \ y \ V \ - x + y = y - x" +proof - + assume xy: "x \ V" "y \ V" + then have "- x + y = y + - x" by (simp add: add_commute) + also from xy have "\ = y - x" by (simp add: diff_eq1) + finally show ?thesis . +qed + +lemma (in vectorspace) add_minus [simp]: + "x \ V \ x + - x = 0" + by (simp add: diff_eq2) + +lemma (in vectorspace) add_minus_left [simp]: + "x \ V \ - x + x = 0" + by (simp add: diff_eq2 add_commute) + +lemma (in vectorspace) minus_minus [simp]: + "x \ V \ - (- x) = x" + by (simp add: negate_eq1 mult_assoc2) + +lemma (in vectorspace) minus_zero [simp]: + "- (0::'a) = 0" + by (simp add: negate_eq1) + +lemma (in vectorspace) minus_zero_iff [simp]: + "x \ V \ (- x = 0) = (x = 0)" +proof + assume x: "x \ V" + { + from x have "x = - (- x)" by (simp add: minus_minus) + also assume "- x = 0" + also have "- \ = 0" by (rule minus_zero) + finally show "x = 0" . + next + assume "x = 0" + then show "- x = 0" by simp + } +qed + +lemma (in vectorspace) add_minus_cancel [simp]: + "x \ V \ y \ V \ x + (- x + y) = y" + by (simp add: add_assoc [symmetric] del: add_commute) + +lemma (in vectorspace) minus_add_cancel [simp]: + "x \ V \ y \ V \ - x + (x + y) = y" + by (simp add: add_assoc [symmetric] del: add_commute) + +lemma (in vectorspace) minus_add_distrib [simp]: + "x \ V \ y \ V \ - (x + y) = - x + - y" + by (simp add: negate_eq1 add_mult_distrib1) + +lemma (in vectorspace) diff_zero [simp]: + "x \ V \ x - 0 = x" + by (simp add: diff_eq1) + +lemma (in vectorspace) diff_zero_right [simp]: + "x \ V \ 0 - x = - x" + by (simp add: diff_eq1) + +lemma (in vectorspace) add_left_cancel: + "x \ V \ y \ V \ z \ V \ (x + y = x + z) = (y = z)" +proof + assume x: "x \ V" and y: "y \ V" and z: "z \ V" + { + from y have "y = 0 + y" by simp + also from x y have "\ = (- x + x) + y" by simp + also from x y have "\ = - x + (x + y)" + by (simp add: add_assoc neg_closed) + also assume "x + y = x + z" + also from x z have "- x + (x + z) = - x + x + z" + by (simp add: add_assoc [symmetric] neg_closed) + also from x z have "\ = z" by simp + finally show "y = z" . + next + assume "y = z" + then show "x + y = x + z" by (simp only:) + } +qed + +lemma (in vectorspace) add_right_cancel: + "x \ V \ y \ V \ z \ V \ (y + x = z + x) = (y = z)" + by (simp only: add_commute add_left_cancel) + +lemma (in vectorspace) add_assoc_cong: + "x \ V \ y \ V \ x' \ V \ y' \ V \ z \ V + \ x + y = x' + y' \ x + (y + z) = x' + (y' + z)" + by (simp only: add_assoc [symmetric]) + +lemma (in vectorspace) mult_left_commute: + "x \ V \ a \ b \ x = b \ a \ x" + by (simp add: real_mult_commute mult_assoc2) + +lemma (in vectorspace) mult_zero_uniq: + "x \ V \ x \ 0 \ a \ x = 0 \ a = 0" +proof (rule classical) + assume a: "a \ 0" + assume x: "x \ V" "x \ 0" and ax: "a \ x = 0" + from x a have "x = (inverse a * a) \ x" by simp + also from `x \ V` have "\ = inverse a \ (a \ x)" by (rule mult_assoc) + also from ax have "\ = inverse a \ 0" by simp + also have "\ = 0" by simp + finally have "x = 0" . + with `x \ 0` show "a = 0" by contradiction +qed + +lemma (in vectorspace) mult_left_cancel: + "x \ V \ y \ V \ a \ 0 \ (a \ x = a \ y) = (x = y)" +proof + assume x: "x \ V" and y: "y \ V" and a: "a \ 0" + from x have "x = 1 \ x" by simp + also from a have "\ = (inverse a * a) \ x" by simp + also from x have "\ = inverse a \ (a \ x)" + by (simp only: mult_assoc) + also assume "a \ x = a \ y" + also from a y have "inverse a \ \ = y" + by (simp add: mult_assoc2) + finally show "x = y" . +next + assume "x = y" + then show "a \ x = a \ y" by (simp only:) +qed + +lemma (in vectorspace) mult_right_cancel: + "x \ V \ x \ 0 \ (a \ x = b \ x) = (a = b)" +proof + assume x: "x \ V" and neq: "x \ 0" + { + from x have "(a - b) \ x = a \ x - b \ x" + by (simp add: diff_mult_distrib2) + also assume "a \ x = b \ x" + with x have "a \ x - b \ x = 0" by simp + finally have "(a - b) \ x = 0" . + with x neq have "a - b = 0" by (rule mult_zero_uniq) + then show "a = b" by simp + next + assume "a = b" + then show "a \ x = b \ x" by (simp only:) + } +qed + +lemma (in vectorspace) eq_diff_eq: + "x \ V \ y \ V \ z \ V \ (x = z - y) = (x + y = z)" +proof + assume x: "x \ V" and y: "y \ V" and z: "z \ V" + { + assume "x = z - y" + then have "x + y = z - y + y" by simp + also from y z have "\ = z + - y + y" + by (simp add: diff_eq1) + also have "\ = z + (- y + y)" + by (rule add_assoc) (simp_all add: y z) + also from y z have "\ = z + 0" + by (simp only: add_minus_left) + also from z have "\ = z" + by (simp only: add_zero_right) + finally show "x + y = z" . + next + assume "x + y = z" + then have "z - y = (x + y) - y" by simp + also from x y have "\ = x + y + - y" + by (simp add: diff_eq1) + also have "\ = x + (y + - y)" + by (rule add_assoc) (simp_all add: x y) + also from x y have "\ = x" by simp + finally show "x = z - y" .. + } +qed + +lemma (in vectorspace) add_minus_eq_minus: + "x \ V \ y \ V \ x + y = 0 \ x = - y" +proof - + assume x: "x \ V" and y: "y \ V" + from x y have "x = (- y + y) + x" by simp + also from x y have "\ = - y + (x + y)" by (simp add: add_ac) + also assume "x + y = 0" + also from y have "- y + 0 = - y" by simp + finally show "x = - y" . +qed + +lemma (in vectorspace) add_minus_eq: + "x \ V \ y \ V \ x - y = 0 \ x = y" +proof - + assume x: "x \ V" and y: "y \ V" + assume "x - y = 0" + with x y have eq: "x + - y = 0" by (simp add: diff_eq1) + with _ _ have "x = - (- y)" + by (rule add_minus_eq_minus) (simp_all add: x y) + with x y show "x = y" by simp +qed + +lemma (in vectorspace) add_diff_swap: + "a \ V \ b \ V \ c \ V \ d \ V \ a + b = c + d + \ a - c = d - b" +proof - + assume vs: "a \ V" "b \ V" "c \ V" "d \ V" + and eq: "a + b = c + d" + then have "- c + (a + b) = - c + (c + d)" + by (simp add: add_left_cancel) + also have "\ = d" using `c \ V` `d \ V` by (rule minus_add_cancel) + finally have eq: "- c + (a + b) = d" . + from vs have "a - c = (- c + (a + b)) + - b" + by (simp add: add_ac diff_eq1) + also from vs eq have "\ = d + - b" + by (simp add: add_right_cancel) + also from vs have "\ = d - b" by (simp add: diff_eq2) + finally show "a - c = d - b" . +qed + +lemma (in vectorspace) vs_add_cancel_21: + "x \ V \ y \ V \ z \ V \ u \ V + \ (x + (y + z) = y + u) = (x + z = u)" +proof + assume vs: "x \ V" "y \ V" "z \ V" "u \ V" + { + from vs have "x + z = - y + y + (x + z)" by simp + also have "\ = - y + (y + (x + z))" + by (rule add_assoc) (simp_all add: vs) + also from vs have "y + (x + z) = x + (y + z)" + by (simp add: add_ac) + also assume "x + (y + z) = y + u" + also from vs have "- y + (y + u) = u" by simp + finally show "x + z = u" . + next + assume "x + z = u" + with vs show "x + (y + z) = y + u" + by (simp only: add_left_commute [of x]) + } +qed + +lemma (in vectorspace) add_cancel_end: + "x \ V \ y \ V \ z \ V \ (x + (y + z) = y) = (x = - z)" +proof + assume vs: "x \ V" "y \ V" "z \ V" + { + assume "x + (y + z) = y" + with vs have "(x + z) + y = 0 + y" + by (simp add: add_ac) + with vs have "x + z = 0" + by (simp only: add_right_cancel add_closed zero) + with vs show "x = - z" by (simp add: add_minus_eq_minus) + next + assume eq: "x = - z" + then have "x + (y + z) = - z + (y + z)" by simp + also have "\ = y + (- z + z)" + by (rule add_left_commute) (simp_all add: vs) + also from vs have "\ = y" by simp + finally show "x + (y + z) = y" . + } +qed + +end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/Zorn_Lemma.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,57 @@ +(* Title: HOL/Hahn_Banach/Zorn_Lemma.thy + Author: Gertrud Bauer, TU Munich +*) + +header {* Zorn's Lemma *} + +theory Zorn_Lemma +imports Zorn +begin + +text {* + Zorn's Lemmas states: if every linear ordered subset of an ordered + set @{text S} has an upper bound in @{text S}, then there exists a + maximal element in @{text S}. In our application, @{text S} is a + set of sets ordered by set inclusion. Since the union of a chain of + sets is an upper bound for all elements of the chain, the conditions + of Zorn's lemma can be modified: if @{text S} is non-empty, it + suffices to show that for every non-empty chain @{text c} in @{text + S} the union of @{text c} also lies in @{text S}. +*} + +theorem Zorn's_Lemma: + assumes r: "\c. c \ chain S \ \x. x \ c \ \c \ S" + and aS: "a \ S" + shows "\y \ S. \z \ S. y \ z \ y = z" +proof (rule Zorn_Lemma2) + show "\c \ chain S. \y \ S. \z \ c. z \ y" + proof + fix c assume "c \ chain S" + show "\y \ S. \z \ c. z \ y" + proof cases + + txt {* If @{text c} is an empty chain, then every element in + @{text S} is an upper bound of @{text c}. *} + + assume "c = {}" + with aS show ?thesis by fast + + txt {* If @{text c} is non-empty, then @{text "\c"} is an upper + bound of @{text c}, lying in @{text S}. *} + + next + assume "c \ {}" + show ?thesis + proof + show "\z \ c. z \ \c" by fast + show "\c \ S" + proof (rule r) + from `c \ {}` show "\x. x \ c" by fast + show "c \ chain S" by fact + qed + qed + qed + qed +qed + +end diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/document/root.bib Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,27 @@ + +@Book{Heuser:1986, + author = {H. Heuser}, + title = {Funktionalanalysis: Theorie und Anwendung}, + publisher = {Teubner}, + year = 1986 +} + +@InCollection{Narici:1996, + author = {L. Narici and E. Beckenstein}, + title = {The {Hahn-Banach Theorem}: The Life and Times}, + booktitle = {Topology Atlas}, + publisher = {York University, Toronto, Ontario, Canada}, + year = 1996, + note = {\url{http://at.yorku.ca/topology/preprint.htm} and + \url{http://at.yorku.ca/p/a/a/a/16.htm}} +} + +@Article{Nowak:1993, + author = {B. Nowak and A. Trybulec}, + title = {{Hahn-Banach} Theorem}, + journal = {Journal of Formalized Mathematics}, + year = {1993}, + volume = {5}, + institution = {University of Bialystok}, + note = {\url{http://mizar.uwb.edu.pl/JFM/Vol5/hahnban.html}} +} diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/Hahn_Banach/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hahn_Banach/document/root.tex Wed Jun 24 21:46:54 2009 +0200 @@ -0,0 +1,83 @@ +\documentclass[10pt,a4paper,twoside]{article} +\usepackage{graphicx} +\usepackage{latexsym,theorem} +\usepackage{isabelle,isabellesym} +\usepackage{pdfsetup} %last one! + +\isabellestyle{it} +\urlstyle{rm} + +\newcommand{\isasymsup}{\isamath{\sup\,}} +\newcommand{\skp}{\smallskip} + + +\begin{document} + +\pagestyle{headings} +\pagenumbering{arabic} + +\title{The Hahn-Banach Theorem \\ for Real Vector Spaces} +\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}} +\maketitle + +\begin{abstract} + The Hahn-Banach Theorem is one of the most fundamental results in functional + analysis. We present a fully formal proof of two versions of the theorem, + one for general linear spaces and another for normed spaces. This + development is based on simply-typed classical set-theory, as provided by + Isabelle/HOL. +\end{abstract} + + +\tableofcontents +\parindent 0pt \parskip 0.5ex + +\clearpage +\section{Preface} + +This is a fully formal proof of the Hahn-Banach Theorem. It closely follows +the informal presentation given in Heuser's textbook \cite[{\S} 36]{Heuser:1986}. +Another formal proof of the same theorem has been done in Mizar +\cite{Nowak:1993}. A general overview of the relevance and history of the +Hahn-Banach Theorem is given by Narici and Beckenstein \cite{Narici:1996}. + +\medskip The document is structured as follows. The first part contains +definitions of basic notions of linear algebra: vector spaces, subspaces, +normed spaces, continuous linear-forms, norm of functions and an order on +functions by domain extension. The second part contains some lemmas about the +supremum (w.r.t.\ the function order) and extension of non-maximal functions. +With these preliminaries, the main proof of the theorem (in its two versions) +is conducted in the third part. The dependencies of individual theories are +as follows. + +\begin{center} + \includegraphics[scale=0.5]{session_graph} +\end{center} + +\clearpage +\part {Basic Notions} + +\input{Bounds} +\input{Vector_Space} +\input{Subspace} +\input{Normed_Space} +\input{Linearform} +\input{Function_Order} +\input{Function_Norm} +\input{Zorn_Lemma} + +\clearpage +\part {Lemmas for the Proof} + +\input{Hahn_Banach_Sup_Lemmas} +\input{Hahn_Banach_Ext_Lemmas} +\input{Hahn_Banach_Lemmas} + +\clearpage +\part {The Main Proof} + +\input{Hahn_Banach} +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jun 24 21:28:02 2009 +0200 +++ b/src/HOL/IsaMakefile Wed Jun 24 21:46:54 2009 +0200 @@ -16,7 +16,7 @@ HOL-Bali \ HOL-Decision_Procs \ HOL-Extraction \ - HOL-HahnBanach \ + HOL-Hahn_Banach \ HOL-Hoare \ HOL-HoareParallel \ HOL-Import \ @@ -360,21 +360,19 @@ @cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library -## HOL-HahnBanach +## HOL-Hahn_Banach -HOL-HahnBanach: HOL $(LOG)/HOL-HahnBanach.gz +HOL-Hahn_Banach: HOL $(LOG)/HOL-Hahn_Banach.gz -$(LOG)/HOL-HahnBanach.gz: $(OUT)/HOL \ - HahnBanach/Bounds.thy HahnBanach/FunctionNorm.thy \ - HahnBanach/FunctionOrder.thy HahnBanach/HahnBanach.thy \ - HahnBanach/HahnBanachExtLemmas.thy \ - HahnBanach/HahnBanachSupLemmas.thy \ - HahnBanach/Linearform.thy HahnBanach/NormedSpace.thy \ - HahnBanach/README.html HahnBanach/ROOT.ML \ - HahnBanach/Subspace.thy HahnBanach/VectorSpace.thy \ - HahnBanach/ZornLemma.thy HahnBanach/document/root.bib \ - HahnBanach/document/root.tex - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HahnBanach +$(LOG)/HOL-Hahn_Banach.gz: $(OUT)/HOL Hahn_Banach/Bounds.thy \ + Hahn_Banach/Function_Norm.thy Hahn_Banach/Function_Order.thy \ + Hahn_Banach/Hahn_Banach.thy Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy \ + Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Hahn_Banach/Linearform.thy \ + Hahn_Banach/Normed_Space.thy Hahn_Banach/README.html \ + Hahn_Banach/ROOT.ML Hahn_Banach/Subspace.thy \ + Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy \ + Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex + @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach ## HOL-Subst @@ -1138,7 +1136,7 @@ $(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \ $(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-IOA.gz \ $(LOG)/HOL-Lattice $(LOG)/HOL-Matrix \ - $(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \ + $(LOG)/HOL-Hahn_Banach.gz $(LOG)/HOL-SET-Protocol.gz \ $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \ $(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz \ $(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz \ diff -r 71af1fd6a5e4 -r be3e1cc5005c src/HOL/README.html --- a/src/HOL/README.html Wed Jun 24 21:28:02 2009 +0200 +++ b/src/HOL/README.html Wed Jun 24 21:46:54 2009 +0200 @@ -96,7 +96,7 @@
Real
the real numbers, part of Complex -
Real/HahnBanach +
Hahn_Banach
the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
SET-Protocol