1(* Title: HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy 2 Author: Gertrud Bauer, TU Munich 3*) 4 5section \<open>Extending non-maximal functions\<close> 6 7theory Hahn_Banach_Ext_Lemmas 8imports Function_Norm 9begin 10 11text \<open> 12 In this section the following context is presumed. Let \<open>E\<close> be a real vector 13 space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close> a linear 14 function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a superspace of 15 \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close> and \<open>x\<^sub>0\<close> is an 16 element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H' = H + lin x\<^sub>0\<close>, so 17 for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close> with \<open>y \<in> H\<close> is 18 unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close> for a certain \<open>\<xi>\<close>. 19 20 Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>. 21 22 \<^medskip> 23 This lemma will be used to show the existence of a linear extension of \<open>f\<close> 24 (see page \pageref{ex-xi-use}). It is a consequence of the completeness of 25 \<open>\<real>\<close>. To show 26 \begin{center} 27 \begin{tabular}{l} 28 \<open>\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y\<close> 29 \end{tabular} 30 \end{center} 31 \<^noindent> it suffices to show that 32 \begin{center} 33 \begin{tabular}{l} 34 \<open>\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v\<close> 35 \end{tabular} 36 \end{center} 37\<close> 38 39lemma ex_xi: 40 assumes "vectorspace F" 41 assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v" 42 shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" 43proof - 44 interpret vectorspace F by fact 45 txt \<open>From the completeness of the reals follows: 46 The set \<open>S = {a u. u \<in> F}\<close> has a supremum, if it is 47 non-empty and has an upper bound.\<close> 48 49 let ?S = "{a u | u. u \<in> F}" 50 have "\<exists>xi. lub ?S xi" 51 proof (rule real_complete) 52 have "a 0 \<in> ?S" by blast 53 then show "\<exists>X. X \<in> ?S" .. 54 have "\<forall>y \<in> ?S. y \<le> b 0" 55 proof 56 fix y assume y: "y \<in> ?S" 57 then obtain u where u: "u \<in> F" and y: "y = a u" by blast 58 from u and zero have "a u \<le> b 0" by (rule r) 59 with y show "y \<le> b 0" by (simp only:) 60 qed 61 then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" .. 62 qed 63 then obtain xi where xi: "lub ?S xi" .. 64 { 65 fix y assume "y \<in> F" 66 then have "a y \<in> ?S" by blast 67 with xi have "a y \<le> xi" by (rule lub.upper) 68 } 69 moreover { 70 fix y assume y: "y \<in> F" 71 from xi have "xi \<le> b y" 72 proof (rule lub.least) 73 fix au assume "au \<in> ?S" 74 then obtain u where u: "u \<in> F" and au: "au = a u" by blast 75 from u y have "a u \<le> b y" by (rule r) 76 with au show "au \<le> b y" by (simp only:) 77 qed 78 } 79 ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast 80qed 81 82text \<open> 83 \<^medskip> 84 The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where \<open>x = y + a \<cdot> \<xi>\<close> 85 is a linear extension of \<open>h\<close> to \<open>H'\<close>. 86\<close> 87 88lemma h'_lf: 89 assumes h'_def: "\<And>x. h' x = (let (y, a) = 90 SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi)" 91 and H'_def: "H' = H + lin x0" 92 and HE: "H \<unlhd> E" 93 assumes "linearform H h" 94 assumes x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" 95 assumes E: "vectorspace E" 96 shows "linearform H' h'" 97proof - 98 interpret linearform H h by fact 99 interpret vectorspace E by fact 100 show ?thesis 101 proof 102 note E = \<open>vectorspace E\<close> 103 have H': "vectorspace H'" 104 proof (unfold H'_def) 105 from \<open>x0 \<in> E\<close> 106 have "lin x0 \<unlhd> E" .. 107 with HE show "vectorspace (H + lin x0)" using E .. 108 qed 109 { 110 fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'" 111 show "h' (x1 + x2) = h' x1 + h' x2" 112 proof - 113 from H' x1 x2 have "x1 + x2 \<in> H'" 114 by (rule vectorspace.add_closed) 115 with x1 x2 obtain y y1 y2 a a1 a2 where 116 x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H" 117 and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H" 118 and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H" 119 unfolding H'_def sum_def lin_def by blast 120 121 have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0 122 proof (rule decomp_H') text_raw \<open>\label{decomp-H-use}\<close> 123 from HE y1 y2 show "y1 + y2 \<in> H" 124 by (rule subspace.add_closed) 125 from x0 and HE y y1 y2 126 have "x0 \<in> E" "y \<in> E" "y1 \<in> E" "y2 \<in> E" by auto 127 with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2" 128 by (simp add: add_ac add_mult_distrib2) 129 also note x1x2 130 finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" . 131 qed 132 133 from h'_def x1x2 E HE y x0 134 have "h' (x1 + x2) = h y + a * xi" 135 by (rule h'_definite) 136 also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi" 137 by (simp only: ya) 138 also from y1 y2 have "h (y1 + y2) = h y1 + h y2" 139 by simp 140 also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)" 141 by (simp add: distrib_right) 142 also from h'_def x1_rep E HE y1 x0 143 have "h y1 + a1 * xi = h' x1" 144 by (rule h'_definite [symmetric]) 145 also from h'_def x2_rep E HE y2 x0 146 have "h y2 + a2 * xi = h' x2" 147 by (rule h'_definite [symmetric]) 148 finally show ?thesis . 149 qed 150 next 151 fix x1 c assume x1: "x1 \<in> H'" 152 show "h' (c \<cdot> x1) = c * (h' x1)" 153 proof - 154 from H' x1 have ax1: "c \<cdot> x1 \<in> H'" 155 by (rule vectorspace.mult_closed) 156 with x1 obtain y a y1 a1 where 157 cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H" 158 and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H" 159 unfolding H'_def sum_def lin_def by blast 160 161 have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0 162 proof (rule decomp_H') 163 from HE y1 show "c \<cdot> y1 \<in> H" 164 by (rule subspace.mult_closed) 165 from x0 and HE y y1 166 have "x0 \<in> E" "y \<in> E" "y1 \<in> E" by auto 167 with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1" 168 by (simp add: mult_assoc add_mult_distrib1) 169 also note cx1_rep 170 finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" . 171 qed 172 173 from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi" 174 by (rule h'_definite) 175 also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi" 176 by (simp only: ya) 177 also from y1 have "h (c \<cdot> y1) = c * h y1" 178 by simp 179 also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)" 180 by (simp only: distrib_left) 181 also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1" 182 by (rule h'_definite [symmetric]) 183 finally show ?thesis . 184 qed 185 } 186 qed 187qed 188 189text \<open> 190 \<^medskip> 191 The linear extension \<open>h'\<close> of \<open>h\<close> is bounded by the seminorm \<open>p\<close>. 192\<close> 193 194lemma h'_norm_pres: 195 assumes h'_def: "\<And>x. h' x = (let (y, a) = 196 SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi)" 197 and H'_def: "H' = H + lin x0" 198 and x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" 199 assumes E: "vectorspace E" and HE: "subspace H E" 200 and "seminorm E p" and "linearform H h" 201 assumes a: "\<forall>y \<in> H. h y \<le> p y" 202 and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y" 203 shows "\<forall>x \<in> H'. h' x \<le> p x" 204proof - 205 interpret vectorspace E by fact 206 interpret subspace H E by fact 207 interpret seminorm E p by fact 208 interpret linearform H h by fact 209 show ?thesis 210 proof 211 fix x assume x': "x \<in> H'" 212 show "h' x \<le> p x" 213 proof - 214 from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi" 215 and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto 216 from x' obtain y a where 217 x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H" 218 unfolding H'_def sum_def lin_def by blast 219 from y have y': "y \<in> E" .. 220 from y have ay: "inverse a \<cdot> y \<in> H" by simp 221 222 from h'_def x_rep E HE y x0 have "h' x = h y + a * xi" 223 by (rule h'_definite) 224 also have "\<dots> \<le> p (y + a \<cdot> x0)" 225 proof (rule linorder_cases) 226 assume z: "a = 0" 227 then have "h y + a * xi = h y" by simp 228 also from a y have "\<dots> \<le> p y" .. 229 also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp 230 finally show ?thesis . 231 next 232 txt \<open>In the case \<open>a < 0\<close>, we use \<open>a\<^sub>1\<close> 233 with \<open>ya\<close> taken as \<open>y / a\<close>:\<close> 234 assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp 235 from a1 ay 236 have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" .. 237 with lz have "a * xi \<le> 238 a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))" 239 by (simp add: mult_left_mono_neg order_less_imp_le) 240 241 also have "\<dots> = 242 - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))" 243 by (simp add: right_diff_distrib) 244 also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) = 245 p (a \<cdot> (inverse a \<cdot> y + x0))" 246 by (simp add: abs_homogenous) 247 also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)" 248 by (simp add: add_mult_distrib1 mult_assoc [symmetric]) 249 also from nz y have "a * (h (inverse a \<cdot> y)) = h y" 250 by simp 251 finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" . 252 then show ?thesis by simp 253 next 254 txt \<open>In the case \<open>a > 0\<close>, we use \<open>a\<^sub>2\<close> 255 with \<open>ya\<close> taken as \<open>y / a\<close>:\<close> 256 assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp 257 from a2 ay 258 have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" .. 259 with gz have "a * xi \<le> 260 a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))" 261 by simp 262 also have "\<dots> = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)" 263 by (simp add: right_diff_distrib) 264 also from gz x0 y' 265 have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))" 266 by (simp add: abs_homogenous) 267 also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)" 268 by (simp add: add_mult_distrib1 mult_assoc [symmetric]) 269 also from nz y have "a * h (inverse a \<cdot> y) = h y" 270 by simp 271 finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" . 272 then show ?thesis by simp 273 qed 274 also from x_rep have "\<dots> = p x" by (simp only:) 275 finally show ?thesis . 276 qed 277 qed 278qed 279 280end 281