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

src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy

author | blanchet |

Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) | |

changeset 58306 | 117ba6cbe414 |

parent 49962 | a8cc904a6820 |

child 58744 | c434e37f290e |

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

renamed 'rep_datatype' to 'old_rep_datatype' (HOL)

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

2 Author: Gertrud Bauer, TU Munich

3 *)

5 header {* Extending non-maximal functions *}

7 theory Hahn_Banach_Ext_Lemmas

8 imports Function_Norm

9 begin

11 text {*

12 In this section the following context is presumed. Let @{text E} be

13 a real vector space with a seminorm @{text q} on @{text E}. @{text

14 F} is a subspace of @{text E} and @{text f} a linear function on

15 @{text F}. We consider a subspace @{text H} of @{text E} that is a

16 superspace of @{text F} and a linear form @{text h} on @{text

17 H}. @{text H} is a not equal to @{text E} and @{text "x\<^sub>0"} is

18 an element in @{text "E - H"}. @{text H} is extended to the direct

19 sum @{text "H' = H + lin x\<^sub>0"}, so for any @{text "x \<in> H'"}

20 the decomposition of @{text "x = y + a \<cdot> x"} with @{text "y \<in> H"} is

21 unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y +

22 a \<cdot> \<xi>"} for a certain @{text \<xi>}.

24 Subsequently we show some properties of this extension @{text h'} of

25 @{text h}.

27 \medskip This lemma will be used to show the existence of a linear

28 extension of @{text f} (see page \pageref{ex-xi-use}). It is a

29 consequence of the completeness of @{text \<real>}. To show

30 \begin{center}

31 \begin{tabular}{l}

32 @{text "\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y"}

33 \end{tabular}

34 \end{center}

35 \noindent it suffices to show that

36 \begin{center}

37 \begin{tabular}{l}

38 @{text "\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v"}

39 \end{tabular}

40 \end{center}

41 *}

43 lemma ex_xi:

44 assumes "vectorspace F"

45 assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"

46 shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"

47 proof -

48 interpret vectorspace F by fact

49 txt {* From the completeness of the reals follows:

50 The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is

51 non-empty and has an upper bound. *}

53 let ?S = "{a u | u. u \<in> F}"

54 have "\<exists>xi. lub ?S xi"

55 proof (rule real_complete)

56 have "a 0 \<in> ?S" by blast

57 then show "\<exists>X. X \<in> ?S" ..

58 have "\<forall>y \<in> ?S. y \<le> b 0"

59 proof

60 fix y assume y: "y \<in> ?S"

61 then obtain u where u: "u \<in> F" and y: "y = a u" by blast

62 from u and zero have "a u \<le> b 0" by (rule r)

63 with y show "y \<le> b 0" by (simp only:)

64 qed

65 then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" ..

66 qed

67 then obtain xi where xi: "lub ?S xi" ..

68 {

69 fix y assume "y \<in> F"

70 then have "a y \<in> ?S" by blast

71 with xi have "a y \<le> xi" by (rule lub.upper)

72 } moreover {

73 fix y assume y: "y \<in> F"

74 from xi have "xi \<le> b y"

75 proof (rule lub.least)

76 fix au assume "au \<in> ?S"

77 then obtain u where u: "u \<in> F" and au: "au = a u" by blast

78 from u y have "a u \<le> b y" by (rule r)

79 with au show "au \<le> b y" by (simp only:)

80 qed

81 } ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast

82 qed

84 text {*

85 \medskip The function @{text h'} is defined as a @{text "h' x = h y

86 + a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a linear extension of

87 @{text h} to @{text H'}.

88 *}

90 lemma h'_lf:

91 assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =

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

93 and H'_def: "H' \<equiv> H + lin x0"

94 and HE: "H \<unlhd> E"

95 assumes "linearform H h"

96 assumes x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"

97 assumes E: "vectorspace E"

98 shows "linearform H' h'"

99 proof -

100 interpret linearform H h by fact

101 interpret vectorspace E by fact

102 show ?thesis

103 proof

104 note E = `vectorspace E`

105 have H': "vectorspace H'"

106 proof (unfold H'_def)

107 from `x0 \<in> E`

108 have "lin x0 \<unlhd> E" ..

109 with HE show "vectorspace (H + lin x0)" using E ..

110 qed

111 {

112 fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"

113 show "h' (x1 + x2) = h' x1 + h' x2"

114 proof -

115 from H' x1 x2 have "x1 + x2 \<in> H'"

116 by (rule vectorspace.add_closed)

117 with x1 x2 obtain y y1 y2 a a1 a2 where

118 x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"

119 and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"

120 and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"

121 unfolding H'_def sum_def lin_def by blast

123 have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0

124 proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}

125 from HE y1 y2 show "y1 + y2 \<in> H"

126 by (rule subspace.add_closed)

127 from x0 and HE y y1 y2

128 have "x0 \<in> E" "y \<in> E" "y1 \<in> E" "y2 \<in> E" by auto

129 with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"

130 by (simp add: add_ac add_mult_distrib2)

131 also note x1x2

132 finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .

133 qed

135 from h'_def x1x2 E HE y x0

136 have "h' (x1 + x2) = h y + a * xi"

137 by (rule h'_definite)

138 also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"

139 by (simp only: ya)

140 also from y1 y2 have "h (y1 + y2) = h y1 + h y2"

141 by simp

142 also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"

143 by (simp add: distrib_right)

144 also from h'_def x1_rep E HE y1 x0

145 have "h y1 + a1 * xi = h' x1"

146 by (rule h'_definite [symmetric])

147 also from h'_def x2_rep E HE y2 x0

148 have "h y2 + a2 * xi = h' x2"

149 by (rule h'_definite [symmetric])

150 finally show ?thesis .

151 qed

152 next

153 fix x1 c assume x1: "x1 \<in> H'"

154 show "h' (c \<cdot> x1) = c * (h' x1)"

155 proof -

156 from H' x1 have ax1: "c \<cdot> x1 \<in> H'"

157 by (rule vectorspace.mult_closed)

158 with x1 obtain y a y1 a1 where

159 cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"

160 and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"

161 unfolding H'_def sum_def lin_def by blast

163 have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0

164 proof (rule decomp_H')

165 from HE y1 show "c \<cdot> y1 \<in> H"

166 by (rule subspace.mult_closed)

167 from x0 and HE y y1

168 have "x0 \<in> E" "y \<in> E" "y1 \<in> E" by auto

169 with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"

170 by (simp add: mult_assoc add_mult_distrib1)

171 also note cx1_rep

172 finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .

173 qed

175 from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"

176 by (rule h'_definite)

177 also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"

178 by (simp only: ya)

179 also from y1 have "h (c \<cdot> y1) = c * h y1"

180 by simp

181 also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"

182 by (simp only: distrib_left)

183 also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"

184 by (rule h'_definite [symmetric])

185 finally show ?thesis .

186 qed

187 }

188 qed

189 qed

191 text {* \medskip The linear extension @{text h'} of @{text h}

192 is bounded by the seminorm @{text p}. *}

194 lemma h'_norm_pres:

195 assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =

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

197 and H'_def: "H' \<equiv> H + lin x0"

198 and x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"

199 assumes E: "vectorspace E" and HE: "subspace H E"

200 and "seminorm E p" and "linearform H h"

201 assumes a: "\<forall>y \<in> H. h y \<le> p y"

202 and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"

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

204 proof -

205 interpret vectorspace E by fact

206 interpret subspace H E by fact

207 interpret seminorm E p by fact

208 interpret linearform H h by fact

209 show ?thesis

210 proof

211 fix x assume x': "x \<in> H'"

212 show "h' x \<le> p x"

213 proof -

214 from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"

215 and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto

216 from x' obtain y a where

217 x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"

218 unfolding H'_def sum_def lin_def by blast

219 from y have y': "y \<in> E" ..

220 from y have ay: "inverse a \<cdot> y \<in> H" by simp

222 from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"

223 by (rule h'_definite)

224 also have "\<dots> \<le> p (y + a \<cdot> x0)"

225 proof (rule linorder_cases)

226 assume z: "a = 0"

227 then have "h y + a * xi = h y" by simp

228 also from a y have "\<dots> \<le> p y" ..

229 also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp

230 finally show ?thesis .

231 next

232 txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}

233 with @{text ya} taken as @{text "y / a"}: *}

234 assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp

235 from a1 ay

236 have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..

237 with lz have "a * xi \<le>

238 a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"

239 by (simp add: mult_left_mono_neg order_less_imp_le)

241 also have "\<dots> =

242 - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"

243 by (simp add: right_diff_distrib)

244 also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =

245 p (a \<cdot> (inverse a \<cdot> y + x0))"

246 by (simp add: abs_homogenous)

247 also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"

248 by (simp add: add_mult_distrib1 mult_assoc [symmetric])

249 also from nz y have "a * (h (inverse a \<cdot> y)) = h y"

250 by simp

251 finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .

252 then show ?thesis by simp

253 next

254 txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}

255 with @{text ya} taken as @{text "y / a"}: *}

256 assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp

257 from a2 ay

258 have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..

259 with gz have "a * xi \<le>

260 a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"

261 by simp

262 also have "\<dots> = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"

263 by (simp add: right_diff_distrib)

264 also from gz x0 y'

265 have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"

266 by (simp add: abs_homogenous)

267 also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"

268 by (simp add: add_mult_distrib1 mult_assoc [symmetric])

269 also from nz y have "a * h (inverse a \<cdot> y) = h y"

270 by simp

271 finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .

272 then show ?thesis by simp

273 qed

274 also from x_rep have "\<dots> = p x" by (simp only:)

275 finally show ?thesis .

276 qed

277 qed

278 qed

280 end