author | wenzelm |
Fri, 29 Oct 1999 20:18:34 +0200 | |
changeset 7978 | 1b99ee57d131 |
parent 7927 | b50446a33c16 |
child 8084 | c3790c6b4470 |
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 |
|
7917 | 16 |
subsection {* The case of general linear spaces *}; |
7656 | 17 |
|
7978 | 18 |
text {* Let $f$ be a linear form $f$ defined on a subspace $F$ |
19 |
of a norm vector space $E$. If $f$ is |
|
20 |
bounded by some seminorm $q$ on $E$, it can be extended |
|
21 |
to a function on $E$ in a norm-preserving way. *}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
22 |
|
7917 | 23 |
theorem HahnBanach: |
7978 | 24 |
"[| is_vectorspace E; is_subspace F E; is_seminorm E p; |
7808 | 25 |
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
|
26 |
==> EX h. is_linearform E h |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
27 |
& (ALL x:F. h x = f x) |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
28 |
& (ALL x:E. h x <= p x)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
29 |
proof -; |
7978 | 30 |
assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" |
7808 | 31 |
"is_linearform F f" "ALL x:F. f x <= p x"; |
7656 | 32 |
|
7917 | 33 |
txt{* We define $M$ to be the set of all linear extensions |
34 |
of $f$ to superspaces of $F$, which are bounded by $p$. *}; |
|
35 |
||
7656 | 36 |
def M == "norm_pres_extensions E p F f"; |
7917 | 37 |
|
38 |
txt{* We show that $M$ is non-empty: *}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
39 |
|
7656 | 40 |
have aM: "graph F f : norm_pres_extensions E p F f"; |
41 |
proof (rule norm_pres_extensionI2); |
|
7917 | 42 |
have "is_vectorspace F"; ..; |
43 |
thus "is_subspace F F"; ..; |
|
7566 | 44 |
qed (blast!)+; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
45 |
|
7978 | 46 |
subsubsect {* Existence of a limit function the norm-preserving |
7917 | 47 |
extensions *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
48 |
|
7978 | 49 |
txt {* For every non-empty chain of norm-preserving extensions |
50 |
the union of all functions in the chain is again a norm-preserving |
|
51 |
extension. (The union is an upper bound for all elements. |
|
7917 | 52 |
It is even the least upper bound, because every upper bound of $M$ |
7927 | 53 |
is also an upper bound for $\Union c$.) *}; |
7917 | 54 |
|
7978 | 55 |
{{; |
7917 | 56 |
fix c; assume "c:chain M" "EX x. x:c"; |
7978 | 57 |
have "Union c : M"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
58 |
|
7656 | 59 |
proof (unfold M_def, rule norm_pres_extensionI); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
60 |
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
|
61 |
& is_linearform H h |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
62 |
& is_subspace H E |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
63 |
& is_subspace F H |
7917 | 64 |
& graph F f <= graph H h |
65 |
& (ALL x::'a:H. h x <= p x)"; |
|
7656 | 66 |
proof (intro exI conjI); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
67 |
let ?H = "domain (Union c)"; |
7656 | 68 |
let ?h = "funct (Union c)"; |
69 |
||
7978 | 70 |
show a: "graph ?H ?h = Union c"; |
7656 | 71 |
proof (rule graph_domain_funct); |
72 |
fix x y z; assume "(x, y) : Union c" "(x, z) : Union c"; |
|
7917 | 73 |
show "z = y"; by (rule sup_definite); |
7656 | 74 |
qed; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
75 |
|
7978 | 76 |
show "is_linearform ?H ?h"; |
7917 | 77 |
by (simp! add: sup_lf a); |
78 |
show "is_subspace ?H E"; |
|
7656 | 79 |
by (rule sup_subE, rule a) (simp!)+; |
7917 | 80 |
show "is_subspace F ?H"; |
7656 | 81 |
by (rule sup_supF, rule a) (simp!)+; |
7917 | 82 |
show "graph F f <= graph ?H ?h"; |
7656 | 83 |
by (rule sup_ext, rule a) (simp!)+; |
84 |
show "ALL x::'a:?H. ?h x <= p x"; |
|
85 |
by (rule sup_norm_pres, rule a) (simp!)+; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
86 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
87 |
qed; |
7978 | 88 |
}}; |
7656 | 89 |
|
7927 | 90 |
txt {* According to Zorn's Lemma there is |
7917 | 91 |
a maximal norm-preserving extension $g\in M$. *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
92 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
93 |
with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x"; |
7566 | 94 |
by (simp! add: Zorn's_Lemma); |
7656 | 95 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
96 |
thus ?thesis; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
97 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
98 |
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
|
99 |
|
7917 | 100 |
have ex_Hh: |
101 |
"EX H h. graph H h = g |
|
102 |
& is_linearform H h |
|
103 |
& is_subspace H E |
|
104 |
& is_subspace F H |
|
105 |
& graph F f <= graph H h |
|
106 |
& (ALL x:H. h x <= p x) "; |
|
7656 | 107 |
by (simp! add: norm_pres_extension_D); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
108 |
thus ?thesis; |
7917 | 109 |
proof (elim exE conjE, intro exI); |
7656 | 110 |
fix H h; |
7808 | 111 |
assume "graph H h = g" "is_linearform (H::'a set) h" |
112 |
"is_subspace H E" "is_subspace F H" |
|
7917 | 113 |
and h_ext: "graph F f <= graph H h" |
114 |
and h_bound: "ALL x:H. h x <= p x"; |
|
7656 | 115 |
|
7917 | 116 |
have h: "is_vectorspace H"; ..; |
117 |
have f: "is_vectorspace F"; ..; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
118 |
|
7978 | 119 |
subsubsect {* The domain of the limit function *}; |
7656 | 120 |
|
7808 | 121 |
have eq: "H = E"; |
122 |
proof (rule classical); |
|
7656 | 123 |
|
7978 | 124 |
txt {* Assume that the domain of the supremum is not $E$, *}; |
7917 | 125 |
; |
7808 | 126 |
assume "H ~= E"; |
7917 | 127 |
have "H <= E"; ..; |
128 |
hence "H < E"; ..; |
|
129 |
||
7978 | 130 |
txt{* then there exists an element $x_0$ in $E \ H$: *}; |
7656 | 131 |
|
7917 | 132 |
hence "EX x0:E. x0~:H"; |
133 |
by (rule set_less_imp_diff_not_empty); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
134 |
|
7917 | 135 |
txt {* We get that $h$ can be extended in a |
136 |
norm-preserving way to some $H_0$. *}; |
|
137 |
; |
|
138 |
hence "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 |
|
139 |
& graph H0 h0 : M"; |
|
140 |
proof; |
|
141 |
fix x0; assume "x0:E" "x0~:H"; |
|
7656 | 142 |
|
7917 | 143 |
have x0: "x0 ~= <0>"; |
144 |
proof (rule classical); |
|
145 |
presume "x0 = <0>"; |
|
146 |
with h; have "x0:H"; by simp; |
|
147 |
thus ?thesis; by contradiction; |
|
148 |
qed blast; |
|
149 |
||
150 |
txt {* Define $H_0$ as the (direct) sum of H and the |
|
7978 | 151 |
linear closure of $x_0$. \label{ex-xi-use}*}; |
7917 | 152 |
|
153 |
def H0 == "H + lin x0"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
154 |
|
7978 | 155 |
from h; have xi: "EX xi. ALL y:H. - p (y + x0) - h y <= xi |
156 |
& xi <= p (y + x0) - h y"; |
|
7917 | 157 |
proof (rule ex_xi); |
158 |
fix u v; assume "u:H" "v:H"; |
|
159 |
from h; have "h v - h u = h (v - u)"; |
|
7978 | 160 |
by (simp! add: linearform_diff); |
7917 | 161 |
also; from h_bound; have "... <= p (v - u)"; |
162 |
by (simp!); |
|
163 |
also; have "v - u = x0 + - x0 + v + - u"; |
|
164 |
by (simp! add: diff_eq1); |
|
165 |
also; have "... = v + x0 + - (u + x0)"; |
|
166 |
by (simp!); |
|
167 |
also; have "... = (v + x0) - (u + x0)"; |
|
168 |
by (simp! add: diff_eq1); |
|
169 |
also; have "p ... <= p (v + x0) + p (u + x0)"; |
|
7978 | 170 |
by (rule seminorm_diff_subadditive) (simp!)+; |
7917 | 171 |
finally; have "h v - h u <= p (v + x0) + p (u + x0)"; .; |
7808 | 172 |
|
7917 | 173 |
thus "- p (u + x0) - h u <= p (v + x0) - h v"; |
174 |
by (rule real_diff_ineq_swap); |
|
175 |
qed; |
|
176 |
hence "EX h0. g <= graph H0 h0 & g ~= graph H0 h0 |
|
177 |
& graph H0 h0 : M"; |
|
178 |
proof (elim exE, intro exI conjI); |
|
179 |
fix xi; |
|
7978 | 180 |
assume a: "ALL y:H. - p (y + x0) - h y <= xi |
181 |
& xi <= p (y + x0) - h y"; |
|
7917 | 182 |
|
7978 | 183 |
txt {* Define $h_0$ as the canonical linear extension |
184 |
of $h$ on $H_0$:*}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
185 |
|
7917 | 186 |
def h0 == |
7978 | 187 |
"\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0 & y:H |
7917 | 188 |
in (h y) + a * xi"; |
7808 | 189 |
|
7917 | 190 |
txt {* We get that the graph of $h_0$ extend that of |
191 |
$h$. *}; |
|
192 |
||
193 |
have "graph H h <= graph H0 h0"; |
|
194 |
proof (rule graph_extI); |
|
195 |
fix t; assume "t:H"; |
|
196 |
have "(SOME (y, a). t = y + a <*> x0 & y : H) = (t,0r)"; |
|
197 |
by (rule decomp_H0_H, rule x0); |
|
198 |
thus "h t = h0 t"; by (simp! add: Let_def); |
|
199 |
next; |
|
200 |
show "H <= H0"; |
|
201 |
proof (rule subspace_subset); |
|
202 |
show "is_subspace H H0"; |
|
203 |
proof (unfold H0_def, rule subspace_vs_sum1); |
|
204 |
show "is_vectorspace H"; ..; |
|
205 |
show "is_vectorspace (lin x0)"; ..; |
|
7566 | 206 |
qed; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
207 |
qed; |
7808 | 208 |
qed; |
7917 | 209 |
thus "g <= graph H0 h0"; by (simp!); |
7808 | 210 |
|
7917 | 211 |
txt {* Apparently $h_0$ is not equal to $h$. *}; |
212 |
||
213 |
have "graph H h ~= graph H0 h0"; |
|
214 |
proof; |
|
215 |
assume e: "graph H h = graph H0 h0"; |
|
216 |
have "x0 : H0"; |
|
217 |
proof (unfold H0_def, rule vs_sumI); |
|
218 |
show "x0 = <0> + x0"; by (simp!); |
|
219 |
from h; show "<0> : H"; ..; |
|
220 |
show "x0 : lin x0"; by (rule x_lin_x); |
|
221 |
qed; |
|
222 |
hence "(x0, h0 x0) : graph H0 h0"; ..; |
|
223 |
with e; have "(x0, h0 x0) : graph H h"; by simp; |
|
224 |
hence "x0 : H"; ..; |
|
225 |
thus False; by contradiction; |
|
226 |
qed; |
|
227 |
thus "g ~= graph H0 h0"; by (simp!); |
|
228 |
||
7978 | 229 |
txt {* Furthermore $h_0$ is a norm-preserving extension |
7917 | 230 |
of $f$. *}; |
231 |
||
232 |
have "graph H0 h0 : norm_pres_extensions E p F f"; |
|
233 |
proof (rule norm_pres_extensionI2); |
|
234 |
show "is_linearform H0 h0"; |
|
235 |
by (rule h0_lf, rule x0) (simp!)+; |
|
236 |
show "is_subspace H0 E"; |
|
237 |
by (unfold H0_def, rule vs_sum_subspace, |
|
238 |
rule lin_subspace); |
|
239 |
||
240 |
have "is_subspace F H"; .; |
|
241 |
also; from h lin_vs; |
|
242 |
have [fold H0_def]: "is_subspace H (H + lin x0)"; ..; |
|
243 |
finally (subspace_trans [OF _ h]); |
|
244 |
show f_h0: "is_subspace F H0"; .; (*** |
|
245 |
backwards: |
|
246 |
show f_h0: "is_subspace F H0"; .; |
|
247 |
proof (rule subspace_trans [of F H H0]); |
|
248 |
from h lin_vs; |
|
249 |
have "is_subspace H (H + lin x0)"; ..; |
|
250 |
thus "is_subspace H H0"; by (unfold H0_def); |
|
251 |
qed; ***) |
|
252 |
||
253 |
show "graph F f <= graph H0 h0"; |
|
254 |
proof (rule graph_extI); |
|
255 |
fix x; assume "x:F"; |
|
256 |
have "f x = h x"; ..; |
|
257 |
also; have " ... = h x + 0r * xi"; by simp; |
|
258 |
also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)"; |
|
259 |
by (simp add: Let_def); |
|
260 |
also; have |
|
261 |
"(x, 0r) = (SOME (y, a). x = y + a <*> x0 & y : H)"; |
|
262 |
by (rule decomp_H0_H [RS sym], rule x0) (simp!)+; |
|
263 |
also; have |
|
264 |
"(let (y,a) = (SOME (y,a). x = y + a <*> x0 & y : H) |
|
265 |
in h y + a * xi) |
|
266 |
= h0 x"; by (simp!); |
|
267 |
finally; show "f x = h0 x"; .; |
|
268 |
next; |
|
269 |
from f_h0; show "F <= H0"; ..; |
|
270 |
qed; |
|
271 |
||
272 |
show "ALL x:H0. h0 x <= p x"; |
|
273 |
by (rule h0_norm_pres, rule x0) (assumption | (simp!))+; |
|
274 |
qed; |
|
275 |
thus "graph H0 h0 : M"; by (simp!); |
|
7808 | 276 |
qed; |
7917 | 277 |
thus ?thesis; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
278 |
qed; |
7917 | 279 |
|
7927 | 280 |
txt {* We have shown that $h$ can still be extended to |
7917 | 281 |
some $h_0$, in contradiction to the assumption that |
282 |
$h$ is a maximal element. *}; |
|
283 |
||
284 |
hence "EX x:M. g <= x & g ~= x"; |
|
285 |
by (elim exE conjE, intro bexI conjI); |
|
286 |
hence "~ (ALL x:M. g <= x --> g = x)"; by simp; |
|
287 |
thus ?thesis; by contradiction; |
|
7808 | 288 |
qed; |
289 |
||
7927 | 290 |
txt{* It follows $H = E$, and the thesis can be shown. *}; |
7917 | 291 |
|
7808 | 292 |
show "is_linearform E h & (ALL x:F. h x = f x) |
293 |
& (ALL x:E. h x <= p x)"; |
|
294 |
proof (intro conjI); |
|
295 |
from eq; show "is_linearform E h"; by (simp!); |
|
296 |
show "ALL x:F. h x = f x"; |
|
297 |
proof (intro ballI, rule sym); |
|
298 |
fix x; assume "x:F"; show "f x = h x "; ..; |
|
299 |
qed; |
|
300 |
from eq; show "ALL x:E. h x <= p x"; by (force!); |
|
7917 | 301 |
qed; |
302 |
||
303 |
qed; |
|
304 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
305 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
306 |
|
7917 | 307 |
|
308 |
||
309 |
subsection {* An alternative formulation of the theorem *}; |
|
7656 | 310 |
|
7978 | 311 |
text {* The following alternative formulation of the Hahn-Banach |
312 |
Theorem\label{rabs-HahnBanach} uses the fact that for real numbers the |
|
313 |
following inequations are equivalent:\footnote{This was shown in lemma |
|
314 |
$\idt{rabs{\dsh}ineq{\dsh}iff}$ (see page \pageref{rabs-ineq-iff}).} |
|
7917 | 315 |
\begin{matharray}{ll} |
316 |
\forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\ |
|
317 |
\forall x\in H.\ap h\ap x\leq p\ap x\\ |
|
318 |
\end{matharray} |
|
7978 | 319 |
*}; |
7917 | 320 |
|
321 |
theorem rabs_HahnBanach: |
|
7978 | 322 |
"[| is_vectorspace E; is_subspace F E; is_seminorm E p; |
7808 | 323 |
is_linearform F f; ALL x:F. rabs (f x) <= p x |] |
324 |
==> EX g. is_linearform E g |
|
325 |
& (ALL x:F. g x = f x) |
|
326 |
& (ALL x:E. rabs (g x) <= p x)"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
327 |
proof -; |
7978 | 328 |
assume e: "is_vectorspace E" "is_subspace F E" "is_seminorm E p" |
7808 | 329 |
"is_linearform F f" "ALL x:F. rabs (f x) <= p x"; |
7917 | 330 |
have "ALL x:F. f x <= p x"; |
331 |
by (rule rabs_ineq_iff [RS iffD1]); |
|
7808 | 332 |
hence "EX g. is_linearform E g & (ALL x:F. g x = f x) |
333 |
& (ALL x:E. g x <= p x)"; |
|
7917 | 334 |
by (simp! only: HahnBanach); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
335 |
thus ?thesis; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
336 |
proof (elim exE conjE); |
7808 | 337 |
fix g; assume "is_linearform E g" "ALL x:F. g x = f x" |
338 |
"ALL x:E. g x <= p x"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
339 |
show ?thesis; |
7917 | 340 |
proof (intro exI conjI); |
7566 | 341 |
from e; show "ALL x:E. rabs (g x) <= p x"; |
7917 | 342 |
by (simp! add: rabs_ineq_iff [OF subspace_refl]); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
343 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
344 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
345 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
346 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
347 |
|
7917 | 348 |
subsection {* The Hahn-Banach Theorem for normed spaces *}; |
7656 | 349 |
|
7978 | 350 |
text {* Every continuous linear form $f$ on a subspace $F$ of a |
351 |
norm space $E$, can be extended to a continuous linear form $g$ on |
|
352 |
$E$ such that $\fnorm{f} = \fnorm {g}$. *}; |
|
7656 | 353 |
|
7917 | 354 |
theorem norm_HahnBanach: |
355 |
"[| is_normed_vectorspace E norm; is_subspace F E; |
|
7978 | 356 |
is_linearform F f; is_continuous F norm f |] |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
357 |
==> EX g. is_linearform E g |
7978 | 358 |
& is_continuous E norm g |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
359 |
& (ALL x:F. g x = f x) |
7917 | 360 |
& 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
|
361 |
proof -; |
7917 | 362 |
assume e_norm: "is_normed_vectorspace E norm"; |
363 |
assume f: "is_subspace F E" "is_linearform F f"; |
|
7978 | 364 |
assume f_cont: "is_continuous F norm f"; |
7566 | 365 |
have e: "is_vectorspace E"; ..; |
7917 | 366 |
with _; have f_norm: "is_normed_vectorspace F norm"; ..; |
7656 | 367 |
|
7917 | 368 |
txt{* We define the function $p$ on $E$ as follows: |
369 |
\begin{matharray}{l} |
|
7978 | 370 |
p \ap x = \fnorm f \cdot \norm x\\ |
7917 | 371 |
\end{matharray} |
372 |
*}; |
|
373 |
||
374 |
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
|
375 |
|
7978 | 376 |
txt{* $p$ is a seminorm on $E$: *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
377 |
|
7978 | 378 |
have q: "is_seminorm E p"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
379 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
380 |
fix x y a; assume "x:E" "y:E"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
381 |
|
7917 | 382 |
txt{* $p$ is positive definite: *}; |
383 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
384 |
show "0r <= p x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
385 |
proof (unfold p_def, rule real_le_mult_order); |
7917 | 386 |
from _ f_norm; show "0r <= function_norm F norm f"; ..; |
7566 | 387 |
show "0r <= norm x"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
388 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
389 |
|
7978 | 390 |
txt{* $p$ is absolutely homogenous: *}; |
7917 | 391 |
|
392 |
show "p (a <*> x) = rabs a * p x"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
393 |
proof -; |
7917 | 394 |
have "p (a <*> x) = function_norm F norm f * norm (a <*> x)"; |
7808 | 395 |
by (simp!); |
7917 | 396 |
also; have "norm (a <*> x) = rabs a * norm x"; |
7978 | 397 |
by (rule normed_vs_norm_rabs_homogenous); |
7917 | 398 |
also; have "function_norm F norm f * (rabs a * norm x) |
399 |
= rabs a * (function_norm F norm f * norm x)"; |
|
7566 | 400 |
by (simp! only: real_mult_left_commute); |
7917 | 401 |
also; have "... = rabs a * p x"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
402 |
finally; show ?thesis; .; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
403 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
404 |
|
7978 | 405 |
txt{* Furthermore, $p$ is subadditive: *}; |
7917 | 406 |
|
407 |
show "p (x + y) <= p x + p y"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
408 |
proof -; |
7917 | 409 |
have "p (x + y) = function_norm F norm f * norm (x + y)"; |
7808 | 410 |
by (simp!); |
7917 | 411 |
also; |
412 |
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
|
413 |
proof (rule real_mult_le_le_mono1); |
7917 | 414 |
from _ f_norm; show "0r <= function_norm F norm f"; ..; |
415 |
show "norm (x + y) <= norm x + norm y"; ..; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
416 |
qed; |
7917 | 417 |
also; have "... = function_norm F norm f * norm x |
418 |
+ function_norm F norm f * norm y"; |
|
7566 | 419 |
by (simp! only: real_add_mult_distrib2); |
420 |
finally; show ?thesis; by (simp!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
421 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
422 |
qed; |
7917 | 423 |
|
424 |
txt{* $f$ is bounded by $p$. *}; |
|
425 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
426 |
have "ALL x:F. rabs (f x) <= p x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
427 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
428 |
fix x; assume "x:F"; |
7917 | 429 |
from f_norm; show "rabs (f x) <= p x"; |
7808 | 430 |
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
|
431 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
432 |
|
7978 | 433 |
txt{* Using the fact that $p$ is a seminorm and |
434 |
$f$ is bounded by $q$ we can apply the Hahn-Banach Theorem |
|
435 |
for real vector spaces. |
|
436 |
So $f$ can be extended in a norm-preserving way to some function |
|
7917 | 437 |
$g$ on the whole vector space $E$. *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
438 |
|
7917 | 439 |
with e f q; |
440 |
have "EX g. is_linearform E g & (ALL x:F. g x = f x) |
|
441 |
& (ALL x:E. rabs (g x) <= p x)"; |
|
442 |
by (simp! add: rabs_HahnBanach); |
|
443 |
||
444 |
thus ?thesis; |
|
445 |
proof (elim exE conjE); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
446 |
fix g; |
7808 | 447 |
assume "is_linearform E g" and a: "ALL x:F. g x = f x" |
7978 | 448 |
and b: "ALL x:E. rabs (g x) <= p x"; |
7917 | 449 |
|
450 |
show "EX g. is_linearform E g |
|
7978 | 451 |
& is_continuous E norm g |
7917 | 452 |
& (ALL x:F. g x = f x) |
453 |
& function_norm E norm g = function_norm F norm f"; |
|
454 |
proof (intro exI conjI); |
|
455 |
||
7978 | 456 |
txt{* We futhermore have to show that |
457 |
$g$ is also continuous: *}; |
|
7917 | 458 |
|
7978 | 459 |
show g_cont: "is_continuous E norm g"; |
7917 | 460 |
proof; |
461 |
fix x; assume "x:E"; |
|
7978 | 462 |
from b [RS bspec, OF this]; |
7917 | 463 |
show "rabs (g x) <= function_norm F norm f * norm x"; |
7978 | 464 |
by (unfold p_def); |
7917 | 465 |
qed; |
466 |
||
7978 | 467 |
txt {* To complete the proof, we show that |
468 |
$\fnorm g = \fnorm f$. *}; |
|
469 |
||
7917 | 470 |
show "function_norm E norm g = function_norm F norm f" |
471 |
(is "?L = ?R"); |
|
472 |
proof (rule order_antisym); |
|
473 |
||
7978 | 474 |
txt{* First we show $\fnorm g \leq \fnorm f$. The function norm |
475 |
$\fnorm g$ is defined as the smallest $c\in\bbbR$ such that |
|
7917 | 476 |
\begin{matharray}{l} |
7978 | 477 |
\All {x\in E} {|g\ap x| \leq c \cdot \norm x} |
478 |
\end{matharray} |
|
479 |
Furthermore holds |
|
480 |
\begin{matharray}{l} |
|
481 |
\All {x\in E} {|g\ap x| \leq \fnorm f \cdot \norm x} |
|
482 |
\end{matharray} |
|
483 |
*}; |
|
484 |
||
7917 | 485 |
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
|
486 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
487 |
fix x; assume "x:E"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
488 |
show "rabs (g x) <= function_norm F norm f * norm x"; |
7917 | 489 |
by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
490 |
qed; |
7917 | 491 |
|
7978 | 492 |
with _ g_cont; show "?L <= ?R"; |
7917 | 493 |
proof (rule fnorm_le_ub); |
494 |
from f_cont f_norm; show "0r <= function_norm F norm f"; ..; |
|
495 |
qed; |
|
496 |
||
497 |
txt{* The other direction is achieved by a similar |
|
498 |
argument. *}; |
|
499 |
||
500 |
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
|
501 |
proof; |
7566 | 502 |
fix x; assume "x : F"; |
503 |
from a; have "g x = f x"; ..; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
504 |
hence "rabs (f x) = rabs (g x)"; by simp; |
7917 | 505 |
also; from _ _ g_cont; |
506 |
have "... <= function_norm E norm g * norm x"; |
|
507 |
by (rule norm_fx_le_norm_f_norm_x) (simp!)+; |
|
7808 | 508 |
finally; |
509 |
show "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
|
510 |
qed; |
7917 | 511 |
|
512 |
with f_norm f_cont; show "?R <= ?L"; |
|
513 |
proof (rule fnorm_le_ub); |
|
514 |
from g_cont; show "0r <= function_norm E norm g"; ..; |
|
515 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
516 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
517 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
518 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
519 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
520 |
|
7808 | 521 |
end; |