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

src/HOL/Real/HahnBanach/FunctionNorm.thy

author | wenzelm |

Sun Jul 23 12:01:05 2000 +0200 (2000-07-23) | |

changeset 9408 | d3d56e1d2ec1 |

parent 9394 | 1ff8a6234c6a |

child 9503 | 3324cbbecef8 |

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

classical atts now intro! / intro / intro?;

1 (* Title: HOL/Real/HahnBanach/FunctionNorm.thy

2 ID: $Id$

3 Author: Gertrud Bauer, TU Munich

4 *)

6 header {* The norm of a function *}

8 theory FunctionNorm = NormedSpace + FunctionOrder:

10 subsection {* Continuous linear forms*}

12 text{* A linear form $f$ on a normed vector space $(V, \norm{\cdot})$

13 is \emph{continuous}, iff it is bounded, i.~e.

14 \[\Ex {c\in R}{\All {x\in V} {|f\ap x| \leq c \cdot \norm x}}\]

15 In our application no other functions than linear forms are considered,

16 so we can define continuous linear forms as bounded linear forms:

17 *}

19 constdefs

20 is_continuous ::

21 "['a::{plus, minus, zero} set, 'a => real, 'a => real] => bool"

22 "is_continuous V norm f ==

23 is_linearform V f \\<and> (\\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x)"

25 lemma continuousI [intro]:

26 "[| is_linearform V f; !! x. x \\<in> V ==> |f x| <= c * norm x |]

27 ==> is_continuous V norm f"

28 proof (unfold is_continuous_def, intro exI conjI ballI)

29 assume r: "!! x. x \\<in> V ==> |f x| <= c * norm x"

30 fix x assume "x \\<in> V" show "|f x| <= c * norm x" by (rule r)

31 qed

33 lemma continuous_linearform [intro?]:

34 "is_continuous V norm f ==> is_linearform V f"

35 by (unfold is_continuous_def) force

37 lemma continuous_bounded [intro?]:

38 "is_continuous V norm f

39 ==> \\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"

40 by (unfold is_continuous_def) force

42 subsection{* The norm of a linear form *}

45 text{* The least real number $c$ for which holds

46 \[\All {x\in V}{|f\ap x| \leq c \cdot \norm x}\]

47 is called the \emph{norm} of $f$.

49 For non-trivial vector spaces $V \neq \{\zero\}$ the norm can be defined as

50 \[\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x} \]

52 For the case $V = \{\zero\}$ the supremum would be taken from an

53 empty set. Since $\bbbR$ is unbounded, there would be no supremum. To

54 avoid this situation it must be guaranteed that there is an element in

55 this set. This element must be ${} \ge 0$ so that

56 $\idt{function{\dsh}norm}$ has the norm properties. Furthermore it

57 does not have to change the norm in all other cases, so it must be

58 $0$, as all other elements of are ${} \ge 0$.

60 Thus we define the set $B$ the supremum is taken from as

61 \[

62 \{ 0 \} \Union \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}

63 \]

64 *}

66 constdefs

67 B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set"

68 "B V norm f ==

69 {#0} \\<union> {|f x| * rinv (norm x) | x. x \\<noteq> 0 \\<and> x \\<in> V}"

71 text{* $n$ is the function norm of $f$, iff

72 $n$ is the supremum of $B$.

73 *}

75 constdefs

76 is_function_norm ::

77 " ['a::{minus,plus,zero} => real, 'a set, 'a => real] => real => bool"

78 "is_function_norm f V norm fn == is_Sup UNIV (B V norm f) fn"

80 text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$,

81 if the supremum exists. Otherwise it is undefined. *}

83 constdefs

84 function_norm :: " ['a::{minus,plus,zero} => real, 'a set, 'a => real] => real"

85 "function_norm f V norm == Sup UNIV (B V norm f)"

87 syntax

88 function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\\<parallel>_\\<parallel>_,_")

90 lemma B_not_empty: "#0 \\<in> B V norm f"

