author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46867  0883804b67bb 
child 47445  69e96e5500df 
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 

5 
header {* The HahnBanach Theorem *} 

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 

11 
text {* 

10687  12 
We present the proof of two different versions of the HahnBanach 
9374  13 
Theorem, closely following \cite[\S36]{Heuser:1986}. 
14 
*} 

15 

16 
subsection {* The HahnBanach Theorem for vector spaces *} 

17 

18 
text {* 

10687  19 
\textbf{HahnBanach Theorem.} Let @{text F} be a subspace of a real 
20 
vector space @{text E}, let @{text p} be a seminorm on @{text E}, 

21 
and @{text f} be a linear form defined on @{text F} such that @{text 

22 
f} is bounded by @{text p}, i.e. @{text "\<forall>x \<in> F. f x \<le> p x"}. Then 

23 
@{text f} can be extended to a linear form @{text h} on @{text E} 

24 
such that @{text h} is normpreserving, i.e. @{text h} is also 

25 
bounded by @{text p}. 

26 

27 
\bigskip 

28 
\textbf{Proof Sketch.} 

29 
\begin{enumerate} 

30 

31 
\item Define @{text M} as the set of normpreserving extensions of 

32 
@{text f} to subspaces of @{text E}. The linear forms in @{text M} 

33 
are ordered by domain extension. 

9374  34 

10687  35 
\item We show that every nonempty chain in @{text M} has an upper 
36 
bound in @{text M}. 

37 

38 
\item With Zorn's Lemma we conclude that there is a maximal function 

39 
@{text g} in @{text M}. 

40 

41 
\item The domain @{text H} of @{text g} is the whole space @{text 

42 
E}, as shown by classical contradiction: 

43 

44 
\begin{itemize} 

45 

46 
\item Assuming @{text g} is not defined on whole @{text E}, it can 

47 
still be extended in a normpreserving way to a superspace @{text 

48 
H'} of @{text H}. 

49 

50 
\item Thus @{text g} can not be maximal. Contradiction! 

51 

52 
\end{itemize} 

53 
\end{enumerate} 

9374  54 
*} 
55 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29291
diff
changeset

56 
theorem Hahn_Banach: 
27611  57 
assumes E: "vectorspace E" and "subspace F E" 
58 
and "seminorm E p" and "linearform F f" 

13515  59 
assumes fp: "\<forall>x \<in> F. f x \<le> p x" 
60 
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  61 
 {* Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E}, *} 
62 
 {* and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p}, *} 

63 
 {* then @{text f} can be extended to a linear form @{text h} on @{text E} in a normpreserving way. \skp *} 

9035  64 
proof  
29234  65 
interpret vectorspace E by fact 
66 
interpret subspace F E by fact 

67 
interpret seminorm E p by fact 

68 
interpret linearform F f by fact 

10687  69 
def M \<equiv> "norm_pres_extensions E p F f" 
27612  70 
then have M: "M = \<dots>" by (simp only:) 
27611  71 
from E have F: "vectorspace F" .. 
23378  72 
note FE = `F \<unlhd> E` 
9035  73 
{ 
13515  74 
fix c assume cM: "c \<in> chain M" and ex: "\<exists>x. x \<in> c" 
9503  75 
have "\<Union>c \<in> M" 
13515  76 
 {* Show that every nonempty chain @{text c} of @{text M} has an upper bound in @{text M}: *} 
77 
 {* @{text "\<Union>c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\<Union>c \<in> M"}. *} 

27612  78 
unfolding M_def 
79 
proof (rule norm_pres_extensionI) 

13515  80 
let ?H = "domain (\<Union>c)" 
81 
let ?h = "funct (\<Union>c)" 

8084  82 

13515  83 
have a: "graph ?H ?h = \<Union>c" 
84 
proof (rule graph_domain_funct) 

85 
fix x y z assume "(x, y) \<in> \<Union>c" and "(x, z) \<in> \<Union>c" 

86 
with M_def cM show "z = y" by (rule sup_definite) 

9035  87 
qed 
13515  88 
moreover from M cM a have "linearform ?H ?h" 
89 
by (rule sup_lf) 

23378  90 
moreover from a M cM ex FE E have "?H \<unlhd> E" 
13515  91 
by (rule sup_subE) 
23378  92 
moreover from a M cM ex FE have "F \<unlhd> ?H" 
13515  93 
by (rule sup_supF) 
94 
moreover from a M cM ex have "graph F f \<subseteq> graph ?H ?h" 

95 
by (rule sup_ext) 

96 
moreover from a M cM have "\<forall>x \<in> ?H. ?h x \<le> p x" 

97 
by (rule sup_norm_pres) 

98 
ultimately show "\<exists>H h. \<Union>c = graph H h 

99 
\<and> linearform H h 

100 
\<and> H \<unlhd> E 

101 
\<and> F \<unlhd> H 

102 
\<and> graph F f \<subseteq> graph H h 

103 
\<and> (\<forall>x \<in> H. h x \<le> p x)" by blast 

9035  104 
qed 
105 
} 

