summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy

changeset 27611 | 2c01c0bdb385 |

parent 23378 | 1d138d6bb461 |

child 27612 | d3eb431db035 |

1.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Tue Jul 15 16:02:10 2008 +0200 1.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Tue Jul 15 16:50:09 2008 +0200 1.3 @@ -40,10 +40,11 @@ 1.4 *} 1.5 1.6 lemma ex_xi: 1.7 - includes vectorspace F 1.8 + assumes "vectorspace F" 1.9 assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v" 1.10 shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" 1.11 proof - 1.12 + interpret vectorspace [F] by fact 1.13 txt {* From the completeness of the reals follows: 1.14 The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is 1.15 non-empty and has an upper bound. *} 1.16 @@ -86,183 +87,190 @@ 1.17 *} 1.18 1.19 lemma h'_lf: 1.20 - includes var H + var h + var E 1.21 assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) = 1.22 SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi" 1.23 and H'_def: "H' \<equiv> H + lin x0" 1.24 and HE: "H \<unlhd> E" 1.25 - includes linearform H h 1.26 + assumes "linearform H h" 1.27 assumes x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" 1.28 - includes vectorspace E 1.29 + assumes E: "vectorspace E" 1.30 shows "linearform H' h'" 1.31 -proof 1.32 - note E = `vectorspace E` 1.33 - have H': "vectorspace H'" 1.34 - proof (unfold H'_def) 1.35 - from `x0 \<in> E` 1.36 - have "lin x0 \<unlhd> E" .. 1.37 - with HE show "vectorspace (H + lin x0)" using E .. 1.38 - qed 1.39 - { 1.40 - fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'" 1.41 - show "h' (x1 + x2) = h' x1 + h' x2" 1.42 - proof - 1.43 - from H' x1 x2 have "x1 + x2 \<in> H'" 1.44 - by (rule vectorspace.add_closed) 1.45 - with x1 x2 obtain y y1 y2 a a1 a2 where 1.46 - x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H" 1.47 +proof - 1.48 + interpret linearform [H h] by fact 1.49 + interpret vectorspace [E] by fact 1.50 + show ?thesis proof 1.51 + note E = `vectorspace E` 1.52 + have H': "vectorspace H'" 1.53 + proof (unfold H'_def) 1.54 + from `x0 \<in> E` 1.55 + have "lin x0 \<unlhd> E" .. 1.56 + with HE show "vectorspace (H + lin x0)" using E .. 1.57 + qed 1.58 + { 1.59 + fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'" 1.60 + show "h' (x1 + x2) = h' x1 + h' x2" 1.61 + proof - 1.62 + from H' x1 x2 have "x1 + x2 \<in> H'" 1.63 + by (rule vectorspace.add_closed) 1.64 + with x1 x2 obtain y y1 y2 a a1 a2 where 1.65 + x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H" 1.66 and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H" 1.67 and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H" 1.68 - by (unfold H'_def sum_def lin_def) blast 1.69 - 1.70 - have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0 1.71 - proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *} 1.72 - from HE y1 y2 show "y1 + y2 \<in> H" 1.73 - by (rule subspace.add_closed) 1.74 - from x0 and HE y y1 y2 1.75 - have "x0 \<in> E" "y \<in> E" "y1 \<in> E" "y2 \<in> E" by auto 1.76 - with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2" 1.77 - by (simp add: add_ac add_mult_distrib2) 1.78 - also note x1x2 1.79 - finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" . 1.80 + by (unfold H'_def sum_def lin_def) blast 1.81 + 1.82 + have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0 1.83 + proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *} 1.84 + from HE y1 y2 show "y1 + y2 \<in> H" 1.85 + by (rule subspace.add_closed) 1.86 + from x0 and HE y y1 y2 1.87 + have "x0 \<in> E" "y \<in> E" "y1 \<in> E" "y2 \<in> E" by auto 1.88 + with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2" 1.89 + by (simp add: add_ac add_mult_distrib2) 1.90 + also note x1x2 1.91 + finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" . 1.92 + qed 1.93 + 1.94 + from h'_def x1x2 E HE y x0 1.95 + have "h' (x1 + x2) = h y + a * xi" 1.96 + by (rule h'_definite) 1.97 + also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi" 1.98 + by (simp only: ya) 1.99 + also from y1 y2 have "h (y1 + y2) = h y1 + h y2" 1.100 + by simp 1.101 + also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)" 1.102 + by (simp add: left_distrib) 1.103 + also from h'_def x1_rep E HE y1 x0 1.104 + have "h y1 + a1 * xi = h' x1" 1.105 + by (rule h'_definite [symmetric]) 1.106 + also from h'_def x2_rep E HE y2 x0 1.107 + have "h y2 + a2 * xi = h' x2" 1.108 + by (rule h'_definite [symmetric]) 1.109 + finally show ?thesis . 1.110 qed 1.111 - 1.112 - from h'_def x1x2 E HE y x0 1.113 - have "h' (x1 + x2) = h y + a * xi" 1.114 - by (rule h'_definite) 1.115 - also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi" 1.116 - by (simp only: ya) 1.117 - also from y1 y2 have "h (y1 + y2) = h y1 + h y2" 1.118 - by simp 1.119 - also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)" 1.120 - by (simp add: left_distrib) 1.121 - also from h'_def x1_rep E HE y1 x0 1.122 - have "h y1 + a1 * xi = h' x1" 1.123 - by (rule h'_definite [symmetric]) 1.124 - also from h'_def x2_rep E HE y2 x0 1.125 - have "h y2 + a2 * xi = h' x2" 1.126 - by (rule h'_definite [symmetric]) 1.127 - finally show ?thesis . 1.128 - qed 1.129 - next 1.130 - fix x1 c assume x1: "x1 \<in> H'" 1.131 - show "h' (c \<cdot> x1) = c * (h' x1)" 1.132 - proof - 1.133 - from H' x1 have ax1: "c \<cdot> x1 \<in> H'" 1.134 - by (rule vectorspace.mult_closed) 1.135 - with x1 obtain y a y1 a1 where 1.136 - cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H" 1.137 + next 1.138 + fix x1 c assume x1: "x1 \<in> H'" 1.139 + show "h' (c \<cdot> x1) = c * (h' x1)" 1.140 + proof - 1.141 + from H' x1 have ax1: "c \<cdot> x1 \<in> H'" 1.142 + by (rule vectorspace.mult_closed) 1.143 + with x1 obtain y a y1 a1 where 1.144 + cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H" 1.145 and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H" 1.146 - by (unfold H'_def sum_def lin_def) blast 1.147 - 1.148 - have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0 1.149 - proof (rule decomp_H') 1.150 - from HE y1 show "c \<cdot> y1 \<in> H" 1.151 - by (rule subspace.mult_closed) 1.152 - from x0 and HE y y1 1.153 - have "x0 \<in> E" "y \<in> E" "y1 \<in> E" by auto 1.154 - with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1" 1.155 - by (simp add: mult_assoc add_mult_distrib1) 1.156 - also note cx1_rep 1.157 - finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" . 1.158 + by (unfold H'_def sum_def lin_def) blast 1.159 + 1.160 + have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0 1.161 + proof (rule decomp_H') 1.162 + from HE y1 show "c \<cdot> y1 \<in> H" 1.163 + by (rule subspace.mult_closed) 1.164 + from x0 and HE y y1 1.165 + have "x0 \<in> E" "y \<in> E" "y1 \<in> E" by auto 1.166 + with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1" 1.167 + by (simp add: mult_assoc add_mult_distrib1) 1.168 + also note cx1_rep 1.169 + finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" . 1.170 + qed 1.171 + 1.172 + from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi" 1.173 + by (rule h'_definite) 1.174 + also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi" 1.175 + by (simp only: ya) 1.176 + also from y1 have "h (c \<cdot> y1) = c * h y1" 1.177 + by simp 1.178 + also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)" 1.179 + by (simp only: right_distrib) 1.180 + also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1" 1.181 + by (rule h'_definite [symmetric]) 1.182 + finally show ?thesis . 1.183 qed 1.184 - 1.185 - from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi" 1.186 - by (rule h'_definite) 1.187 - also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi" 1.188 - by (simp only: ya) 1.189 - also from y1 have "h (c \<cdot> y1) = c * h y1" 1.190 - by simp 1.191 - also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)" 1.192 - by (simp only: right_distrib) 1.193 - also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1" 1.194 - by (rule h'_definite [symmetric]) 1.195 - finally show ?thesis . 1.196 - qed 1.197 - } 1.198 + } 1.199 + qed 1.200 qed 1.201 1.202 text {* \medskip The linear extension @{text h'} of @{text h} 1.203 is bounded by the seminorm @{text p}. *} 1.204 1.205 lemma h'_norm_pres: 1.206 - includes var H + var h + var E 1.207 assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) = 1.208 SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi" 1.209 and H'_def: "H' \<equiv> H + lin x0" 1.210 and x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" 1.211 - includes vectorspace E + subspace H E + seminorm E p + linearform H h 1.212 + assumes E: "vectorspace E" and HE: "subspace H E" 1.213 + and "seminorm E p" and "linearform H h" 1.214 assumes a: "\<forall>y \<in> H. h y \<le> p y" 1.215 and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y" 1.216 shows "\<forall>x \<in> H'. h' x \<le> p x" 1.217 -proof 1.218 - note E = `vectorspace E` 1.219 - note HE = `subspace H E` 1.220 - fix x assume x': "x \<in> H'" 1.221 - show "h' x \<le> p x" 1.222 - proof - 1.223 - from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi" 1.224 - and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto 1.225 - from x' obtain y a where 1.226 +proof - 1.227 + interpret vectorspace [E] by fact 1.228 + interpret subspace [H E] by fact 1.229 + interpret seminorm [E p] by fact 1.230 + interpret linearform [H h] by fact 1.231 + show ?thesis proof 1.232 + fix x assume x': "x \<in> H'" 1.233 + show "h' x \<le> p x" 1.234 + proof - 1.235 + from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi" 1.236 + and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto 1.237 + from x' obtain y a where 1.238 x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H" 1.239 - by (unfold H'_def sum_def lin_def) blast 1.240 - from y have y': "y \<in> E" .. 1.241 - from y have ay: "inverse a \<cdot> y \<in> H" by simp 1.242 - 1.243 - from h'_def x_rep E HE y x0 have "h' x = h y + a * xi" 1.244 - by (rule h'_definite) 1.245 - also have "\<dots> \<le> p (y + a \<cdot> x0)" 1.246 - proof (rule linorder_cases) 1.247 - assume z: "a = 0" 1.248 - then have "h y + a * xi = h y" by simp 1.249 - also from a y have "\<dots> \<le> p y" .. 1.250 - also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp 1.251 - finally show ?thesis . 1.252 - next 1.253 - txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"} 1.254 - with @{text ya} taken as @{text "y / a"}: *} 1.255 - assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp 1.256 - from a1 ay 1.257 - have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" .. 1.258 - with lz have "a * xi \<le> 1.259 + by (unfold H'_def sum_def lin_def) blast 1.260 + from y have y': "y \<in> E" .. 1.261 + from y have ay: "inverse a \<cdot> y \<in> H" by simp 1.262 + 1.263 + from h'_def x_rep E HE y x0 have "h' x = h y + a * xi" 1.264 + by (rule h'_definite) 1.265 + also have "\<dots> \<le> p (y + a \<cdot> x0)" 1.266 + proof (rule linorder_cases) 1.267 + assume z: "a = 0" 1.268 + then have "h y + a * xi = h y" by simp 1.269 + also from a y have "\<dots> \<le> p y" .. 1.270 + also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp 1.271 + finally show ?thesis . 1.272 + next 1.273 + txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"} 1.274 + with @{text ya} taken as @{text "y / a"}: *} 1.275 + assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp 1.276 + from a1 ay 1.277 + have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" .. 1.278 + with lz have "a * xi \<le> 1.279 a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))" 1.280 - by (simp add: mult_left_mono_neg order_less_imp_le) 1.281 - 1.282 - also have "\<dots> = 1.283 + by (simp add: mult_left_mono_neg order_less_imp_le) 1.284 + 1.285 + also have "\<dots> = 1.286 - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))" 1.287 - by (simp add: right_diff_distrib) 1.288 - also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) = 1.289 + by (simp add: right_diff_distrib) 1.290 + also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) = 1.291 p (a \<cdot> (inverse a \<cdot> y + x0))" 1.292 - by (simp add: abs_homogenous) 1.293 - also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)" 1.294 - by (simp add: add_mult_distrib1 mult_assoc [symmetric]) 1.295 - also from nz y have "a * (h (inverse a \<cdot> y)) = h y" 1.296 - by simp 1.297 - finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" . 1.298 - then show ?thesis by simp 1.299 - next 1.300 - txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"} 1.301 - with @{text ya} taken as @{text "y / a"}: *} 1.302 - assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp 1.303 - from a2 ay 1.304 - have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" .. 1.305 - with gz have "a * xi \<le> 1.306 + by (simp add: abs_homogenous) 1.307 + also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)" 1.308 + by (simp add: add_mult_distrib1 mult_assoc [symmetric]) 1.309 + also from nz y have "a * (h (inverse a \<cdot> y)) = h y" 1.310 + by simp 1.311 + finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" . 1.312 + then show ?thesis by simp 1.313 + next 1.314 + txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"} 1.315 + with @{text ya} taken as @{text "y / a"}: *} 1.316 + assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp 1.317 + from a2 ay 1.318 + have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" .. 1.319 + with gz have "a * xi \<le> 1.320 a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))" 1.321 - by simp 1.322 - also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)" 1.323 - by (simp add: right_diff_distrib) 1.324 - also from gz x0 y' 1.325 - have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))" 1.326 - by (simp add: abs_homogenous) 1.327 - also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)" 1.328 - by (simp add: add_mult_distrib1 mult_assoc [symmetric]) 1.329 - also from nz y have "a * h (inverse a \<cdot> y) = h y" 1.330 - by simp 1.331 - finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" . 1.332 - then show ?thesis by simp 1.333 + by simp 1.334 + also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)" 1.335 + by (simp add: right_diff_distrib) 1.336 + also from gz x0 y' 1.337 + have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))" 1.338 + by (simp add: abs_homogenous) 1.339 + also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)" 1.340 + by (simp add: add_mult_distrib1 mult_assoc [symmetric]) 1.341 + also from nz y have "a * h (inverse a \<cdot> y) = h y" 1.342 + by simp 1.343 + finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" . 1.344 + then show ?thesis by simp 1.345 + qed 1.346 + also from x_rep have "\<dots> = p x" by (simp only:) 1.347 + finally show ?thesis . 1.348 qed 1.349 - also from x_rep have "\<dots> = p x" by (simp only:) 1.350 - finally show ?thesis . 1.351 qed 1.352 qed 1.353