91 by (unfold B_def, force)

93 text {* The following lemma states that every continuous linear form

94 on a normed space $(V, \norm{\cdot})$ has a function norm. *}

96 lemma ex_fnorm [intro?]:

97 "[| is_normed_vectorspace V norm; is_continuous V norm f|]

98 ==> is_function_norm f V norm \\<parallel>f\\<parallel>V,norm"

99 proof (unfold function_norm_def is_function_norm_def

100 is_continuous_def Sup_def, elim conjE, rule selectI2EX)

101 assume "is_normed_vectorspace V norm"

102 assume "is_linearform V f"

103 and e: "\\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"

105 txt {* The existence of the supremum is shown using the

106 completeness of the reals. Completeness means, that

107 every non-empty bounded set of reals has a

108 supremum. *}

109 show "\\<exists>a. is_Sup UNIV (B V norm f) a"

110 proof (unfold is_Sup_def, rule reals_complete)

112 txt {* First we have to show that $B$ is non-empty: *}

114 show "\\<exists>X. X \\<in> B V norm f"

115 proof (intro exI)

116 show "#0 \\<in> (B V norm f)" by (unfold B_def, force)

117 qed

119 txt {* Then we have to show that $B$ is bounded: *}

121 from e show "\\<exists>Y. isUb UNIV (B V norm f) Y"

122 proof

124 txt {* We know that $f$ is bounded by some value $c$. *}

126 fix c assume a: "\\<forall>x \\<in> V. |f x| <= c * norm x"

127 def b == "max c #0"

129 show "?thesis"

130 proof (intro exI isUbI setleI ballI, unfold B_def,

131 elim UnE CollectE exE conjE singletonE)

133 txt{* To proof the thesis, we have to show that there is

134 some constant $b$, such that $y \leq b$ for all $y\in B$.

135 Due to the definition of $B$ there are two cases for

136 $y\in B$. If $y = 0$ then $y \leq \idt{max}\ap c\ap 0$: *}

138 fix y assume "y = (#0::real)"

139 show "y <= b" by (simp! add: le_maxI2)

141 txt{* The second case is

142 $y = {|f\ap x|}/{\norm x}$ for some

143 $x\in V$ with $x \neq \zero$. *}

145 next

146 fix x y

147 assume "x \\<in> V" "x \\<noteq> 0" (***

149 have ge: "#0 <= rinv (norm x)";

150 by (rule real_less_imp_le, rule real_rinv_gt_zero,

151 rule normed_vs_norm_gt_zero); ( ***

152 proof (rule real_less_imp_le);

153 show "#0 < rinv (norm x)";

154 proof (rule real_rinv_gt_zero);

155 show "#0 < norm x"; ..;

156 qed;

157 qed; *** )

158 have nz: "norm x \\<noteq> #0"

159 by (rule not_sym, rule lt_imp_not_eq,

160 rule normed_vs_norm_gt_zero) (***

161 proof (rule not_sym);

162 show "#0 \\<noteq> norm x";

163 proof (rule lt_imp_not_eq);

164 show "#0 < norm x"; ..;

165 qed;

166 qed; ***)***)

168 txt {* The thesis follows by a short calculation using the

169 fact that $f$ is bounded. *}

171 assume "y = |f x| * rinv (norm x)"

172 also have "... <= c * norm x * rinv (norm x)"

173 proof (rule real_mult_le_le_mono2)

174 show "#0 <= rinv (norm x)"

175 by (rule real_less_imp_le, rule real_rinv_gt_zero1,

176 rule normed_vs_norm_gt_zero)

177 from a show "|f x| <= c * norm x" ..

178 qed

179 also have "... = c * (norm x * rinv (norm x))"

180 by (rule real_mult_assoc)

181 also have "(norm x * rinv (norm x)) = (#1::real)"

182 proof (rule real_mult_inv_right1)

183 show nz: "norm x \\<noteq> #0"

