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