1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Wed Jun 24 21:46:54 2009 +0200
1.3 @@ -0,0 +1,280 @@
1.4 +(* Title: HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
1.5 + Author: Gertrud Bauer, TU Munich
1.6 +*)
1.7 +
1.8 +header {* Extending non-maximal functions *}
1.9 +
1.10 +theory Hahn_Banach_Ext_Lemmas
1.11 +imports Function_Norm
1.12 +begin
1.13 +
1.14 +text {*
1.15 + In this section the following context is presumed. Let @{text E} be
1.16 + a real vector space with a seminorm @{text q} on @{text E}. @{text
1.17 + F} is a subspace of @{text E} and @{text f} a linear function on
1.18 + @{text F}. We consider a subspace @{text H} of @{text E} that is a
1.19 + superspace of @{text F} and a linear form @{text h} on @{text
1.20 + H}. @{text H} is a not equal to @{text E} and @{text "x\<^sub>0"} is
1.21 + an element in @{text "E - H"}. @{text H} is extended to the direct
1.22 + sum @{text "H' = H + lin x\<^sub>0"}, so for any @{text "x \<in> H'"}
1.23 + the decomposition of @{text "x = y + a \<cdot> x"} with @{text "y \<in> H"} is
1.24 + unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y +
1.25 + a \<cdot> \<xi>"} for a certain @{text \<xi>}.
1.26 +
1.27 + Subsequently we show some properties of this extension @{text h'} of
1.28 + @{text h}.
1.29 +
1.30 + \medskip This lemma will be used to show the existence of a linear
1.31 + extension of @{text f} (see page \pageref{ex-xi-use}). It is a
1.32 + consequence of the completeness of @{text \<real>}. To show
1.33 + \begin{center}
1.34 + \begin{tabular}{l}
1.35 + @{text "\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y"}
1.36 + \end{tabular}
1.37 + \end{center}
1.38 + \noindent it suffices to show that
1.39 + \begin{center}
1.40 + \begin{tabular}{l}
1.41 + @{text "\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v"}
1.42 + \end{tabular}
1.43 + \end{center}
1.44 +*}
1.45 +
1.46 +lemma ex_xi:
1.47 + assumes "vectorspace F"
1.48 + assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"
1.49 + shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
1.50 +proof -
1.51 + interpret vectorspace F by fact
1.52 + txt {* From the completeness of the reals follows:
1.53 + The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
1.54 + non-empty and has an upper bound. *}
1.55 +
1.56 + let ?S = "{a u | u. u \<in> F}"
1.57 + have "\<exists>xi. lub ?S xi"
1.58 + proof (rule real_complete)
1.59 + have "a 0 \<in> ?S" by blast
1.60 + then show "\<exists>X. X \<in> ?S" ..
1.61 + have "\<forall>y \<in> ?S. y \<le> b 0"
1.62 + proof
1.63 + fix y assume y: "y \<in> ?S"
1.64 + then obtain u where u: "u \<in> F" and y: "y = a u" by blast
1.65 + from u and zero have "a u \<le> b 0" by (rule r)
1.66 + with y show "y \<le> b 0" by (simp only:)
1.67 + qed
1.68 + then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" ..
1.69 + qed
1.70 + then obtain xi where xi: "lub ?S xi" ..
1.71 + {
1.72 + fix y assume "y \<in> F"
1.73 + then have "a y \<in> ?S" by blast
1.74 + with xi have "a y \<le> xi" by (rule lub.upper)
1.75 + } moreover {
1.76 + fix y assume y: "y \<in> F"
1.77 + from xi have "xi \<le> b y"
1.78 + proof (rule lub.least)
1.79 + fix au assume "au \<in> ?S"
1.80 + then obtain u where u: "u \<in> F" and au: "au = a u" by blast
1.81 + from u y have "a u \<le> b y" by (rule r)
1.82 + with au show "au \<le> b y" by (simp only:)
1.83 + qed
1.84 + } ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
1.85 +qed
1.86 +
1.87 +text {*
1.88 + \medskip The function @{text h'} is defined as a @{text "h' x = h y
1.89 + + a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a linear extension of
1.90 + @{text h} to @{text H'}.
1.91 +*}
1.92 +
1.93 +lemma h'_lf:
1.94 + assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
1.95 + SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
1.96 + and H'_def: "H' \<equiv> H + lin x0"
1.97 + and HE: "H \<unlhd> E"
1.98 + assumes "linearform H h"
1.99 + assumes x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"
1.100 + assumes E: "vectorspace E"
1.101 + shows "linearform H' h'"
1.102 +proof -
1.103 + interpret linearform H h by fact
1.104 + interpret vectorspace E by fact
1.105 + show ?thesis
1.106 + proof
1.107 + note E = `vectorspace E`
1.108 + have H': "vectorspace H'"
1.109 + proof (unfold H'_def)
1.110 + from `x0 \<in> E`
1.111 + have "lin x0 \<unlhd> E" ..
1.112 + with HE show "vectorspace (H + lin x0)" using E ..
1.113 + qed
1.114 + {
1.115 + fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
1.116 + show "h' (x1 + x2) = h' x1 + h' x2"
1.117 + proof -
1.118 + from H' x1 x2 have "x1 + x2 \<in> H'"
1.119 + by (rule vectorspace.add_closed)
1.120 + with x1 x2 obtain y y1 y2 a a1 a2 where
1.121 + x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
1.122 + and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
1.123 + and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
1.124 + unfolding H'_def sum_def lin_def by blast
1.125 +
1.126 + have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
1.127 + proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
1.128 + from HE y1 y2 show "y1 + y2 \<in> H"
1.129 + by (rule subspace.add_closed)
1.130 + from x0 and HE y y1 y2
1.131 + have "x0 \<in> E" "y \<in> E" "y1 \<in> E" "y2 \<in> E" by auto
1.132 + with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
1.133 + by (simp add: add_ac add_mult_distrib2)
1.134 + also note x1x2
1.135 + finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
1.136 + qed
1.137 +
1.138 + from h'_def x1x2 E HE y x0
1.139 + have "h' (x1 + x2) = h y + a * xi"
1.140 + by (rule h'_definite)
1.141 + also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
1.142 + by (simp only: ya)
1.143 + also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
1.144 + by simp
1.145 + also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
1.146 + by (simp add: left_distrib)
1.147 + also from h'_def x1_rep E HE y1 x0
1.148 + have "h y1 + a1 * xi = h' x1"
1.149 + by (rule h'_definite [symmetric])
1.150 + also from h'_def x2_rep E HE y2 x0
1.151 + have "h y2 + a2 * xi = h' x2"
1.152 + by (rule h'_definite [symmetric])
1.153 + finally show ?thesis .
1.154 + qed
1.155 + next
1.156 + fix x1 c assume x1: "x1 \<in> H'"
1.157 + show "h' (c \<cdot> x1) = c * (h' x1)"
1.158 + proof -
1.159 + from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
1.160 + by (rule vectorspace.mult_closed)
1.161 + with x1 obtain y a y1 a1 where
1.162 + cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
1.163 + and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
1.164 + unfolding H'_def sum_def lin_def by blast
1.165 +
1.166 + have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
1.167 + proof (rule decomp_H')
1.168 + from HE y1 show "c \<cdot> y1 \<in> H"
1.169 + by (rule subspace.mult_closed)
1.170 + from x0 and HE y y1
1.171 + have "x0 \<in> E" "y \<in> E" "y1 \<in> E" by auto
1.172 + with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
1.173 + by (simp add: mult_assoc add_mult_distrib1)
1.174 + also note cx1_rep
1.175 + finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
1.176 + qed
1.177 +
1.178 + from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
1.179 + by (rule h'_definite)
1.180 + also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
1.181 + by (simp only: ya)
1.182 + also from y1 have "h (c \<cdot> y1) = c * h y1"
1.183 + by simp
1.184 + also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
1.185 + by (simp only: right_distrib)
1.186 + also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
1.187 + by (rule h'_definite [symmetric])
1.188 + finally show ?thesis .
1.189 + qed
1.190 + }
1.191 + qed
1.192 +qed
1.193 +
1.194 +text {* \medskip The linear extension @{text h'} of @{text h}
1.195 + is bounded by the seminorm @{text p}. *}
1.196 +
1.197 +lemma h'_norm_pres:
1.198 + assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
1.199 + SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
1.200 + and H'_def: "H' \<equiv> H + lin x0"
1.201 + and x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"
1.202 + assumes E: "vectorspace E" and HE: "subspace H E"
1.203 + and "seminorm E p" and "linearform H h"
1.204 + assumes a: "\<forall>y \<in> H. h y \<le> p y"
1.205 + and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
1.206 + shows "\<forall>x \<in> H'. h' x \<le> p x"
1.207 +proof -
1.208 + interpret vectorspace E by fact
1.209 + interpret subspace H E by fact
1.210 + interpret seminorm E p by fact
1.211 + interpret linearform H h by fact
1.212 + show ?thesis
1.213 + proof
1.214 + fix x assume x': "x \<in> H'"
1.215 + show "h' x \<le> p x"
1.216 + proof -
1.217 + from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
1.218 + and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
1.219 + from x' obtain y a where
1.220 + x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
1.221 + unfolding H'_def sum_def lin_def by blast
1.222 + from y have y': "y \<in> E" ..
1.223 + from y have ay: "inverse a \<cdot> y \<in> H" by simp
1.224 +
1.225 + from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"
1.226 + by (rule h'_definite)
1.227 + also have "\<dots> \<le> p (y + a \<cdot> x0)"
1.228 + proof (rule linorder_cases)
1.229 + assume z: "a = 0"
1.230 + then have "h y + a * xi = h y" by simp
1.231 + also from a y have "\<dots> \<le> p y" ..
1.232 + also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
1.233 + finally show ?thesis .
1.234 + next
1.235 + txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
1.236 + with @{text ya} taken as @{text "y / a"}: *}
1.237 + assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp
1.238 + from a1 ay
1.239 + have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
1.240 + with lz have "a * xi \<le>
1.241 + a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
1.242 + by (simp add: mult_left_mono_neg order_less_imp_le)
1.243 +
1.244 + also have "\<dots> =
1.245 + - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
1.246 + by (simp add: right_diff_distrib)
1.247 + also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
1.248 + p (a \<cdot> (inverse a \<cdot> y + x0))"
1.249 + by (simp add: abs_homogenous)
1.250 + also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
1.251 + by (simp add: add_mult_distrib1 mult_assoc [symmetric])
1.252 + also from nz y have "a * (h (inverse a \<cdot> y)) = h y"
1.253 + by simp
1.254 + finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
1.255 + then show ?thesis by simp
1.256 + next
1.257 + txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
1.258 + with @{text ya} taken as @{text "y / a"}: *}
1.259 + assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp
1.260 + from a2 ay
1.261 + have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
1.262 + with gz have "a * xi \<le>
1.263 + a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
1.264 + by simp
1.265 + also have "\<dots> = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
1.266 + by (simp add: right_diff_distrib)
1.267 + also from gz x0 y'
1.268 + have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
1.269 + by (simp add: abs_homogenous)
1.270 + also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
1.271 + by (simp add: add_mult_distrib1 mult_assoc [symmetric])
1.272 + also from nz y have "a * h (inverse a \<cdot> y) = h y"
1.273 + by simp
1.274 + finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
1.275 + then show ?thesis by simp
1.276 + qed
1.277 + also from x_rep have "\<dots> = p x" by (simp only:)
1.278 + finally show ?thesis .
1.279 + qed
1.280 + qed
1.281 +qed
1.282 +
1.283 +end