184 by (rule not_sym, rule lt_imp_not_eq,

185 rule normed_vs_norm_gt_zero)

186 qed

187 also have "c * ... <= b " by (simp! add: le_maxI1)

188 finally show "y <= b" .

189 qed simp

190 qed

191 qed

192 qed

194 text {* The norm of a continuous function is always $\geq 0$. *}

196 lemma fnorm_ge_zero [intro?]:

197 "[| is_continuous V norm f; is_normed_vectorspace V norm |]

198 ==> #0 <= \\<parallel>f\\<parallel>V,norm"

199 proof -

200 assume c: "is_continuous V norm f"

201 and n: "is_normed_vectorspace V norm"

203 txt {* The function norm is defined as the supremum of $B$.

204 So it is $\geq 0$ if all elements in $B$ are $\geq 0$, provided

205 the supremum exists and $B$ is not empty. *}

207 show ?thesis

208 proof (unfold function_norm_def, rule sup_ub1)

209 show "\\<forall>x \\<in> (B V norm f). #0 <= x"

210 proof (intro ballI, unfold B_def,

211 elim UnE singletonE CollectE exE conjE)

212 fix x r

213 assume "x \\<in> V" "x \\<noteq> 0"

214 and r: "r = |f x| * rinv (norm x)"

216 have ge: "#0 <= |f x|" by (simp! only: abs_ge_zero)

217 have "#0 <= rinv (norm x)"

218 by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule)(***

219 proof (rule real_less_imp_le);

220 show "#0 < rinv (norm x)";

221 proof (rule real_rinv_gt_zero);

222 show "#0 < norm x"; ..;

223 qed;

224 qed; ***)

225 with ge show "#0 <= r"

226 by (simp only: r, rule real_le_mult_order1a)

227 qed (simp!)

229 txt {* Since $f$ is continuous the function norm exists: *}

231 have "is_function_norm f V norm \\<parallel>f\\<parallel>V,norm" ..

232 thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"

233 by (unfold is_function_norm_def function_norm_def)

235 txt {* $B$ is non-empty by construction: *}

237 show "#0 \\<in> B V norm f" by (rule B_not_empty)

238 qed

239 qed

241 text{* \medskip The fundamental property of function norms is:

242 \begin{matharray}{l}

243 | f\ap x | \leq {\fnorm {f}} \cdot {\norm x}

244 \end{matharray}

245 *}

247 lemma norm_fx_le_norm_f_norm_x:

248 "[| is_continuous V norm f; is_normed_vectorspace V norm; x \\<in> V |]

249 ==> |f x| <= \\<parallel>f\\<parallel>V,norm * norm x"

250 proof -

251 assume "is_normed_vectorspace V norm" "x \\<in> V"

252 and c: "is_continuous V norm f"

253 have v: "is_vectorspace V" ..

255 txt{* The proof is by case analysis on $x$. *}

257 show ?thesis

258 proof cases

260 txt {* For the case $x = \zero$ the thesis follows

261 from the linearity of $f$: for every linear function

262 holds $f\ap \zero = 0$. *}

264 assume "x = 0"

265 have "|f x| = |f 0|" by (simp!)

266 also from v continuous_linearform have "f 0 = #0" ..

267 also note abs_zero

268 also have "#0 <= \\<parallel>f\\<parallel>V,norm * norm x"

269 proof (rule real_le_mult_order1a)

270 show "#0 <= \\<parallel>f\\<parallel>V,norm" ..

271 show "#0 <= norm x" ..

272 qed

273 finally

274 show "|f x| <= \\<parallel>f\\<parallel>V,norm * norm x" .

276 next

277 assume "x \\<noteq> 0"

278 have n: "#0 < norm x" ..

279 hence nz: "norm x \\<noteq> #0"

280 by (simp only: lt_imp_not_eq)

282 txt {* For the case $x\neq \zero$ we derive the following

283 fact from the definition of the function norm:*}

285 have l: "|f x| * rinv (norm x) <= \\<parallel>f\\<parallel>V,norm"

