author | wenzelm |
Thu, 06 Jan 2000 16:00:18 +0100 | |
changeset 8109 | aca11f954993 |
parent 8108 | ce4bb031d664 |
child 8674 | ac6c028e0249 |
permissions | -rw-r--r-- |
7566 | 1 |
(* Title: HOL/Real/HahnBanach/HahnBanach.thy |
2 |
ID: $Id$ |
|
7978 | 3 |
Author: Gertrud Bauer, TU Munich |
7566 | 4 |
*) |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
5 |
|
7917 | 6 |
header {* The Hahn-Banach Theorem *}; |
7656 | 7 |
|
7917 | 8 |
theory HahnBanach |
9 |
= HahnBanachSupLemmas + HahnBanachExtLemmas + ZornLemma:; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
10 |
|
7808 | 11 |
text {* |
7917 | 12 |
We present the proof of two different versions of the Hahn-Banach |
7927 | 13 |
Theorem, closely following \cite[\S36]{Heuser:1986}. |
7808 | 14 |
*}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
15 |
|
8084 | 16 |
subsection {* The Hahn-Banach Theorem for vector spaces *}; |
17 |
||
18 |
text {* {\bf Theorem.} Let $f$ be a linear form defined on a subspace |
|
19 |
$F$ of a real vector space $E$, such that $f$ is bounded by a seminorm |
|
20 |
$p$. |
|
21 |
||
22 |
Then $f$ can be extended to a linear form $h$ on $E$ that is again |
|
23 |
bounded by $p$. |
|
24 |
||
25 |
\bigskip{\bf Proof Outline.} |
|
26 |
First we define the set $M$ of all norm-preserving extensions of $f$. |
|
27 |
We show that every chain in $M$ has an upper bound in $M$. |
|
28 |
With Zorn's lemma we can conclude that $M$ has a maximal element $g$. |
|
29 |
We further show by contradiction that the domain $H$ of $g$ is the whole |
|
30 |
vector space $E$. |
|
31 |
If $H \neq E$, then $g$ can be extended in |
|
32 |
a norm-preserving way to a greater vector space $H_0$. |
|
33 |
So $g$ cannot be maximal in $M$. |
|
34 |
\bigskip |
|
35 |
*}; |
|
36 |
||
37 |
theorem HahnBanach: "[| is_vectorspace E; is_subspace F E; |
|
38 |
is_seminorm E p; is_linearform F f; ALL x:F. f x <= p x |] |
|
39 |
==> EX h. is_linearform E h & (ALL x:F. h x = f x) |
|
40 |
& (ALL x:E. h x <= p x)"; |
|
41 |
proof -; |
|
42 |
||
43 |
txt {* Let $E$ be a vector space, $F$ a subspace of $E$, $p$ a seminorm on $E$ and $f$ a linear form on $F$ such that $f$ is bounded by $p$. *}; |
|
44 |
||
45 |
assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" |
|
46 |
"is_linearform F f" "ALL x:F. f x <= p x"; |
|
47 |
||
48 |
txt {* Define $M$ as the set of all norm-preserving extensions of $F$. *}; |
|
49 |
||
50 |
def M == "norm_pres_extensions E p F f"; |
|
51 |
{{; |
|
52 |
fix c; assume "c : chain M" "EX x. x:c"; |
|
53 |
||
54 |
txt {* Show that every non-empty chain $c$ in $M$ has an upper bound in $M$: $\Union c$ is greater that every element of the chain $c$, so $\Union c$ is an upper bound of $c$ that lies in $M$. *}; |
|
55 |
||
56 |
have "Union c : M"; |
|
57 |
proof (unfold M_def, rule norm_pres_extensionI); |
|
58 |
show "EX (H::'a set) h::'a => real. graph H h = Union c |
|
59 |
& is_linearform H h |
|
60 |
& is_subspace H E |
|
61 |
& is_subspace F H |
|
62 |
& graph F f <= graph H h |
|
63 |
& (ALL x::'a:H. h x <= p x)"; |
|
64 |
proof (intro exI conjI); |
|
65 |
let ?H = "domain (Union c)"; |
|
66 |
let ?h = "funct (Union c)"; |
|
67 |
||
68 |
show a: "graph ?H ?h = Union c"; |
|
69 |
proof (rule graph_domain_funct); |
|
70 |
fix x y z; assume "(x, y) : Union c" "(x, z) : Union c"; |
|
71 |
show "z = y"; by (rule sup_definite); |
|
72 |
qed; |
|
73 |
show "is_linearform ?H ?h"; |
|
74 |
by (simp! add: sup_lf a); |
|
75 |
show "is_subspace ?H E"; |
|
76 |
by (rule sup_subE, rule a) (simp!)+; |
|
77 |
show "is_subspace F ?H"; |
|
78 |
by (rule sup_supF, rule a) (simp!)+; |
|
79 |
show "graph F f <= graph ?H ?h"; |
|
80 |
by (rule sup_ext, rule a) (simp!)+; |
|
81 |
show "ALL x::'a:?H. ?h x <= p x"; |
|
82 |
by (rule sup_norm_pres, rule a) (simp!)+; |
|
83 |
qed; |
|
84 |
qed; |
|
85 |
}}; |
|
86 |
||
87 |
txt {* With Zorn's Lemma we can conclude that there is a maximal element $g$ in $M$. *}; |
|
88 |
||
8104 | 89 |
hence "EX g:M. ALL x:M. g <= x --> g = x"; |
8084 | 90 |
proof (rule Zorn's_Lemma); |
8104 | 91 |
txt {* We show that $M$ is non-empty: *}; |
8084 | 92 |
have "graph F f : norm_pres_extensions E p F f"; |
93 |
proof (rule norm_pres_extensionI2); |
|
94 |
have "is_vectorspace F"; ..; |
|
95 |
thus "is_subspace F F"; ..; |
|
96 |
qed (blast!)+; |
|
8104 | 97 |
thus "graph F f : M"; by (simp!); |
8084 | 98 |
qed; |
99 |
thus ?thesis; |
|
100 |
proof; |
|
101 |
||
102 |
txt {* We take this maximal element $g$. *}; |
|
103 |
||
104 |
fix g; assume "g:M" "ALL x:M. g <= x --> g = x"; |
|
105 |
show ?thesis; |
|
106 |
||
8104 | 107 |
txt {* $g$ is a norm-preserving extension of $f$, that is: $g$ |
108 |
is the graph of a linear form $h$, defined on a subspace $H$ of |
|
109 |
$E$, which is a superspace of $F$. $h$ is an extension of $f$ |
|
110 |
and $h$ is again bounded by $p$. *}; |
|
8084 | 111 |
|
8109 | 112 |
obtain H h where "graph H h = g" "is_linearform H h" |
8084 | 113 |
"is_subspace H E" "is_subspace F H" "graph F f <= graph H h" |
114 |
"ALL x:H. h x <= p x"; |
|
115 |
proof -; |
|
116 |
have "EX H h. graph H h = g & is_linearform H h |
|
117 |
& is_subspace H E & is_subspace F H |
|
118 |
& graph F f <= graph H h |
|
119 |
& (ALL x:H. h x <= p x)"; by (simp! add: norm_pres_extension_D); |
|
8107 | 120 |
thus ?thesis; by (elim exE conjE) rule; |
8084 | 121 |
qed; |
122 |
have h: "is_vectorspace H"; ..; |
|
123 |
||
124 |
txt {* We show that $h$ is defined on whole $E$ by classical contradiction. *}; |
|
125 |
||
126 |
have "H = E"; |
|
127 |
proof (rule classical); |
|
128 |
||
8104 | 129 |
txt {* Assume $h$ is not defined on whole $E$. *}; |
8084 | 130 |
|
131 |
assume "H ~= E"; |
|
132 |
||
133 |
txt {* Then show that $h$ can be extended in a norm-preserving way to a function $h_0$ with the graph $g_{h0}$. *}; |
|
134 |
||
135 |
have "EX g_h0 : M. g <= g_h0 & g ~= g_h0"; |
|
136 |
||
8104 | 137 |
txt {* Consider $x_0 \in E \setminus H$. *}; |
8084 | 138 |
|
8109 | 139 |
obtain x0 where "x0:E" "x0~:H"; |
8084 | 140 |
proof -; |
141 |
have "EX x0:E. x0~:H"; |
|
142 |
proof (rule set_less_imp_diff_not_empty); |
|
143 |
have "H <= E"; ..; |
|
144 |
thus "H < E"; ..; |
|
145 |
qed; |
|
8104 | 146 |
thus ?thesis; by blast; |
8084 | 147 |
qed; |
148 |
have x0: "x0 ~= <0>"; |
|
149 |
proof (rule classical); |
|
150 |
presume "x0 = <0>"; |
|
151 |
with h; have "x0:H"; by simp; |
|
152 |
thus ?thesis; by contradiction; |
|
153 |
qed blast; |
|
154 |
||
155 |
txt {* Define $H_0$ as the direct sum of $H$ and the linear closure of $x_0$. *}; |
|
156 |
||
157 |
def H0 == "H + lin x0"; |
|
158 |
show ?thesis; |
|
159 |
||
8104 | 160 |
txt {* Pick a real number $\xi$ that fulfills certain |
161 |
inequations, which will be used to establish that $h_0$ is |
|
162 |
a norm-preserving extension of $h$. *}; |
|
7656 | 163 |
|
8109 | 164 |
obtain xi where "ALL y:H. - p (y + x0) - h y <= xi |
8084 | 165 |
& xi <= p (y + x0) - h y"; |
166 |
proof -; |
|
167 |
from h; have "EX xi. ALL y:H. - p (y + x0) - h y <= xi |
|
168 |
& xi <= p (y + x0) - h y"; |
|
169 |
proof (rule ex_xi); |
|
170 |
fix u v; assume "u:H" "v:H"; |
|
171 |
from h; have "h v - h u = h (v - u)"; |
|
172 |
by (simp! add: linearform_diff); |
|
173 |
also; have "... <= p (v - u)"; |
|
174 |
by (simp!); |
|
175 |
also; have "v - u = x0 + - x0 + v + - u"; |
|
176 |
by (simp! add: diff_eq1); |
|
177 |
also; have "... = v + x0 + - (u + x0)"; |
|
178 |
by (simp!); |
|
179 |
also; have "... = (v + x0) - (u + x0)"; |
|
180 |
by (simp! add: diff_eq1); |
|
181 |
also; have "p ... <= p (v + x0) + p (u + x0)"; |
|
182 |
by (rule seminorm_diff_subadditive) (simp!)+; |
|
183 |
finally; have "h v - h u <= p (v + x0) + p (u + x0)"; .; |
|
184 |
||
185 |
thus "- p (u + x0) - h u <= p (v + x0) - h v"; |
|
186 |
by (rule real_diff_ineq_swap); |
|
187 |
qed; |
|
8107 | 188 |
thus ?thesis; by rule rule; |
8084 | 189 |
qed; |
190 |
||
191 |
txt {* Define the extension $h_0$ of $h$ to $H_0$ using $\xi$. *}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
192 |
|
8084 | 193 |
def h0 == "\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0 |
194 |
& y:H |
|
195 |
in (h y) + a * xi"; |
|
196 |
show ?thesis; |
|
197 |
proof; |
|
198 |
||
199 |
txt {* Show that $h_0$ is an extension of $h$ *}; |
|
200 |
||
201 |
show "g <= graph H0 h0 & g ~= graph H0 h0"; |
|
202 |
proof; |
|
203 |
show "g <= graph H0 h0"; |
|
204 |
proof -; |
|
205 |
have "graph H h <= graph H0 h0"; |
|
206 |
proof (rule graph_extI); |
|
207 |
fix t; assume "t:H"; |
|
208 |
have "(SOME (y, a). t = y + a <*> x0 & y : H) |
|
209 |
= (t,0r)"; |
|
210 |
by (rule decomp_H0_H, rule x0); |
|
211 |
thus "h t = h0 t"; by (simp! add: Let_def); |
|
212 |
next; |
|
213 |
show "H <= H0"; |
|
214 |
proof (rule subspace_subset); |
|
215 |
show "is_subspace H H0"; |
|
216 |
proof (unfold H0_def, rule subspace_vs_sum1); |
|
217 |
show "is_vectorspace H"; ..; |
|
218 |
show "is_vectorspace (lin x0)"; ..; |
|
219 |
qed; |
|
220 |
qed; |
|
221 |
qed; |
|
222 |
thus ?thesis; by (simp!); |
|
223 |
qed; |
|
224 |
show "g ~= graph H0 h0"; |
|
225 |
proof -; |
|
226 |
have "graph H h ~= graph H0 h0"; |
|
227 |
proof; |
|
228 |
assume e: "graph H h = graph H0 h0"; |
|
229 |
have "x0 : H0"; |
|
230 |
proof (unfold H0_def, rule vs_sumI); |
|
231 |
show "x0 = <0> + x0"; by (simp!); |
|
232 |
from h; show "<0> : H"; ..; |
|
233 |
show "x0 : lin x0"; by (rule x_lin_x); |
|
234 |
qed; |
|
235 |
hence "(x0, h0 x0) : graph H0 h0"; ..; |
|
236 |
with e; have "(x0, h0 x0) : graph H h"; by simp; |
|
237 |
hence "x0 : H"; ..; |
|
238 |
thus False; by contradiction; |
|
239 |
qed; |
|
240 |
thus ?thesis; by (simp!); |
|
241 |
qed; |
|
242 |
qed; |
|
243 |
||
244 |
txt {* and $h_0$ is norm-preserving. *}; |
|
245 |
||
246 |
show "graph H0 h0 : M"; |
|
247 |
proof -; |
|
248 |
have "graph H0 h0 : norm_pres_extensions E p F f"; |
|
249 |
proof (rule norm_pres_extensionI2); |
|
250 |
show "is_linearform H0 h0"; |
|
251 |
by (rule h0_lf, rule x0) (simp!)+; |
|
252 |
show "is_subspace H0 E"; |
|
253 |
by (unfold H0_def, rule vs_sum_subspace, |
|
254 |
rule lin_subspace); |
|
255 |
have "is_subspace F H"; .; |
|
256 |
also; from h lin_vs; |
|
257 |
have [fold H0_def]: "is_subspace H (H + lin x0)"; ..; |
|
258 |
finally (subspace_trans [OF _ h]); |
|
259 |
show f_h0: "is_subspace F H0"; .; |
|
260 |
||
261 |
show "graph F f <= graph H0 h0"; |
|
262 |
proof (rule graph_extI); |
|
263 |
fix x; assume "x:F"; |
|
264 |
have "f x = h x"; ..; |
|
265 |
also; have " ... = h x + 0r * xi"; by simp; |
|
266 |
also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)"; |
|
267 |
by (simp add: Let_def); |
|
268 |
also; have |
|
269 |
"(x, 0r) = (SOME (y, a). x = y + a <*> x0 & y : H)"; |
|
270 |
by (rule decomp_H0_H [RS sym], rule x0) (simp!)+; |
|
271 |
also; have |
|
272 |
"(let (y,a) = (SOME (y,a). x = y + a <*> x0 & y : H) |
|
273 |
in h y + a * xi) |
|
274 |
= h0 x"; by (simp!); |
|
275 |
finally; show "f x = h0 x"; .; |
|
276 |
next; |
|
277 |
from f_h0; show "F <= H0"; ..; |
|
278 |
qed; |
|
279 |
||
280 |
show "ALL x:H0. h0 x <= p x"; |
|
281 |
by (rule h0_norm_pres, rule x0); |
|
282 |
qed; |
|
283 |
thus "graph H0 h0 : M"; by (simp!); |
|
284 |
qed; |
|
285 |
qed; |
|
286 |
qed; |
|
287 |
qed; |
|
288 |
||
289 |
txt {* So the graph $g$ of $h$ cannot be maximal. Contradiction. *}; |
|
290 |
||
291 |
hence "~ (ALL x:M. g <= x --> g = x)"; by simp; |
|
292 |
thus ?thesis; by contradiction; |
|
293 |
qed; |
|
294 |
||
295 |
txt {* Now we have a linear extension $h$ of $f$ to $E$ that is |
|
296 |
bounded by $p$. *}; |
|
297 |
||
298 |
thus "EX h. is_linearform E h & (ALL x:F. h x = f x) |
|
299 |
& (ALL x:E. h x <= p x)"; |
|
300 |
proof (intro exI conjI); |
|
301 |
assume eq: "H = E"; |
|
302 |
from eq; show "is_linearform E h"; by (simp!); |
|
303 |
show "ALL x:F. h x = f x"; |
|
304 |
proof (intro ballI, rule sym); |
|
305 |
fix x; assume "x:F"; show "f x = h x "; ..; |
|
306 |
qed; |
|
307 |
from eq; show "ALL x:E. h x <= p x"; by (force!); |
|
308 |
qed; |
|
309 |
qed; |
|
310 |
qed; |
|
311 |
qed; |
|
312 |
(* |
|
7917 | 313 |
theorem HahnBanach: |
7978 | 314 |
"[| is_vectorspace E; is_subspace F E; is_seminorm E p; |
7808 | 315 |
is_linearform F f; ALL x:F. f x <= p x |] |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
316 |
==> EX h. is_linearform E h |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
317 |
& (ALL x:F. h x = f x) |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
318 |
& (ALL x:E. h x <= p x)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
319 |
proof -; |
7978 | 320 |
assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" |
7808 | 321 |
"is_linearform F f" "ALL x:F. f x <= p x"; |
7656 | 322 |
|
7917 | 323 |
txt{* We define $M$ to be the set of all linear extensions |
324 |
of $f$ to superspaces of $F$, which are bounded by $p$. *}; |
|
325 |
||
7656 | 326 |
def M == "norm_pres_extensions E p F f"; |
7917 | 327 |
|
328 |
txt{* We show that $M$ is non-empty: *}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
329 |
|
7656 | 330 |
have aM: "graph F f : norm_pres_extensions E p F f"; |
331 |
proof (rule norm_pres_extensionI2); |
|
7917 | 332 |
have "is_vectorspace F"; ..; |
333 |
thus "is_subspace F F"; ..; |
|
7566 | 334 |
qed (blast!)+; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
335 |
|
8084 | 336 |
subsubsect {* Existence of a limit function *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
337 |
|
7978 | 338 |
txt {* For every non-empty chain of norm-preserving extensions |
339 |
the union of all functions in the chain is again a norm-preserving |
|
340 |
extension. (The union is an upper bound for all elements. |
|
7917 | 341 |
It is even the least upper bound, because every upper bound of $M$ |
8084 | 342 |
is also an upper bound for $\Union c$, as $\Union c\in M$) *}; |
7917 | 343 |
|
7978 | 344 |
{{; |
7917 | 345 |
fix c; assume "c:chain M" "EX x. x:c"; |
7978 | 346 |
have "Union c : M"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
347 |
|
7656 | 348 |
proof (unfold M_def, rule norm_pres_extensionI); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
349 |
show "EX (H::'a set) h::'a => real. graph H h = Union c |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
350 |
& is_linearform H h |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
351 |
& is_subspace H E |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
352 |
& is_subspace F H |
7917 | 353 |
& graph F f <= graph H h |
354 |
& (ALL x::'a:H. h x <= p x)"; |
|
7656 | 355 |
proof (intro exI conjI); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
356 |
let ?H = "domain (Union c)"; |
7656 | 357 |
let ?h = "funct (Union c)"; |
358 |
||
7978 | 359 |
show a: "graph ?H ?h = Union c"; |
7656 | 360 |
proof (rule graph_domain_funct); |
361 |
fix x y z; assume "(x, y) : Union c" "(x, z) : Union c"; |
|
7917 | 362 |
show "z = y"; by (rule sup_definite); |
7656 | 363 |
qed; |
7978 | 364 |
show "is_linearform ?H ?h"; |
7917 | 365 |
by (simp! add: sup_lf a); |
366 |
show "is_subspace ?H E"; |
|
7656 | 367 |
by (rule sup_subE, rule a) (simp!)+; |
7917 | 368 |
show "is_subspace F ?H"; |
7656 | 369 |
by (rule sup_supF, rule a) (simp!)+; |
7917 | 370 |
show "graph F f <= graph ?H ?h"; |
7656 | 371 |
by (rule sup_ext, rule a) (simp!)+; |
372 |
show "ALL x::'a:?H. ?h x <= p x"; |
|
373 |
by (rule sup_norm_pres, rule a) (simp!)+; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
374 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
375 |
qed; |
7978 | 376 |
}}; |
7656 | 377 |
|
7927 | 378 |
txt {* According to Zorn's Lemma there is |
7917 | 379 |
a maximal norm-preserving extension $g\in M$. *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
380 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
381 |
with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x"; |
7566 | 382 |
by (simp! add: Zorn's_Lemma); |
7656 | 383 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
384 |
thus ?thesis; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
385 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
386 |
fix g; assume g: "g:M" "ALL x:M. g <= x --> g = x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
387 |
|
7917 | 388 |
have ex_Hh: |
389 |
"EX H h. graph H h = g |
|
390 |
& is_linearform H h |
|
391 |
& is_subspace H E |
|
392 |
& is_subspace F H |
|
393 |
& graph F f <= graph H h |
|
394 |
& (ALL x:H. h x <= p x) "; |
|
7656 | 395 |
by (simp! add: norm_pres_extension_D); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
396 |
thus ?thesis; |
7917 | 397 |
proof (elim exE conjE, intro exI); |
7656 | 398 |
fix H h; |
7808 | 399 |
assume "graph H h = g" "is_linearform (H::'a set) h" |
400 |
"is_subspace H E" "is_subspace F H" |
|
7917 | 401 |
and h_ext: "graph F f <= graph H h" |
402 |
and h_bound: "ALL x:H. h x <= p x"; |
|
7656 | 403 |
|
7917 | 404 |
have h: "is_vectorspace H"; ..; |
405 |
have f: "is_vectorspace F"; ..; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
406 |
|
7978 | 407 |
subsubsect {* The domain of the limit function *}; |
7656 | 408 |
|
7808 | 409 |
have eq: "H = E"; |
410 |
proof (rule classical); |
|
7656 | 411 |
|
7978 | 412 |
txt {* Assume that the domain of the supremum is not $E$, *}; |
8084 | 413 |
|
7808 | 414 |
assume "H ~= E"; |
7917 | 415 |
have "H <= E"; ..; |
416 |
hence "H < E"; ..; |
|
417 |
||
8084 | 418 |
txt{* then there exists an element $x_0$ in $E \setminus H$: *}; |
7656 | 419 |
|
7917 | 420 |
hence "EX x0:E. x0~:H"; |
421 |
by (rule set_less_imp_diff_not_empty); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
422 |
|
7917 | 423 |
txt {* We get that $h$ can be extended in a |
424 |
norm-preserving way to some $H_0$. *}; |
|
8084 | 425 |
|
7917 | 426 |
hence "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 |
427 |
& graph H0 h0 : M"; |
|
428 |
proof; |
|
429 |
fix x0; assume "x0:E" "x0~:H"; |
|
7656 | 430 |
|
7917 | 431 |
have x0: "x0 ~= <0>"; |
432 |
proof (rule classical); |
|
433 |
presume "x0 = <0>"; |
|
434 |
with h; have "x0:H"; by simp; |
|
435 |
thus ?thesis; by contradiction; |
|
436 |
qed blast; |
|
437 |
||
438 |
txt {* Define $H_0$ as the (direct) sum of H and the |
|
7978 | 439 |
linear closure of $x_0$. \label{ex-xi-use}*}; |
7917 | 440 |
|
441 |
def H0 == "H + lin x0"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
442 |
|
7978 | 443 |
from h; have xi: "EX xi. ALL y:H. - p (y + x0) - h y <= xi |
444 |
& xi <= p (y + x0) - h y"; |
|
7917 | 445 |
proof (rule ex_xi); |
446 |
fix u v; assume "u:H" "v:H"; |
|
447 |
from h; have "h v - h u = h (v - u)"; |
|
7978 | 448 |
by (simp! add: linearform_diff); |
7917 | 449 |
also; from h_bound; have "... <= p (v - u)"; |
450 |
by (simp!); |
|
451 |
also; have "v - u = x0 + - x0 + v + - u"; |
|
452 |
by (simp! add: diff_eq1); |
|
453 |
also; have "... = v + x0 + - (u + x0)"; |
|
454 |
by (simp!); |
|
455 |
also; have "... = (v + x0) - (u + x0)"; |
|
456 |
by (simp! add: diff_eq1); |
|
457 |
also; have "p ... <= p (v + x0) + p (u + x0)"; |
|
7978 | 458 |
by (rule seminorm_diff_subadditive) (simp!)+; |
7917 | 459 |
finally; have "h v - h u <= p (v + x0) + p (u + x0)"; .; |
7808 | 460 |
|
7917 | 461 |
thus "- p (u + x0) - h u <= p (v + x0) - h v"; |
462 |
by (rule real_diff_ineq_swap); |
|
463 |
qed; |
|
464 |
hence "EX h0. g <= graph H0 h0 & g ~= graph H0 h0 |
|
465 |
& graph H0 h0 : M"; |
|
466 |
proof (elim exE, intro exI conjI); |
|
467 |
fix xi; |
|
7978 | 468 |
assume a: "ALL y:H. - p (y + x0) - h y <= xi |
469 |
& xi <= p (y + x0) - h y"; |
|
7917 | 470 |
|
7978 | 471 |
txt {* Define $h_0$ as the canonical linear extension |
472 |
of $h$ on $H_0$:*}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
473 |
|
7917 | 474 |
def h0 == |
7978 | 475 |
"\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0 & y:H |
7917 | 476 |
in (h y) + a * xi"; |
7808 | 477 |
|
8084 | 478 |
txt {* We get that the graph of $h_0$ extends that of |
7917 | 479 |
$h$. *}; |
480 |
||
481 |
have "graph H h <= graph H0 h0"; |
|
482 |
proof (rule graph_extI); |
|
483 |
fix t; assume "t:H"; |
|
484 |
have "(SOME (y, a). t = y + a <*> x0 & y : H) = (t,0r)"; |
|
485 |
by (rule decomp_H0_H, rule x0); |
|
486 |
thus "h t = h0 t"; by (simp! add: Let_def); |
|
487 |
next; |
|
488 |
show "H <= H0"; |
|
489 |
proof (rule subspace_subset); |
|
490 |
show "is_subspace H H0"; |
|
491 |
proof (unfold H0_def, rule subspace_vs_sum1); |
|
492 |
show "is_vectorspace H"; ..; |
|
493 |
show "is_vectorspace (lin x0)"; ..; |
|
7566 | 494 |
qed; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
495 |
qed; |
7808 | 496 |
qed; |
7917 | 497 |
thus "g <= graph H0 h0"; by (simp!); |
7808 | 498 |
|
7917 | 499 |
txt {* Apparently $h_0$ is not equal to $h$. *}; |
500 |
||
501 |
have "graph H h ~= graph H0 h0"; |
|
502 |
proof; |
|
503 |
assume e: "graph H h = graph H0 h0"; |
|
504 |
have "x0 : H0"; |
|
505 |
proof (unfold H0_def, rule vs_sumI); |
|
506 |
show "x0 = <0> + x0"; by (simp!); |
|
507 |
from h; show "<0> : H"; ..; |
|
508 |
show "x0 : lin x0"; by (rule x_lin_x); |
|
509 |
qed; |
|
510 |
hence "(x0, h0 x0) : graph H0 h0"; ..; |
|
511 |
with e; have "(x0, h0 x0) : graph H h"; by simp; |
|
512 |
hence "x0 : H"; ..; |
|
513 |
thus False; by contradiction; |
|
514 |
qed; |
|
515 |
thus "g ~= graph H0 h0"; by (simp!); |
|
516 |
||
7978 | 517 |
txt {* Furthermore $h_0$ is a norm-preserving extension |
7917 | 518 |
of $f$. *}; |
519 |
||
520 |
have "graph H0 h0 : norm_pres_extensions E p F f"; |
|
521 |
proof (rule norm_pres_extensionI2); |
|
522 |
show "is_linearform H0 h0"; |
|
523 |
by (rule h0_lf, rule x0) (simp!)+; |
|
524 |
show "is_subspace H0 E"; |
|
525 |
by (unfold H0_def, rule vs_sum_subspace, |
|
526 |
rule lin_subspace); |
|
527 |
||
528 |
have "is_subspace F H"; .; |
|
529 |
also; from h lin_vs; |
|
530 |
have [fold H0_def]: "is_subspace H (H + lin x0)"; ..; |
|
531 |
finally (subspace_trans [OF _ h]); |
|
532 |
show f_h0: "is_subspace F H0"; .; (*** |
|
533 |
backwards: |
|
534 |
show f_h0: "is_subspace F H0"; .; |
|
535 |
proof (rule subspace_trans [of F H H0]); |
|
536 |
from h lin_vs; |
|
537 |
have "is_subspace H (H + lin x0)"; ..; |
|
538 |
thus "is_subspace H H0"; by (unfold H0_def); |
|
539 |
qed; ***) |
|
540 |
||
541 |
show "graph F f <= graph H0 h0"; |
|
542 |
proof (rule graph_extI); |
|
543 |
fix x; assume "x:F"; |
|
544 |
have "f x = h x"; ..; |
|
545 |
also; have " ... = h x + 0r * xi"; by simp; |
|
546 |
also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)"; |
|
547 |
by (simp add: Let_def); |
|
548 |
also; have |
|
549 |
"(x, 0r) = (SOME (y, a). x = y + a <*> x0 & y : H)"; |
|
550 |
by (rule decomp_H0_H [RS sym], rule x0) (simp!)+; |
|
551 |
also; have |
|
552 |
"(let (y,a) = (SOME (y,a). x = y + a <*> x0 & y : H) |
|
553 |
in h y + a * xi) |
|
554 |
= h0 x"; by (simp!); |
|
555 |
finally; show "f x = h0 x"; .; |
|
556 |
next; |
|
557 |
from f_h0; show "F <= H0"; ..; |
|
558 |
qed; |
|
559 |
||
560 |
show "ALL x:H0. h0 x <= p x"; |
|
8084 | 561 |
by (rule h0_norm_pres, rule x0) (assumption | simp!)+; |
7917 | 562 |
qed; |
563 |
thus "graph H0 h0 : M"; by (simp!); |
|
7808 | 564 |
qed; |
7917 | 565 |
thus ?thesis; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
566 |
qed; |
7917 | 567 |
|
7927 | 568 |
txt {* We have shown that $h$ can still be extended to |
7917 | 569 |
some $h_0$, in contradiction to the assumption that |
570 |
$h$ is a maximal element. *}; |
|
571 |
||
572 |
hence "EX x:M. g <= x & g ~= x"; |
|
573 |
by (elim exE conjE, intro bexI conjI); |
|
574 |
hence "~ (ALL x:M. g <= x --> g = x)"; by simp; |
|
575 |
thus ?thesis; by contradiction; |
|
7808 | 576 |
qed; |
577 |
||
7927 | 578 |
txt{* It follows $H = E$, and the thesis can be shown. *}; |
7917 | 579 |
|
7808 | 580 |
show "is_linearform E h & (ALL x:F. h x = f x) |
581 |
& (ALL x:E. h x <= p x)"; |
|
582 |
proof (intro conjI); |
|
583 |
from eq; show "is_linearform E h"; by (simp!); |
|
584 |
show "ALL x:F. h x = f x"; |
|
585 |
proof (intro ballI, rule sym); |
|
586 |
fix x; assume "x:F"; show "f x = h x "; ..; |
|
587 |
qed; |
|
588 |
from eq; show "ALL x:E. h x <= p x"; by (force!); |
|
7917 | 589 |
qed; |
590 |
||
591 |
qed; |
|
592 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
593 |
qed; |
8084 | 594 |
*) |
7917 | 595 |
|
596 |
||
8084 | 597 |
subsection {* Alternative formulation *}; |
7656 | 598 |
|
7978 | 599 |
text {* The following alternative formulation of the Hahn-Banach |
8084 | 600 |
Theorem\label{rabs-HahnBanach} uses the fact that for a real linear form |
601 |
$f$ and a seminorm $p$ the |
|
7978 | 602 |
following inequations are equivalent:\footnote{This was shown in lemma |
603 |
$\idt{rabs{\dsh}ineq{\dsh}iff}$ (see page \pageref{rabs-ineq-iff}).} |
|
7917 | 604 |
\begin{matharray}{ll} |
605 |
\forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\ |
|
606 |
\forall x\in H.\ap h\ap x\leq p\ap x\\ |
|
607 |
\end{matharray} |
|
7978 | 608 |
*}; |
7917 | 609 |
|
610 |
theorem rabs_HahnBanach: |
|
8084 | 611 |
"[| is_vectorspace E; is_subspace F E; is_linearform F f; |
612 |
is_seminorm E p; ALL x:F. rabs (f x) <= p x |] |
|
613 |
==> EX g. is_linearform E g & (ALL x:F. g x = f x) |
|
614 |
& (ALL x:E. rabs (g x) <= p x)"; |
|
615 |
proof -; |
|
616 |
assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" |
|
617 |
"is_linearform F f" "ALL x:F. rabs (f x) <= p x"; |
|
618 |
have "ALL x:F. f x <= p x"; by (rule rabs_ineq_iff [RS iffD1]); |
|
7808 | 619 |
hence "EX g. is_linearform E g & (ALL x:F. g x = f x) |
620 |
& (ALL x:E. g x <= p x)"; |
|
7917 | 621 |
by (simp! only: HahnBanach); |
8084 | 622 |
thus ?thesis; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
623 |
proof (elim exE conjE); |
7808 | 624 |
fix g; assume "is_linearform E g" "ALL x:F. g x = f x" |
625 |
"ALL x:E. g x <= p x"; |
|
8084 | 626 |
hence "ALL x:E. rabs (g x) <= p x"; |
627 |
by (simp! add: rabs_ineq_iff [OF subspace_refl]); |
|
628 |
thus ?thesis; by (intro exI conjI); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
629 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
630 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
631 |
|
7917 | 632 |
subsection {* The Hahn-Banach Theorem for normed spaces *}; |
7656 | 633 |
|
7978 | 634 |
text {* Every continuous linear form $f$ on a subspace $F$ of a |
635 |
norm space $E$, can be extended to a continuous linear form $g$ on |
|
636 |
$E$ such that $\fnorm{f} = \fnorm {g}$. *}; |
|
7656 | 637 |
|
7917 | 638 |
theorem norm_HahnBanach: |
639 |
"[| is_normed_vectorspace E norm; is_subspace F E; |
|
7978 | 640 |
is_linearform F f; is_continuous F norm f |] |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
641 |
==> EX g. is_linearform E g |
7978 | 642 |
& is_continuous E norm g |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
643 |
& (ALL x:F. g x = f x) |
7917 | 644 |
& function_norm E norm g = function_norm F norm f"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
645 |
proof -; |
7917 | 646 |
assume e_norm: "is_normed_vectorspace E norm"; |
647 |
assume f: "is_subspace F E" "is_linearform F f"; |
|
7978 | 648 |
assume f_cont: "is_continuous F norm f"; |
7566 | 649 |
have e: "is_vectorspace E"; ..; |
7917 | 650 |
with _; have f_norm: "is_normed_vectorspace F norm"; ..; |
7656 | 651 |
|
8084 | 652 |
txt{* We define a function $p$ on $E$ as follows: |
7917 | 653 |
\begin{matharray}{l} |
8084 | 654 |
p \: x = \fnorm f \cdot \norm x\\ |
7917 | 655 |
\end{matharray} |
656 |
*}; |
|
657 |
||
658 |
def p == "\<lambda>x. function_norm F norm f * norm x"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
659 |
|
7978 | 660 |
txt{* $p$ is a seminorm on $E$: *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
661 |
|
7978 | 662 |
have q: "is_seminorm E p"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
663 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
664 |
fix x y a; assume "x:E" "y:E"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
665 |
|
7917 | 666 |
txt{* $p$ is positive definite: *}; |
667 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
668 |
show "0r <= p x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
669 |
proof (unfold p_def, rule real_le_mult_order); |
7917 | 670 |
from _ f_norm; show "0r <= function_norm F norm f"; ..; |
7566 | 671 |
show "0r <= norm x"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
672 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
673 |
|
7978 | 674 |
txt{* $p$ is absolutely homogenous: *}; |
7917 | 675 |
|
676 |
show "p (a <*> x) = rabs a * p x"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
677 |
proof -; |
7917 | 678 |
have "p (a <*> x) = function_norm F norm f * norm (a <*> x)"; |
7808 | 679 |
by (simp!); |
7917 | 680 |
also; have "norm (a <*> x) = rabs a * norm x"; |
7978 | 681 |
by (rule normed_vs_norm_rabs_homogenous); |
7917 | 682 |
also; have "function_norm F norm f * (rabs a * norm x) |
683 |
= rabs a * (function_norm F norm f * norm x)"; |
|
7566 | 684 |
by (simp! only: real_mult_left_commute); |
7917 | 685 |
also; have "... = rabs a * p x"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
686 |
finally; show ?thesis; .; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
687 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
688 |
|
7978 | 689 |
txt{* Furthermore, $p$ is subadditive: *}; |
7917 | 690 |
|
691 |
show "p (x + y) <= p x + p y"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
692 |
proof -; |
7917 | 693 |
have "p (x + y) = function_norm F norm f * norm (x + y)"; |
7808 | 694 |
by (simp!); |
7917 | 695 |
also; |
696 |
have "... <= function_norm F norm f * (norm x + norm y)"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
697 |
proof (rule real_mult_le_le_mono1); |
7917 | 698 |
from _ f_norm; show "0r <= function_norm F norm f"; ..; |
699 |
show "norm (x + y) <= norm x + norm y"; ..; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
700 |
qed; |
7917 | 701 |
also; have "... = function_norm F norm f * norm x |
702 |
+ function_norm F norm f * norm y"; |
|
7566 | 703 |
by (simp! only: real_add_mult_distrib2); |
704 |
finally; show ?thesis; by (simp!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
705 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
706 |
qed; |
7917 | 707 |
|
708 |
txt{* $f$ is bounded by $p$. *}; |
|
709 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
710 |
have "ALL x:F. rabs (f x) <= p x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
711 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
712 |
fix x; assume "x:F"; |
7917 | 713 |
from f_norm; show "rabs (f x) <= p x"; |
7808 | 714 |
by (simp! add: norm_fx_le_norm_f_norm_x); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
715 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
716 |
|
7978 | 717 |
txt{* Using the fact that $p$ is a seminorm and |
8084 | 718 |
$f$ is bounded by $p$ we can apply the Hahn-Banach Theorem |
7978 | 719 |
for real vector spaces. |
720 |
So $f$ can be extended in a norm-preserving way to some function |
|
7917 | 721 |
$g$ on the whole vector space $E$. *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
722 |
|
7917 | 723 |
with e f q; |
724 |
have "EX g. is_linearform E g & (ALL x:F. g x = f x) |
|
725 |
& (ALL x:E. rabs (g x) <= p x)"; |
|
726 |
by (simp! add: rabs_HahnBanach); |
|
727 |
||
728 |
thus ?thesis; |
|
729 |
proof (elim exE conjE); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
730 |
fix g; |
7808 | 731 |
assume "is_linearform E g" and a: "ALL x:F. g x = f x" |
7978 | 732 |
and b: "ALL x:E. rabs (g x) <= p x"; |
7917 | 733 |
|
734 |
show "EX g. is_linearform E g |
|
7978 | 735 |
& is_continuous E norm g |
7917 | 736 |
& (ALL x:F. g x = f x) |
737 |
& function_norm E norm g = function_norm F norm f"; |
|
738 |
proof (intro exI conjI); |
|
739 |
||
8084 | 740 |
txt{* We furthermore have to show that |
7978 | 741 |
$g$ is also continuous: *}; |
7917 | 742 |
|
7978 | 743 |
show g_cont: "is_continuous E norm g"; |
7917 | 744 |
proof; |
745 |
fix x; assume "x:E"; |
|
7978 | 746 |
from b [RS bspec, OF this]; |
7917 | 747 |
show "rabs (g x) <= function_norm F norm f * norm x"; |
7978 | 748 |
by (unfold p_def); |
7917 | 749 |
qed; |
750 |
||
7978 | 751 |
txt {* To complete the proof, we show that |
8084 | 752 |
$\fnorm g = \fnorm f$. \label{order_antisym} *}; |
7978 | 753 |
|
7917 | 754 |
show "function_norm E norm g = function_norm F norm f" |
755 |
(is "?L = ?R"); |
|
756 |
proof (rule order_antisym); |
|
757 |
||
7978 | 758 |
txt{* First we show $\fnorm g \leq \fnorm f$. The function norm |
759 |
$\fnorm g$ is defined as the smallest $c\in\bbbR$ such that |
|
7917 | 760 |
\begin{matharray}{l} |
7978 | 761 |
\All {x\in E} {|g\ap x| \leq c \cdot \norm x} |
762 |
\end{matharray} |
|
763 |
Furthermore holds |
|
764 |
\begin{matharray}{l} |
|
765 |
\All {x\in E} {|g\ap x| \leq \fnorm f \cdot \norm x} |
|
766 |
\end{matharray} |
|
767 |
*}; |
|
768 |
||
7917 | 769 |
have "ALL x:E. rabs (g x) <= function_norm F norm f * norm x"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
770 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
771 |
fix x; assume "x:E"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
772 |
show "rabs (g x) <= function_norm F norm f * norm x"; |
7917 | 773 |
by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
774 |
qed; |
7917 | 775 |
|
7978 | 776 |
with _ g_cont; show "?L <= ?R"; |
7917 | 777 |
proof (rule fnorm_le_ub); |
778 |
from f_cont f_norm; show "0r <= function_norm F norm f"; ..; |
|
779 |
qed; |
|
780 |
||
781 |
txt{* The other direction is achieved by a similar |
|
782 |
argument. *}; |
|
783 |
||
784 |
have "ALL x:F. rabs (f x) <= function_norm E norm g * norm x"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
785 |
proof; |
7566 | 786 |
fix x; assume "x : F"; |
787 |
from a; have "g x = f x"; ..; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
788 |
hence "rabs (f x) = rabs (g x)"; by simp; |
8108 | 789 |
also; from _ _ g_cont; |
7917 | 790 |
have "... <= function_norm E norm g * norm x"; |
8084 | 791 |
proof (rule norm_fx_le_norm_f_norm_x); |
792 |
show "x:E"; ..; |
|
793 |
qed; |
|
794 |
finally; show "rabs (f x) <= function_norm E norm g * norm x"; .; |
|
795 |
qed; |
|
796 |
thus "?R <= ?L"; |
|
797 |
proof (rule fnorm_le_ub [OF f_norm f_cont]); |
|
7917 | 798 |
from g_cont; show "0r <= function_norm E norm g"; ..; |
799 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
800 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
801 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
802 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
803 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
804 |
|
7808 | 805 |
end; |