7917
|
1 |
(* Title: HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Gertrud Bauer, TU Munich
|
|
4 |
*)
|
|
5 |
|
7978
|
6 |
header {* Extending non-maximal functions *};
|
7917
|
7 |
|
|
8 |
theory HahnBanachExtLemmas = FunctionNorm:;
|
|
9 |
|
|
10 |
text{* In this section the following context is presumed.
|
|
11 |
Let $E$ be a real vector space with a
|
7978
|
12 |
seminorm $q$ on $E$. $F$ is a subspace of $E$ and $f$ a linear
|
7917
|
13 |
function on $F$. We consider a subspace $H$ of $E$ that is a
|
7978
|
14 |
superspace of $F$ and a linear form $h$ on $H$. $H$ is a not equal
|
7917
|
15 |
to $E$ and $x_0$ is an element in $E \backslash H$.
|
|
16 |
$H$ is extended to the direct sum $H_0 = H + \idt{lin}\ap x_0$, so for
|
|
17 |
any $x\in H_0$ the decomposition of $x = y + a \mult x$
|
|
18 |
with $y\in H$ is unique. $h_0$ is defined on $H_0$ by
|
7978
|
19 |
$h_0\ap x = h\ap y + a \cdot \xi$ for a certain $\xi$.
|
7917
|
20 |
|
|
21 |
Subsequently we show some properties of this extension $h_0$ of $h$.
|
|
22 |
*};
|
|
23 |
|
|
24 |
|
7978
|
25 |
text {* This lemma will be used to show the existence of a linear
|
|
26 |
extension of $f$ (see page \pageref{ex-xi-use}).
|
|
27 |
It is a consequence
|
|
28 |
of the completeness of $\bbbR$. To show
|
7917
|
29 |
\begin{matharray}{l}
|
7978
|
30 |
\Ex{\xi}{\All {y\in F}{a\ap y \leq \xi \land \xi \leq b\ap y}}
|
|
31 |
\end{matharray}
|
7917
|
32 |
it suffices to show that
|
7978
|
33 |
\begin{matharray}{l} \All
|
|
34 |
{u\in F}{\All {v\in F}{a\ap u \leq b \ap v}}
|
|
35 |
\end{matharray} *};
|
7917
|
36 |
|
|
37 |
lemma ex_xi:
|
|
38 |
"[| is_vectorspace F; !! u v. [| u:F; v:F |] ==> a u <= b v |]
|
7978
|
39 |
==> EX (xi::real). ALL y:F. a y <= xi & xi <= b y";
|
7917
|
40 |
proof -;
|
|
41 |
assume vs: "is_vectorspace F";
|
|
42 |
assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))";
|
|
43 |
|
|
44 |
txt {* From the completeness of the reals follows:
|
8084
|
45 |
The set $S = \{a\: u\dt\: u\in F\}$ has a supremum, if
|
7978
|
46 |
it is non-empty and has an upper bound. *};
|
7917
|
47 |
|
7978
|
48 |
let ?S = "{a u :: real | u. u:F}";
|
7917
|
49 |
|
|
50 |
have "EX xi. isLub UNIV ?S xi";
|
|
51 |
proof (rule reals_complete);
|
|
52 |
|
7978
|
53 |
txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *};
|
7917
|
54 |
|
8703
|
55 |
from vs; have "a 00 : ?S"; by force;
|
7917
|
56 |
thus "EX X. X : ?S"; ..;
|
|
57 |
|
7978
|
58 |
txt {* $b\ap \zero$ is an upper bound of $S$: *};
|
7917
|
59 |
|
|
60 |
show "EX Y. isUb UNIV ?S Y";
|
|
61 |
proof;
|
8703
|
62 |
show "isUb UNIV ?S (b 00)";
|
7917
|
63 |
proof (intro isUbI setleI ballI);
|
8703
|
64 |
show "b 00 : UNIV"; ..;
|
7978
|
65 |
next;
|
7917
|
66 |
|
7978
|
67 |
txt {* Every element $y\in S$ is less than $b\ap \zero$: *};
|
7917
|
68 |
|
|
69 |
fix y; assume y: "y : ?S";
|
7978
|
70 |
from y; have "EX u:F. y = a u"; by fast;
|
8703
|
71 |
thus "y <= b 00";
|
7917
|
72 |
proof;
|
7978
|
73 |
fix u; assume "u:F";
|
|
74 |
assume "y = a u";
|
8703
|
75 |
also; have "a u <= b 00"; by (rule r) (simp!)+;
|
7917
|
76 |
finally; show ?thesis; .;
|
|
77 |
qed;
|
|
78 |
qed;
|
|
79 |
qed;
|
|
80 |
qed;
|
|
81 |
|
7978
|
82 |
thus "EX xi. ALL y:F. a y <= xi & xi <= b y";
|
7917
|
83 |
proof (elim exE);
|
|
84 |
fix xi; assume "isLub UNIV ?S xi";
|
|
85 |
show ?thesis;
|
|
86 |
proof (intro exI conjI ballI);
|
|
87 |
|
7978
|
88 |
txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *};
|
7917
|
89 |
|
|
90 |
fix y; assume y: "y:F";
|
|
91 |
show "a y <= xi";
|
|
92 |
proof (rule isUbD);
|
|
93 |
show "isUb UNIV ?S xi"; ..;
|
|
94 |
qed (force!);
|
|
95 |
next;
|
|
96 |
|
7978
|
97 |
txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *};
|
7917
|
98 |
|
|
99 |
fix y; assume "y:F";
|
|
100 |
show "xi <= b y";
|
|
101 |
proof (intro isLub_le_isUb isUbI setleI);
|
7978
|
102 |
show "b y : UNIV"; ..;
|
7917
|
103 |
show "ALL ya : ?S. ya <= b y";
|
|
104 |
proof;
|
|
105 |
fix au; assume au: "au : ?S ";
|
7978
|
106 |
hence "EX u:F. au = a u"; by fast;
|
7917
|
107 |
thus "au <= b y";
|
|
108 |
proof;
|
|
109 |
fix u; assume "u:F"; assume "au = a u";
|
|
110 |
also; have "... <= b y"; by (rule r);
|
|
111 |
finally; show ?thesis; .;
|
|
112 |
qed;
|
|
113 |
qed;
|
|
114 |
qed;
|
|
115 |
qed;
|
|
116 |
qed;
|
|
117 |
qed;
|
|
118 |
|
8084
|
119 |
text{* \medskip The function $h_0$ is defined as a
|
|
120 |
$h_0\ap x = h\ap y + a\cdot \xi$ where $x = y + a\mult \xi$
|
7978
|
121 |
is a linear extension of $h$ to $H_0$. *};
|
7917
|
122 |
|
|
123 |
lemma h0_lf:
|
8703
|
124 |
"[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
|
7917
|
125 |
in h y + a * xi);
|
7978
|
126 |
H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H;
|
8703
|
127 |
x0 : E; x0 ~= 00; is_vectorspace E |]
|
7917
|
128 |
==> is_linearform H0 h0";
|
|
129 |
proof -;
|
|
130 |
assume h0_def:
|
8703
|
131 |
"h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
|
7917
|
132 |
in h y + a * xi)"
|
7978
|
133 |
and H0_def: "H0 == H + lin x0"
|
|
134 |
and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
|
8703
|
135 |
"x0 ~= 00" "x0 : E" "is_vectorspace E";
|
7917
|
136 |
|
|
137 |
have h0: "is_vectorspace H0";
|
7978
|
138 |
proof (unfold H0_def, rule vs_sum_vs);
|
7917
|
139 |
show "is_subspace (lin x0) E"; ..;
|
|
140 |
qed;
|
|
141 |
|
|
142 |
show ?thesis;
|
|
143 |
proof;
|
|
144 |
fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0";
|
|
145 |
|
7978
|
146 |
txt{* We now have to show that $h_0$ is additive, i.~e.\
|
7917
|
147 |
$h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$
|
|
148 |
for $x_1, x_2\in H$. *};
|
|
149 |
|
|
150 |
have x1x2: "x1 + x2 : H0";
|
|
151 |
by (rule vs_add_closed, rule h0);
|
|
152 |
from x1;
|
8703
|
153 |
have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H";
|
7978
|
154 |
by (unfold H0_def vs_sum_def lin_def) fast;
|
7917
|
155 |
from x2;
|
8703
|
156 |
have ex_x2: "EX y2 a2. x2 = y2 + a2 (*) x0 & y2 : H";
|
7978
|
157 |
by (unfold H0_def vs_sum_def lin_def) fast;
|
7917
|
158 |
from x1x2;
|
8703
|
159 |
have ex_x1x2: "EX y a. x1 + x2 = y + a (*) x0 & y : H";
|
7978
|
160 |
by (unfold H0_def vs_sum_def lin_def) fast;
|
7917
|
161 |
|
|
162 |
from ex_x1 ex_x2 ex_x1x2;
|
|
163 |
show "h0 (x1 + x2) = h0 x1 + h0 x2";
|
|
164 |
proof (elim exE conjE);
|
|
165 |
fix y1 y2 y a1 a2 a;
|
8703
|
166 |
assume y1: "x1 = y1 + a1 (*) x0" and y1': "y1 : H"
|
|
167 |
and y2: "x2 = y2 + a2 (*) x0" and y2': "y2 : H"
|
|
168 |
and y: "x1 + x2 = y + a (*) x0" and y': "y : H";
|
7917
|
169 |
|
|
170 |
have ya: "y1 + y2 = y & a1 + a2 = a";
|
8084
|
171 |
proof (rule decomp_H0);;
|
|
172 |
txt_raw {* \label{decomp-H0-use} *};;
|
8703
|
173 |
show "y1 + y2 + (a1 + a2) (*) x0 = y + a (*) x0";
|
7917
|
174 |
by (simp! add: vs_add_mult_distrib2 [of E]);
|
|
175 |
show "y1 + y2 : H"; ..;
|
|
176 |
qed;
|
|
177 |
|
|
178 |
have "h0 (x1 + x2) = h y + a * xi";
|
|
179 |
by (rule h0_definite);
|
|
180 |
also; have "... = h (y1 + y2) + (a1 + a2) * xi";
|
|
181 |
by (simp add: ya);
|
|
182 |
also; from vs y1' y2';
|
|
183 |
have "... = h y1 + h y2 + a1 * xi + a2 * xi";
|
7978
|
184 |
by (simp add: linearform_add [of H]
|
7917
|
185 |
real_add_mult_distrib);
|
|
186 |
also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)";
|
|
187 |
by simp;
|
|
188 |
also; have "h y1 + a1 * xi = h0 x1";
|
|
189 |
by (rule h0_definite [RS sym]);
|
|
190 |
also; have "h y2 + a2 * xi = h0 x2";
|
|
191 |
by (rule h0_definite [RS sym]);
|
|
192 |
finally; show ?thesis; .;
|
|
193 |
qed;
|
|
194 |
|
7978
|
195 |
txt{* We further have to show that $h_0$ is multiplicative,
|
7927
|
196 |
i.~e.\ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
|
7978
|
197 |
for $x\in H$ and $c\in \bbbR$.
|
7917
|
198 |
*};
|
|
199 |
|
|
200 |
next;
|
|
201 |
fix c x1; assume x1: "x1 : H0";
|
8703
|
202 |
have ax1: "c (*) x1 : H0";
|
7917
|
203 |
by (rule vs_mult_closed, rule h0);
|
|
204 |
from x1; have ex_x: "!! x. x: H0
|
8703
|
205 |
==> EX y a. x = y + a (*) x0 & y : H";
|
7978
|
206 |
by (unfold H0_def vs_sum_def lin_def) fast;
|
7917
|
207 |
|
8703
|
208 |
from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H";
|
7978
|
209 |
by (unfold H0_def vs_sum_def lin_def) fast;
|
8703
|
210 |
with ex_x [of "c (*) x1", OF ax1];
|
|
211 |
show "h0 (c (*) x1) = c * (h0 x1)";
|
7917
|
212 |
proof (elim exE conjE);
|
|
213 |
fix y1 y a1 a;
|
8703
|
214 |
assume y1: "x1 = y1 + a1 (*) x0" and y1': "y1 : H"
|
|
215 |
and y: "c (*) x1 = y + a (*) x0" and y': "y : H";
|
7917
|
216 |
|
8703
|
217 |
have ya: "c (*) y1 = y & c * a1 = a";
|
7917
|
218 |
proof (rule decomp_H0);
|
8703
|
219 |
show "c (*) y1 + (c * a1) (*) x0 = y + a (*) x0";
|
7917
|
220 |
by (simp! add: add: vs_add_mult_distrib1);
|
8703
|
221 |
show "c (*) y1 : H"; ..;
|
7917
|
222 |
qed;
|
|
223 |
|
8703
|
224 |
have "h0 (c (*) x1) = h y + a * xi";
|
7917
|
225 |
by (rule h0_definite);
|
8703
|
226 |
also; have "... = h (c (*) y1) + (c * a1) * xi";
|
7917
|
227 |
by (simp add: ya);
|
|
228 |
also; from vs y1'; have "... = c * h y1 + c * a1 * xi";
|
7978
|
229 |
by (simp add: linearform_mult [of H]);
|
7917
|
230 |
also; from vs y1'; have "... = c * (h y1 + a1 * xi)";
|
|
231 |
by (simp add: real_add_mult_distrib2 real_mult_assoc);
|
|
232 |
also; have "h y1 + a1 * xi = h0 x1";
|
|
233 |
by (rule h0_definite [RS sym]);
|
|
234 |
finally; show ?thesis; .;
|
|
235 |
qed;
|
|
236 |
qed;
|
|
237 |
qed;
|
|
238 |
|
8084
|
239 |
text{* \medskip The linear extension $h_0$ of $h$
|
7978
|
240 |
is bounded by the seminorm $p$. *};
|
7917
|
241 |
|
|
242 |
lemma h0_norm_pres:
|
8703
|
243 |
"[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
|
7917
|
244 |
in h y + a * xi);
|
8703
|
245 |
H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= 00; is_vectorspace E;
|
8084
|
246 |
is_subspace H E; is_seminorm E p; is_linearform H h; ALL y:H. h y <= p y;
|
|
247 |
ALL y:H. - p (y + x0) - h y <= xi & xi <= p (y + x0) - h y |]
|
7917
|
248 |
==> ALL x:H0. h0 x <= p x";
|
|
249 |
proof;
|
|
250 |
assume h0_def:
|
8703
|
251 |
"h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
|
7917
|
252 |
in (h y) + a * xi)"
|
7978
|
253 |
and H0_def: "H0 == H + lin x0"
|
8703
|
254 |
and vs: "x0 ~: H" "x0 : E" "x0 ~= 00" "is_vectorspace E"
|
7978
|
255 |
"is_subspace H E" "is_seminorm E p" "is_linearform H h"
|
|
256 |
and a: "ALL y:H. h y <= p y";
|
|
257 |
presume a1: "ALL ya:H. - p (ya + x0) - h ya <= xi";
|
|
258 |
presume a2: "ALL ya:H. xi <= p (ya + x0) - h ya";
|
7917
|
259 |
fix x; assume "x : H0";
|
|
260 |
have ex_x:
|
8703
|
261 |
"!! x. x : H0 ==> EX y a. x = y + a (*) x0 & y : H";
|
7978
|
262 |
by (unfold H0_def vs_sum_def lin_def) fast;
|
8703
|
263 |
have "EX y a. x = y + a (*) x0 & y : H";
|
7917
|
264 |
by (rule ex_x);
|
|
265 |
thus "h0 x <= p x";
|
|
266 |
proof (elim exE conjE);
|
8703
|
267 |
fix y a; assume x: "x = y + a (*) x0" and y: "y : H";
|
7917
|
268 |
have "h0 x = h y + a * xi";
|
|
269 |
by (rule h0_definite);
|
|
270 |
|
|
271 |
txt{* Now we show
|
7978
|
272 |
$h\ap y + a \cdot \xi\leq p\ap (y\plus a \mult x_0)$
|
8084
|
273 |
by case analysis on $a$. \label{linorder_linear_split}*};
|
7917
|
274 |
|
8703
|
275 |
also; have "... <= p (y + a (*) x0)";
|
7917
|
276 |
proof (rule linorder_linear_split);
|
|
277 |
|
|
278 |
assume z: "a = 0r";
|
|
279 |
with vs y a; show ?thesis; by simp;
|
|
280 |
|
7978
|
281 |
txt {* In the case $a < 0$, we use $a_1$ with $\idt{ya}$
|
|
282 |
taken as $y/a$: *};
|
7917
|
283 |
|
|
284 |
next;
|
|
285 |
assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
|
|
286 |
from a1;
|
8703
|
287 |
have "- p (rinv a (*) y + x0) - h (rinv a (*) y) <= xi";
|
7978
|
288 |
by (rule bspec) (simp!);
|
7917
|
289 |
|
7978
|
290 |
txt {* The thesis for this case now follows by a short
|
|
291 |
calculation. *};
|
7917
|
292 |
hence "a * xi
|
8703
|
293 |
<= a * (- p (rinv a (*) y + x0) - h (rinv a (*) y))";
|
7917
|
294 |
by (rule real_mult_less_le_anti [OF lz]);
|
8703
|
295 |
also; have "... = - a * (p (rinv a (*) y + x0))
|
|
296 |
- a * (h (rinv a (*) y))";
|
7917
|
297 |
by (rule real_mult_diff_distrib);
|
8703
|
298 |
also; from lz vs y; have "- a * (p (rinv a (*) y + x0))
|
|
299 |
= p (a (*) (rinv a (*) y + x0))";
|
8838
|
300 |
by (simp add: seminorm_abs_homogenous abs_minus_eqI2);
|
8703
|
301 |
also; from nz vs y; have "... = p (y + a (*) x0)";
|
7917
|
302 |
by (simp add: vs_add_mult_distrib1);
|
8703
|
303 |
also; from nz vs y; have "a * (h (rinv a (*) y)) = h y";
|
7978
|
304 |
by (simp add: linearform_mult [RS sym]);
|
8703
|
305 |
finally; have "a * xi <= p (y + a (*) x0) - h y"; .;
|
7917
|
306 |
|
8703
|
307 |
hence "h y + a * xi <= h y + p (y + a (*) x0) - h y";
|
7917
|
308 |
by (simp add: real_add_left_cancel_le);
|
|
309 |
thus ?thesis; by simp;
|
|
310 |
|
7978
|
311 |
txt {* In the case $a > 0$, we use $a_2$ with $\idt{ya}$
|
|
312 |
taken as $y/a$: *};
|
|
313 |
|
7917
|
314 |
next;
|
|
315 |
assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
|
7978
|
316 |
from a2;
|
8703
|
317 |
have "xi <= p (rinv a (*) y + x0) - h (rinv a (*) y)";
|
7978
|
318 |
by (rule bspec) (simp!);
|
7917
|
319 |
|
7978
|
320 |
txt {* The thesis for this case follows by a short
|
|
321 |
calculation: *};
|
7917
|
322 |
|
|
323 |
with gz; have "a * xi
|
8703
|
324 |
<= a * (p (rinv a (*) y + x0) - h (rinv a (*) y))";
|
7917
|
325 |
by (rule real_mult_less_le_mono);
|
8703
|
326 |
also; have "... = a * p (rinv a (*) y + x0)
|
|
327 |
- a * h (rinv a (*) y)";
|
7917
|
328 |
by (rule real_mult_diff_distrib2);
|
|
329 |
also; from gz vs y;
|
8703
|
330 |
have "a * p (rinv a (*) y + x0)
|
|
331 |
= p (a (*) (rinv a (*) y + x0))";
|
8838
|
332 |
by (simp add: seminorm_abs_homogenous abs_eqI2);
|
7917
|
333 |
also; from nz vs y;
|
8703
|
334 |
have "... = p (y + a (*) x0)";
|
7917
|
335 |
by (simp add: vs_add_mult_distrib1);
|
8703
|
336 |
also; from nz vs y; have "a * h (rinv a (*) y) = h y";
|
7978
|
337 |
by (simp add: linearform_mult [RS sym]);
|
8703
|
338 |
finally; have "a * xi <= p (y + a (*) x0) - h y"; .;
|
7917
|
339 |
|
8703
|
340 |
hence "h y + a * xi <= h y + (p (y + a (*) x0) - h y)";
|
7917
|
341 |
by (simp add: real_add_left_cancel_le);
|
|
342 |
thus ?thesis; by simp;
|
|
343 |
qed;
|
|
344 |
also; from x; have "... = p x"; by simp;
|
|
345 |
finally; show ?thesis; .;
|
|
346 |
qed;
|
|
347 |
qed blast+;
|
|
348 |
|
|
349 |
end; |