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