author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45605  a89b4bc311a5 
child 52183  667961fa6a60 
permissions  rwrr 
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

1 
(* Title: HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy 
7917  2 
Author: Gertrud Bauer, TU Munich 
3 
*) 

4 

9261  5 
header {* The supremum w.r.t.~the function order *} 
7917  6 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

7 
theory Hahn_Banach_Sup_Lemmas 
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

8 
imports Function_Norm Zorn_Lemma 
27612  9 
begin 
9256  10 

10687  11 
text {* 
12 
This section contains some lemmas that will be used in the proof of 

13 
the HahnBanach Theorem. In this section the following context is 

14 
presumed. Let @{text E} be a real vector space with a seminorm 

15 
@{text p} on @{text E}. @{text F} is a subspace of @{text E} and 

16 
@{text f} a linear form on @{text F}. We consider a chain @{text c} 

13515  17 
of normpreserving extensions of @{text f}, such that @{text "\<Union>c = 
18 
graph H h"}. We will show some properties about the limit function 

19 
@{text h}, i.e.\ the supremum of the chain @{text c}. 

7917  20 

13515  21 
\medskip Let @{text c} be a chain of normpreserving extensions of 
22 
the function @{text f} and let @{text "graph H h"} be the supremum 

23 
of @{text c}. Every element in @{text H} is member of one of the 

10687  24 
elements of the chain. 
25 
*} 

14710  26 
lemmas [dest?] = chainD 
45605  27 
lemmas chainE2 [elim?] = chainD2 [elim_format] 
7917  28 

29 
lemma some_H'h't: 

13515  30 
assumes M: "M = norm_pres_extensions E p F f" 
31 
and cM: "c \<in> chain M" 

32 
and u: "graph H h = \<Union>c" 

33 
and x: "x \<in> H" 

34 
shows "\<exists>H' h'. graph H' h' \<in> c 

35 
\<and> (x, h x) \<in> graph H' h' 

36 
\<and> linearform H' h' \<and> H' \<unlhd> E 

37 
\<and> F \<unlhd> H' \<and> graph F f \<subseteq> graph H' h' 

38 
\<and> (\<forall>x \<in> H'. h' x \<le> p x)" 

9261  39 
proof  
13515  40 
from x have "(x, h x) \<in> graph H h" .. 
41 
also from u have "\<dots> = \<Union>c" . 

42 
finally obtain g where gc: "g \<in> c" and gh: "(x, h x) \<in> g" by blast 

7917  43 

13515  44 
from cM have "c \<subseteq> M" .. 
45 
with gc have "g \<in> M" .. 

46 
also from M have "\<dots> = norm_pres_extensions E p F f" . 

47 
finally obtain H' and h' where g: "g = graph H' h'" 

48 
and * : "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'" 

49 
"graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" .. 

50 

51 
from gc and g have "graph H' h' \<in> c" by (simp only:) 

52 
moreover from gh and g have "(x, h x) \<in> graph H' h'" by (simp only:) 

53 
ultimately show ?thesis using * by blast 

9261  54 
qed 
7917  55 

10687  56 
text {* 
57 
\medskip Let @{text c} be a chain of normpreserving extensions of 

58 
the function @{text f} and let @{text "graph H h"} be the supremum 

59 
of @{text c}. Every element in the domain @{text H} of the supremum 

60 
function is member of the domain @{text H'} of some function @{text 

61 
h'}, such that @{text h} extends @{text h'}. 

9261  62 
*} 
7917  63 

10687  64 
lemma some_H'h': 
13515  65 
assumes M: "M = norm_pres_extensions E p F f" 
66 
and cM: "c \<in> chain M" 

67 
and u: "graph H h = \<Union>c" 

68 
and x: "x \<in> H" 

69 
shows "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h 

70 
\<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H' 

71 
\<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)" 

9261  72 
proof  
13515  73 
from M cM u x obtain H' h' where 
74 
x_hx: "(x, h x) \<in> graph H' h'" 

75 
and c: "graph H' h' \<in> c" 

76 
and * : "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'" 

10687  77 
"graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" 
13515  78 
by (rule some_H'h't [elim_format]) blast 
79 
from x_hx have "x \<in> H'" .. 

80 
moreover from cM u c have "graph H' h' \<subseteq> graph H h" 

81 
by (simp only: chain_ball_Union_upper) 

