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