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