82 
ultimately show ?thesis using * by blast 

9261  83 
qed 
7917  84 

10687  85 
text {* 
86 
\medskip Any two elements @{text x} and @{text y} in the domain 

87 
@{text H} of the supremum function @{text h} are both in the domain 

88 
@{text H'} of some function @{text h'}, such that @{text h} extends 

89 
@{text h'}. 

90 
*} 

7917  91 

10687  92 
lemma some_H'h'2: 
13515  93 
assumes M: "M = norm_pres_extensions E p F f" 
94 
and cM: "c \<in> chain M" 

95 
and u: "graph H h = \<Union>c" 

96 
and x: "x \<in> H" 

97 
and y: "y \<in> H" 

98 
shows "\<exists>H' h'. x \<in> H' \<and> y \<in> H' 

99 
\<and> graph H' h' \<subseteq> graph H h 

100 
\<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H' 

101 
\<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)" 

9261  102 
proof  
10687  103 
txt {* @{text y} is in the domain @{text H''} of some function @{text h''}, 
104 
such that @{text h} extends @{text h''}. *} 

7917  105 

13515  106 
from M cM u and y obtain H' h' where 
107 
y_hy: "(y, h y) \<in> graph H' h'" 

108 
and c': "graph H' h' \<in> c" 

109 
and * : 

110 
"linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'" 

111 
"graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" 

112 
by (rule some_H'h't [elim_format]) blast 

113 

