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