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.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.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.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.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.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.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.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.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.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.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.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.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