27612  106 
then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x" 
10687  107 
 {* With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp *} 
9035  108 
proof (rule Zorn's_Lemma) 
13515  109 
 {* We show that @{text M} is nonempty: *} 
110 
show "graph F f \<in> M" 

27612  111 
unfolding M_def 
112 
proof (rule norm_pres_extensionI2) 

23378  113 
show "linearform F f" by fact 
114 
show "F \<unlhd> E" by fact 

13515  115 
from F show "F \<unlhd> F" by (rule vectorspace.subspace_refl) 
116 
show "graph F f \<subseteq> graph F f" .. 

23378  117 
show "\<forall>x\<in>F. f x \<le> p x" by fact 
13515  118 
qed 
9035  119 
qed 
23378  120 
then obtain g where gM: "g \<in> M" and gx: "\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x" 
13515  121 
by blast 
27612  122 
from gM obtain H h where 
13515  123 
g_rep: "g = graph H h" 
124 
and linearform: "linearform H h" 

125 
and HE: "H \<unlhd> E" and FH: "F \<unlhd> H" 

126 
and graphs: "graph F f \<subseteq> graph H h" 

27612  127 
and hp: "\<forall>x \<in> H. h x \<le> p x" unfolding M_def .. 
10687  128 
 {* @{text g} is a normpreserving extension of @{text f}, in other words: *} 
129 
 {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *} 

130 
 {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *} 

23378  131 
from HE E have H: "vectorspace H" 
13547  132 
by (rule subspace.vectorspace) 
13515  133 

134 
have HE_eq: "H = E" 

10687  135 
 {* We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp *} 
13515  136 
proof (rule classical) 
137 
assume neq: "H \<noteq> E" 

10687  138 
 {* Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended *} 
139 
 {* in a normpreserving way to a function @{text h'} with the graph @{text g'}. \skp *} 

13515  140 
have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'" 
141 
proof  

142 
from HE have "H \<subseteq> E" .. 

143 
with neq obtain x' where x'E: "x' \<in> E" and "x' \<notin> H" by blast 

144 
obtain x': "x' \<noteq> 0" 

145 
proof 

146 
show "x' \<noteq> 0" 

147 
proof 

148 
assume "x' = 0" 

149 
with H have "x' \<in> H" by (simp only: vectorspace.zero) 

23378  150 
with `x' \<notin> H` show False by contradiction 
9475  151 
qed 
13515  152 
qed 
153 

44190  154 
def H' \<equiv> "H \<oplus> lin x'" 
10687  155 
 {* Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp *} 
13515  156 
have HH': "H \<unlhd> H'" 
157 
proof (unfold H'_def) 

23378  158 
from x'E have "vectorspace (lin x')" .. 
44190  159 
with H show "H \<unlhd> H \<oplus> lin x'" .. 
13515  160 
qed 
161 

162 
obtain xi where 

23378  163 
xi: "\<forall>y \<in> H.  p (y + x')  h y \<le> xi 
13515  164 
\<and> xi \<le> p (y + x')  h y" 
10687  165 
 {* Pick a real number @{text \<xi>} that fulfills certain inequations; this will *} 
166 
 {* be used to establish that @{text h'} is a normpreserving extension of @{text h}. 

9475  167 
\label{exxiuse}\skp *} 
13515  168 
proof  
169 
from H have "\<exists>xi. \<forall>y \<in> H.  p (y + x')  h y \<le> xi 

170 
\<and> xi \<le> p (y + x')  h y" 

171 
proof (rule ex_xi) 

172 
fix u v assume u: "u \<in> H" and v: "v \<in> H" 

173 
with HE have uE: "u \<in> E" and vE: "v \<in> E" by auto 

174 
from H u v linearform have "h v  h u = h (v  u)" 

13547  175 
by (simp add: linearform.diff) 
13515  176 
also from hp and H u v have "\<dots> \<le> p (v  u)" 
177 
by (simp only: vectorspace.diff_closed) 

178 
also from x'E uE vE have "v  u = x' +  x' + v +  u" 

179 
by (simp add: diff_eq1) 

180 
also from x'E uE vE have "\<dots> = v + x' +  (u + x')" 

181 
by (simp add: add_ac) 

182 
also from x'E uE vE have "\<dots> = (v + x')  (u + x')" 

183 
by (simp add: diff_eq1) 

13547  184 
also from x'E uE vE E have "p \<dots> \<le> p (v + x') + p (u + x')" 
13515  185 
by (simp add: diff_subadditive) 
186 
finally have "h v  h u \<le> p (v + x') + p (u + x')" . 

13547  187 
then show " p (u + x')  h u \<le> p (v + x')  h v" by simp 
13515  188 
qed 
23378  189 
then show thesis by (blast intro: that) 
13515  190 
qed 
191 

192 
def h' \<equiv> "\<lambda>x. let (y, a) = 

193 
SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi" 

194 
 {* Define the extension @{text h'} of @{text h} to @{text H'} using @{text \<xi>}. \skp *} 

195 

196 
have "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'" 

197 
 {* @{text h'} is an extension of @{text h} \dots \skp *} 

198 
proof 

199 
show "g \<subseteq> graph H' h'" 

9475  200 
proof  
13515  201 
have "graph H h \<subseteq> graph H' h'" 
202 
proof (rule graph_extI) 

203 
fix t assume t: "t \<in> H" 

23378  204 
from E HE t have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

205 
using `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` by (rule decomp_H'_H) 
13515  206 
with h'_def show "h t = h' t" by (simp add: Let_def) 
207 
next 

208 
from HH' show "H \<subseteq> H'" .. 

9475  209 
qed 
13515  210 
with g_rep show ?thesis by (simp only:) 
9475  211 
qed 
212 

13515  213 
show "g \<noteq> graph H' h'" 
214 
proof  

215 
have "graph H h \<noteq> graph H' h'" 

9475  216 
proof 
13515  217 
assume eq: "graph H h = graph H' h'" 
218 
have "x' \<in> H'" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

219 
unfolding H'_def 
27612  220 
proof 
13515  221 
from H show "0 \<in> H" by (rule vectorspace.zero) 
222 
from x'E show "x' \<in> lin x'" by (rule x_lin_x) 

223 
from x'E show "x' = 0 + x'" by simp 

9261  224 
qed 
27612  225 
then have "(x', h' x') \<in> graph H' h'" .. 
13515  226 
with eq have "(x', h' x') \<in> graph H h" by (simp only:) 
27612  227 
then have "x' \<in> H" .. 
23378  228 
with `x' \<notin> H` show False by contradiction 
9035  229 
qed 
13515  230 
with g_rep show ?thesis by simp 
9035  231 
qed 
9256  232 
qed 
13515  233 
moreover have "graph H' h' \<in> M" 
234 
 {* and @{text h'} is normpreserving. \skp *} 

235 
proof (unfold M_def) 

236 
show "graph H' h' \<in> norm_pres_extensions E p F f" 

237 
proof (rule norm_pres_extensionI2) 

23378  238 
show "linearform H' h'" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

239 
using h'_def H'_def HE linearform `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

240 
by (rule h'_lf) 
13515  241 
show "H' \<unlhd> E" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

242 
unfolding H'_def 
23378  243 
proof 
244 
show "H \<unlhd> E" by fact 

245 
show "vectorspace E" by fact 

13515  246 
from x'E show "lin x' \<unlhd> E" .. 
247 
qed 

23378  248 
from H `F \<unlhd> H` HH' show FH': "F \<unlhd> H'" 
13515  249 
by (rule vectorspace.subspace_trans) 
250 
show "graph F f \<subseteq> graph H' h'" 

251 
proof (rule graph_extI) 

252 
fix x assume x: "x \<in> F" 

253 
with graphs have "f x = h x" .. 

254 
also have "\<dots> = h x + 0 * xi" by simp 

255 
also have "\<dots> = (let (y, a) = (x, 0) in h y + a * xi)" 

256 
by (simp add: Let_def) 

257 
also have "(x, 0) = 

258 
(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

259 
using E HE 
13515  260 
proof (rule decomp_H'_H [symmetric]) 
261 
from FH x show "x \<in> H" .. 

262 
from x' show "x' \<noteq> 0" . 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

263 
show "x' \<notin> H" by fact 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

264 
show "x' \<in> E" by fact 
13515  265 
qed 
266 
also have 

267 
"(let (y, a) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) 

268 
in h y + a * xi) = h' x" by (simp only: h'_def) 

269 
finally show "f x = h' x" . 

270 
next 

271 
from FH' show "F \<subseteq> H'" .. 

272 
qed 

23378  273 
show "\<forall>x \<in> H'. h' x \<le> p x" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

274 
using h'_def H'_def `x' \<notin> H` `x' \<in> E` `x' \<noteq> 0` E HE 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

275 
`seminorm E p` linearform and hp xi 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

276 
by (rule h'_norm_pres) 
13515  277 
qed 
278 
qed 

279 
ultimately show ?thesis .. 

9475  280 
qed 
27612  281 
then have "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp 
13515  282 
 {* So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp *} 
23378  283 
with gx show "H = E" by contradiction 
9035  284 
qed 
13515  285 

286 
from HE_eq and linearform have "linearform E h" 

287 
by (simp only:) 

288 
moreover have "\<forall>x \<in> F. h x = f x" 

289 
proof 

290 
fix x assume "x \<in> F" 

291 
with graphs have "f x = h x" .. 

292 
then show "h x = f x" .. 

293 
qed 

294 
moreover from HE_eq and hp have "\<forall>x \<in> E. h x \<le> p x" 

295 
by (simp only:) 

296 
ultimately show ?thesis by blast 

9475  297 
qed 
9374  298 

299 

300 
subsection {* Alternative formulation *} 

301 

10687  302 
text {* 
303 
The following alternative formulation of the HahnBanach 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29291
diff
changeset

304 
Theorem\label{absHahnBanach} uses the fact that for a real linear 
10687  305 
form @{text f} and a seminorm @{text p} the following inequations 
306 
are equivalent:\footnote{This was shown in lemma @{thm [source] 

307 
abs_ineq_iff} (see page \pageref{absineqiff}).} 

308 
\begin{center} 

309 
\begin{tabular}{lll} 

310 
@{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and & 

311 
@{text "\<forall>x \<in> H. h x \<le> p x"} \\ 

312 
\end{tabular} 

313 
\end{center} 

9374  314 
*} 
315 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29291
diff
changeset

316 
theorem abs_Hahn_Banach: 
27611  317 
assumes E: "vectorspace E" and FE: "subspace F E" 
318 
and lf: "linearform F f" and sn: "seminorm E p" 

13515  319 
assumes fp: "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x" 
320 
shows "\<exists>g. linearform E g 

321 
\<and> (\<forall>x \<in> F. g x = f x) 

10687  322 
\<and> (\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x)" 
9374  323 
proof  
29234  324 
interpret vectorspace E by fact 
325 
interpret subspace F E by fact 

326 
interpret linearform F f by fact 

327 
interpret seminorm E p by fact 

27612  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)" 
329 
using E FE sn lf 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29291
diff
changeset

330 
proof (rule Hahn_Banach) 
13515  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" 
27612  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 HahnBanach 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 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29291
diff
changeset

353 
theorem norm_Hahn_Banach: 
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" 

46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44190
diff
changeset

359 
and linearform: "linearform F f" and "continuous F f norm" 
13515  360 
shows "\<exists>g. linearform E g 
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44190
diff
changeset

361 
\<and> continuous E g norm 
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  
29234  365 
interpret normed_vectorspace E norm by fact 
366 
interpret normed_vectorspace_with_fn_norm E norm B fn_norm 

27611  367 
by (auto simp: B_def fn_norm_def) intro_locales 
29234  368 
interpret subspace F E by fact 
369 
interpret linearform F f by fact 

46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44190
diff
changeset

370 
interpret continuous F f norm by fact 
28823  371 
have E: "vectorspace E" by intro_locales 
372 
have F: "vectorspace F" by rule intro_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, 

46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44190
diff
changeset

378 
OF F_norm `continuous F f norm` , 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" 

27612  387 

13515  388 
txt {* @{text p} is positive definite: *} 
27612  389 
have "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero) 
390 
moreover from x have "0 \<le> \<parallel>x\<parallel>" .. 

14710  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" 

46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44190
diff
changeset

425 
with `continuous F f norm` and linearform 
13515  426 
show "\<bar>f x\<bar> \<le> p x" 
27612  427 
unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong 
27611  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 HahnBanach Theorem for real vector 

434 
spaces. So @{text f} can be extended in a normpreserving 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 
27612  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" 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29291
diff
changeset

441 
by (rule abs_Hahn_Banach [elim_format]) iprover 
9475  442 

13515  443 
txt {* We furthermore have to show that @{text g} is also continuous: *} 
444 

46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44190
diff
changeset

445 
have g_cont: "continuous E g norm" 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 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

486 
[OF normed_vectorspace_with_fn_norm.intro, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

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 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

490 
fix x assume x: "x \<in> F" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

491 
from a x have "g x = f x" .. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

492 
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

493 
also from g_cont 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

494 
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

495 
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

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

497 
qed 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

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

501 
using g_cont 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

502 
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

503 
show "continuous F f norm" by fact 
10687  504 
qed 
9374  505 
qed 
13547  506 
with linearformE a g_cont show ?thesis by blast 
9475  507 
qed 
9374  508 

9475  509 
end 