src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
 author wenzelm Mon Apr 25 16:09:26 2016 +0200 (2016-04-25) changeset 63040 eb4ddd18d635 parent 61879 e4f9d8f094fe permissions -rw-r--r--
eliminated old 'def';
1 (*  Title:      HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
2     Author:     Gertrud Bauer, TU Munich
3 *)
5 section \<open>The supremum wrt.\ the function order\<close>
7 theory Hahn_Banach_Sup_Lemmas
8 imports Function_Norm Zorn_Lemma
9 begin
11 text \<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>.
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>
25 lemmas [dest?] = chainsD
26 lemmas chainsE2 [elim?] = chainsD2 [elim_format]
28 lemma 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)"
38 proof -
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
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" ..
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
53 qed
55 text \<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>
63 lemma 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)"
71 proof -
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
81 qed
83 text \<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>
90 lemma 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)"
100 proof -
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>
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
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>
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
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>
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
152 qed
154 text \<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>
160 lemma 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"
166 proof -
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" ..
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
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
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>
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
202 qed
204 text \<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>
213 lemma 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"
218 proof
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
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
238 next
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
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
257 qed
259 text \<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>
266 lemma 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"
272 proof -
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 .
283 qed
285 text \<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>
292 lemma 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"
299 proof
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)
305 next
306   fix x a assume "x \<in> F"
307   with FE show "a \<cdot> x \<in> F" by (rule subspace.mult_closed)
308 qed
310 text \<open>
311   \<^medskip>
312   The domain \<open>H\<close> of the limit function is a subspace of \<open>E\<close>.
313 \<close>
315 lemma 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"
323 proof
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
352 next
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
364 qed
366 text \<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>
372 lemma 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"
377 proof
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" .
386 qed
388 text \<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>
402 lemma 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")
406 proof
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   }
443 qed
445 end