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