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