114 
txt {* @{text x} is in the domain @{text H'} of some function @{text h'}, 

115 
such that @{text h} extends @{text h'}. *} 

7917  116 

13515  117 
from M cM u and x obtain H'' h'' where 
118 
x_hx: "(x, h x) \<in> graph H'' h''" 

119 
and c'': "graph H'' h'' \<in> c" 

120 
and ** : 

121 
"linearform H'' h''" "H'' \<unlhd> E" "F \<unlhd> H''" 

122 
"graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x" 

123 
by (rule some_H'h't [elim_format]) blast 

7917  124 

13515  125 
txt {* Since both @{text h'} and @{text h''} are elements of the chain, 
126 
@{text h''} is an extension of @{text h'} or vice versa. Thus both 

127 
@{text x} and @{text y} are contained in the greater 

128 
one. \label{cases1}*} 

7917  129 

23378  130 
from cM c'' c' have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''" 
13515  131 
(is "?case1 \<or> ?case2") .. 
132 
then show ?thesis 

133 
proof 

134 
assume ?case1 

23378  135 
have "(x, h x) \<in> graph H'' h''" by fact 
27612  136 
also have "\<dots> \<subseteq> graph H' h'" by fact 
13515  137 
finally have xh:"(x, h x) \<in> graph H' h'" . 
138 
then have "x \<in> H'" .. 

139 
moreover from y_hy have "y \<in> H'" .. 

140 
moreover from cM u and c' have "graph H' h' \<subseteq> graph H h" 

141 
by (simp only: chain_ball_Union_upper) 

142 
ultimately show ?thesis using * by blast 

143 
next 

144 
assume ?case2 

145 
from x_hx have "x \<in> H''" .. 

146 
moreover { 

23378  147 
have "(y, h y) \<in> graph H' h'" by (rule y_hy) 
148 
also have "\<dots> \<subseteq> graph H'' h''" by fact 

13515  149 
finally have "(y, h y) \<in> graph H'' h''" . 
150 
} then have "y \<in> H''" .. 

151 
moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h" 

152 
by (simp only: chain_ball_Union_upper) 

153 
ultimately show ?thesis using ** by blast 

9261  154 
qed 
155 
qed 

7917  156 

10687  157 
text {* 
158 
\medskip The relation induced by the graph of the supremum of a 

13515  159 
chain @{text c} is definite, i.~e.~t is the graph of a function. 
160 
*} 

7917  161 

10687  162 
lemma sup_definite: 
13515  163 
assumes M_def: "M \<equiv> norm_pres_extensions E p F f" 
164 
and cM: "c \<in> chain M" 

165 
and xy: "(x, y) \<in> \<Union>c" 

166 
and xz: "(x, z) \<in> \<Union>c" 

167 
shows "z = y" 

10687  168 
proof  
13515  169 
from cM have c: "c \<subseteq> M" .. 
170 
from xy obtain G1 where xy': "(x, y) \<in> G1" and G1: "G1 \<in> c" .. 

171 
from xz obtain G2 where xz': "(x, z) \<in> G2" and G2: "G2 \<in> c" .. 

7917  172 

13515  173 
from G1 c have "G1 \<in> M" .. 
174 
then obtain H1 h1 where G1_rep: "G1 = graph H1 h1" 

27612  175 
unfolding M_def by blast 
7917  176 

13515  177 
from G2 c have "G2 \<in> M" .. 
178 
then obtain H2 h2 where G2_rep: "G2 = graph H2 h2" 

27612  179 
unfolding M_def by blast 
7917  180 

13515  181 
txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"} 
182 
or vice versa, since both @{text "G\<^sub>1"} and @{text 

183 
"G\<^sub>2"} are members of @{text c}. \label{cases2}*} 

7917  184 

13515  185 
from cM G1 G2 have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") .. 
186 
then show ?thesis 

187 
proof 

188 
assume ?case1 

189 
with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast 

27612  190 
then have "y = h2 x" .. 
13515  191 
also 
192 
from xz' G2_rep have "(x, z) \<in> graph H2 h2" by (simp only:) 

27612  193 
then have "z = h2 x" .. 
13515  194 
finally show ?thesis . 
195 
next 

196 
assume ?case2 

197 
with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast 

27612  198 
then have "z = h1 x" .. 
13515  199 
also 
200 
from xy' G1_rep have "(x, y) \<in> graph H1 h1" by (simp only:) 

27612  201 
then have "y = h1 x" .. 
13515  202 
finally show ?thesis .. 
9261  203 
qed 
204 
qed 

7917  205 

10687  206 
text {* 
207 
\medskip The limit function @{text h} is linear. Every element 

208 
@{text x} in the domain of @{text h} is in the domain of a function 

209 
@{text h'} in the chain of norm preserving extensions. Furthermore, 

210 
@{text h} is an extension of @{text h'} so the function values of 

211 
@{text x} are identical for @{text h'} and @{text h}. Finally, the 

212 
function @{text h'} is linear by construction of @{text M}. 

213 
*} 

7917  214 

10687  215 
lemma sup_lf: 
13515  216 
assumes M: "M = norm_pres_extensions E p F f" 
217 
and cM: "c \<in> chain M" 

218 
and u: "graph H h = \<Union>c" 

219 
shows "linearform H h" 

220 
proof 

221 
fix x y assume x: "x \<in> H" and y: "y \<in> H" 

222 
with M cM u obtain H' h' where 

223 
x': "x \<in> H'" and y': "y \<in> H'" 

224 
and b: "graph H' h' \<subseteq> graph H h" 

225 
and linearform: "linearform H' h'" 

226 
and subspace: "H' \<unlhd> E" 

227 
by (rule some_H'h'2 [elim_format]) blast 

7917  228 

13515  229 
show "h (x + y) = h x + h y" 
230 
proof  

231 
from linearform x' y' have "h' (x + y) = h' x + h' y" 

232 
by (rule linearform.add) 

233 
also from b x' have "h' x = h x" .. 

234 
also from b y' have "h' y = h y" .. 

235 
also from subspace x' y' have "x + y \<in> H'" 

236 
by (rule subspace.add_closed) 

237 
with b have "h' (x + y) = h (x + y)" .. 

238 
finally show ?thesis . 

239 
qed 

240 
next 

241 
fix x a assume x: "x \<in> H" 

242 
with M cM u obtain H' h' where 

243 
x': "x \<in> H'" 

244 
and b: "graph H' h' \<subseteq> graph H h" 

245 
and linearform: "linearform H' h'" 

246 
and subspace: "H' \<unlhd> E" 

247 
by (rule some_H'h' [elim_format]) blast 

7917  248 

13515  249 
show "h (a \<cdot> x) = a * h x" 
250 
proof  

251 
from linearform x' have "h' (a \<cdot> x) = a * h' x" 

252 
by (rule linearform.mult) 

253 
also from b x' have "h' x = h x" .. 

254 
also from subspace x' have "a \<cdot> x \<in> H'" 

255 
by (rule subspace.mult_closed) 

256 
with b have "h' (a \<cdot> x) = h (a \<cdot> x)" .. 

257 
finally show ?thesis . 

9261  258 
qed 
259 
qed 

7917  260 

10687  261 
text {* 
262 
\medskip The limit of a nonempty chain of norm preserving 

263 
extensions of @{text f} is an extension of @{text f}, since every 

264 
element of the chain is an extension of @{text f} and the supremum 

265 
is an extension for every element of the chain. 

266 
*} 

7917  267 

268 
lemma sup_ext: 

13515  269 
assumes graph: "graph H h = \<Union>c" 
270 
and M: "M = norm_pres_extensions E p F f" 

271 
and cM: "c \<in> chain M" 

272 
and ex: "\<exists>x. x \<in> c" 

273 
shows "graph F f \<subseteq> graph H h" 

9261  274 
proof  
13515  275 
from ex obtain x where xc: "x \<in> c" .. 
276 
from cM have "c \<subseteq> M" .. 

277 
with xc have "x \<in> M" .. 

278 
with M have "x \<in> norm_pres_extensions E p F f" 

279 
by (simp only:) 

280 
then obtain G g where "x = graph G g" and "graph F f \<subseteq> graph G g" .. 

281 
then have "graph F f \<subseteq> x" by (simp only:) 

282 
also from xc have "\<dots> \<subseteq> \<Union>c" by blast 

283 
also from graph have "\<dots> = graph H h" .. 

284 
finally show ?thesis . 

9261  285 
qed 
7917  286 

10687  287 
text {* 
288 
\medskip The domain @{text H} of the limit function is a superspace 

289 
of @{text F}, since @{text F} is a subset of @{text H}. The 

290 
existence of the @{text 0} element in @{text F} and the closure 

291 
properties follow from the fact that @{text F} is a vector space. 

292 
*} 

7917  293 

10687  294 
lemma sup_supF: 
13515  295 
assumes graph: "graph H h = \<Union>c" 
296 
and M: "M = norm_pres_extensions E p F f" 

297 
and cM: "c \<in> chain M" 

298 
and ex: "\<exists>x. x \<in> c" 

299 
and FE: "F \<unlhd> E" 

300 
shows "F \<unlhd> H" 

301 
proof 

302 
from FE show "F \<noteq> {}" by (rule subspace.non_empty) 

303 
from graph M cM ex have "graph F f \<subseteq> graph H h" by (rule sup_ext) 

304 
then show "F \<subseteq> H" .. 

305 
fix x y assume "x \<in> F" and "y \<in> F" 

306 
with FE show "x + y \<in> F" by (rule subspace.add_closed) 

307 
next 

308 
fix x a assume "x \<in> F" 

309 
with FE show "a \<cdot> x \<in> F" by (rule subspace.mult_closed) 

9261  310 
qed 
7917  311 

10687  312 
text {* 
313 
\medskip The domain @{text H} of the limit function is a subspace of 

314 
@{text E}. 

315 
*} 

7917  316 

10687  317 
lemma sup_subE: 
13515  318 
assumes graph: "graph H h = \<Union>c" 
319 
and M: "M = norm_pres_extensions E p F f" 

320 
and cM: "c \<in> chain M" 

321 
and ex: "\<exists>x. x \<in> c" 

322 
and FE: "F \<unlhd> E" 

323 
and E: "vectorspace E" 

324 
shows "H \<unlhd> E" 

325 
proof 

326 
show "H \<noteq> {}" 

327 
proof  

13547  328 
from FE E have "0 \<in> F" by (rule subspace.zero) 
13515  329 
also from graph M cM ex FE have "F \<unlhd> H" by (rule sup_supF) 
330 
then have "F \<subseteq> H" .. 

331 
finally show ?thesis by blast 

332 
qed 

333 
show "H \<subseteq> E" 

9261  334 
proof 
13515  335 
fix x assume "x \<in> H" 
336 
with M cM graph 

44887  337 
obtain H' where x: "x \<in> H'" and H'E: "H' \<unlhd> E" 
13515  338 
by (rule some_H'h' [elim_format]) blast 
339 
from H'E have "H' \<subseteq> E" .. 

340 
with x show "x \<in> E" .. 

341 
qed 

342 
fix x y assume x: "x \<in> H" and y: "y \<in> H" 

343 
show "x + y \<in> H" 

344 
proof  

345 
from M cM graph x y obtain H' h' where 

346 
x': "x \<in> H'" and y': "y \<in> H'" and H'E: "H' \<unlhd> E" 

347 
and graphs: "graph H' h' \<subseteq> graph H h" 

348 
by (rule some_H'h'2 [elim_format]) blast 

349 
from H'E x' y' have "x + y \<in> H'" 

350 
by (rule subspace.add_closed) 

351 
also from graphs have "H' \<subseteq> H" .. 

352 
finally show ?thesis . 

353 
qed 

354 
next 

355 
fix x a assume x: "x \<in> H" 

356 
show "a \<cdot> x \<in> H" 

357 
proof  

358 
from M cM graph x 

359 
obtain H' h' where x': "x \<in> H'" and H'E: "H' \<unlhd> E" 

360 
and graphs: "graph H' h' \<subseteq> graph H h" 

361 
by (rule some_H'h' [elim_format]) blast 

362 
from H'E x' have "a \<cdot> x \<in> H'" by (rule subspace.mult_closed) 

363 
also from graphs have "H' \<subseteq> H" .. 

364 
finally show ?thesis . 

9261  365 
qed 
366 
qed 

7917  367 

10687  368 
text {* 
369 
\medskip The limit function is bounded by the norm @{text p} as 

370 
well, since all elements in the chain are bounded by @{text p}. 

9261  371 
*} 
7917  372 

9374  373 
lemma sup_norm_pres: 
13515  374 
assumes graph: "graph H h = \<Union>c" 
375 
and M: "M = norm_pres_extensions E p F f" 

376 
and cM: "c \<in> chain M" 

377 
shows "\<forall>x \<in> H. h x \<le> p x" 

9261  378 
proof 
9503  379 
fix x assume "x \<in> H" 
13515  380 
with M cM graph obtain H' h' where x': "x \<in> H'" 
381 
and graphs: "graph H' h' \<subseteq> graph H h" 

10687  382 
and a: "\<forall>x \<in> H'. h' x \<le> p x" 
13515  383 
by (rule some_H'h' [elim_format]) blast 
384 
from graphs x' have [symmetric]: "h' x = h x" .. 

385 
also from a x' have "h' x \<le> p x " .. 

386 
finally show "h x \<le> p x" . 

9261  387 
qed 
7917  388 

10687  389 
text {* 
390 
\medskip The following lemma is a property of linear forms on real 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

391 
vector spaces. It will be used for the lemma @{text abs_Hahn_Banach} 
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

392 
(see page \pageref{absHahn_Banach}). \label{absineqiff} For real 
10687  393 
vector spaces the following inequations are equivalent: 
394 
\begin{center} 

395 
\begin{tabular}{lll} 

396 
@{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and & 

397 
@{text "\<forall>x \<in> H. h x \<le> p x"} \\ 

398 
\end{tabular} 

399 
\end{center} 

9261  400 
*} 
7917  401 

10687  402 
lemma abs_ineq_iff: 
27611  403 
assumes "subspace H E" and "vectorspace E" and "seminorm E p" 
404 
and "linearform H h" 

13515  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") 
406 
proof 

29234  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 

23378  411 
have H: "vectorspace H" using `vectorspace E` .. 
13515  412 
{ 
9261  413 
assume l: ?L 
414 
show ?R 

415 
proof 

9503  416 
fix x assume x: "x \<in> H" 
13515  417 
have "h x \<le> \<bar>h x\<bar>" by arith 
418 
also from l x have "\<dots> \<le> p x" .. 

10687  419 
finally show "h x \<le> p x" . 
9261  420 
qed 
421 
next 

422 
assume r: ?R 

423 
show ?L 

10687  424 
proof 
13515  425 
fix x assume x: "x \<in> H" 
10687  426 
show "\<And>a b :: real.  a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a" 
9261  427 
by arith 
23378  428 
from `linearform H h` and H x 
429 
have " h x = h ( x)" by (rule linearform.neg [symmetric]) 

14710  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" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

434 
using `seminorm E p` `vectorspace E` 
14710  435 
proof (rule seminorm.minus) 
436 
from x show "x \<in> E" .. 

9261  437 
qed 
14710  438 
finally have " h x \<le> p x" . 
439 
then show " p x \<le> h x" by simp 

13515  440 
from r x show "h x \<le> p x" .. 
9261  441 
qed 
13515  442 
} 
10687  443 
qed 
7917  444 

10687  445 
end 