author | paulson |
Thu, 01 Jan 2004 10:06:32 +0100 | |
changeset 14334 | 6137d24eef79 |
parent 14291 | 61df18481f53 |
child 14710 | 247615bfffb8 |
permissions | -rw-r--r-- |
9374 | 1 |
(* Title: HOL/Real/HahnBanach/HahnBanach.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gertrud Bauer, TU Munich |
|
4 |
*) |
|
5 |
||
6 |
header {* The Hahn-Banach Theorem *} |
|
7 |
||
10687 | 8 |
theory HahnBanach = HahnBanachLemmas: |
9374 | 9 |
|
10 |
text {* |
|
10687 | 11 |
We present the proof of two different versions of the Hahn-Banach |
9374 | 12 |
Theorem, closely following \cite[\S36]{Heuser:1986}. |
13 |
*} |
|
14 |
||
15 |
subsection {* The Hahn-Banach Theorem for vector spaces *} |
|
16 |
||
17 |
text {* |
|
10687 | 18 |
\textbf{Hahn-Banach Theorem.} Let @{text F} be a subspace of a real |
19 |
vector space @{text E}, let @{text p} be a semi-norm on @{text E}, |
|
20 |
and @{text f} be a linear form defined on @{text F} such that @{text |
|
21 |
f} is bounded by @{text p}, i.e. @{text "\<forall>x \<in> F. f x \<le> p x"}. Then |
|
22 |
@{text f} can be extended to a linear form @{text h} on @{text E} |
|
23 |
such that @{text h} is norm-preserving, i.e. @{text h} is also |
|
24 |
bounded by @{text p}. |
|
25 |
||
26 |
\bigskip |
|
27 |
\textbf{Proof Sketch.} |
|
28 |
\begin{enumerate} |
|
29 |
||
30 |
\item Define @{text M} as the set of norm-preserving extensions of |
|
31 |
@{text f} to subspaces of @{text E}. The linear forms in @{text M} |
|
32 |
are ordered by domain extension. |
|
9374 | 33 |
|
10687 | 34 |
\item We show that every non-empty chain in @{text M} has an upper |
35 |
bound in @{text M}. |
|
36 |
||
37 |
\item With Zorn's Lemma we conclude that there is a maximal function |
|
38 |
@{text g} in @{text M}. |
|
39 |
||
40 |
\item The domain @{text H} of @{text g} is the whole space @{text |
|
41 |
E}, as shown by classical contradiction: |
|
42 |
||
43 |
\begin{itemize} |
|
44 |
||
45 |
\item Assuming @{text g} is not defined on whole @{text E}, it can |
|
46 |
still be extended in a norm-preserving way to a super-space @{text |
|
47 |
H'} of @{text H}. |
|
48 |
||
49 |
\item Thus @{text g} can not be maximal. Contradiction! |
|
50 |
||
51 |
\end{itemize} |
|
52 |
\end{enumerate} |
|
9374 | 53 |
*} |
54 |
||
9256 | 55 |
theorem HahnBanach: |
13547 | 56 |
includes vectorspace E + subspace F E + seminorm E p + linearform F f |
13515 | 57 |
assumes fp: "\<forall>x \<in> F. f x \<le> p x" |
58 |
shows "\<exists>h. linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)" |
|
10687 | 59 |
-- {* Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E}, *} |
60 |
-- {* and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p}, *} |
|
61 |
-- {* then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp *} |
|
9035 | 62 |
proof - |
10687 | 63 |
def M \<equiv> "norm_pres_extensions E p F f" |
13515 | 64 |
hence M: "M = \<dots>" by (simp only:) |
13547 | 65 |
have E: "vectorspace E" . |
13515 | 66 |
have F: "vectorspace F" .. |
9035 | 67 |
{ |
13515 | 68 |
fix c assume cM: "c \<in> chain M" and ex: "\<exists>x. x \<in> c" |
9503 | 69 |
have "\<Union>c \<in> M" |
13515 | 70 |
-- {* Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}: *} |
71 |
-- {* @{text "\<Union>c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\<Union>c \<in> M"}. *} |
|
9035 | 72 |
proof (unfold M_def, rule norm_pres_extensionI) |
13515 | 73 |
let ?H = "domain (\<Union>c)" |
74 |
let ?h = "funct (\<Union>c)" |
|
8084 | 75 |
|
13515 | 76 |
have a: "graph ?H ?h = \<Union>c" |
77 |
proof (rule graph_domain_funct) |
|
78 |
fix x y z assume "(x, y) \<in> \<Union>c" and "(x, z) \<in> \<Union>c" |
|
79 |
with M_def cM show "z = y" by (rule sup_definite) |
|
9035 | 80 |
qed |
13515 | 81 |
moreover from M cM a have "linearform ?H ?h" |
82 |
by (rule sup_lf) |
|
83 |
moreover from a M cM ex have "?H \<unlhd> E" |
|
84 |
by (rule sup_subE) |
|
85 |
moreover from a M cM ex have "F \<unlhd> ?H" |
|
86 |
by (rule sup_supF) |
|
87 |
moreover from a M cM ex have "graph F f \<subseteq> graph ?H ?h" |
|
88 |
by (rule sup_ext) |
|
89 |
moreover from a M cM have "\<forall>x \<in> ?H. ?h x \<le> p x" |
|
90 |
by (rule sup_norm_pres) |
|
91 |
ultimately show "\<exists>H h. \<Union>c = graph H h |
|
92 |
\<and> linearform H h |
|
93 |
\<and> H \<unlhd> E |
|
94 |
\<and> F \<unlhd> H |
|
95 |
\<and> graph F f \<subseteq> graph H h |
|
96 |
\<and> (\<forall>x \<in> H. h x \<le> p x)" by blast |
|
9035 | 97 |
qed |
98 |
} |
|
10687 | 99 |
hence "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x" |
100 |
-- {* With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp *} |
|
9035 | 101 |
proof (rule Zorn's_Lemma) |
13515 | 102 |
-- {* We show that @{text M} is non-empty: *} |
103 |
show "graph F f \<in> M" |
|
104 |
proof (unfold M_def, rule norm_pres_extensionI2) |
|
105 |
show "linearform F f" . |
|
106 |
show "F \<unlhd> E" . |
|
107 |
from F show "F \<unlhd> F" by (rule vectorspace.subspace_refl) |
|
108 |
show "graph F f \<subseteq> graph F f" .. |
|
109 |
show "\<forall>x\<in>F. f x \<le> p x" . |
|
110 |
qed |
|
9035 | 111 |
qed |
13515 | 112 |
then obtain g where gM: "g \<in> M" and "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x" |
113 |
by blast |
|
114 |
from gM [unfolded M_def] obtain H h where |
|
115 |
g_rep: "g = graph H h" |
|
116 |
and linearform: "linearform H h" |
|
117 |
and HE: "H \<unlhd> E" and FH: "F \<unlhd> H" |
|
118 |
and graphs: "graph F f \<subseteq> graph H h" |
|
119 |
and hp: "\<forall>x \<in> H. h x \<le> p x" .. |
|
10687 | 120 |
-- {* @{text g} is a norm-preserving extension of @{text f}, in other words: *} |
121 |
-- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *} |
|
122 |
-- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *} |
|
13515 | 123 |
from HE have H: "vectorspace H" |
13547 | 124 |
by (rule subspace.vectorspace) |
13515 | 125 |
|
126 |
have HE_eq: "H = E" |
|
10687 | 127 |
-- {* We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp *} |
13515 | 128 |
proof (rule classical) |
129 |
assume neq: "H \<noteq> E" |
|
10687 | 130 |
-- {* Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended *} |
131 |
-- {* in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \skp *} |
|
13515 | 132 |
have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'" |
133 |
proof - |
|
134 |
from HE have "H \<subseteq> E" .. |
|
135 |
with neq obtain x' where x'E: "x' \<in> E" and "x' \<notin> H" by blast |
|
136 |
obtain x': "x' \<noteq> 0" |
|
137 |
proof |
|
138 |
show "x' \<noteq> 0" |
|
139 |
proof |
|
140 |
assume "x' = 0" |
|
141 |
with H have "x' \<in> H" by (simp only: vectorspace.zero) |
|
142 |
then show False by contradiction |
|
9475 | 143 |
qed |
13515 | 144 |
qed |
145 |
||
146 |
def H' \<equiv> "H + lin x'" |
|
10687 | 147 |
-- {* Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp *} |
13515 | 148 |
have HH': "H \<unlhd> H'" |
149 |
proof (unfold H'_def) |
|
150 |
have "vectorspace (lin x')" .. |
|
151 |
with H show "H \<unlhd> H + lin x'" .. |
|
152 |
qed |
|
153 |
||
154 |
obtain xi where |
|
155 |
"\<forall>y \<in> H. - p (y + x') - h y \<le> xi |
|
156 |
\<and> xi \<le> p (y + x') - h y" |
|
10687 | 157 |
-- {* Pick a real number @{text \<xi>} that fulfills certain inequations; this will *} |
158 |
-- {* be used to establish that @{text h'} is a norm-preserving extension of @{text h}. |
|
9475 | 159 |
\label{ex-xi-use}\skp *} |
13515 | 160 |
proof - |
161 |
from H have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi |
|
162 |
\<and> xi \<le> p (y + x') - h y" |
|
163 |
proof (rule ex_xi) |
|
164 |
fix u v assume u: "u \<in> H" and v: "v \<in> H" |
|
165 |
with HE have uE: "u \<in> E" and vE: "v \<in> E" by auto |
|
166 |
from H u v linearform have "h v - h u = h (v - u)" |
|
13547 | 167 |
by (simp add: linearform.diff) |
13515 | 168 |
also from hp and H u v have "\<dots> \<le> p (v - u)" |
169 |
by (simp only: vectorspace.diff_closed) |
|
170 |
also from x'E uE vE have "v - u = x' + - x' + v + - u" |
|
171 |
by (simp add: diff_eq1) |
|
172 |
also from x'E uE vE have "\<dots> = v + x' + - (u + x')" |
|
173 |
by (simp add: add_ac) |
|
174 |
also from x'E uE vE have "\<dots> = (v + x') - (u + x')" |
|
175 |
by (simp add: diff_eq1) |
|
13547 | 176 |
also from x'E uE vE E have "p \<dots> \<le> p (v + x') + p (u + x')" |
13515 | 177 |
by (simp add: diff_subadditive) |
178 |
finally have "h v - h u \<le> p (v + x') + p (u + x')" . |
|
13547 | 179 |
then show "- p (u + x') - h u \<le> p (v + x') - h v" by simp |
13515 | 180 |
qed |
181 |
then show ?thesis .. |
|
182 |
qed |
|
183 |
||
184 |
def h' \<equiv> "\<lambda>x. let (y, a) = |
|
185 |
SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi" |
|
186 |
-- {* Define the extension @{text h'} of @{text h} to @{text H'} using @{text \<xi>}. \skp *} |
|
187 |
||
188 |
have "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'" |
|
189 |
-- {* @{text h'} is an extension of @{text h} \dots \skp *} |
|
190 |
proof |
|
191 |
show "g \<subseteq> graph H' h'" |
|
9475 | 192 |
proof - |
13515 | 193 |
have "graph H h \<subseteq> graph H' h'" |
194 |
proof (rule graph_extI) |
|
195 |
fix t assume t: "t \<in> H" |
|
196 |
have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)" |
|
197 |
by (rule decomp_H'_H) |
|
198 |
with h'_def show "h t = h' t" by (simp add: Let_def) |
|
199 |
next |
|
200 |
from HH' show "H \<subseteq> H'" .. |
|
9475 | 201 |
qed |
13515 | 202 |
with g_rep show ?thesis by (simp only:) |
9475 | 203 |
qed |
204 |
||
13515 | 205 |
show "g \<noteq> graph H' h'" |
206 |
proof - |
|
207 |
have "graph H h \<noteq> graph H' h'" |
|
9475 | 208 |
proof |
13515 | 209 |
assume eq: "graph H h = graph H' h'" |
210 |
have "x' \<in> H'" |
|
211 |
proof (unfold H'_def, rule) |
|
212 |
from H show "0 \<in> H" by (rule vectorspace.zero) |
|
213 |
from x'E show "x' \<in> lin x'" by (rule x_lin_x) |
|
214 |
from x'E show "x' = 0 + x'" by simp |
|
9261 | 215 |
qed |
13515 | 216 |
hence "(x', h' x') \<in> graph H' h'" .. |
217 |
with eq have "(x', h' x') \<in> graph H h" by (simp only:) |
|
218 |
hence "x' \<in> H" .. |
|
219 |
thus False by contradiction |
|
9035 | 220 |
qed |
13515 | 221 |
with g_rep show ?thesis by simp |
9035 | 222 |
qed |
9256 | 223 |
qed |
13515 | 224 |
moreover have "graph H' h' \<in> M" |
225 |
-- {* and @{text h'} is norm-preserving. \skp *} |
|
226 |
proof (unfold M_def) |
|
227 |
show "graph H' h' \<in> norm_pres_extensions E p F f" |
|
228 |
proof (rule norm_pres_extensionI2) |
|
229 |
show "linearform H' h'" by (rule h'_lf) |
|
230 |
show "H' \<unlhd> E" |
|
231 |
proof (unfold H'_def, rule) |
|
232 |
show "H \<unlhd> E" . |
|
233 |
show "vectorspace E" . |
|
234 |
from x'E show "lin x' \<unlhd> E" .. |
|
235 |
qed |
|
236 |
have "F \<unlhd> H" . |
|
237 |
from H this HH' show FH': "F \<unlhd> H'" |
|
238 |
by (rule vectorspace.subspace_trans) |
|
239 |
show "graph F f \<subseteq> graph H' h'" |
|
240 |
proof (rule graph_extI) |
|
241 |
fix x assume x: "x \<in> F" |
|
242 |
with graphs have "f x = h x" .. |
|
243 |
also have "\<dots> = h x + 0 * xi" by simp |
|
244 |
also have "\<dots> = (let (y, a) = (x, 0) in h y + a * xi)" |
|
245 |
by (simp add: Let_def) |
|
246 |
also have "(x, 0) = |
|
247 |
(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)" |
|
248 |
proof (rule decomp_H'_H [symmetric]) |
|
249 |
from FH x show "x \<in> H" .. |
|
250 |
from x' show "x' \<noteq> 0" . |
|
251 |
qed |
|
252 |
also have |
|
253 |
"(let (y, a) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) |
|
254 |
in h y + a * xi) = h' x" by (simp only: h'_def) |
|
255 |
finally show "f x = h' x" . |
|
256 |
next |
|
257 |
from FH' show "F \<subseteq> H'" .. |
|
258 |
qed |
|
259 |
show "\<forall>x \<in> H'. h' x \<le> p x" by (rule h'_norm_pres) |
|
260 |
qed |
|
261 |
qed |
|
262 |
ultimately show ?thesis .. |
|
9475 | 263 |
qed |
13515 | 264 |
hence "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp |
265 |
-- {* So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp *} |
|
266 |
then show "H = E" by contradiction |
|
9035 | 267 |
qed |
13515 | 268 |
|
269 |
from HE_eq and linearform have "linearform E h" |
|
270 |
by (simp only:) |
|
271 |
moreover have "\<forall>x \<in> F. h x = f x" |
|
272 |
proof |
|
273 |
fix x assume "x \<in> F" |
|
274 |
with graphs have "f x = h x" .. |
|
275 |
then show "h x = f x" .. |
|
276 |
qed |
|
277 |
moreover from HE_eq and hp have "\<forall>x \<in> E. h x \<le> p x" |
|
278 |
by (simp only:) |
|
279 |
ultimately show ?thesis by blast |
|
9475 | 280 |
qed |
9374 | 281 |
|
282 |
||
283 |
subsection {* Alternative formulation *} |
|
284 |
||
10687 | 285 |
text {* |
286 |
The following alternative formulation of the Hahn-Banach |
|
287 |
Theorem\label{abs-HahnBanach} uses the fact that for a real linear |
|
288 |
form @{text f} and a seminorm @{text p} the following inequations |
|
289 |
are equivalent:\footnote{This was shown in lemma @{thm [source] |
|
290 |
abs_ineq_iff} (see page \pageref{abs-ineq-iff}).} |
|
291 |
\begin{center} |
|
292 |
\begin{tabular}{lll} |
|
293 |
@{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and & |
|
294 |
@{text "\<forall>x \<in> H. h x \<le> p x"} \\ |
|
295 |
\end{tabular} |
|
296 |
\end{center} |
|
9374 | 297 |
*} |
298 |
||
299 |
theorem abs_HahnBanach: |
|
13547 | 300 |
includes vectorspace E + subspace F E + linearform F f + seminorm E p |
13515 | 301 |
assumes fp: "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x" |
302 |
shows "\<exists>g. linearform E g |
|
303 |
\<and> (\<forall>x \<in> F. g x = f x) |
|
10687 | 304 |
\<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)" |
9374 | 305 |
proof - |
13515 | 306 |
have "\<exists>g. linearform E g \<and> (\<forall>x \<in> F. g x = f x) |
307 |
\<and> (\<forall>x \<in> E. g x \<le> p x)" |
|
308 |
proof (rule HahnBanach) |
|
309 |
show "\<forall>x \<in> F. f x \<le> p x" |
|
310 |
by (rule abs_ineq_iff [THEN iffD1]) |
|
311 |
qed |
|
312 |
then obtain g where * : "linearform E g" "\<forall>x \<in> F. g x = f x" |
|
313 |
and "\<forall>x \<in> E. g x \<le> p x" by blast |
|
314 |
have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x" |
|
315 |
proof (rule abs_ineq_iff [THEN iffD2]) |
|
316 |
show "E \<unlhd> E" .. |
|
317 |
qed |
|
318 |
with * show ?thesis by blast |
|
9475 | 319 |
qed |
13515 | 320 |
|
9374 | 321 |
|
322 |
subsection {* The Hahn-Banach Theorem for normed spaces *} |
|
323 |
||
10687 | 324 |
text {* |
325 |
Every continuous linear form @{text f} on a subspace @{text F} of a |
|
326 |
norm space @{text E}, can be extended to a continuous linear form |
|
327 |
@{text g} on @{text E} such that @{text "\<parallel>f\<parallel> = \<parallel>g\<parallel>"}. |
|
328 |
*} |
|
9374 | 329 |
|
330 |
theorem norm_HahnBanach: |
|
13547 | 331 |
includes normed_vectorspace E + subspace F E + linearform F f + fn_norm + continuous F norm f |
13515 | 332 |
shows "\<exists>g. linearform E g |
333 |
\<and> continuous E norm g |
|
10687 | 334 |
\<and> (\<forall>x \<in> F. g x = f x) |
13515 | 335 |
\<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F" |
9475 | 336 |
proof - |
13515 | 337 |
have E: "vectorspace E" . |
338 |
have E_norm: "normed_vectorspace E norm" .. |
|
339 |
have FE: "F \<unlhd> E" . |
|
340 |
have F: "vectorspace F" .. |
|
341 |
have linearform: "linearform F f" . |
|
14214
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
342 |
have F_norm: "normed_vectorspace F norm" |
14291 | 343 |
by (rule subspace_normed_vs [OF _ _ norm.intro]) |
13547 | 344 |
have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F" |
345 |
by (rule normed_vectorspace.fn_norm_ge_zero |
|
14214
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
346 |
[OF F_norm _ continuous.intro, folded B_def fn_norm_def]) |
13515 | 347 |
|
348 |
txt {* We define a function @{text p} on @{text E} as follows: |
|
349 |
@{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *} |
|
350 |
def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>" |
|
351 |
||
352 |
txt {* @{text p} is a seminorm on @{text E}: *} |
|
353 |
have q: "seminorm E p" |
|
354 |
proof |
|
355 |
fix x y a assume x: "x \<in> E" and y: "y \<in> E" |
|
9374 | 356 |
|
13515 | 357 |
txt {* @{text p} is positive definite: *} |
358 |
show "0 \<le> p x" |
|
359 |
proof (unfold p_def, rule real_le_mult_order1a) |
|
13547 | 360 |
show "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero) |
13515 | 361 |
from x show "0 \<le> \<parallel>x\<parallel>" .. |
362 |
qed |
|
363 |
||
364 |
txt {* @{text p} is absolutely homogenous: *} |
|
9475 | 365 |
|
13515 | 366 |
show "p (a \<cdot> x) = \<bar>a\<bar> * p x" |
367 |
proof - |
|
13547 | 368 |
have "p (a \<cdot> x) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>a \<cdot> x\<parallel>" by (simp only: p_def) |
369 |
also from x have "\<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>" by (rule abs_homogenous) |
|
370 |
also have "\<parallel>f\<parallel>\<hyphen>F * (\<bar>a\<bar> * \<parallel>x\<parallel>) = \<bar>a\<bar> * (\<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>)" by simp |
|
371 |
also have "\<dots> = \<bar>a\<bar> * p x" by (simp only: p_def) |
|
13515 | 372 |
finally show ?thesis . |
373 |
qed |
|
374 |
||
375 |
txt {* Furthermore, @{text p} is subadditive: *} |
|
9475 | 376 |
|
13515 | 377 |
show "p (x + y) \<le> p x + p y" |
378 |
proof - |
|
13547 | 379 |
have "p (x + y) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel>" by (simp only: p_def) |
13515 | 380 |
also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>F * (\<parallel>x\<parallel> + \<parallel>y\<parallel>)" |
381 |
proof (rule real_mult_le_le_mono1a) |
|
13547 | 382 |
show "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero) |
13515 | 383 |
from x y show "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" .. |
384 |
qed |
|
14334 | 385 |
also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>" by (simp only: right_distrib) |
13547 | 386 |
also have "\<dots> = p x + p y" by (simp only: p_def) |
13515 | 387 |
finally show ?thesis . |
388 |
qed |
|
389 |
qed |
|
9475 | 390 |
|
13515 | 391 |
txt {* @{text f} is bounded by @{text p}. *} |
9374 | 392 |
|
13515 | 393 |
have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x" |
394 |
proof |
|
395 |
fix x assume "x \<in> F" |
|
396 |
show "\<bar>f x\<bar> \<le> p x" |
|
13547 | 397 |
by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong |
14214
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
398 |
[OF F_norm _ continuous.intro, folded B_def fn_norm_def]) |
13515 | 399 |
qed |
9475 | 400 |
|
13515 | 401 |
txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded |
402 |
by @{text p} we can apply the Hahn-Banach Theorem for real vector |
|
403 |
spaces. So @{text f} can be extended in a norm-preserving way to |
|
404 |
some function @{text g} on the whole vector space @{text E}. *} |
|
9475 | 405 |
|
13515 | 406 |
with E FE linearform q obtain g where |
407 |
linearformE: "linearform E g" |
|
408 |
and a: "\<forall>x \<in> F. g x = f x" |
|
409 |
and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x" |
|
410 |
by (rule abs_HahnBanach [elim_format]) rules |
|
9475 | 411 |
|
13515 | 412 |
txt {* We furthermore have to show that @{text g} is also continuous: *} |
413 |
||
414 |
have g_cont: "continuous E norm g" using linearformE |
|
9475 | 415 |
proof |
9503 | 416 |
fix x assume "x \<in> E" |
13515 | 417 |
with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>" |
418 |
by (simp only: p_def) |
|
10687 | 419 |
qed |
9374 | 420 |
|
13515 | 421 |
txt {* To complete the proof, we show that @{text "\<parallel>g\<parallel> = \<parallel>f\<parallel>"}. *} |
9475 | 422 |
|
13515 | 423 |
have "\<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F" |
9475 | 424 |
proof (rule order_antisym) |
10687 | 425 |
txt {* |
426 |
First we show @{text "\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>"}. The function norm @{text |
|
427 |
"\<parallel>g\<parallel>"} is defined as the smallest @{text "c \<in> \<real>"} such that |
|
428 |
\begin{center} |
|
429 |
\begin{tabular}{l} |
|
430 |
@{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} |
|
431 |
\end{tabular} |
|
432 |
\end{center} |
|
433 |
\noindent Furthermore holds |
|
434 |
\begin{center} |
|
435 |
\begin{tabular}{l} |
|
436 |
@{text "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} |
|
437 |
\end{tabular} |
|
438 |
\end{center} |
|
9475 | 439 |
*} |
10687 | 440 |
|
13515 | 441 |
have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>" |
9475 | 442 |
proof |
10687 | 443 |
fix x assume "x \<in> E" |
13515 | 444 |
with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>" |
445 |
by (simp only: p_def) |
|
9374 | 446 |
qed |
14214
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
447 |
from linearformE g_cont this ge_zero |
13515 | 448 |
show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F" |
13547 | 449 |
by (rule fn_norm_least [of g, folded B_def fn_norm_def]) |
9374 | 450 |
|
13515 | 451 |
txt {* The other direction is achieved by a similar argument. *} |
452 |
||
13547 | 453 |
show "\<parallel>f\<parallel>\<hyphen>F \<le> \<parallel>g\<parallel>\<hyphen>E" |
454 |
proof (rule normed_vectorspace.fn_norm_least [OF F_norm, folded B_def fn_norm_def]) |
|
455 |
show "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" |
|
456 |
proof |
|
457 |
fix x assume x: "x \<in> F" |
|
458 |
from a have "g x = f x" .. |
|
459 |
hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:) |
|
14214
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
460 |
also from linearformE g_cont |
13547 | 461 |
have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" |
462 |
proof (rule fn_norm_le_cong [of g, folded B_def fn_norm_def]) |
|
463 |
from FE x show "x \<in> E" .. |
|
464 |
qed |
|
465 |
finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" . |
|
9374 | 466 |
qed |
13547 | 467 |
show "0 \<le> \<parallel>g\<parallel>\<hyphen>E" |
14214
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
468 |
using linearformE g_cont |
13547 | 469 |
by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def]) |
14214
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
470 |
next |
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
471 |
show "continuous F norm f" by (rule continuous.intro) |
10687 | 472 |
qed |
9374 | 473 |
qed |
13547 | 474 |
with linearformE a g_cont show ?thesis by blast |
9475 | 475 |
qed |
9374 | 476 |
|
9475 | 477 |
end |