author | wenzelm |
Mon, 08 May 2000 20:57:02 +0200 | |
changeset 8838 | 4eaa99f0d223 |
parent 8703 | 816d8f6513be |
child 8902 | a705822f4e2a |
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); |
|
8674 | 75 |
show "is_subspace ?H E"; |
76 |
by (rule sup_subE [OF _ _ _ a]) (simp!)+; |
|
8084 | 77 |
show "is_subspace F ?H"; |
8674 | 78 |
by (rule sup_supF [OF _ _ _ a]) (simp!)+; |
8084 | 79 |
show "graph F f <= graph ?H ?h"; |
8674 | 80 |
by (rule sup_ext [OF _ _ _ a]) (simp!)+; |
8084 | 81 |
show "ALL x::'a:?H. ?h x <= p x"; |
8674 | 82 |
by (rule sup_norm_pres [OF _ _ a]) (simp!)+; |
8084 | 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; |
8703 | 148 |
have x0: "x0 ~= 00"; |
8084 | 149 |
proof (rule classical); |
8703 | 150 |
presume "x0 = 00"; |
8084 | 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 |
|
8703 | 193 |
def h0 == "\\<lambda>x. let (y,a) = SOME (y, a). x = y + a (*) x0 |
8084 | 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"; |
|
8703 | 208 |
have "(SOME (y, a). t = y + a (*) x0 & y : H) |
8084 | 209 |
= (t,0r)"; |
8674 | 210 |
by (rule decomp_H0_H [OF _ _ _ _ _ x0]); |
8084 | 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); |
|
8703 | 231 |
show "x0 = 00 + x0"; by (simp!); |
232 |
from h; show "00 : H"; ..; |
|
8084 | 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"; |
|
8674 | 251 |
by (rule h0_lf [OF _ _ _ _ _ _ x0]) (simp!)+; |
8084 | 252 |
show "is_subspace H0 E"; |
8674 | 253 |
by (unfold H0_def) (rule vs_sum_subspace [OF _ lin_subspace]); |
8084 | 254 |
have "is_subspace F H"; .; |
255 |
also; from h lin_vs; |
|
256 |
have [fold H0_def]: "is_subspace H (H + lin x0)"; ..; |
|
257 |
finally (subspace_trans [OF _ h]); |
|
258 |
show f_h0: "is_subspace F H0"; .; |
|
259 |
||
260 |
show "graph F f <= graph H0 h0"; |
|
261 |
proof (rule graph_extI); |
|
262 |
fix x; assume "x:F"; |
|
263 |
have "f x = h x"; ..; |
|
264 |
also; have " ... = h x + 0r * xi"; by simp; |
|
265 |
also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)"; |
|
266 |
by (simp add: Let_def); |
|
267 |
also; have |
|
8703 | 268 |
"(x, 0r) = (SOME (y, a). x = y + a (*) x0 & y : H)"; |
8674 | 269 |
by (rule decomp_H0_H [RS sym, OF _ _ _ _ _ x0]) (simp!)+; |
8084 | 270 |
also; have |
8703 | 271 |
"(let (y,a) = (SOME (y,a). x = y + a (*) x0 & y : H) |
8084 | 272 |
in h y + a * xi) |
273 |
= h0 x"; by (simp!); |
|
274 |
finally; show "f x = h0 x"; .; |
|
275 |
next; |
|
276 |
from f_h0; show "F <= H0"; ..; |
|
277 |
qed; |
|
278 |
||
279 |
show "ALL x:H0. h0 x <= p x"; |
|
8674 | 280 |
by (rule h0_norm_pres [OF _ _ _ _ x0]); |
8084 | 281 |
qed; |
282 |
thus "graph H0 h0 : M"; by (simp!); |
|
283 |
qed; |
|
284 |
qed; |
|
285 |
qed; |
|
286 |
qed; |
|
287 |
||
288 |
txt {* So the graph $g$ of $h$ cannot be maximal. Contradiction. *}; |
|
289 |
||
290 |
hence "~ (ALL x:M. g <= x --> g = x)"; by simp; |
|
291 |
thus ?thesis; by contradiction; |
|
292 |
qed; |
|
293 |
||
294 |
txt {* Now we have a linear extension $h$ of $f$ to $E$ that is |
|
295 |
bounded by $p$. *}; |
|
296 |
||
297 |
thus "EX h. is_linearform E h & (ALL x:F. h x = f x) |
|
298 |
& (ALL x:E. h x <= p x)"; |
|
299 |
proof (intro exI conjI); |
|
300 |
assume eq: "H = E"; |
|
301 |
from eq; show "is_linearform E h"; by (simp!); |
|
302 |
show "ALL x:F. h x = f x"; |
|
303 |
proof (intro ballI, rule sym); |
|
304 |
fix x; assume "x:F"; show "f x = h x "; ..; |
|
305 |
qed; |
|
306 |
from eq; show "ALL x:E. h x <= p x"; by (force!); |
|
307 |
qed; |
|
308 |
qed; |
|
309 |
qed; |
|
310 |
qed; |
|
311 |
(* |
|
7917 | 312 |
theorem HahnBanach: |
7978 | 313 |
"[| is_vectorspace E; is_subspace F E; is_seminorm E p; |
7808 | 314 |
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
|
315 |
==> EX h. is_linearform E h |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
316 |
& (ALL x:F. h x = f x) |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
317 |
& (ALL x:E. h x <= p x)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
318 |
proof -; |
7978 | 319 |
assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" |
7808 | 320 |
"is_linearform F f" "ALL x:F. f x <= p x"; |
7656 | 321 |
|
7917 | 322 |
txt{* We define $M$ to be the set of all linear extensions |
323 |
of $f$ to superspaces of $F$, which are bounded by $p$. *}; |
|
324 |
||
7656 | 325 |
def M == "norm_pres_extensions E p F f"; |
7917 | 326 |
|
327 |
txt{* We show that $M$ is non-empty: *}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
328 |
|
7656 | 329 |
have aM: "graph F f : norm_pres_extensions E p F f"; |
330 |
proof (rule norm_pres_extensionI2); |
|
7917 | 331 |
have "is_vectorspace F"; ..; |
332 |
thus "is_subspace F F"; ..; |
|
7566 | 333 |
qed (blast!)+; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
334 |
|
8084 | 335 |
subsubsect {* Existence of a limit function *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
336 |
|
7978 | 337 |
txt {* For every non-empty chain of norm-preserving extensions |
338 |
the union of all functions in the chain is again a norm-preserving |
|
339 |
extension. (The union is an upper bound for all elements. |
|
7917 | 340 |
It is even the least upper bound, because every upper bound of $M$ |
8084 | 341 |
is also an upper bound for $\Union c$, as $\Union c\in M$) *}; |
7917 | 342 |
|
7978 | 343 |
{{; |
7917 | 344 |
fix c; assume "c:chain M" "EX x. x:c"; |
7978 | 345 |
have "Union c : M"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
346 |
|
7656 | 347 |
proof (unfold M_def, rule norm_pres_extensionI); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
348 |
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
|
349 |
& is_linearform H h |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
350 |
& is_subspace H E |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
351 |
& is_subspace F H |
7917 | 352 |
& graph F f <= graph H h |
353 |
& (ALL x::'a:H. h x <= p x)"; |
|
7656 | 354 |
proof (intro exI conjI); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
355 |
let ?H = "domain (Union c)"; |
7656 | 356 |
let ?h = "funct (Union c)"; |
357 |
||
7978 | 358 |
show a: "graph ?H ?h = Union c"; |
7656 | 359 |
proof (rule graph_domain_funct); |
360 |
fix x y z; assume "(x, y) : Union c" "(x, z) : Union c"; |
|
7917 | 361 |
show "z = y"; by (rule sup_definite); |
7656 | 362 |
qed; |
7978 | 363 |
show "is_linearform ?H ?h"; |
7917 | 364 |
by (simp! add: sup_lf a); |
365 |
show "is_subspace ?H E"; |
|
7656 | 366 |
by (rule sup_subE, rule a) (simp!)+; |
7917 | 367 |
show "is_subspace F ?H"; |
7656 | 368 |
by (rule sup_supF, rule a) (simp!)+; |
7917 | 369 |
show "graph F f <= graph ?H ?h"; |
7656 | 370 |
by (rule sup_ext, rule a) (simp!)+; |
371 |
show "ALL x::'a:?H. ?h x <= p x"; |
|
372 |
by (rule sup_norm_pres, rule a) (simp!)+; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
373 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
374 |
qed; |
7978 | 375 |
}}; |
7656 | 376 |
|
7927 | 377 |
txt {* According to Zorn's Lemma there is |
7917 | 378 |
a maximal norm-preserving extension $g\in M$. *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
379 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
380 |
with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x"; |
7566 | 381 |
by (simp! add: Zorn's_Lemma); |
7656 | 382 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
383 |
thus ?thesis; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
384 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
385 |
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
|
386 |
|
7917 | 387 |
have ex_Hh: |
388 |
"EX H h. graph H h = g |
|
389 |
& is_linearform H h |
|
390 |
& is_subspace H E |
|
391 |
& is_subspace F H |
|
392 |
& graph F f <= graph H h |
|
393 |
& (ALL x:H. h x <= p x) "; |
|
7656 | 394 |
by (simp! add: norm_pres_extension_D); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
395 |
thus ?thesis; |
7917 | 396 |
proof (elim exE conjE, intro exI); |
7656 | 397 |
fix H h; |
7808 | 398 |
assume "graph H h = g" "is_linearform (H::'a set) h" |
399 |
"is_subspace H E" "is_subspace F H" |
|
7917 | 400 |
and h_ext: "graph F f <= graph H h" |
401 |
and h_bound: "ALL x:H. h x <= p x"; |
|
7656 | 402 |
|
7917 | 403 |
have h: "is_vectorspace H"; ..; |
404 |
have f: "is_vectorspace F"; ..; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
405 |
|
7978 | 406 |
subsubsect {* The domain of the limit function *}; |
7656 | 407 |
|
7808 | 408 |
have eq: "H = E"; |
409 |
proof (rule classical); |
|
7656 | 410 |
|
7978 | 411 |
txt {* Assume that the domain of the supremum is not $E$, *}; |
8084 | 412 |
|
7808 | 413 |
assume "H ~= E"; |
7917 | 414 |
have "H <= E"; ..; |
415 |
hence "H < E"; ..; |
|
416 |
||
8084 | 417 |
txt{* then there exists an element $x_0$ in $E \setminus H$: *}; |
7656 | 418 |
|
7917 | 419 |
hence "EX x0:E. x0~:H"; |
420 |
by (rule set_less_imp_diff_not_empty); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
421 |
|
7917 | 422 |
txt {* We get that $h$ can be extended in a |
423 |
norm-preserving way to some $H_0$. *}; |
|
8084 | 424 |
|
7917 | 425 |
hence "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 |
426 |
& graph H0 h0 : M"; |
|
427 |
proof; |
|
428 |
fix x0; assume "x0:E" "x0~:H"; |
|
7656 | 429 |
|
8703 | 430 |
have x0: "x0 ~= 00"; |
7917 | 431 |
proof (rule classical); |
8703 | 432 |
presume "x0 = 00"; |
7917 | 433 |
with h; have "x0:H"; by simp; |
434 |
thus ?thesis; by contradiction; |
|
435 |
qed blast; |
|
436 |
||
437 |
txt {* Define $H_0$ as the (direct) sum of H and the |
|
7978 | 438 |
linear closure of $x_0$. \label{ex-xi-use}*}; |
7917 | 439 |
|
440 |
def H0 == "H + lin x0"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
441 |
|
7978 | 442 |
from h; have xi: "EX xi. ALL y:H. - p (y + x0) - h y <= xi |
443 |
& xi <= p (y + x0) - h y"; |
|
7917 | 444 |
proof (rule ex_xi); |
445 |
fix u v; assume "u:H" "v:H"; |
|
446 |
from h; have "h v - h u = h (v - u)"; |
|
7978 | 447 |
by (simp! add: linearform_diff); |
7917 | 448 |
also; from h_bound; have "... <= p (v - u)"; |
449 |
by (simp!); |
|
450 |
also; have "v - u = x0 + - x0 + v + - u"; |
|
451 |
by (simp! add: diff_eq1); |
|
452 |
also; have "... = v + x0 + - (u + x0)"; |
|
453 |
by (simp!); |
|
454 |
also; have "... = (v + x0) - (u + x0)"; |
|
455 |
by (simp! add: diff_eq1); |
|
456 |
also; have "p ... <= p (v + x0) + p (u + x0)"; |
|
7978 | 457 |
by (rule seminorm_diff_subadditive) (simp!)+; |
7917 | 458 |
finally; have "h v - h u <= p (v + x0) + p (u + x0)"; .; |
7808 | 459 |
|
7917 | 460 |
thus "- p (u + x0) - h u <= p (v + x0) - h v"; |
461 |
by (rule real_diff_ineq_swap); |
|
462 |
qed; |
|
463 |
hence "EX h0. g <= graph H0 h0 & g ~= graph H0 h0 |
|
464 |
& graph H0 h0 : M"; |
|
465 |
proof (elim exE, intro exI conjI); |
|
466 |
fix xi; |
|
7978 | 467 |
assume a: "ALL y:H. - p (y + x0) - h y <= xi |
468 |
& xi <= p (y + x0) - h y"; |
|
7917 | 469 |
|
7978 | 470 |
txt {* Define $h_0$ as the canonical linear extension |
471 |
of $h$ on $H_0$:*}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
472 |
|
7917 | 473 |
def h0 == |
8703 | 474 |
"\\<lambda>x. let (y,a) = SOME (y, a). x = y + a ( * ) x0 & y:H |
7917 | 475 |
in (h y) + a * xi"; |
7808 | 476 |
|
8084 | 477 |
txt {* We get that the graph of $h_0$ extends that of |
7917 | 478 |
$h$. *}; |
479 |
||
480 |
have "graph H h <= graph H0 h0"; |
|
481 |
proof (rule graph_extI); |
|
482 |
fix t; assume "t:H"; |
|
8703 | 483 |
have "(SOME (y, a). t = y + a ( * ) x0 & y : H) = (t,0r)"; |
7917 | 484 |
by (rule decomp_H0_H, rule x0); |
485 |
thus "h t = h0 t"; by (simp! add: Let_def); |
|
486 |
next; |
|
487 |
show "H <= H0"; |
|
488 |
proof (rule subspace_subset); |
|
489 |
show "is_subspace H H0"; |
|
490 |
proof (unfold H0_def, rule subspace_vs_sum1); |
|
491 |
show "is_vectorspace H"; ..; |
|
492 |
show "is_vectorspace (lin x0)"; ..; |
|
7566 | 493 |
qed; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
494 |
qed; |
7808 | 495 |
qed; |
7917 | 496 |
thus "g <= graph H0 h0"; by (simp!); |
7808 | 497 |
|
7917 | 498 |
txt {* Apparently $h_0$ is not equal to $h$. *}; |
499 |
||
500 |
have "graph H h ~= graph H0 h0"; |
|
501 |
proof; |
|
502 |
assume e: "graph H h = graph H0 h0"; |
|
503 |
have "x0 : H0"; |
|
504 |
proof (unfold H0_def, rule vs_sumI); |
|
8703 | 505 |
show "x0 = 00 + x0"; by (simp!); |
506 |
from h; show "00 : H"; ..; |
|
7917 | 507 |
show "x0 : lin x0"; by (rule x_lin_x); |
508 |
qed; |
|
509 |
hence "(x0, h0 x0) : graph H0 h0"; ..; |
|
510 |
with e; have "(x0, h0 x0) : graph H h"; by simp; |
|
511 |
hence "x0 : H"; ..; |
|
512 |
thus False; by contradiction; |
|
513 |
qed; |
|
514 |
thus "g ~= graph H0 h0"; by (simp!); |
|
515 |
||
7978 | 516 |
txt {* Furthermore $h_0$ is a norm-preserving extension |
7917 | 517 |
of $f$. *}; |
518 |
||
519 |
have "graph H0 h0 : norm_pres_extensions E p F f"; |
|
520 |
proof (rule norm_pres_extensionI2); |
|
521 |
show "is_linearform H0 h0"; |
|
522 |
by (rule h0_lf, rule x0) (simp!)+; |
|
523 |
show "is_subspace H0 E"; |
|
524 |
by (unfold H0_def, rule vs_sum_subspace, |
|
525 |
rule lin_subspace); |
|
526 |
||
527 |
have "is_subspace F H"; .; |
|
528 |
also; from h lin_vs; |
|
529 |
have [fold H0_def]: "is_subspace H (H + lin x0)"; ..; |
|
530 |
finally (subspace_trans [OF _ h]); |
|
531 |
show f_h0: "is_subspace F H0"; .; (*** |
|
532 |
backwards: |
|
533 |
show f_h0: "is_subspace F H0"; .; |
|
534 |
proof (rule subspace_trans [of F H H0]); |
|
535 |
from h lin_vs; |
|
536 |
have "is_subspace H (H + lin x0)"; ..; |
|
537 |
thus "is_subspace H H0"; by (unfold H0_def); |
|
538 |
qed; ***) |
|
539 |
||
540 |
show "graph F f <= graph H0 h0"; |
|
541 |
proof (rule graph_extI); |
|
542 |
fix x; assume "x:F"; |
|
543 |
have "f x = h x"; ..; |
|
544 |
also; have " ... = h x + 0r * xi"; by simp; |
|
545 |
also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)"; |
|
546 |
by (simp add: Let_def); |
|
547 |
also; have |
|
8703 | 548 |
"(x, 0r) = (SOME (y, a). x = y + a ( * ) x0 & y : H)"; |
7917 | 549 |
by (rule decomp_H0_H [RS sym], rule x0) (simp!)+; |
550 |
also; have |
|
8703 | 551 |
"(let (y,a) = (SOME (y,a). x = y + a ( * ) x0 & y : H) |
7917 | 552 |
in h y + a * xi) |
553 |
= h0 x"; by (simp!); |
|
554 |
finally; show "f x = h0 x"; .; |
|
555 |
next; |
|
556 |
from f_h0; show "F <= H0"; ..; |
|
557 |
qed; |
|
558 |
||
559 |
show "ALL x:H0. h0 x <= p x"; |
|
8084 | 560 |
by (rule h0_norm_pres, rule x0) (assumption | simp!)+; |
7917 | 561 |
qed; |
562 |
thus "graph H0 h0 : M"; by (simp!); |
|
7808 | 563 |
qed; |
7917 | 564 |
thus ?thesis; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
565 |
qed; |
7917 | 566 |
|
7927 | 567 |
txt {* We have shown that $h$ can still be extended to |
7917 | 568 |
some $h_0$, in contradiction to the assumption that |
569 |
$h$ is a maximal element. *}; |
|
570 |
||
571 |
hence "EX x:M. g <= x & g ~= x"; |
|
572 |
by (elim exE conjE, intro bexI conjI); |
|
573 |
hence "~ (ALL x:M. g <= x --> g = x)"; by simp; |
|
574 |
thus ?thesis; by contradiction; |
|
7808 | 575 |
qed; |
576 |
||
7927 | 577 |
txt{* It follows $H = E$, and the thesis can be shown. *}; |
7917 | 578 |
|
7808 | 579 |
show "is_linearform E h & (ALL x:F. h x = f x) |
580 |
& (ALL x:E. h x <= p x)"; |
|
581 |
proof (intro conjI); |
|
582 |
from eq; show "is_linearform E h"; by (simp!); |
|
583 |
show "ALL x:F. h x = f x"; |
|
584 |
proof (intro ballI, rule sym); |
|
585 |
fix x; assume "x:F"; show "f x = h x "; ..; |
|
586 |
qed; |
|
587 |
from eq; show "ALL x:E. h x <= p x"; by (force!); |
|
7917 | 588 |
qed; |
589 |
||
590 |
qed; |
|
591 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
592 |
qed; |
8084 | 593 |
*) |
7917 | 594 |
|
595 |
||
8084 | 596 |
subsection {* Alternative formulation *}; |
7656 | 597 |
|
7978 | 598 |
text {* The following alternative formulation of the Hahn-Banach |
8838 | 599 |
Theorem\label{abs-HahnBanach} uses the fact that for a real linear form |
8084 | 600 |
$f$ and a seminorm $p$ the |
7978 | 601 |
following inequations are equivalent:\footnote{This was shown in lemma |
8838 | 602 |
$\idt{abs{\dsh}ineq{\dsh}iff}$ (see page \pageref{abs-ineq-iff}).} |
7917 | 603 |
\begin{matharray}{ll} |
604 |
\forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\ |
|
605 |
\forall x\in H.\ap h\ap x\leq p\ap x\\ |
|
606 |
\end{matharray} |
|
7978 | 607 |
*}; |
7917 | 608 |
|
8838 | 609 |
theorem abs_HahnBanach: |
8084 | 610 |
"[| is_vectorspace E; is_subspace F E; is_linearform F f; |
8838 | 611 |
is_seminorm E p; ALL x:F. abs (f x) <= p x |] |
8084 | 612 |
==> EX g. is_linearform E g & (ALL x:F. g x = f x) |
8838 | 613 |
& (ALL x:E. abs (g x) <= p x)"; |
8084 | 614 |
proof -; |
615 |
assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" |
|
8838 | 616 |
"is_linearform F f" "ALL x:F. abs (f x) <= p x"; |
617 |
have "ALL x:F. f x <= p x"; by (rule abs_ineq_iff [RS iffD1]); |
|
7808 | 618 |
hence "EX g. is_linearform E g & (ALL x:F. g x = f x) |
619 |
& (ALL x:E. g x <= p x)"; |
|
7917 | 620 |
by (simp! only: HahnBanach); |
8084 | 621 |
thus ?thesis; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
622 |
proof (elim exE conjE); |
7808 | 623 |
fix g; assume "is_linearform E g" "ALL x:F. g x = f x" |
624 |
"ALL x:E. g x <= p x"; |
|
8838 | 625 |
hence "ALL x:E. abs (g x) <= p x"; |
626 |
by (simp! add: abs_ineq_iff [OF subspace_refl]); |
|
8084 | 627 |
thus ?thesis; by (intro exI conjI); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
628 |
qed; |
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 |
|
7917 | 631 |
subsection {* The Hahn-Banach Theorem for normed spaces *}; |
7656 | 632 |
|
7978 | 633 |
text {* Every continuous linear form $f$ on a subspace $F$ of a |
634 |
norm space $E$, can be extended to a continuous linear form $g$ on |
|
635 |
$E$ such that $\fnorm{f} = \fnorm {g}$. *}; |
|
7656 | 636 |
|
7917 | 637 |
theorem norm_HahnBanach: |
638 |
"[| is_normed_vectorspace E norm; is_subspace F E; |
|
7978 | 639 |
is_linearform F f; is_continuous F norm f |] |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
640 |
==> EX g. is_linearform E g |
7978 | 641 |
& is_continuous E norm g |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
642 |
& (ALL x:F. g x = f x) |
7917 | 643 |
& 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
|
644 |
proof -; |
7917 | 645 |
assume e_norm: "is_normed_vectorspace E norm"; |
646 |
assume f: "is_subspace F E" "is_linearform F f"; |
|
7978 | 647 |
assume f_cont: "is_continuous F norm f"; |
7566 | 648 |
have e: "is_vectorspace E"; ..; |
7917 | 649 |
with _; have f_norm: "is_normed_vectorspace F norm"; ..; |
7656 | 650 |
|
8084 | 651 |
txt{* We define a function $p$ on $E$ as follows: |
7917 | 652 |
\begin{matharray}{l} |
8084 | 653 |
p \: x = \fnorm f \cdot \norm x\\ |
7917 | 654 |
\end{matharray} |
655 |
*}; |
|
656 |
||
8674 | 657 |
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
|
658 |
|
7978 | 659 |
txt{* $p$ is a seminorm on $E$: *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
660 |
|
7978 | 661 |
have q: "is_seminorm E p"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
662 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
663 |
fix x y a; assume "x:E" "y:E"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
664 |
|
7917 | 665 |
txt{* $p$ is positive definite: *}; |
666 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
667 |
show "0r <= p x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
668 |
proof (unfold p_def, rule real_le_mult_order); |
7917 | 669 |
from _ f_norm; show "0r <= function_norm F norm f"; ..; |
7566 | 670 |
show "0r <= norm x"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
671 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
672 |
|
7978 | 673 |
txt{* $p$ is absolutely homogenous: *}; |
7917 | 674 |
|
8838 | 675 |
show "p (a (*) x) = abs a * p x"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
676 |
proof -; |
8703 | 677 |
have "p (a (*) x) = function_norm F norm f * norm (a (*) x)"; |
7808 | 678 |
by (simp!); |
8838 | 679 |
also; have "norm (a (*) x) = abs a * norm x"; |
680 |
by (rule normed_vs_norm_abs_homogenous); |
|
681 |
also; have "function_norm F norm f * (abs a * norm x) |
|
682 |
= abs a * (function_norm F norm f * norm x)"; |
|
7566 | 683 |
by (simp! only: real_mult_left_commute); |
8838 | 684 |
also; have "... = abs a * p x"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
685 |
finally; show ?thesis; .; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
686 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
687 |
|
7978 | 688 |
txt{* Furthermore, $p$ is subadditive: *}; |
7917 | 689 |
|
690 |
show "p (x + y) <= p x + p y"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
691 |
proof -; |
7917 | 692 |
have "p (x + y) = function_norm F norm f * norm (x + y)"; |
7808 | 693 |
by (simp!); |
7917 | 694 |
also; |
695 |
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
|
696 |
proof (rule real_mult_le_le_mono1); |
7917 | 697 |
from _ f_norm; show "0r <= function_norm F norm f"; ..; |
698 |
show "norm (x + y) <= norm x + norm y"; ..; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
699 |
qed; |
7917 | 700 |
also; have "... = function_norm F norm f * norm x |
701 |
+ function_norm F norm f * norm y"; |
|
7566 | 702 |
by (simp! only: real_add_mult_distrib2); |
703 |
finally; show ?thesis; by (simp!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
704 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
705 |
qed; |
7917 | 706 |
|
707 |
txt{* $f$ is bounded by $p$. *}; |
|
708 |
||
8838 | 709 |
have "ALL x:F. abs (f x) <= p x"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
710 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
711 |
fix x; assume "x:F"; |
8838 | 712 |
from f_norm; show "abs (f x) <= p x"; |
7808 | 713 |
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
|
714 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
715 |
|
7978 | 716 |
txt{* Using the fact that $p$ is a seminorm and |
8084 | 717 |
$f$ is bounded by $p$ we can apply the Hahn-Banach Theorem |
7978 | 718 |
for real vector spaces. |
719 |
So $f$ can be extended in a norm-preserving way to some function |
|
7917 | 720 |
$g$ on the whole vector space $E$. *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
721 |
|
7917 | 722 |
with e f q; |
723 |
have "EX g. is_linearform E g & (ALL x:F. g x = f x) |
|
8838 | 724 |
& (ALL x:E. abs (g x) <= p x)"; |
725 |
by (simp! add: abs_HahnBanach); |
|
7917 | 726 |
|
727 |
thus ?thesis; |
|
728 |
proof (elim exE conjE); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
729 |
fix g; |
7808 | 730 |
assume "is_linearform E g" and a: "ALL x:F. g x = f x" |
8838 | 731 |
and b: "ALL x:E. abs (g x) <= p x"; |
7917 | 732 |
|
733 |
show "EX g. is_linearform E g |
|
7978 | 734 |
& is_continuous E norm g |
7917 | 735 |
& (ALL x:F. g x = f x) |
736 |
& function_norm E norm g = function_norm F norm f"; |
|
737 |
proof (intro exI conjI); |
|
738 |
||
8084 | 739 |
txt{* We furthermore have to show that |
7978 | 740 |
$g$ is also continuous: *}; |
7917 | 741 |
|
7978 | 742 |
show g_cont: "is_continuous E norm g"; |
7917 | 743 |
proof; |
744 |
fix x; assume "x:E"; |
|
7978 | 745 |
from b [RS bspec, OF this]; |
8838 | 746 |
show "abs (g x) <= function_norm F norm f * norm x"; |
7978 | 747 |
by (unfold p_def); |
7917 | 748 |
qed; |
749 |
||
7978 | 750 |
txt {* To complete the proof, we show that |
8084 | 751 |
$\fnorm g = \fnorm f$. \label{order_antisym} *}; |
7978 | 752 |
|
7917 | 753 |
show "function_norm E norm g = function_norm F norm f" |
754 |
(is "?L = ?R"); |
|
755 |
proof (rule order_antisym); |
|
756 |
||
7978 | 757 |
txt{* First we show $\fnorm g \leq \fnorm f$. The function norm |
758 |
$\fnorm g$ is defined as the smallest $c\in\bbbR$ such that |
|
7917 | 759 |
\begin{matharray}{l} |
7978 | 760 |
\All {x\in E} {|g\ap x| \leq c \cdot \norm x} |
761 |
\end{matharray} |
|
762 |
Furthermore holds |
|
763 |
\begin{matharray}{l} |
|
764 |
\All {x\in E} {|g\ap x| \leq \fnorm f \cdot \norm x} |
|
765 |
\end{matharray} |
|
766 |
*}; |
|
767 |
||
8838 | 768 |
have "ALL x:E. abs (g x) <= function_norm F norm f * norm x"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
769 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
770 |
fix x; assume "x:E"; |
8838 | 771 |
show "abs (g x) <= function_norm F norm f * norm x"; |
7917 | 772 |
by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
773 |
qed; |
7917 | 774 |
|
7978 | 775 |
with _ g_cont; show "?L <= ?R"; |
7917 | 776 |
proof (rule fnorm_le_ub); |
777 |
from f_cont f_norm; show "0r <= function_norm F norm f"; ..; |
|
778 |
qed; |
|
779 |
||
780 |
txt{* The other direction is achieved by a similar |
|
781 |
argument. *}; |
|
782 |
||
8838 | 783 |
have "ALL x:F. abs (f x) <= function_norm E norm g * norm x"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
784 |
proof; |
7566 | 785 |
fix x; assume "x : F"; |
786 |
from a; have "g x = f x"; ..; |
|
8838 | 787 |
hence "abs (f x) = abs (g x)"; by simp; |
8108 | 788 |
also; from _ _ g_cont; |
7917 | 789 |
have "... <= function_norm E norm g * norm x"; |
8084 | 790 |
proof (rule norm_fx_le_norm_f_norm_x); |
791 |
show "x:E"; ..; |
|
792 |
qed; |
|
8838 | 793 |
finally; show "abs (f x) <= function_norm E norm g * norm x"; .; |
8084 | 794 |
qed; |
795 |
thus "?R <= ?L"; |
|
796 |
proof (rule fnorm_le_ub [OF f_norm f_cont]); |
|
7917 | 797 |
from g_cont; show "0r <= function_norm E norm g"; ..; |
798 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
799 |
qed; |
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 |
|
8703 | 804 |
end; |