summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy

author | hoelzl |

Thu Sep 02 10:14:32 2010 +0200 (2010-09-02) | |

changeset 39072 | 1030b1a166ef |

parent 32960 | 69916a850301 |

child 44887 | 7ca82df6e951 |

permissions | -rw-r--r-- |

Add lessThan_Suc_eq_insert_0

1 (* Title: HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy

2 Author: Gertrud Bauer, TU Munich

3 *)

5 header {* The supremum w.r.t.~the function order *}

7 theory Hahn_Banach_Sup_Lemmas

8 imports Function_Norm Zorn_Lemma

9 begin

11 text {*

12 This section contains some lemmas that will be used in the proof of

13 the Hahn-Banach Theorem. In this section the following context is

14 presumed. Let @{text E} be a real vector space with a seminorm

15 @{text p} on @{text E}. @{text F} is a subspace of @{text E} and

16 @{text f} a linear form on @{text F}. We consider a chain @{text c}

17 of norm-preserving extensions of @{text f}, such that @{text "\<Union>c =

18 graph H h"}. We will show some properties about the limit function

19 @{text h}, i.e.\ the supremum of the chain @{text c}.

21 \medskip Let @{text c} be a chain of norm-preserving extensions of

22 the function @{text f} and let @{text "graph H h"} be the supremum

23 of @{text c}. Every element in @{text H} is member of one of the

24 elements of the chain.

25 *}

26 lemmas [dest?] = chainD

27 lemmas chainE2 [elim?] = chainD2 [elim_format, standard]

29 lemma some_H'h't:

30 assumes M: "M = norm_pres_extensions E p F f"

31 and cM: "c \<in> chain M"

32 and u: "graph H h = \<Union>c"

33 and x: "x \<in> H"

34 shows "\<exists>H' h'. graph H' h' \<in> c

35 \<and> (x, h x) \<in> graph H' h'

36 \<and> linearform H' h' \<and> H' \<unlhd> E

37 \<and> F \<unlhd> H' \<and> graph F f \<subseteq> graph H' h'

38 \<and> (\<forall>x \<in> H'. h' x \<le> p x)"

39 proof -

40 from x have "(x, h x) \<in> graph H h" ..

41 also from u have "\<dots> = \<Union>c" .

42 finally obtain g where gc: "g \<in> c" and gh: "(x, h x) \<in> g" by blast

44 from cM have "c \<subseteq> M" ..

45 with gc have "g \<in> M" ..

46 also from M have "\<dots> = norm_pres_extensions E p F f" .

47 finally obtain H' and h' where g: "g = graph H' h'"

48 and * : "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'"

49 "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" ..

51 from gc and g have "graph H' h' \<in> c" by (simp only:)

52 moreover from gh and g have "(x, h x) \<in> graph H' h'" by (simp only:)

53 ultimately show ?thesis using * by blast

54 qed

56 text {*

57 \medskip Let @{text c} be a chain of norm-preserving extensions of

58 the function @{text f} and let @{text "graph H h"} be the supremum

59 of @{text c}. Every element in the domain @{text H} of the supremum

60 function is member of the domain @{text H'} of some function @{text

61 h'}, such that @{text h} extends @{text h'}.

62 *}

64 lemma some_H'h':

65 assumes M: "M = norm_pres_extensions E p F f"

66 and cM: "c \<in> chain M"

67 and u: "graph H h = \<Union>c"

68 and x: "x \<in> H"

69 shows "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h

70 \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'

71 \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"

72 proof -

73 from M cM u x obtain H' h' where

74 x_hx: "(x, h x) \<in> graph H' h'"

75 and c: "graph H' h' \<in> c"

76 and * : "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'"

77 "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"

78 by (rule some_H'h't [elim_format]) blast

79 from x_hx have "x \<in> H'" ..

80 moreover from cM u c have "graph H' h' \<subseteq> graph H h"

81 by (simp only: chain_ball_Union_upper)

82 ultimately show ?thesis using * by blast

83 qed

85 text {*

86 \medskip Any two elements @{text x} and @{text y} in the domain

87 @{text H} of the supremum function @{text h} are both in the domain

88 @{text H'} of some function @{text h'}, such that @{text h} extends

89 @{text h'}.

90 *}

92 lemma some_H'h'2:

93 assumes M: "M = norm_pres_extensions E p F f"

94 and cM: "c \<in> chain M"

95 and u: "graph H h = \<Union>c"

96 and x: "x \<in> H"

97 and y: "y \<in> H"

98 shows "\<exists>H' h'. x \<in> H' \<and> y \<in> H'

99 \<and> graph H' h' \<subseteq> graph H h

100 \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'

101 \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"

102 proof -

103 txt {* @{text y} is in the domain @{text H''} of some function @{text h''},

104 such that @{text h} extends @{text h''}. *}

106 from M cM u and y obtain H' h' where

107 y_hy: "(y, h y) \<in> graph H' h'"

108 and c': "graph H' h' \<in> c"

109 and * :

110 "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'"

111 "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"

112 by (rule some_H'h't [elim_format]) blast

114 txt {* @{text x} is in the domain @{text H'} of some function @{text h'},

115 such that @{text h} extends @{text h'}. *}

117 from M cM u and x obtain H'' h'' where

118 x_hx: "(x, h x) \<in> graph H'' h''"

119 and c'': "graph H'' h'' \<in> c"

120 and ** :

121 "linearform H'' h''" "H'' \<unlhd> E" "F \<unlhd> H''"

122 "graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x"

123 by (rule some_H'h't [elim_format]) blast

125 txt {* Since both @{text h'} and @{text h''} are elements of the chain,

126 @{text h''} is an extension of @{text h'} or vice versa. Thus both

127 @{text x} and @{text y} are contained in the greater

128 one. \label{cases1}*}

130 from cM c'' c' have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"

131 (is "?case1 \<or> ?case2") ..

132 then show ?thesis

133 proof

134 assume ?case1

135 have "(x, h x) \<in> graph H'' h''" by fact

136 also have "\<dots> \<subseteq> graph H' h'" by fact

137 finally have xh:"(x, h x) \<in> graph H' h'" .

138 then have "x \<in> H'" ..

139 moreover from y_hy have "y \<in> H'" ..

140 moreover from cM u and c' have "graph H' h' \<subseteq> graph H h"

141 by (simp only: chain_ball_Union_upper)

142 ultimately show ?thesis using * by blast

143 next

144 assume ?case2

145 from x_hx have "x \<in> H''" ..

146 moreover {

147 have "(y, h y) \<in> graph H' h'" by (rule y_hy)

148 also have "\<dots> \<subseteq> graph H'' h''" by fact

149 finally have "(y, h y) \<in> graph H'' h''" .

150 } then have "y \<in> H''" ..

151 moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h"

152 by (simp only: chain_ball_Union_upper)

153 ultimately show ?thesis using ** by blast

154 qed

155 qed

157 text {*

158 \medskip The relation induced by the graph of the supremum of a

159 chain @{text c} is definite, i.~e.~t is the graph of a function.

160 *}

162 lemma sup_definite:

163 assumes M_def: "M \<equiv> norm_pres_extensions E p F f"

164 and cM: "c \<in> chain M"

165 and xy: "(x, y) \<in> \<Union>c"

166 and xz: "(x, z) \<in> \<Union>c"

167 shows "z = y"

168 proof -

169 from cM have c: "c \<subseteq> M" ..

170 from xy obtain G1 where xy': "(x, y) \<in> G1" and G1: "G1 \<in> c" ..

171 from xz obtain G2 where xz': "(x, z) \<in> G2" and G2: "G2 \<in> c" ..

173 from G1 c have "G1 \<in> M" ..

174 then obtain H1 h1 where G1_rep: "G1 = graph H1 h1"

175 unfolding M_def by blast

177 from G2 c have "G2 \<in> M" ..

178 then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"

179 unfolding M_def by blast

181 txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}

182 or vice versa, since both @{text "G\<^sub>1"} and @{text

183 "G\<^sub>2"} are members of @{text c}. \label{cases2}*}

185 from cM G1 G2 have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") ..

186 then show ?thesis

187 proof

188 assume ?case1

189 with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast

190 then have "y = h2 x" ..

191 also

192 from xz' G2_rep have "(x, z) \<in> graph H2 h2" by (simp only:)

193 then have "z = h2 x" ..

194 finally show ?thesis .

195 next

196 assume ?case2

197 with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast

198 then have "z = h1 x" ..

199 also

200 from xy' G1_rep have "(x, y) \<in> graph H1 h1" by (simp only:)

201 then have "y = h1 x" ..

202 finally show ?thesis ..

203 qed

204 qed

206 text {*

207 \medskip The limit function @{text h} is linear. Every element

208 @{text x} in the domain of @{text h} is in the domain of a function

209 @{text h'} in the chain of norm preserving extensions. Furthermore,

210 @{text h} is an extension of @{text h'} so the function values of

211 @{text x} are identical for @{text h'} and @{text h}. Finally, the

212 function @{text h'} is linear by construction of @{text M}.

213 *}

215 lemma sup_lf:

216 assumes M: "M = norm_pres_extensions E p F f"

217 and cM: "c \<in> chain M"

218 and u: "graph H h = \<Union>c"

219 shows "linearform H h"

220 proof

221 fix x y assume x: "x \<in> H" and y: "y \<in> H"

222 with M cM u obtain H' h' where

223 x': "x \<in> H'" and y': "y \<in> H'"

224 and b: "graph H' h' \<subseteq> graph H h"

225 and linearform: "linearform H' h'"

226 and subspace: "H' \<unlhd> E"

227 by (rule some_H'h'2 [elim_format]) blast

229 show "h (x + y) = h x + h y"

230 proof -

231 from linearform x' y' have "h' (x + y) = h' x + h' y"

232 by (rule linearform.add)

233 also from b x' have "h' x = h x" ..

234 also from b y' have "h' y = h y" ..

235 also from subspace x' y' have "x + y \<in> H'"

236 by (rule subspace.add_closed)

237 with b have "h' (x + y) = h (x + y)" ..

238 finally show ?thesis .

239 qed

240 next

241 fix x a assume x: "x \<in> H"

242 with M cM u obtain H' h' where

243 x': "x \<in> H'"

244 and b: "graph H' h' \<subseteq> graph H h"

245 and linearform: "linearform H' h'"

246 and subspace: "H' \<unlhd> E"

247 by (rule some_H'h' [elim_format]) blast

249 show "h (a \<cdot> x) = a * h x"

250 proof -

251 from linearform x' have "h' (a \<cdot> x) = a * h' x"

252 by (rule linearform.mult)

253 also from b x' have "h' x = h x" ..

254 also from subspace x' have "a \<cdot> x \<in> H'"

255 by (rule subspace.mult_closed)

256 with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..

257 finally show ?thesis .

258 qed

259 qed

261 text {*

262 \medskip The limit of a non-empty chain of norm preserving

263 extensions of @{text f} is an extension of @{text f}, since every

264 element of the chain is an extension of @{text f} and the supremum

265 is an extension for every element of the chain.

266 *}

268 lemma sup_ext:

269 assumes graph: "graph H h = \<Union>c"

270 and M: "M = norm_pres_extensions E p F f"

271 and cM: "c \<in> chain M"

272 and ex: "\<exists>x. x \<in> c"

273 shows "graph F f \<subseteq> graph H h"

274 proof -

275 from ex obtain x where xc: "x \<in> c" ..

276 from cM have "c \<subseteq> M" ..

277 with xc have "x \<in> M" ..

278 with M have "x \<in> norm_pres_extensions E p F f"

279 by (simp only:)

280 then obtain G g where "x = graph G g" and "graph F f \<subseteq> graph G g" ..

281 then have "graph F f \<subseteq> x" by (simp only:)

282 also from xc have "\<dots> \<subseteq> \<Union>c" by blast

283 also from graph have "\<dots> = graph H h" ..

284 finally show ?thesis .

285 qed

287 text {*

288 \medskip The domain @{text H} of the limit function is a superspace

289 of @{text F}, since @{text F} is a subset of @{text H}. The

290 existence of the @{text 0} element in @{text F} and the closure

291 properties follow from the fact that @{text F} is a vector space.

292 *}

294 lemma sup_supF:

295 assumes graph: "graph H h = \<Union>c"

296 and M: "M = norm_pres_extensions E p F f"

297 and cM: "c \<in> chain M"

298 and ex: "\<exists>x. x \<in> c"

299 and FE: "F \<unlhd> E"

300 shows "F \<unlhd> H"

301 proof

302 from FE show "F \<noteq> {}" by (rule subspace.non_empty)

303 from graph M cM ex have "graph F f \<subseteq> graph H h" by (rule sup_ext)

304 then show "F \<subseteq> H" ..

305 fix x y assume "x \<in> F" and "y \<in> F"

306 with FE show "x + y \<in> F" by (rule subspace.add_closed)

307 next

308 fix x a assume "x \<in> F"

309 with FE show "a \<cdot> x \<in> F" by (rule subspace.mult_closed)

310 qed

312 text {*

313 \medskip The domain @{text H} of the limit function is a subspace of

314 @{text E}.

315 *}

317 lemma sup_subE:

318 assumes graph: "graph H h = \<Union>c"

319 and M: "M = norm_pres_extensions E p F f"

320 and cM: "c \<in> chain M"

321 and ex: "\<exists>x. x \<in> c"

322 and FE: "F \<unlhd> E"

323 and E: "vectorspace E"

324 shows "H \<unlhd> E"

325 proof

326 show "H \<noteq> {}"

327 proof -

328 from FE E have "0 \<in> F" by (rule subspace.zero)

329 also from graph M cM ex FE have "F \<unlhd> H" by (rule sup_supF)

330 then have "F \<subseteq> H" ..

331 finally show ?thesis by blast

332 qed

333 show "H \<subseteq> E"

334 proof

335 fix x assume "x \<in> H"

336 with M cM graph

337 obtain H' h' where x: "x \<in> H'" and H'E: "H' \<unlhd> E"

338 by (rule some_H'h' [elim_format]) blast

339 from H'E have "H' \<subseteq> E" ..

340 with x show "x \<in> E" ..

341 qed

342 fix x y assume x: "x \<in> H" and y: "y \<in> H"

343 show "x + y \<in> H"

344 proof -

345 from M cM graph x y obtain H' h' where

346 x': "x \<in> H'" and y': "y \<in> H'" and H'E: "H' \<unlhd> E"

347 and graphs: "graph H' h' \<subseteq> graph H h"

348 by (rule some_H'h'2 [elim_format]) blast

349 from H'E x' y' have "x + y \<in> H'"

350 by (rule subspace.add_closed)

351 also from graphs have "H' \<subseteq> H" ..

352 finally show ?thesis .

353 qed

354 next

355 fix x a assume x: "x \<in> H"

356 show "a \<cdot> x \<in> H"

357 proof -

358 from M cM graph x

359 obtain H' h' where x': "x \<in> H'" and H'E: "H' \<unlhd> E"

360 and graphs: "graph H' h' \<subseteq> graph H h"

361 by (rule some_H'h' [elim_format]) blast

362 from H'E x' have "a \<cdot> x \<in> H'" by (rule subspace.mult_closed)

363 also from graphs have "H' \<subseteq> H" ..

364 finally show ?thesis .

365 qed

366 qed

368 text {*

369 \medskip The limit function is bounded by the norm @{text p} as

370 well, since all elements in the chain are bounded by @{text p}.

371 *}

373 lemma sup_norm_pres:

374 assumes graph: "graph H h = \<Union>c"

375 and M: "M = norm_pres_extensions E p F f"

376 and cM: "c \<in> chain M"

377 shows "\<forall>x \<in> H. h x \<le> p x"

378 proof

379 fix x assume "x \<in> H"

380 with M cM graph obtain H' h' where x': "x \<in> H'"

381 and graphs: "graph H' h' \<subseteq> graph H h"

382 and a: "\<forall>x \<in> H'. h' x \<le> p x"

383 by (rule some_H'h' [elim_format]) blast

384 from graphs x' have [symmetric]: "h' x = h x" ..

385 also from a x' have "h' x \<le> p x " ..

386 finally show "h x \<le> p x" .

387 qed

389 text {*

390 \medskip The following lemma is a property of linear forms on real

391 vector spaces. It will be used for the lemma @{text abs_Hahn_Banach}

392 (see page \pageref{abs-Hahn_Banach}). \label{abs-ineq-iff} For real

393 vector spaces the following inequations are equivalent:

394 \begin{center}

395 \begin{tabular}{lll}

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

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

398 \end{tabular}

399 \end{center}

400 *}

402 lemma abs_ineq_iff:

403 assumes "subspace H E" and "vectorspace E" and "seminorm E p"

404 and "linearform H h"

405 shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")

406 proof

407 interpret subspace H E by fact

408 interpret vectorspace E by fact

409 interpret seminorm E p by fact

410 interpret linearform H h by fact

411 have H: "vectorspace H" using `vectorspace E` ..

412 {

413 assume l: ?L

414 show ?R

415 proof

416 fix x assume x: "x \<in> H"

417 have "h x \<le> \<bar>h x\<bar>" by arith

418 also from l x have "\<dots> \<le> p x" ..

419 finally show "h x \<le> p x" .

420 qed

421 next

422 assume r: ?R

423 show ?L

424 proof

425 fix x assume x: "x \<in> H"

426 show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"

427 by arith

428 from `linearform H h` and H x

429 have "- h x = h (- x)" by (rule linearform.neg [symmetric])

430 also

431 from H x have "- x \<in> H" by (rule vectorspace.neg_closed)

432 with r have "h (- x) \<le> p (- x)" ..

433 also have "\<dots> = p x"

434 using `seminorm E p` `vectorspace E`

435 proof (rule seminorm.minus)

436 from x show "x \<in> E" ..

437 qed

438 finally have "- h x \<le> p x" .

439 then show "- p x \<le> h x" by simp

440 from r x show "h x \<le> p x" ..

441 qed

442 }

443 qed

445 end