# HG changeset patch # User wenzelm # Date 1030630110 -7200 # Node ID bf399f3bd7dc22a105eb4892be4ad059db6655e7 # Parent f76237c2be75cbb351684516c423f0cebce7b0dc tuned; diff -r f76237c2be75 -r bf399f3bd7dc src/HOL/Real/HahnBanach/FunctionNorm.thy --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Aug 29 11:15:36 2002 +0200 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Aug 29 16:08:30 2002 +0200 @@ -53,9 +53,9 @@ 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 function_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"}. + @{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: @@ -63,31 +63,25 @@ @{text "{0} \ {\f x\ / \x\. x \ 0 \ x \ F}"} \end{center} - @{text function_norm} is equal to the supremum of @{text B}, if the + @{text fn_norm} is equal to the supremum of @{text B}, if the supremum exists (otherwise it is undefined). *} -locale function_norm = norm_syntax + - fixes B - defines "B V f \ {0} \ {\f x\ / \x\ | x. x \ 0 \ x \ V}" - fixes function_norm ("\_\\_" [0, 1000] 999) +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)" -lemma (in function_norm) B_not_empty [intro]: "0 \ B V f" - by (unfold B_def) simp - -locale (open) functional_vectorspace = - normed_vectorspace + function_norm + - fixes cont - defines "cont f \ continuous V norm f" +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 functional_vectorspace) function_norm_works: - includes continuous +lemma (in normed_vectorspace) fn_norm_works: (* FIXME bug with "(in fn_norm)" !? *) + includes fn_norm + continuous shows "lub (B V f) (\f\\V)" proof - txt {* The existence of the supremum is shown using the @@ -148,38 +142,40 @@ thus ?thesis .. qed qed - then show ?thesis - by (unfold function_norm_def) (rule the_lubI_ex) + then show ?thesis by (unfold fn_norm_def) (rule the_lubI_ex) qed -lemma (in functional_vectorspace) function_norm_ub [intro?]: - includes continuous +lemma (in normed_vectorspace) fn_norm_ub [iff?]: + includes fn_norm + continuous assumes b: "b \ B V f" shows "b \ \f\\V" proof - - have "lub (B V f) (\f\\V)" by (rule function_norm_works) + have "lub (B V f) (\f\\V)" + by (unfold B_def fn_norm_def) (rule fn_norm_works) from this and b show ?thesis .. qed -lemma (in functional_vectorspace) function_norm_least' [intro?]: - includes continuous +lemma (in normed_vectorspace) fn_norm_leastB: + includes fn_norm + continuous assumes b: "\b. b \ B V f \ b \ y" shows "\f\\V \ y" proof - - have "lub (B V f) (\f\\V)" by (rule function_norm_works) + have "lub (B V f) (\f\\V)" + by (unfold B_def fn_norm_def) (rule fn_norm_works) from this and b show ?thesis .. qed text {* The norm of a continuous function is always @{text "\ 0"}. *} -lemma (in functional_vectorspace) function_norm_ge_zero [iff]: - includes continuous +lemma (in normed_vectorspace) fn_norm_ge_zero [iff]: + includes fn_norm + continuous shows "0 \ \f\\V" proof - 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)" by (rule function_norm_works) + have "lub (B V f) (\f\\V)" + by (unfold B_def fn_norm_def) (rule fn_norm_works) moreover have "0 \ B V f" .. ultimately show ?thesis .. qed @@ -191,8 +187,8 @@ \end{center} *} -lemma (in functional_vectorspace) function_norm_le_cong: - includes continuous + vectorspace_linearform +lemma (in normed_vectorspace) fn_norm_le_cong: + includes fn_norm + continuous + linearform assumes x: "x \ V" shows "\f x\ \ \f\\V * \x\" proof cases @@ -202,7 +198,7 @@ also have "\\\ = 0" by simp also have "\ \ \f\\V * \x\" proof (rule real_le_mult_order1a) - show "0 \ \f\\V" .. + show "0 \ \f\\V" by (unfold B_def fn_norm_def) rule show "0 \ norm x" .. qed finally show "\f x\ \ \f\\V * \x\" . @@ -213,11 +209,10 @@ also have "\ \ \f\\V * \x\" proof (rule real_mult_le_le_mono2) from x show "0 \ \x\" .. - show "\f x\ * inverse \x\ \ \f\\V" - proof - from x and neq show "\f x\ * inverse \x\ \ B V f" - by (auto simp add: B_def real_divide_def) - qed + from x and neq have "\f x\ * inverse \x\ \ B V f" + by (auto simp add: B_def real_divide_def) + then show "\f x\ * inverse \x\ \ \f\\V" + by (unfold B_def fn_norm_def) (rule fn_norm_ub) qed finally show ?thesis . qed @@ -230,11 +225,11 @@ \end{center} *} -lemma (in functional_vectorspace) function_norm_least [intro?]: - includes continuous +lemma (in normed_vectorspace) fn_norm_least [intro?]: + includes fn_norm + continuous assumes ineq: "\x \ V. \f x\ \ c * \x\" and ge: "0 \ c" shows "\f\\V \ c" -proof (rule function_norm_least') +proof (rule fn_norm_leastB [folded B_def fn_norm_def]) fix b assume b: "b \ B V f" show "b \ c" proof cases @@ -261,9 +256,4 @@ qed qed -lemmas [iff?] = - functional_vectorspace.function_norm_ge_zero - functional_vectorspace.function_norm_le_cong - functional_vectorspace.function_norm_least - end diff -r f76237c2be75 -r bf399f3bd7dc src/HOL/Real/HahnBanach/HahnBanach.thy --- a/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Aug 29 11:15:36 2002 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Aug 29 16:08:30 2002 +0200 @@ -53,8 +53,7 @@ *} theorem HahnBanach: - includes vectorspace E + subvectorspace F E + - seminorm_vectorspace E p + linearform F f + includes vectorspace E + subspace F E + seminorm E p + 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}, *} @@ -63,6 +62,7 @@ proof - def M \ "norm_pres_extensions E p F f" hence M: "M = \" by (simp only:) + have E: "vectorspace E" . have F: "vectorspace F" .. { fix c assume cM: "c \ chain M" and ex: "\x. x \ c" @@ -121,7 +121,7 @@ -- {* @{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 have H: "vectorspace H" - by (rule subvectorspace.vectorspace) + by (rule subspace.vectorspace) have HE_eq: "H = E" -- {* We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp *} @@ -164,7 +164,7 @@ 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: vectorspace_linearform.diff) + 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" @@ -173,11 +173,10 @@ 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 have "p \ \ p (v + x') + p (u + x')" + 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 + then show "- p (u + x') - h u \ p (v + x') - h v" by simp qed then show ?thesis .. qed @@ -298,8 +297,7 @@ *} theorem abs_HahnBanach: - includes vectorspace E + subvectorspace F E + - linearform F f + seminorm_vectorspace E p + includes vectorspace E + subspace F E + linearform F f + seminorm E p assumes fp: "\x \ F. \f x\ \ p x" shows "\g. linearform E g \ (\x \ F. g x = f x) @@ -330,8 +328,7 @@ *} theorem norm_HahnBanach: - includes functional_vectorspace E + subvectorspace F E + - linearform F f + continuous F norm f + includes normed_vectorspace E + subspace F E + linearform F f + fn_norm + continuous F norm f shows "\g. linearform E g \ continuous E norm g \ (\x \ F. g x = f x) @@ -343,6 +340,9 @@ have F: "vectorspace F" .. have linearform: "linearform F f" . have F_norm: "normed_vectorspace F norm" .. + have ge_zero: "0 \ \f\\F" + by (rule normed_vectorspace.fn_norm_ge_zero + [OF F_norm, folded B_def fn_norm_def]) txt {* We define a function @{text p} on @{text E} as follows: @{text "p x = \f\ \ \x\"} *} @@ -356,9 +356,7 @@ txt {* @{text p} is positive definite: *} show "0 \ p x" proof (unfold p_def, rule real_le_mult_order1a) - show "0 \ \f\\F" - apply (unfold function_norm_def B_def) - using normed_vectorspace.axioms [OF F_norm] .. + show "0 \ \f\\F" by (rule ge_zero) from x show "0 \ \x\" .. qed @@ -366,14 +364,10 @@ 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) + 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 @@ -381,19 +375,14 @@ show "p (x + y) \ p x + p y" proof - - have "p (x + y) = \f\\F * \x + y\" - by (simp only: p_def) + have "p (x + y) = \f\\F * \x + y\" by (simp only: p_def) also have "\ \ \f\\F * (\x\ + \y\)" proof (rule real_mult_le_le_mono1a) - show "0 \ \f\\F" - apply (unfold function_norm_def B_def) - using normed_vectorspace.axioms [OF F_norm] .. (* FIXME *) + show "0 \ \f\\F" by (rule ge_zero) from x y show "\x + y\ \ \x\ + \y\" .. qed - also have "\ = \f\\F * \x\ + \f\\F * \y\" - by (simp only: real_add_mult_distrib2) - also have "\ = p x + p y" - by (simp only: p_def) + also have "\ = \f\\F * \x\ + \f\\F * \y\" by (simp only: real_add_mult_distrib2) + also have "\ = p x + p y" by (simp only: p_def) finally show ?thesis . qed qed @@ -404,8 +393,8 @@ proof fix x assume "x \ F" show "\f x\ \ p x" - apply (unfold p_def function_norm_def B_def) - using normed_vectorspace.axioms [OF F_norm] .. (* FIXME *) + by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong + [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 @@ -454,45 +443,32 @@ with b show "\g x\ \ \f\\F * \x\" by (simp only: p_def) qed + from continuous.axioms [OF g_cont] this ge_zero show "\g\\E \ \f\\F" - apply (unfold function_norm_def B_def) - apply rule - apply (rule normed_vectorspace.axioms [OF E_norm])+ - apply (rule continuous.axioms [OF g_cont])+ - apply (rule b [unfolded p_def function_norm_def B_def]) - using normed_vectorspace.axioms [OF F_norm] .. (* FIXME *) + by (rule fn_norm_least [of g, folded B_def fn_norm_def]) txt {* The other direction is achieved by a similar argument. *} - have ** : "\x \ F. \f x\ \ \g\\E * \x\" - proof - fix x assume x: "x \ F" - from a have "g x = f x" .. - hence "\f x\ = \g x\" by (simp only:) - also have "\ \ \