7917
|
1 |
(* Title: HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Gertrud Bauer, TU Munich
|
|
4 |
*)
|
|
5 |
|
9261
|
6 |
header {* The supremum w.r.t.~the function order *}
|
7917
|
7 |
|
27612
|
8 |
theory HahnBanachSupLemmas
|
|
9 |
imports FunctionNorm ZornLemma
|
|
10 |
begin
|
9256
|
11 |
|
10687
|
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}
|
13515
|
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}.
|
7917
|
21 |
|
13515
|
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
|
10687
|
25 |
elements of the chain.
|
|
26 |
*}
|
14710
|
27 |
lemmas [dest?] = chainD
|
|
28 |
lemmas chainE2 [elim?] = chainD2 [elim_format, standard]
|
7917
|
29 |
|
|
30 |
lemma some_H'h't:
|
13515
|
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)"
|
9261
|
40 |
proof -
|
13515
|
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
|
7917
|
44 |
|
13515
|
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
|
9261
|
55 |
qed
|
7917
|
56 |
|
10687
|
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'}.
|
9261
|
63 |
*}
|
7917
|
64 |
|
10687
|
65 |
lemma some_H'h':
|
13515
|
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)"
|
9261
|
73 |
proof -
|
13515
|
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'"
|
10687
|
78 |
"graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
|
13515
|
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
|
9261
|
84 |
qed
|
7917
|
85 |
|
10687
|
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 |
*}
|
7917
|
92 |
|
10687
|
93 |
lemma some_H'h'2:
|
13515
|
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)"
|
9261
|
103 |
proof -
|
10687
|
104 |
txt {* @{text y} is in the domain @{text H''} of some function @{text h''},
|
|
105 |
such that @{text h} extends @{text h''}. *}
|
7917
|
106 |
|
13515
|
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'}. *}
|
7917
|
117 |
|
13515
|
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
|
7917
|
125 |
|
13515
|
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}*}
|
7917
|
130 |
|
23378
|
131 |
from cM c'' c' have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
|
13515
|
132 |
(is "?case1 \<or> ?case2") ..
|
|
133 |
then show ?thesis
|
|
134 |
proof
|
|
135 |
assume ?case1
|
23378
|
136 |
have "(x, h x) \<in> graph H'' h''" by fact
|
27612
|
137 |
also have "\<dots> \<subseteq> graph H' h'" by fact
|
13515
|
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 {
|
23378
|
148 |
have "(y, h y) \<in> graph H' h'" by (rule y_hy)
|
|
149 |
also have "\<dots> \<subseteq> graph H'' h''" by fact
|
13515
|
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
|
9261
|
155 |
qed
|
|
156 |
qed
|
7917
|
157 |
|
10687
|
158 |
text {*
|
|
159 |
\medskip The relation induced by the graph of the supremum of a
|
13515
|
160 |
chain @{text c} is definite, i.~e.~t is the graph of a function.
|
|
161 |
*}
|
7917
|
162 |
|
10687
|
163 |
lemma sup_definite:
|
13515
|
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"
|
10687
|
169 |
proof -
|
13515
|
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" ..
|
7917
|
173 |
|
13515
|
174 |
from G1 c have "G1 \<in> M" ..
|
|
175 |
then obtain H1 h1 where G1_rep: "G1 = graph H1 h1"
|
27612
|
176 |
unfolding M_def by blast
|
7917
|
177 |
|
13515
|
178 |
from G2 c have "G2 \<in> M" ..
|
|
179 |
then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
|
27612
|
180 |
unfolding M_def by blast
|
7917
|
181 |
|
13515
|
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}*}
|
7917
|
185 |
|
13515
|
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
|
27612
|
191 |
then have "y = h2 x" ..
|
13515
|
192 |
also
|
|
193 |
from xz' G2_rep have "(x, z) \<in> graph H2 h2" by (simp only:)
|
27612
|
194 |
then have "z = h2 x" ..
|
13515
|
195 |
finally show ?thesis .
|
|
196 |
next
|
|
197 |
assume ?case2
|
|
198 |
with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast
|
27612
|
199 |
then have "z = h1 x" ..
|
13515
|
200 |
also
|
|
201 |
from xy' G1_rep have "(x, y) \<in> graph H1 h1" by (simp only:)
|
27612
|
202 |
then have "y = h1 x" ..
|
13515
|
203 |
finally show ?thesis ..
|
9261
|
204 |
qed
|
|
205 |
qed
|
7917
|
206 |
|
10687
|
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 |
*}
|
7917
|
215 |
|
10687
|
216 |
lemma sup_lf:
|
13515
|
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
|
7917
|
229 |
|
13515
|
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
|
7917
|
249 |
|
13515
|
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 .
|
9261
|
259 |
qed
|
|
260 |
qed
|
7917
|
261 |
|
10687
|
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 |
*}
|
7917
|
268 |
|
|
269 |
lemma sup_ext:
|
13515
|
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"
|
9261
|
275 |
proof -
|
13515
|
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 .
|
9261
|
286 |
qed
|
7917
|
287 |
|
10687
|
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 |
*}
|
7917
|
294 |
|
10687
|
295 |
lemma sup_supF:
|
13515
|
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)
|
9261
|
311 |
qed
|
7917
|
312 |
|
10687
|
313 |
text {*
|
|
314 |
\medskip The domain @{text H} of the limit function is a subspace of
|
|
315 |
@{text E}.
|
|
316 |
*}
|
7917
|
317 |
|
10687
|
318 |
lemma sup_subE:
|
13515
|
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 -
|
13547
|
329 |
from FE E have "0 \<in> F" by (rule subspace.zero)
|
13515
|
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"
|
9261
|
335 |
proof
|
13515
|
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 .
|
9261
|
366 |
qed
|
|
367 |
qed
|
7917
|
368 |
|
10687
|
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}.
|
9261
|
372 |
*}
|
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"
|
|
377 |
and cM: "c \<in> chain M"
|
|
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 |
|
10687
|
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}
|
9261
|
401 |
*}
|
7917
|
402 |
|
10687
|
403 |
lemma abs_ineq_iff:
|
27611
|
404 |
assumes "subspace H E" and "vectorspace E" and "seminorm E p"
|
|
405 |
and "linearform H h"
|
13515
|
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
|
27611
|
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
|
23378
|
412 |
have H: "vectorspace H" using `vectorspace E` ..
|
13515
|
413 |
{
|
9261
|
414 |
assume l: ?L
|
|
415 |
show ?R
|
|
416 |
proof
|
9503
|
417 |
fix x assume x: "x \<in> H"
|
13515
|
418 |
have "h x \<le> \<bar>h x\<bar>" by arith
|
|
419 |
also from l x have "\<dots> \<le> p x" ..
|
10687
|
420 |
finally show "h x \<le> p x" .
|
9261
|
421 |
qed
|
|
422 |
next
|
|
423 |
assume r: ?R
|
|
424 |
show ?L
|
10687
|
425 |
proof
|
13515
|
426 |
fix x assume x: "x \<in> H"
|
10687
|
427 |
show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
|
9261
|
428 |
by arith
|
23378
|
429 |
from `linearform H h` and H x
|
|
430 |
have "- h x = h (- x)" by (rule linearform.neg [symmetric])
|
14710
|
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"
|
23378
|
435 |
using `seminorm E p` `vectorspace E`
|
14710
|
436 |
proof (rule seminorm.minus)
|
|
437 |
from x show "x \<in> E" ..
|
9261
|
438 |
qed
|
14710
|
439 |
finally have "- h x \<le> p x" .
|
|
440 |
then show "- p x \<le> h x" by simp
|
13515
|
441 |
from r x show "h x \<le> p x" ..
|
9261
|
442 |
qed
|
13515
|
443 |
}
|
10687
|
444 |
qed
|
7917
|
445 |
|
10687
|
446 |
end
|