286 proof (unfold function_norm_def, rule sup_ub)

287 from ex_fnorm [OF _ c]

288 show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"

289 by (simp! add: is_function_norm_def function_norm_def)

290 show "|f x| * rinv (norm x) \\<in> B V norm f"

291 by (unfold B_def, intro UnI2 CollectI exI [of _ x]

292 conjI, simp)

293 qed

295 txt {* The thesis now follows by a short calculation: *}

297 have "|f x| = |f x| * #1" by (simp!)

298 also from nz have "#1 = rinv (norm x) * norm x"

299 by (simp add: real_mult_inv_left1)

300 also have "|f x| * ... = |f x| * rinv (norm x) * norm x"

301 by (simp! add: real_mult_assoc)

302 also from n l have "... <= \\<parallel>f\\<parallel>V,norm * norm x"

303 by (simp add: real_mult_le_le_mono2)

304 finally show "|f x| <= \\<parallel>f\\<parallel>V,norm * norm x" .

305 qed

306 qed

308 text{* \medskip The function norm is the least positive real number for

309 which the following inequation holds:

310 \begin{matharray}{l}

311 | f\ap x | \leq c \cdot {\norm x}

312 \end{matharray}

313 *}

315 lemma fnorm_le_ub:

316 "[| is_continuous V norm f; is_normed_vectorspace V norm;

317 \\<forall>x \\<in> V. |f x| <= c * norm x; #0 <= c |]

318 ==> \\<parallel>f\\<parallel>V,norm <= c"

319 proof (unfold function_norm_def)

320 assume "is_normed_vectorspace V norm"

321 assume c: "is_continuous V norm f"

322 assume fb: "\\<forall>x \\<in> V. |f x| <= c * norm x"

323 and "#0 <= c"

325 txt {* Suppose the inequation holds for some $c\geq 0$.

326 If $c$ is an upper bound of $B$, then $c$ is greater

327 than the function norm since the function norm is the

328 least upper bound.

329 *}

331 show "Sup UNIV (B V norm f) <= c"

332 proof (rule sup_le_ub)

333 from ex_fnorm [OF _ c]

334 show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"

335 by (simp! add: is_function_norm_def function_norm_def)

337 txt {* $c$ is an upper bound of $B$, i.e. every

338 $y\in B$ is less than $c$. *}

340 show "isUb UNIV (B V norm f) c"

341 proof (intro isUbI setleI ballI)

342 fix y assume "y \\<in> B V norm f"

343 thus le: "y <= c"

344 proof (unfold B_def, elim UnE CollectE exE conjE singletonE)

346 txt {* The first case for $y\in B$ is $y=0$. *}

348 assume "y = #0"

349 show "y <= c" by (force!)

351 txt{* The second case is

352 $y = {|f\ap x|}/{\norm x}$ for some

353 $x\in V$ with $x \neq \zero$. *}

355 next

356 fix x

357 assume "x \\<in> V" "x \\<noteq> 0"

359 have lz: "#0 < norm x"

360 by (simp! add: normed_vs_norm_gt_zero)

362 have nz: "norm x \\<noteq> #0"

363 proof (rule not_sym)

364 from lz show "#0 \\<noteq> norm x"

365 by (simp! add: order_less_imp_not_eq)

366 qed

368 from lz have "#0 < rinv (norm x)"

369 by (simp! add: real_rinv_gt_zero1)

370 hence rinv_gez: "#0 <= rinv (norm x)"

371 by (rule real_less_imp_le)

373 assume "y = |f x| * rinv (norm x)"

374 also from rinv_gez have "... <= c * norm x * rinv (norm x)"

375 proof (rule real_mult_le_le_mono2)

376 show "|f x| <= c * norm x" by (rule bspec)

377 qed

378 also have "... <= c" by (simp add: nz real_mult_assoc)

379 finally show ?thesis .

380 qed

381 qed force

382 qed

383 qed

385 end