author | wenzelm |
Mon, 02 Nov 2015 11:43:02 +0100 | |
changeset 61540 | f92bf6674699 |
parent 61539 | a29295dac1ca |
child 61879 | e4f9d8f094fe |
permissions | -rw-r--r-- |
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 |
||
61540 | 5 |
section \<open>The supremum wrt.\ the function order\<close> |
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 |
|
58744 | 11 |
text \<open> |
61540 | 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. |
|
14 |
Let \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a |
|
15 |
subspace of \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of |
|
16 |
norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will |
|
17 |
show some properties about the limit function \<open>h\<close>, i.e.\ the supremum of |
|
18 |
the chain \<open>c\<close>. |
|
7917 | 19 |
|
61486 | 20 |
\<^medskip> |
61540 | 21 |
Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and |
22 |
let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of |
|
23 |
one of the elements of the chain. |
|
58744 | 24 |
\<close> |
61486 | 25 |
|
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
45605
diff
changeset
|
26 |
lemmas [dest?] = chainsD |
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
45605
diff
changeset
|
27 |
lemmas chainsE2 [elim?] = chainsD2 [elim_format] |
7917 | 28 |
|
29 |
lemma some_H'h't: |
|
13515 | 30 |
assumes M: "M = norm_pres_extensions E p F f" |
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
45605
diff
changeset
|
31 |
and cM: "c \<in> chains M" |
13515 | 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 |
|
58744 | 56 |
text \<open> |
61486 | 57 |
\<^medskip> |
61540 | 58 |
Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and |
59 |
let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of |
|
60 |
the supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, |
|
61 |
such that \<open>h\<close> extends \<open>h'\<close>. |
|
58744 | 62 |
\<close> |
7917 | 63 |
|
10687 | 64 |
lemma some_H'h': |
13515 | 65 |
assumes M: "M = norm_pres_extensions E p F f" |
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
45605
diff
changeset
|
66 |
and cM: "c \<in> chains M" |
13515 | 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'" .. |
|
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
45605
diff
changeset
|
80 |
moreover from cM u c have "graph H' h' \<subseteq> graph H h" by blast |
13515 | 81 |
ultimately show ?thesis using * by blast |
9261 | 82 |
qed |
7917 | 83 |
|
58744 | 84 |
text \<open> |
61486 | 85 |
\<^medskip> |
61540 | 86 |
Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function |
87 |
\<open>h\<close> are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> |
|
88 |
extends \<open>h'\<close>. |
|
58744 | 89 |
\<close> |
7917 | 90 |
|
10687 | 91 |
lemma some_H'h'2: |
13515 | 92 |
assumes M: "M = norm_pres_extensions E p F f" |
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
45605
diff
changeset
|
93 |
and cM: "c \<in> chains M" |
13515 | 94 |
and u: "graph H h = \<Union>c" |
95 |
and x: "x \<in> H" |
|
96 |
and y: "y \<in> H" |
|
97 |
shows "\<exists>H' h'. x \<in> H' \<and> y \<in> H' |
|
98 |
\<and> graph H' h' \<subseteq> graph H h |
|
99 |
\<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H' |
|
100 |
\<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)" |
|
9261 | 101 |
proof - |
61539 | 102 |
txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>, |
103 |
such that \<open>h\<close> extends \<open>h''\<close>.\<close> |
|
7917 | 104 |
|
13515 | 105 |
from M cM u and y obtain H' h' where |
106 |
y_hy: "(y, h y) \<in> graph H' h'" |
|
107 |
and c': "graph H' h' \<in> c" |
|
108 |
and * : |
|
109 |
"linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'" |
|
110 |
"graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" |
|
111 |
by (rule some_H'h't [elim_format]) blast |
|
112 |
||
61539 | 113 |
txt \<open>\<open>x\<close> is in the domain \<open>H'\<close> of some function \<open>h'\<close>, |
114 |
such that \<open>h\<close> extends \<open>h'\<close>.\<close> |
|
7917 | 115 |
|
13515 | 116 |
from M cM u and x obtain H'' h'' where |
117 |
x_hx: "(x, h x) \<in> graph H'' h''" |
|
118 |
and c'': "graph H'' h'' \<in> c" |
|
119 |
and ** : |
|
120 |
"linearform H'' h''" "H'' \<unlhd> E" "F \<unlhd> H''" |
|
121 |
"graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x" |
|
122 |
by (rule some_H'h't [elim_format]) blast |
|
7917 | 123 |
|
61539 | 124 |
txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain, |
125 |
\<open>h''\<close> is an extension of \<open>h'\<close> or vice versa. Thus both |
|
126 |
\<open>x\<close> and \<open>y\<close> are contained in the greater |
|
58744 | 127 |
one. \label{cases1}\<close> |
7917 | 128 |
|
60458 | 129 |
from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''" |
130 |
by (blast dest: chainsD) |
|
13515 | 131 |
then show ?thesis |
60458 | 132 |
proof cases |
133 |
case 1 |
|
23378 | 134 |
have "(x, h x) \<in> graph H'' h''" by fact |
27612 | 135 |
also have "\<dots> \<subseteq> graph H' h'" by fact |
13515 | 136 |
finally have xh:"(x, h x) \<in> graph H' h'" . |
137 |
then have "x \<in> H'" .. |
|
138 |
moreover from y_hy have "y \<in> H'" .. |
|
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
45605
diff
changeset
|
139 |
moreover from cM u and c' have "graph H' h' \<subseteq> graph H h" by blast |
13515 | 140 |
ultimately show ?thesis using * by blast |
141 |
next |
|
60458 | 142 |
case 2 |
13515 | 143 |
from x_hx have "x \<in> H''" .. |
60458 | 144 |
moreover have "y \<in> H''" |
145 |
proof - |
|
23378 | 146 |
have "(y, h y) \<in> graph H' h'" by (rule y_hy) |
147 |
also have "\<dots> \<subseteq> graph H'' h''" by fact |
|
13515 | 148 |
finally have "(y, h y) \<in> graph H'' h''" . |
60458 | 149 |
then show ?thesis .. |
150 |
qed |
|
151 |
moreover from u c'' have "graph H'' h'' \<subseteq> graph H h" by blast |
|
13515 | 152 |
ultimately show ?thesis using ** by blast |
9261 | 153 |
qed |
154 |
qed |
|
7917 | 155 |
|
58744 | 156 |
text \<open> |
61486 | 157 |
\<^medskip> |
61540 | 158 |
The relation induced by the graph of the supremum of a chain \<open>c\<close> is |
159 |
definite, i.e.\ it is the graph of a function. |
|
58744 | 160 |
\<close> |
7917 | 161 |
|
10687 | 162 |
lemma sup_definite: |
13515 | 163 |
assumes M_def: "M \<equiv> norm_pres_extensions E p F f" |
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
45605
diff
changeset
|
164 |
and cM: "c \<in> chains M" |
13515 | 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 |
|
61540 | 181 |
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> |
182 |
are members of \<open>c\<close>. \label{cases2}\<close> |
|
7917 | 183 |
|
60458 | 184 |
from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1" |
185 |
by (blast dest: chainsD) |
|
13515 | 186 |
then show ?thesis |
60458 | 187 |
proof cases |
188 |
case 1 |
|
13515 | 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 |
|
60458 | 196 |
case 2 |
13515 | 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 |
|
58744 | 206 |
text \<open> |
61486 | 207 |
\<^medskip> |
61540 | 208 |
The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close> |
209 |
is in the domain of a function \<open>h'\<close> in the chain of norm preserving |
|
210 |
extensions. Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function |
|
211 |
values of \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close> |
|
212 |
is linear by construction of \<open>M\<close>. |
|
58744 | 213 |
\<close> |
7917 | 214 |
|
10687 | 215 |
lemma sup_lf: |
13515 | 216 |
assumes M: "M = norm_pres_extensions E p F f" |
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
45605
diff
changeset
|
217 |
and cM: "c \<in> chains M" |
13515 | 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 |
|
58744 | 261 |
text \<open> |
61486 | 262 |
\<^medskip> |
61540 | 263 |
The limit of a non-empty chain of norm preserving extensions of \<open>f\<close> is an |
264 |
extension of \<open>f\<close>, since every element of the chain is an extension of \<open>f\<close> |
|
265 |
and the supremum is an extension for every element of the chain. |
|
58744 | 266 |
\<close> |
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" |
|
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
45605
diff
changeset
|
271 |
and cM: "c \<in> chains M" |
13515 | 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 |
|
58744 | 287 |
text \<open> |
61486 | 288 |
\<^medskip> |
61540 | 289 |
The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is |
290 |
a subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure |
|
61539 | 291 |
properties follow from the fact that \<open>F\<close> is a vector space. |
58744 | 292 |
\<close> |
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" |
|
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
45605
diff
changeset
|
297 |
and cM: "c \<in> chains M" |
13515 | 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 |
|
58744 | 312 |
text \<open> |
61486 | 313 |
\<^medskip> |
61540 | 314 |
The domain \<open>H\<close> of the limit function is a subspace of \<open>E\<close>. |
58744 | 315 |
\<close> |
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" |
|
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
45605
diff
changeset
|
320 |
and cM: "c \<in> chains M" |
13515 | 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 |
|
58744 | 368 |
text \<open> |
61486 | 369 |
\<^medskip> |
61540 | 370 |
The limit function is bounded by the norm \<open>p\<close> as well, since all elements |
371 |
in the chain are bounded by \<open>p\<close>. |
|
58744 | 372 |
\<close> |
7917 | 373 |
|
9374 | 374 |
lemma sup_norm_pres: |
13515 | 375 |
assumes graph: "graph H h = \<Union>c" |
376 |
and M: "M = norm_pres_extensions E p F f" |
|
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
45605
diff
changeset
|
377 |
and cM: "c \<in> chains M" |
13515 | 378 |
shows "\<forall>x \<in> H. h x \<le> p x" |
9261 | 379 |
proof |
9503 | 380 |
fix x assume "x \<in> H" |
13515 | 381 |
with M cM graph obtain H' h' where x': "x \<in> H'" |
382 |
and graphs: "graph H' h' \<subseteq> graph H h" |
|
10687 | 383 |
and a: "\<forall>x \<in> H'. h' x \<le> p x" |
13515 | 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" . |
|
9261 | 388 |
qed |
7917 | 389 |
|
58744 | 390 |
text \<open> |
61486 | 391 |
\<^medskip> |
61540 | 392 |
The following lemma is a property of linear forms on real vector spaces. |
393 |
It will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page |
|
394 |
\pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces |
|
395 |
the following inequality are equivalent: |
|
10687 | 396 |
\begin{center} |
397 |
\begin{tabular}{lll} |
|
61539 | 398 |
\<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and & |
399 |
\<open>\<forall>x \<in> H. h x \<le> p x\<close> \\ |
|
10687 | 400 |
\end{tabular} |
401 |
\end{center} |
|
58744 | 402 |
\<close> |
7917 | 403 |
|
10687 | 404 |
lemma abs_ineq_iff: |
27611 | 405 |
assumes "subspace H E" and "vectorspace E" and "seminorm E p" |
406 |
and "linearform H h" |
|
13515 | 407 |
shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R") |
408 |
proof |
|
29234 | 409 |
interpret subspace H E by fact |
410 |
interpret vectorspace E by fact |
|
411 |
interpret seminorm E p by fact |
|
412 |
interpret linearform H h by fact |
|
58744 | 413 |
have H: "vectorspace H" using \<open>vectorspace E\<close> .. |
13515 | 414 |
{ |
9261 | 415 |
assume l: ?L |
416 |
show ?R |
|
417 |
proof |
|
9503 | 418 |
fix x assume x: "x \<in> H" |
13515 | 419 |
have "h x \<le> \<bar>h x\<bar>" by arith |
420 |
also from l x have "\<dots> \<le> p x" .. |
|
10687 | 421 |
finally show "h x \<le> p x" . |
9261 | 422 |
qed |
423 |
next |
|
424 |
assume r: ?R |
|
425 |
show ?L |
|
10687 | 426 |
proof |
13515 | 427 |
fix x assume x: "x \<in> H" |
60595 | 428 |
show "\<bar>b\<bar> \<le> a" when "- a \<le> b" "b \<le> a" for a b :: real |
429 |
using that by arith |
|
58744 | 430 |
from \<open>linearform H h\<close> and H x |
23378 | 431 |
have "- h x = h (- x)" by (rule linearform.neg [symmetric]) |
14710 | 432 |
also |
433 |
from H x have "- x \<in> H" by (rule vectorspace.neg_closed) |
|
434 |
with r have "h (- x) \<le> p (- x)" .. |
|
435 |
also have "\<dots> = p x" |
|
58744 | 436 |
using \<open>seminorm E p\<close> \<open>vectorspace E\<close> |
14710 | 437 |
proof (rule seminorm.minus) |
438 |
from x show "x \<in> E" .. |
|
9261 | 439 |
qed |
14710 | 440 |
finally have "- h x \<le> p x" . |
441 |
then show "- p x \<le> h x" by simp |
|
13515 | 442 |
from r x show "h x \<le> p x" .. |
9261 | 443 |
qed |
13515 | 444 |
} |
10687 | 445 |
qed |
7917 | 446 |
|
10687 | 447 |
end |