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

src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy

author | wenzelm |

Mon Apr 25 16:09:26 2016 +0200 (2016-04-25) | |

changeset 63040 | eb4ddd18d635 |

parent 61879 | e4f9d8f094fe |

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

eliminated old 'def';

tuned comments;

tuned comments;

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

2 Author: Gertrud Bauer, TU Munich

3 *)

5 section \<open>The supremum wrt.\ the function order\<close>

7 theory Hahn_Banach_Sup_Lemmas

8 imports Function_Norm Zorn_Lemma

9 begin

11 text \<open>

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

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

14 \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of

15 \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of norm-preserving

16 extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will show some properties

17 about the limit function \<open>h\<close>, i.e.\ the supremum of the chain \<open>c\<close>.

19 \<^medskip>

20 Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let

21 \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of one of

22 the elements of the chain.

23 \<close>

25 lemmas [dest?] = chainsD

26 lemmas chainsE2 [elim?] = chainsD2 [elim_format]

28 lemma some_H'h't:

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

30 and cM: "c \<in> chains M"

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

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

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

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

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

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

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

38 proof -

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

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

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

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

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

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

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

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

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

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

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

52 ultimately show ?thesis using * by blast

53 qed

55 text \<open>

56 \<^medskip>

57 Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let

58 \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of the

59 supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, such

60 that \<open>h\<close> extends \<open>h'\<close>.

61 \<close>

63 lemma some_H'h':

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

65 and cM: "c \<in> chains M"

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

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

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

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

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

71 proof -

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

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

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

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

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

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

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

79 moreover from cM u c have "graph H' h' \<subseteq> graph H h" by blast

80 ultimately show ?thesis using * by blast

81 qed

83 text \<open>

84 \<^medskip>

85 Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function \<open>h\<close>

86 are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends

87 \<open>h'\<close>.

88 \<close>

90 lemma some_H'h'2:

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

92 and cM: "c \<in> chains M"

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

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

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

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

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

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

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

100 proof -

101 txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>, such that \<open>h\<close>

102 extends \<open>h''\<close>.\<close>

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

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

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

107 and * :

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

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

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

112 txt \<open>\<open>x\<close> is in the domain \<open>H'\<close> of some function \<open>h'\<close>,

113 such that \<open>h\<close> extends \<open>h'\<close>.\<close>

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

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

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

118 and ** :

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

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

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

123 txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain, \<open>h''\<close> is an

124 extension of \<open>h'\<close> or vice versa. Thus both \<open>x\<close> and \<open>y\<close> are contained in

125 the greater one. \label{cases1}\<close>

127 from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''"

128 by (blast dest: chainsD)

129 then show ?thesis

130 proof cases

131 case 1

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

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

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

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

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

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

138 ultimately show ?thesis using * by blast

139 next

140 case 2

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

142 moreover have "y \<in> H''"

143 proof -

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

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

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

147 then show ?thesis ..

148 qed

149 moreover from u c'' have "graph H'' h'' \<subseteq> graph H h" by blast

150 ultimately show ?thesis using ** by blast

151 qed

152 qed

154 text \<open>

155 \<^medskip>

156 The relation induced by the graph of the supremum of a chain \<open>c\<close> is

157 definite, i.e.\ it is the graph of a function.

158 \<close>

160 lemma sup_definite:

161 assumes M_def: "M = norm_pres_extensions E p F f"

162 and cM: "c \<in> chains M"

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

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

165 shows "z = y"

166 proof -

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

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

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

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

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

173 unfolding M_def by blast

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

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

177 unfolding M_def by blast

179 txt \<open>\<open>G\<^sub>1\<close> is contained in \<open>G\<^sub>2\<close> or vice versa, since both \<open>G\<^sub>1\<close> and \<open>G\<^sub>2\<close>

180 are members of \<open>c\<close>. \label{cases2}\<close>

182 from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1"

183 by (blast dest: chainsD)

184 then show ?thesis

185 proof cases

186 case 1

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

