author  wenzelm 
Mon, 02 Nov 2015 16:02:32 +0100  
changeset 61543  de44d4fa5ef0 
parent 61540  f92bf6674699 
child 61583  c2b7033fa0ba 
permissions  rwrr 
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 HahnBanach 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 HahnBanach Theorem, 
13 
closely following @{cite \<open>\S36\<close> "Heuser:1986"}. 

58744  14 
\<close> 
9374  15 

61540  16 

58744  17 
subsection \<open>The HahnBanach Theorem for vector spaces\<close> 
9374  18 

61486  19 
paragraph \<open>HahnBanach 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 seminorm 
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 normpreserving, 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 normpreserving 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 nonempty 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 normpreserving way to a superspace \<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)" 

61539  52 
 \<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 
 \<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 
 \<open>then \<open>f\<close> can be extended to a linear form \<open>h\<close> on \<open>E\<close> in a normpreserving 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" 
61539  67 
 \<open>Show that every nonempty chain \<open>c\<close> of \<open>M\<close> has an upper bound in \<open>M\<close>:\<close> 
68 
 \<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" 
61539  98 
 \<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) 
61539  100 
 \<open>We show that \<open>M\<close> is nonempty:\<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 .. 
61539  119 
 \<open>\<open>g\<close> is a normpreserving extension of \<open>f\<close>, in other words:\<close> 
120 
 \<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 
 \<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" 

61539  126 
 \<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" 

61539  129 
 \<open>Assume \<open>h\<close> is not defined on whole \<open>E\<close>. Then show that \<open>h\<close> can be extended\<close> 
130 
 \<open>in a normpreserving 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'" 
61539  146 
 \<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" 
61540  156 
 \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequality; this will\<close> 
61539  157 
 \<open>be used to establish that \<open>h'\<close> is a normpreserving extension of \<open>h\<close>. 
61486  158 
\label{exxiuse}\<^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" 

61539  185 
 \<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'" 

61539  188 
 \<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 tabwidth;
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" 
61539  225 
 \<open>and \<open>h'\<close> is normpreserving. \<^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 tabwidth;
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 tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
31795
diff
changeset

254 
show "x' \<notin> H" by fact 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 
61539  273 
 \<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 HahnBanach 
61540  295 
Theorem\label{absHahnBanach} 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{absineqiff}).} 

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 HahnBanach 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 HahnBanach Theorem for real vector spaces. So \<open>f\<close> can be 

425 
extended in a normpreserving 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 tabwidth;
wenzelm
parents:
31795
diff
changeset

475 
[OF normed_vectorspace_with_fn_norm.intro, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
31795
diff
changeset

480 
from a x have "g x = f x" .. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
31795
diff
changeset

482 
also from g_cont 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
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 tabwidth;
wenzelm
parents:
31795
diff
changeset

485 
from FE x show "x \<in> E" .. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
31795
diff
changeset

491 
using g_cont 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 