1 (* Title: HOL/Real/HahnBanach/HahnBanach_lemmas.thy |
|
2 ID: $Id$ |
|
3 Author: Gertrud Bauer, TU Munich |
|
4 *) |
|
5 |
|
6 header {* Lemmas about the supremal function w.r.t.~the function order *}; |
|
7 |
|
8 theory HahnBanach_lemmas = FunctionNorm + Zorn_Lemma:; |
|
9 |
|
10 lemma rabs_ineq: |
|
11 "[| is_subspace H E; is_vectorspace E; is_quasinorm E p; is_linearform H h |] |
|
12 ==> (ALL x:H. rabs (h x) <= p x) = ( ALL x:H. h x <= p x)" |
|
13 (concl is "?L = ?R"); |
|
14 proof -; |
|
15 assume "is_subspace H E" "is_vectorspace E" "is_quasinorm E p" |
|
16 "is_linearform H h"; |
|
17 have h: "is_vectorspace H"; ..; |
|
18 show ?thesis; |
|
19 proof; |
|
20 assume l: ?L; |
|
21 then; show ?R; |
|
22 proof (intro ballI); |
|
23 fix x; assume x: "x:H"; |
|
24 have "h x <= rabs (h x)"; by (rule rabs_ge_self); |
|
25 also; from l; have "... <= p x"; ..; |
|
26 finally; show "h x <= p x"; .; |
|
27 qed; |
|
28 next; |
|
29 assume r: ?R; |
|
30 then; show ?L; |
|
31 proof (intro ballI); |
|
32 fix x; assume "x:H"; |
|
33 |
|
34 show "rabs (h x) <= p x"; |
|
35 proof -; |
|
36 show "!! r x. [| - r <= x; x <= r |] ==> rabs x <= r"; |
|
37 by arith; |
|
38 show "- p x <= h x"; |
|
39 proof (rule real_minus_le); |
|
40 from h; have "- h x = h ([-] x)"; |
|
41 by (rule linearform_neg_linear [RS sym]); |
|
42 also; from r; have "... <= p ([-] x)"; by (simp!); |
|
43 also; have "... = p x"; |
|
44 by (rule quasinorm_minus, rule subspace_subsetD); |
|
45 finally; show "- h x <= p x"; .; |
|
46 qed; |
|
47 from r; show "h x <= p x"; ..; |
|
48 qed; |
|
49 qed; |
|
50 qed; |
|
51 qed; |
|
52 |
|
53 lemma some_H'h't: |
|
54 "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c; |
|
55 x:H|] |
|
56 ==> EX H' h' t. t : (graph H h) & t = (x, h x) & (graph H' h'):c |
|
57 & t:graph H' h' & is_linearform H' h' & is_subspace H' E |
|
58 & is_subspace F H' & (graph F f <= graph H' h') |
|
59 & (ALL x:H'. h' x <= p x)"; |
|
60 proof -; |
|
61 assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M" |
|
62 and u: "graph H h = Union c" "x:H"; |
|
63 |
|
64 let ?P = "%H h. is_linearform H h |
|
65 & is_subspace H E |
|
66 & is_subspace F H |
|
67 & (graph F f <= graph H h) |
|
68 & (ALL x:H. h x <= p x)"; |
|
69 |
|
70 have "EX t : (graph H h). t = (x, h x)"; |
|
71 by (rule graphI2); |
|
72 thus ?thesis; |
|
73 proof (elim bexE); |
|
74 fix t; assume t: "t : (graph H h)" "t = (x, h x)"; |
|
75 with u; have ex1: "EX g:c. t:g"; |
|
76 by (simp only: Union_iff); |
|
77 thus ?thesis; |
|
78 proof (elim bexE); |
|
79 fix g; assume g: "g:c" "t:g"; |
|
80 from cM; have "c <= M"; by (rule chainD2); |
|
81 hence "g : M"; ..; |
|
82 hence "g : norm_pres_extensions E p F f"; by (simp only: m); |
|
83 hence "EX H' h'. graph H' h' = g & ?P H' h'"; |
|
84 by (rule norm_pres_extension_D); |
|
85 thus ?thesis; by (elim exE conjE, intro exI conjI) (simp | simp!)+; |
|
86 qed; |
|
87 qed; |
|
88 qed; |
|
89 |
|
90 lemma some_H'h': "[| M = norm_pres_extensions E p F f; c: chain M; |
|
91 graph H h = Union c; x:H|] |
|
92 ==> EX H' h'. x:H' & (graph H' h' <= graph H h) & |
|
93 is_linearform H' h' & is_subspace H' E & is_subspace F H' & |
|
94 (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; |
|
95 proof -; |
|
96 assume m: "M = norm_pres_extensions E p F f" and cM: "c: chain M" |
|
97 and u: "graph H h = Union c" "x:H"; |
|
98 have "(x, h x): graph H h"; by (rule graphI); |
|
99 also; have "... = Union c"; .; |
|
100 finally; have "(x, h x) : Union c"; .; |
|
101 hence "EX g:c. (x, h x):g"; by (simp only: Union_iff); |
|
102 thus ?thesis; |
|
103 proof (elim bexE); |
|
104 fix g; assume g: "g:c" "(x, h x):g"; |
|
105 from cM; have "c <= M"; by (rule chainD2); |
|
106 hence "g : M"; ..; |
|
107 hence "g : norm_pres_extensions E p F f"; by (simp only: m); |
|
108 hence "EX H' h'. graph H' h' = g |
|
109 & is_linearform H' h' |
|
110 & is_subspace H' E |
|
111 & is_subspace F H' |
|
112 & (graph F f <= graph H' h') |
|
113 & (ALL x:H'. h' x <= p x)"; |
|
114 by (rule norm_pres_extension_D); |
|
115 thus ?thesis; |
|
116 proof (elim exE conjE, intro exI conjI); |
|
117 fix H' h'; assume g': "graph H' h' = g"; |
|
118 with g; have "(x, h x): graph H' h'"; by simp; |
|
119 thus "x:H'"; by (rule graphD1); |
|
120 from g g'; have "graph H' h' : c"; by simp; |
|
121 with cM u; show "graph H' h' <= graph H h"; |
|
122 by (simp only: chain_ball_Union_upper); |
|
123 qed simp+; |
|
124 qed; |
|
125 qed; |
|
126 |
|
127 lemma some_H'h'2: |
|
128 "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c; |
|
129 x:H; y:H|] |
|
130 ==> EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) |
|
131 & is_linearform H' h' & is_subspace H' E & is_subspace F H' & |
|
132 (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; |
|
133 proof -; |
|
134 assume "M = norm_pres_extensions E p F f" "c: chain M" |
|
135 "graph H h = Union c"; |
|
136 |
|
137 let ?P = "%H h. is_linearform H h |
|
138 & is_subspace H E |
|
139 & is_subspace F H |
|
140 & (graph F f <= graph H h) |
|
141 & (ALL x:H. h x <= p x)"; |
|
142 assume "x:H"; |
|
143 have e1: "EX H' h' t. t : (graph H h) & t = (x, h x) & (graph H' h'):c |
|
144 & t:graph H' h' & ?P H' h'"; |
|
145 by (rule some_H'h't); |
|
146 assume "y:H"; |
|
147 have e2: "EX H' h' t. t : (graph H h) & t = (y, h y) & (graph H' h'):c |
|
148 & t:graph H' h' & ?P H' h'"; |
|
149 by (rule some_H'h't); |
|
150 |
|
151 from e1 e2; show ?thesis; |
|
152 proof (elim exE conjE); |
|
153 fix H' h' t' H'' h'' t''; |
|
154 assume "t' : graph H h" "t'' : graph H h" |
|
155 "t' = (y, h y)" "t'' = (x, h x)" |
|
156 "graph H' h' : c" "graph H'' h'' : c" |
|
157 "t' : graph H' h'" "t'' : graph H'' h''" |
|
158 "is_linearform H' h'" "is_linearform H'' h''" |
|
159 "is_subspace H' E" "is_subspace H'' E" |
|
160 "is_subspace F H'" "is_subspace F H''" |
|
161 "graph F f <= graph H' h'" "graph F f <= graph H'' h''" |
|
162 "ALL x:H'. h' x <= p x" "ALL x:H''. h'' x <= p x"; |
|
163 |
|
164 have "(graph H'' h'') <= (graph H' h') |
|
165 | (graph H' h') <= (graph H'' h'')"; |
|
166 by (rule chainD); |
|
167 thus "?thesis"; |
|
168 proof; |
|
169 assume "(graph H'' h'') <= (graph H' h')"; |
|
170 show ?thesis; |
|
171 proof (intro exI conjI); |
|
172 note [trans] = subsetD; |
|
173 have "(x, h x) : graph H'' h''"; by (simp!); |
|
174 also; have "... <= graph H' h'"; .; |
|
175 finally; have xh: "(x, h x): graph H' h'"; .; |
|
176 thus x: "x:H'"; by (rule graphD1); |
|
177 show y: "y:H'"; by (simp!, rule graphD1); |
|
178 show "(graph H' h') <= (graph H h)"; |
|
179 by (simp! only: chain_ball_Union_upper); |
|
180 qed; |
|
181 next; |
|
182 assume "(graph H' h') <= (graph H'' h'')"; |
|
183 show ?thesis; |
|
184 proof (intro exI conjI); |
|
185 show x: "x:H''"; by (simp!, rule graphD1); |
|
186 have "(y, h y) : graph H' h'"; by (simp!); |
|
187 also; have "... <= graph H'' h''"; .; |
|
188 finally; have yh: "(y, h y): graph H'' h''"; .; |
|
189 thus y: "y:H''"; by (rule graphD1); |
|
190 show "(graph H'' h'') <= (graph H h)"; |
|
191 by (simp! only: chain_ball_Union_upper); |
|
192 qed; |
|
193 qed; |
|
194 qed; |
|
195 qed; |
|
196 |
|
197 lemma sup_uniq: |
|
198 "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; |
|
199 is_linearform F f; ALL x:F. f x <= p x; M == norm_pres_extensions E p F f; |
|
200 c : chain M; EX x. x : c; (x, y) : Union c; (x, z) : Union c |] |
|
201 ==> z = y"; |
|
202 proof -; |
|
203 assume "M == norm_pres_extensions E p F f" "c : chain M" |
|
204 "(x, y) : Union c" " (x, z) : Union c"; |
|
205 hence "EX H h. (x, y) : graph H h & (x, z) : graph H h"; |
|
206 proof (elim UnionE chainE2); |
|
207 fix G1 G2; |
|
208 assume "(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M"; |
|
209 have "G1 : M"; ..; |
|
210 hence e1: "EX H1 h1. graph H1 h1 = G1"; |
|
211 by (force! dest: norm_pres_extension_D); |
|
212 have "G2 : M"; ..; |
|
213 hence e2: "EX H2 h2. graph H2 h2 = G2"; |
|
214 by (force! dest: norm_pres_extension_D); |
|
215 from e1 e2; show ?thesis; |
|
216 proof (elim exE); |
|
217 fix H1 h1 H2 h2; assume "graph H1 h1 = G1" "graph H2 h2 = G2"; |
|
218 have "G1 <= G2 | G2 <= G1"; ..; |
|
219 thus ?thesis; |
|
220 proof; |
|
221 assume "G1 <= G2"; |
|
222 thus ?thesis; |
|
223 proof (intro exI conjI); |
|
224 show "(x, y) : graph H2 h2"; by (force!); |
|
225 show "(x, z) : graph H2 h2"; by (simp!); |
|
226 qed; |
|
227 next; |
|
228 assume "G2 <= G1"; |
|
229 thus ?thesis; |
|
230 proof (intro exI conjI); |
|
231 show "(x, y) : graph H1 h1"; by (simp!); |
|
232 show "(x, z) : graph H1 h1"; by (force!); |
|
233 qed; |
|
234 qed; |
|
235 qed; |
|
236 qed; |
|
237 thus ?thesis; |
|
238 proof (elim exE conjE); |
|
239 fix H h; assume "(x, y) : graph H h" "(x, z) : graph H h"; |
|
240 have "y = h x"; ..; |
|
241 also; have "... = z"; by (rule sym, rule); |
|
242 finally; show "z = y"; by (rule sym); |
|
243 qed; |
|
244 qed; |
|
245 |
|
246 lemma sup_lf: |
|
247 "[| M = norm_pres_extensions E p F f; c: chain M; graph H h = Union c|] |
|
248 ==> is_linearform H h"; |
|
249 proof -; |
|
250 assume "M = norm_pres_extensions E p F f" "c: chain M" |
|
251 "graph H h = Union c"; |
|
252 |
|
253 let ?P = "%H h. is_linearform H h |
|
254 & is_subspace H E |
|
255 & is_subspace F H |
|
256 & (graph F f <= graph H h) |
|
257 & (ALL x:H. h x <= p x)"; |
|
258 |
|
259 show "is_linearform H h"; |
|
260 proof; |
|
261 fix x y; assume "x : H" "y : H"; |
|
262 show "h (x [+] y) = h x + h y"; |
|
263 proof -; |
|
264 have "EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) |
|
265 & is_linearform H' h' & is_subspace H' E |
|
266 & is_subspace F H' & (graph F f <= graph H' h') |
|
267 & (ALL x:H'. h' x <= p x)"; |
|
268 by (rule some_H'h'2); |
|
269 thus ?thesis; |
|
270 proof (elim exE conjE); |
|
271 fix H' h'; assume "x:H'" "y:H'" |
|
272 and b: "graph H' h' <= graph H h" |
|
273 and "is_linearform H' h'" "is_subspace H' E"; |
|
274 have h'x: "h' x = h x"; ..; |
|
275 have h'y: "h' y = h y"; ..; |
|
276 have h'xy: "h' (x [+] y) = h' x + h' y"; |
|
277 by (rule linearform_add_linear); |
|
278 have "h' (x [+] y) = h (x [+] y)"; |
|
279 proof -; |
|
280 have "x [+] y : H'"; ..; |
|
281 with b; show ?thesis; ..; |
|
282 qed; |
|
283 with h'x h'y h'xy; show ?thesis; |
|
284 by (simp!); |
|
285 qed; |
|
286 qed; |
|
287 next; |
|
288 fix a x; assume "x : H"; |
|
289 show "h (a [*] x) = a * (h x)"; |
|
290 proof -; |
|
291 have "EX H' h'. x:H' & (graph H' h' <= graph H h) |
|
292 & is_linearform H' h' & is_subspace H' E |
|
293 & is_subspace F H' & (graph F f <= graph H' h') |
|
294 & (ALL x:H'. h' x <= p x)"; |
|
295 by (rule some_H'h'); |
|
296 thus ?thesis; |
|
297 proof (elim exE conjE); |
|
298 fix H' h'; |
|
299 assume b: "graph H' h' <= graph H h"; |
|
300 assume "x:H'" "is_linearform H' h'" "is_subspace H' E"; |
|
301 have h'x: "h' x = h x"; ..; |
|
302 have h'ax: "h' (a [*] x) = a * h' x"; |
|
303 by (rule linearform_mult_linear); |
|
304 have "h' (a [*] x) = h (a [*] x)"; |
|
305 proof -; |
|
306 have "a [*] x : H'"; ..; |
|
307 with b; show ?thesis; ..; |
|
308 qed; |
|
309 with h'x h'ax; show ?thesis; |
|
310 by (simp!); |
|
311 qed; |
|
312 qed; |
|
313 qed; |
|
314 qed; |
|
315 |
|
316 lemma sup_ext: |
|
317 "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; |
|
318 graph H h = Union c|] ==> graph F f <= graph H h"; |
|
319 proof -; |
|
320 assume "M = norm_pres_extensions E p F f" "c: chain M" |
|
321 "graph H h = Union c" |
|
322 and e: "EX x. x:c"; |
|
323 |
|
324 thus ?thesis; |
|
325 proof (elim exE); |
|
326 fix x; assume "x:c"; |
|
327 show ?thesis; |
|
328 proof -; |
|
329 have "x:norm_pres_extensions E p F f"; |
|
330 proof (rule subsetD); |
|
331 show "c <= norm_pres_extensions E p F f"; by (simp! add: chainD2); |
|
332 qed; |
|
333 |
|
334 hence "(EX G g. graph G g = x |
|
335 & is_linearform G g |
|
336 & is_subspace G E |
|
337 & is_subspace F G |
|
338 & (graph F f <= graph G g) |
|
339 & (ALL x:G. g x <= p x))"; |
|
340 by (simp! add: norm_pres_extension_D); |
|
341 |
|
342 thus ?thesis; |
|
343 proof (elim exE conjE); |
|
344 fix G g; assume "graph G g = x" "graph F f <= graph G g"; |
|
345 show ?thesis; |
|
346 proof -; |
|
347 have "graph F f <= graph G g"; .; |
|
348 also; have "graph G g <= graph H h"; by ((simp!), fast); |
|
349 finally; show ?thesis; .; |
|
350 qed; |
|
351 qed; |
|
352 qed; |
|
353 qed; |
|
354 qed; |
|
355 |
|
356 |
|
357 lemma sup_supF: |
|
358 "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; |
|
359 graph H h = Union c; is_subspace F E |] ==> is_subspace F H"; |
|
360 proof -; |
|
361 assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c" |
|
362 "graph H h = Union c" |
|
363 "is_subspace F E"; |
|
364 |
|
365 show ?thesis; |
|
366 proof (rule subspaceI); |
|
367 show "<0> : F"; ..; |
|
368 show "F <= H"; |
|
369 proof (rule graph_extD2); |
|
370 show "graph F f <= graph H h"; |
|
371 by (rule sup_ext); |
|
372 qed; |
|
373 show "ALL x:F. ALL y:F. x [+] y : F"; |
|
374 proof (intro ballI); |
|
375 fix x y; assume "x:F" "y:F"; |
|
376 show "x [+] y : F"; by (simp!); |
|
377 qed; |
|
378 show "ALL x:F. ALL a. a [*] x : F"; |
|
379 proof (intro ballI allI); |
|
380 fix x a; assume "x:F"; |
|
381 show "a [*] x : F"; by (simp!); |
|
382 qed; |
|
383 qed; |
|
384 qed; |
|
385 |
|
386 |
|
387 lemma sup_subE: |
|
388 "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; |
|
389 graph H h = Union c; is_subspace F E|] ==> is_subspace H E"; |
|
390 proof -; |
|
391 assume "M = norm_pres_extensions E p F f" "c: chain M" "EX x. x:c" |
|
392 "graph H h = Union c" "is_subspace F E"; |
|
393 |
|
394 show ?thesis; |
|
395 proof; |
|
396 |
|
397 show "<0> : H"; |
|
398 proof (rule subsetD [of F H]); |
|
399 have "is_subspace F H"; by (rule sup_supF); |
|
400 thus "F <= H"; ..; |
|
401 show "<0> : F"; ..; |
|
402 qed; |
|
403 |
|
404 show "H <= E"; |
|
405 proof; |
|
406 fix x; assume "x:H"; |
|
407 show "x:E"; |
|
408 proof -; |
|
409 have "EX H' h'. x:H' & (graph H' h' <= graph H h) |
|
410 & is_linearform H' h' & is_subspace H' E & is_subspace F H' |
|
411 & (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; |
|
412 by (rule some_H'h'); |
|
413 thus ?thesis; |
|
414 proof (elim exE conjE); |
|
415 fix H' h'; assume "x:H'" "is_subspace H' E"; |
|
416 show "x:E"; |
|
417 proof (rule subsetD); |
|
418 show "H' <= E"; ..; |
|
419 qed; |
|
420 qed; |
|
421 qed; |
|
422 qed; |
|
423 |
|
424 show "ALL x:H. ALL y:H. x [+] y : H"; |
|
425 proof (intro ballI); |
|
426 fix x y; assume "x:H" "y:H"; |
|
427 show "x [+] y : H"; |
|
428 proof -; |
|
429 have "EX H' h'. x:H' & y:H' & (graph H' h' <= graph H h) |
|
430 & is_linearform H' h' & is_subspace H' E & is_subspace F H' |
|
431 & (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; |
|
432 by (rule some_H'h'2); |
|
433 thus ?thesis; |
|
434 proof (elim exE conjE); |
|
435 fix H' h'; |
|
436 assume "x:H'" "y:H'" "is_subspace H' E" |
|
437 "graph H' h' <= graph H h"; |
|
438 have "H' <= H"; ..; |
|
439 thus ?thesis; |
|
440 proof (rule subsetD); |
|
441 show "x [+] y : H'"; ..; |
|
442 qed; |
|
443 qed; |
|
444 qed; |
|
445 qed; |
|
446 |
|
447 show "ALL x:H. ALL a. a [*] x : H"; |
|
448 proof (intro ballI allI); |
|
449 fix x and a::real; assume "x:H"; |
|
450 show "a [*] x : H"; |
|
451 proof -; |
|
452 have "EX H' h'. x:H' & (graph H' h' <= graph H h) & |
|
453 is_linearform H' h' & is_subspace H' E & is_subspace F H' & |
|
454 (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; |
|
455 by (rule some_H'h'); |
|
456 thus ?thesis; |
|
457 proof (elim exE conjE); |
|
458 fix H' h'; |
|
459 assume "x:H'" "is_subspace H' E" "graph H' h' <= graph H h"; |
|
460 have "H' <= H"; ..; |
|
461 thus ?thesis; |
|
462 proof (rule subsetD); |
|
463 show "a [*] x : H'"; ..; |
|
464 qed; |
|
465 qed; |
|
466 qed; |
|
467 qed; |
|
468 qed; |
|
469 qed; |
|
470 |
|
471 lemma sup_norm_pres: "[| M = norm_pres_extensions E p F f; c: chain M; |
|
472 graph H h = Union c|] ==> ALL x::'a:H. h x <= p x"; |
|
473 proof; |
|
474 assume "M = norm_pres_extensions E p F f" "c: chain M" |
|
475 "graph H h = Union c"; |
|
476 fix x; assume "x:H"; |
|
477 show "h x <= p x"; |
|
478 proof -; |
|
479 have "EX H' h'. x:H' & (graph H' h' <= graph H h) |
|
480 & is_linearform H' h' & is_subspace H' E & is_subspace F H' |
|
481 & (graph F f <= graph H' h') & (ALL x:H'. h' x <= p x)"; |
|
482 by (rule some_H'h'); |
|
483 thus ?thesis; |
|
484 proof (elim exE conjE); |
|
485 fix H' h'; assume "x: H'" "graph H' h' <= graph H h" |
|
486 and a: "ALL x: H'. h' x <= p x" ; |
|
487 have "h x = h' x"; |
|
488 proof (rule sym); |
|
489 show "h' x = h x"; ..; |
|
490 qed; |
|
491 also; from a; have "... <= p x "; ..; |
|
492 finally; show ?thesis; .; |
|
493 qed; |
|
494 qed; |
|
495 qed; |
|
496 |
|
497 end; |
|