188 then have "y = h2 x" ..

189 also

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

191 then have "z = h2 x" ..

192 finally show ?thesis .

193 next

194 case 2

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

196 then have "z = h1 x" ..

197 also

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

199 then have "y = h1 x" ..

200 finally show ?thesis ..

201 qed

202 qed

204 text \<open>

205 \<^medskip>

206 The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close> is

207 in the domain of a function \<open>h'\<close> in the chain of norm preserving extensions.

208 Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function values of \<open>x\<close> are

209 identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close> is linear by

210 construction of \<open>M\<close>.

211 \<close>

213 lemma sup_lf:

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

215 and cM: "c \<in> chains M"

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

217 shows "linearform H h"

218 proof

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

220 with M cM u obtain H' h' where

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

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

223 and linearform: "linearform H' h'"

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

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

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

228 proof -

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

230 by (rule linearform.add)

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

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

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

234 by (rule subspace.add_closed)

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

236 finally show ?thesis .

237 qed

238 next

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

240 with M cM u obtain H' h' where

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

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

243 and linearform: "linearform H' h'"

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

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

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

248 proof -

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

250 by (rule linearform.mult)

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

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

253 by (rule subspace.mult_closed)

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

255 finally show ?thesis .

256 qed

257 qed

259 text \<open>

260 \<^medskip>

261 The limit of a non-empty chain of norm preserving extensions of \<open>f\<close> is an

262 extension of \<open>f\<close>, since every element of the chain is an extension of \<open>f\<close>

263 and the supremum is an extension for every element of the chain.

264 \<close>

266 lemma sup_ext:

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

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

269 and cM: "c \<in> chains M"

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

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

272 proof -

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

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

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

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

277 by (simp only:)

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

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

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

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

282 finally show ?thesis .

283 qed

285 text \<open>

286 \<^medskip>

287 The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is a

288 subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure

289 properties follow from the fact that \<open>F\<close> is a vector space.

290 \<close>

292 lemma sup_supF:

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

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

295 and cM: "c \<in> chains M"

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

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

298 shows "F \<unlhd> H"

299 proof

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

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

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

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

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

305 next

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

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

308 qed

310 text \<open>

311 \<^medskip>

312 The domain \<open>H\<close> of the limit function is a subspace of \<open>E\<close>.

313 \<close>

315 lemma sup_subE:

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

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

318 and cM: "c \<in> chains M"

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

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

321 and E: "vectorspace E"

322 shows "H \<unlhd> E"

323 proof

324 show "H \<noteq> {}"

325 proof -

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

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

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

329 finally show ?thesis by blast

330 qed

331 show "H \<subseteq> E"

332 proof

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

334 with M cM graph

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

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

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

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

339 qed

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

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

342 proof -

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

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

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

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

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

348 by (rule subspace.add_closed)

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

350 finally show ?thesis .

351 qed

352 next

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

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

355 proof -

356 from M cM graph x

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

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

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

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

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

362 finally show ?thesis .

363 qed

364 qed

366 text \<open>

367 \<^medskip>

368 The limit function is bounded by the norm \<open>p\<close> as well, since all elements in

369 the chain are bounded by \<open>p\<close>.

370 \<close>

372 lemma sup_norm_pres:

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

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

375 and cM: "c \<in> chains M"

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

377 proof

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

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

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

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

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

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

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

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

386 qed

388 text \<open>

389 \<^medskip>

390 The following lemma is a property of linear forms on real vector spaces. It

391 will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page

392 \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces the

393 following inequality are equivalent:

394 \begin{center}

395 \begin{tabular}{lll}

396 \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &

397 \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\

398 \end{tabular}

399 \end{center}

400 \<close>

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 \<open>vectorspace E\<close> ..

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 "\<bar>b\<bar> \<le> a" when "- a \<le> b" "b \<le> a" for a b :: real

427 using that by arith

428 from \<open>linearform H h\<close> 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 \<open>seminorm E p\<close> \<open>vectorspace E\<close>

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