1(* Title: HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy 2 Author: Gertrud Bauer, TU Munich 3*) 4 5section \<open>The supremum wrt.\ the function order\<close> 6 7theory Hahn_Banach_Sup_Lemmas 8imports Function_Norm Zorn_Lemma 9begin 10 11text \<open> 12 This section contains some lemmas that will be used in the proof of the 13 Hahn-Banach Theorem. In this section the following context is presumed. Let 14 \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of 15 \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of norm-preserving 16 extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will show some properties 17 about the limit function \<open>h\<close>, i.e.\ the supremum of the chain \<open>c\<close>. 18 19 \<^medskip> 20 Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let 21 \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of one of 22 the elements of the chain. 23\<close> 24 25lemmas [dest?] = chainsD 26lemmas chainsE2 [elim?] = chainsD2 [elim_format] 27 28lemma some_H'h't: 29 assumes M: "M = norm_pres_extensions E p F f" 30 and cM: "c \<in> chains M" 31 and u: "graph H h = \<Union>c" 32 and x: "x \<in> H" 33 shows "\<exists>H' h'. graph H' h' \<in> c 34 \<and> (x, h x) \<in> graph H' h' 35 \<and> linearform H' h' \<and> H' \<unlhd> E 36 \<and> F \<unlhd> H' \<and> graph F f \<subseteq> graph H' h' 37 \<and> (\<forall>x \<in> H'. h' x \<le> p x)" 38proof - 39 from x have "(x, h x) \<in> graph H h" .. 40 also from u have "\<dots> = \<Union>c" . 41 finally obtain g where gc: "g \<in> c" and gh: "(x, h x) \<in> g" by blast 42 43 from cM have "c \<subseteq> M" .. 44 with gc have "g \<in> M" .. 45 also from M have "\<dots> = norm_pres_extensions E p F f" . 46 finally obtain H' and h' where g: "g = graph H' h'" 47 and * : "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'" 48 "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" .. 49 50 from gc and g have "graph H' h' \<in> c" by (simp only:) 51 moreover from gh and g have "(x, h x) \<in> graph H' h'" by (simp only:) 52 ultimately show ?thesis using * by blast 53qed 54 55text \<open> 56 \<^medskip> 57 Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let 58 \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of the 59 supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, such 60 that \<open>h\<close> extends \<open>h'\<close>. 61\<close> 62 63lemma some_H'h': 64 assumes M: "M = norm_pres_extensions E p F f" 65 and cM: "c \<in> chains M" 66 and u: "graph H h = \<Union>c" 67 and x: "x \<in> H" 68 shows "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h 69 \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H' 70 \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)" 71proof - 72 from M cM u x obtain H' h' where 73 x_hx: "(x, h x) \<in> graph H' h'" 74 and c: "graph H' h' \<in> c" 75 and * : "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'" 76 "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" 77 by (rule some_H'h't [elim_format]) blast 78 from x_hx have "x \<in> H'" .. 79 moreover from cM u c have "graph H' h' \<subseteq> graph H h" by blast 80 ultimately show ?thesis using * by blast 81qed 82 83text \<open> 84 \<^medskip> 85 Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function \<open>h\<close> 86 are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends 87 \<open>h'\<close>. 88\<close> 89 90lemma some_H'h'2: 91 assumes M: "M = norm_pres_extensions E p F f" 92 and cM: "c \<in> chains M" 93 and u: "graph H h = \<Union>c" 94 and x: "x \<in> H" 95 and y: "y \<in> H" 96 shows "\<exists>H' h'. x \<in> H' \<and> y \<in> H' 97 \<and> graph H' h' \<subseteq> graph H h 98 \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H' 99 \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)" 100proof - 101 txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>, such that \<open>h\<close> 102 extends \<open>h''\<close>.\<close> 103 104 from M cM u and y obtain H' h' where 105 y_hy: "(y, h y) \<in> graph H' h'" 106 and c': "graph H' h' \<in> c" 107 and * : 108 "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'" 109 "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" 110 by (rule some_H'h't [elim_format]) blast 111 112 txt \<open>\<open>x\<close> is in the domain \<open>H'\<close> of some function \<open>h'\<close>, 113 such that \<open>h\<close> extends \<open>h'\<close>.\<close> 114 115 from M cM u and x obtain H'' h'' where 116 x_hx: "(x, h x) \<in> graph H'' h''" 117 and c'': "graph H'' h'' \<in> c" 118 and ** : 119 "linearform H'' h''" "H'' \<unlhd> E" "F \<unlhd> H''" 120 "graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x" 121 by (rule some_H'h't [elim_format]) blast 122 123 txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain, \<open>h''\<close> is an 124 extension of \<open>h'\<close> or vice versa. Thus both \<open>x\<close> and \<open>y\<close> are contained in 125 the greater one. \label{cases1}\<close> 126 127 from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''" 128 by (blast dest: chainsD) 129 then show ?thesis 130 proof cases 131 case 1 132 have "(x, h x) \<in> graph H'' h''" by fact 133 also have "\<dots> \<subseteq> graph H' h'" by fact 134 finally have xh:"(x, h x) \<in> graph H' h'" . 135 then have "x \<in> H'" .. 136 moreover from y_hy have "y \<in> H'" .. 137 moreover from cM u and c' have "graph H' h' \<subseteq> graph H h" by blast 138 ultimately show ?thesis using * by blast 139 next 140 case 2 141 from x_hx have "x \<in> H''" .. 142 moreover have "y \<in> H''" 143 proof - 144 have "(y, h y) \<in> graph H' h'" by (rule y_hy) 145 also have "\<dots> \<subseteq> graph H'' h''" by fact 146 finally have "(y, h y) \<in> graph H'' h''" . 147 then show ?thesis .. 148 qed 149 moreover from u c'' have "graph H'' h'' \<subseteq> graph H h" by blast 150 ultimately show ?thesis using ** by blast 151 qed 152qed 153 154text \<open> 155 \<^medskip> 156 The relation induced by the graph of the supremum of a chain \<open>c\<close> is 157 definite, i.e.\ it is the graph of a function. 158\<close> 159 160lemma sup_definite: 161 assumes M_def: "M = norm_pres_extensions E p F f" 162 and cM: "c \<in> chains M" 163 and xy: "(x, y) \<in> \<Union>c" 164 and xz: "(x, z) \<in> \<Union>c" 165 shows "z = y" 166proof - 167 from cM have c: "c \<subseteq> M" .. 168 from xy obtain G1 where xy': "(x, y) \<in> G1" and G1: "G1 \<in> c" .. 169 from xz obtain G2 where xz': "(x, z) \<in> G2" and G2: "G2 \<in> c" .. 170 171 from G1 c have "G1 \<in> M" .. 172 then obtain H1 h1 where G1_rep: "G1 = graph H1 h1" 173 unfolding M_def by blast 174 175 from G2 c have "G2 \<in> M" .. 176 then obtain H2 h2 where G2_rep: "G2 = graph H2 h2" 177 unfolding M_def by blast 178 179 txt \<open>\<open>G\<^sub>1\<close> is contained in \<open>G\<^sub>2\<close> or vice versa, since both \<open>G\<^sub>1\<close> and \<open>G\<^sub>2\<close> 180 are members of \<open>c\<close>. \label{cases2}\<close> 181 182 from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1" 183 by (blast dest: chainsD) 184 then show ?thesis 185 proof cases 186 case 1 187 with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast 188 then have "y = h2 x" .. 189 also 190 from xz' G2_rep have "(x, z) \<in> graph H2 h2" by (simp only:) 191 then have "z = h2 x" .. 192 finally show ?thesis . 193 next 194 case 2 195 with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast 196 then have "z = h1 x" .. 197 also 198 from xy' G1_rep have "(x, y) \<in> graph H1 h1" by (simp only:) 199 then have "y = h1 x" .. 200 finally show ?thesis .. 201 qed 202qed 203 204text \<open> 205 \<^medskip> 206 The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close> is 207 in the domain of a function \<open>h'\<close> in the chain of norm preserving extensions. 208 Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function values of \<open>x\<close> are 209 identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close> is linear by 210 construction of \<open>M\<close>. 211\<close> 212 213lemma sup_lf: 214 assumes M: "M = norm_pres_extensions E p F f" 215 and cM: "c \<in> chains M" 216 and u: "graph H h = \<Union>c" 217 shows "linearform H h" 218proof 219 fix x y assume x: "x \<in> H" and y: "y \<in> H" 220 with M cM u obtain H' h' where 221 x': "x \<in> H'" and y': "y \<in> H'" 222 and b: "graph H' h' \<subseteq> graph H h" 223 and linearform: "linearform H' h'" 224 and subspace: "H' \<unlhd> E" 225 by (rule some_H'h'2 [elim_format]) blast 226 227 show "h (x + y) = h x + h y" 228 proof - 229 from linearform x' y' have "h' (x + y) = h' x + h' y" 230 by (rule linearform.add) 231 also from b x' have "h' x = h x" .. 232 also from b y' have "h' y = h y" .. 233 also from subspace x' y' have "x + y \<in> H'" 234 by (rule subspace.add_closed) 235 with b have "h' (x + y) = h (x + y)" .. 236 finally show ?thesis . 237 qed 238next 239 fix x a assume x: "x \<in> H" 240 with M cM u obtain H' h' where 241 x': "x \<in> H'" 242 and b: "graph H' h' \<subseteq> graph H h" 243 and linearform: "linearform H' h'" 244 and subspace: "H' \<unlhd> E" 245 by (rule some_H'h' [elim_format]) blast 246 247 show "h (a \<cdot> x) = a * h x" 248 proof - 249 from linearform x' have "h' (a \<cdot> x) = a * h' x" 250 by (rule linearform.mult) 251 also from b x' have "h' x = h x" .. 252 also from subspace x' have "a \<cdot> x \<in> H'" 253 by (rule subspace.mult_closed) 254 with b have "h' (a \<cdot> x) = h (a \<cdot> x)" .. 255 finally show ?thesis . 256 qed 257qed 258 259text \<open> 260 \<^medskip> 261 The limit of a non-empty chain of norm preserving extensions of \<open>f\<close> is an 262 extension of \<open>f\<close>, since every element of the chain is an extension of \<open>f\<close> 263 and the supremum is an extension for every element of the chain. 264\<close> 265 266lemma sup_ext: 267 assumes graph: "graph H h = \<Union>c" 268 and M: "M = norm_pres_extensions E p F f" 269 and cM: "c \<in> chains M" 270 and ex: "\<exists>x. x \<in> c" 271 shows "graph F f \<subseteq> graph H h" 272proof - 273 from ex obtain x where xc: "x \<in> c" .. 274 from cM have "c \<subseteq> M" .. 275 with xc have "x \<in> M" .. 276 with M have "x \<in> norm_pres_extensions E p F f" 277 by (simp only:) 278 then obtain G g where "x = graph G g" and "graph F f \<subseteq> graph G g" .. 279 then have "graph F f \<subseteq> x" by (simp only:) 280 also from xc have "\<dots> \<subseteq> \<Union>c" by blast 281 also from graph have "\<dots> = graph H h" .. 282 finally show ?thesis . 283qed 284 285text \<open> 286 \<^medskip> 287 The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is a 288 subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure 289 properties follow from the fact that \<open>F\<close> is a vector space. 290\<close> 291 292lemma sup_supF: 293 assumes graph: "graph H h = \<Union>c" 294 and M: "M = norm_pres_extensions E p F f" 295 and cM: "c \<in> chains M" 296 and ex: "\<exists>x. x \<in> c" 297 and FE: "F \<unlhd> E" 298 shows "F \<unlhd> H" 299proof 300 from FE show "F \<noteq> {}" by (rule subspace.non_empty) 301 from graph M cM ex have "graph F f \<subseteq> graph H h" by (rule sup_ext) 302 then show "F \<subseteq> H" .. 303 fix x y assume "x \<in> F" and "y \<in> F" 304 with FE show "x + y \<in> F" by (rule subspace.add_closed) 305next 306 fix x a assume "x \<in> F" 307 with FE show "a \<cdot> x \<in> F" by (rule subspace.mult_closed) 308qed 309 310text \<open> 311 \<^medskip> 312 The domain \<open>H\<close> of the limit function is a subspace of \<open>E\<close>. 313\<close> 314 315lemma sup_subE: 316 assumes graph: "graph H h = \<Union>c" 317 and M: "M = norm_pres_extensions E p F f" 318 and cM: "c \<in> chains M" 319 and ex: "\<exists>x. x \<in> c" 320 and FE: "F \<unlhd> E" 321 and E: "vectorspace E" 322 shows "H \<unlhd> E" 323proof 324 show "H \<noteq> {}" 325 proof - 326 from FE E have "0 \<in> F" by (rule subspace.zero) 327 also from graph M cM ex FE have "F \<unlhd> H" by (rule sup_supF) 328 then have "F \<subseteq> H" .. 329 finally show ?thesis by blast 330 qed 331 show "H \<subseteq> E" 332 proof 333 fix x assume "x \<in> H" 334 with M cM graph 335 obtain H' where x: "x \<in> H'" and H'E: "H' \<unlhd> E" 336 by (rule some_H'h' [elim_format]) blast 337 from H'E have "H' \<subseteq> E" .. 338 with x show "x \<in> E" .. 339 qed 340 fix x y assume x: "x \<in> H" and y: "y \<in> H" 341 show "x + y \<in> H" 342 proof - 343 from M cM graph x y obtain H' h' where 344 x': "x \<in> H'" and y': "y \<in> H'" and H'E: "H' \<unlhd> E" 345 and graphs: "graph H' h' \<subseteq> graph H h" 346 by (rule some_H'h'2 [elim_format]) blast 347 from H'E x' y' have "x + y \<in> H'" 348 by (rule subspace.add_closed) 349 also from graphs have "H' \<subseteq> H" .. 350 finally show ?thesis . 351 qed 352next 353 fix x a assume x: "x \<in> H" 354 show "a \<cdot> x \<in> H" 355 proof - 356 from M cM graph x 357 obtain H' h' where x': "x \<in> H'" and H'E: "H' \<unlhd> E" 358 and graphs: "graph H' h' \<subseteq> graph H h" 359 by (rule some_H'h' [elim_format]) blast 360 from H'E x' have "a \<cdot> x \<in> H'" by (rule subspace.mult_closed) 361 also from graphs have "H' \<subseteq> H" .. 362 finally show ?thesis . 363 qed 364qed 365 366text \<open> 367 \<^medskip> 368 The limit function is bounded by the norm \<open>p\<close> as well, since all elements in 369 the chain are bounded by \<open>p\<close>. 370\<close> 371 372lemma sup_norm_pres: 373 assumes graph: "graph H h = \<Union>c" 374 and M: "M = norm_pres_extensions E p F f" 375 and cM: "c \<in> chains M" 376 shows "\<forall>x \<in> H. h x \<le> p x" 377proof 378 fix x assume "x \<in> H" 379 with M cM graph obtain H' h' where x': "x \<in> H'" 380 and graphs: "graph H' h' \<subseteq> graph H h" 381 and a: "\<forall>x \<in> H'. h' x \<le> p x" 382 by (rule some_H'h' [elim_format]) blast 383 from graphs x' have [symmetric]: "h' x = h x" .. 384 also from a x' have "h' x \<le> p x " .. 385 finally show "h x \<le> p x" . 386qed 387 388text \<open> 389 \<^medskip> 390 The following lemma is a property of linear forms on real vector spaces. It 391 will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page 392 \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces the 393 following inequality are equivalent: 394 \begin{center} 395 \begin{tabular}{lll} 396 \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and & 397 \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\ 398 \end{tabular} 399 \end{center} 400\<close> 401 402lemma abs_ineq_iff: 403 assumes "subspace H E" and "vectorspace E" and "seminorm E p" 404 and "linearform H h" 405 shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R") 406proof 407 interpret subspace H E by fact 408 interpret vectorspace E by fact 409 interpret seminorm E p by fact 410 interpret linearform H h by fact 411 have H: "vectorspace H" using \<open>vectorspace E\<close> .. 412 { 413 assume l: ?L 414 show ?R 415 proof 416 fix x assume x: "x \<in> H" 417 have "h x \<le> \<bar>h x\<bar>" by arith 418 also from l x have "\<dots> \<le> p x" .. 419 finally show "h x \<le> p x" . 420 qed 421 next 422 assume r: ?R 423 show ?L 424 proof 425 fix x assume x: "x \<in> H" 426 show "\<bar>b\<bar> \<le> a" when "- a \<le> b" "b \<le> a" for a b :: real 427 using that by arith 428 from \<open>linearform H h\<close> and H x 429 have "- h x = h (- x)" by (rule linearform.neg [symmetric]) 430 also 431 from H x have "- x \<in> H" by (rule vectorspace.neg_closed) 432 with r have "h (- x) \<le> p (- x)" .. 433 also have "\<dots> = p x" 434 using \<open>seminorm E p\<close> \<open>vectorspace E\<close> 435 proof (rule seminorm.minus) 436 from x show "x \<in> E" .. 437 qed 438 finally have "- h x \<le> p x" . 439 then show "- p x \<le> h x" by simp 440 from r x show "h x \<le> p x" .. 441 qed 442 } 443qed 444 445end 446