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

src/HOL/Hahn_Banach/Function_Norm.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/Function_Norm.thy

2 Author: Gertrud Bauer, TU Munich

3 *)

5 section \<open>The norm of a function\<close>

7 theory Function_Norm

8 imports Normed_Space Function_Order

9 begin

11 subsection \<open>Continuous linear forms\<close>

13 text \<open>

14 A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>, iff

15 it is bounded, i.e.

16 \begin{center}

17 \<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>

18 \end{center}

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

20 we can define continuous linear forms as bounded linear forms:

21 \<close>

23 locale continuous = linearform +

24 fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>")

25 assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"

27 declare continuous.intro [intro?] continuous_axioms.intro [intro?]

29 lemma continuousI [intro]:

30 fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>")

31 assumes "linearform V f"

32 assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"

33 shows "continuous V f norm"

34 proof

35 show "linearform V f" by fact

36 from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast

37 then show "continuous_axioms V f norm" ..

38 qed

41 subsection \<open>The norm of a linear form\<close>

43 text \<open>

44 The least real number \<open>c\<close> for which holds

45 \begin{center}

46 \<open>\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>

47 \end{center}

48 is called the \<^emph>\<open>norm\<close> of \<open>f\<close>.

50 For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be defined as

51 \begin{center}

52 \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close>

53 \end{center}

55 For the case \<open>V = {0}\<close> the supremum would be taken from an empty set. Since

56 \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this situation it

57 must be guaranteed that there is an element in this set. This element must

58 be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties. Furthermore it does

59 not have to change the norm in all other cases, so it must be \<open>0\<close>, as all

60 other elements are \<open>{} \<ge> 0\<close>.

62 Thus we define the set \<open>B\<close> where the supremum is taken from as follows:

63 \begin{center}

64 \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close>

65 \end{center}

67 \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists (otherwise

68 it is undefined).

69 \<close>

71 locale fn_norm =

72 fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>")

73 fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"

74 fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)

75 defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"

77 locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm

79 lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f"

80 by (simp add: B_def)

82 text \<open>

83 The following lemma states that every continuous linear form on a normed

84 space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm.

85 \<close>

87 lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:

88 assumes "continuous V f norm"

89 shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"

90 proof -

91 interpret continuous V f norm by fact

92 txt \<open>The existence of the supremum is shown using the

93 completeness of the reals. Completeness means, that every

94 non-empty bounded set of reals has a supremum.\<close>

95 have "\<exists>a. lub (B V f) a"

96 proof (rule real_complete)

97 txt \<open>First we have to show that \<open>B\<close> is non-empty:\<close>

98 have "0 \<in> B V f" ..

99 then show "\<exists>x. x \<in> B V f" ..

101 txt \<open>Then we have to show that \<open>B\<close> is bounded:\<close>

102 show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"

103 proof -

104 txt \<open>We know that \<open>f\<close> is bounded by some value \<open>c\<close>.\<close>

105 from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..

107 txt \<open>To prove the thesis, we have to show that there is some \<open>b\<close>, such

108 that \<open>y \<le> b\<close> for all \<open>y \<in> B\<close>. Due to the definition of \<open>B\<close> there are

109 two cases.\<close>

111 define b where "b = max c 0"

112 have "\<forall>y \<in> B V f. y \<le> b"

113 proof

114 fix y assume y: "y \<in> B V f"

115 show "y \<le> b"

116 proof cases

117 assume "y = 0"

118 then show ?thesis unfolding b_def by arith

119 next

120 txt \<open>The second case is \<open>y = \<bar>f x\<bar> / \<parallel>x\<parallel>\<close> for some

121 \<open>x \<in> V\<close> with \<open>x \<noteq> 0\<close>.\<close>

122 assume "y \<noteq> 0"

123 with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"

124 and x: "x \<in> V" and neq: "x \<noteq> 0"

125 by (auto simp add: B_def divide_inverse)

126 from x neq have gt: "0 < \<parallel>x\<parallel>" ..

128 txt \<open>The thesis follows by a short calculation using the

129 fact that \<open>f\<close> is bounded.\<close>

131 note y_rep

132 also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"

133 proof (rule mult_right_mono)

134 from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..

135 from gt have "0 < inverse \<parallel>x\<parallel>"

136 by (rule positive_imp_inverse_positive)

137 then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)

138 qed

139 also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"

140 by (rule Groups.mult.assoc)

141 also

142 from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp

143 then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp

144 also have "c * 1 \<le> b" by (simp add: b_def)

145 finally show "y \<le> b" .

146 qed

147 qed

148 then show ?thesis ..

149 qed

150 qed

151 then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex)

152 qed

154 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:

155 assumes "continuous V f norm"

156 assumes b: "b \<in> B V f"

157 shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"

158 proof -

159 interpret continuous V f norm by fact

160 have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"

161 using \<open>continuous V f norm\<close> by (rule fn_norm_works)

162 from this and b show ?thesis ..

163 qed

165 lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:

166 assumes "continuous V f norm"

167 assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"

168 shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"

169 proof -

170 interpret continuous V f norm by fact

171 have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"

172 using \<open>continuous V f norm\<close> by (rule fn_norm_works)

173 from this and b show ?thesis ..

174 qed

176 text \<open>The norm of a continuous function is always \<open>\<ge> 0\<close>.\<close>

178 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:

179 assumes "continuous V f norm"

180 shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"

181 proof -

182 interpret continuous V f norm by fact

183 txt \<open>The function norm is defined as the supremum of \<open>B\<close>.

184 So it is \<open>\<ge> 0\<close> if all elements in \<open>B\<close> are \<open>\<ge>

185 0\<close>, provided the supremum exists and \<open>B\<close> is not empty.\<close>

186 have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"

187 using \<open>continuous V f norm\<close> by (rule fn_norm_works)

188 moreover have "0 \<in> B V f" ..

189 ultimately show ?thesis ..

190 qed

192 text \<open>

193 \<^medskip>

194 The fundamental property of function norms is:

195 \begin{center}

196 \<open>\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>

197 \end{center}

198 \<close>

200 lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:

201 assumes "continuous V f norm" "linearform V f"

202 assumes x: "x \<in> V"

203 shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"

204 proof -

205 interpret continuous V f norm by fact

206 interpret linearform V f by fact

207 show ?thesis

208 proof cases

209 assume "x = 0"

210 then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp

211 also have "f 0 = 0" by rule unfold_locales

212 also have "\<bar>\<dots>\<bar> = 0" by simp

213 also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"

214 using \<open>continuous V f norm\<close> by (rule fn_norm_ge_zero)

215 from x have "0 \<le> norm x" ..

216 with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)

217 finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .

218 next

219 assume "x \<noteq> 0"

220 with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp

221 then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp

222 also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"

223 proof (rule mult_right_mono)

224 from x show "0 \<le> \<parallel>x\<parallel>" ..

225 from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"

226 by (auto simp add: B_def divide_inverse)

227 with \<open>continuous V f norm\<close> show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"

228 by (rule fn_norm_ub)

229 qed

230 finally show ?thesis .

231 qed

232 qed

234 text \<open>

235 \<^medskip>

236 The function norm is the least positive real number for which the

237 following inequality holds:

238 \begin{center}

239 \<open>\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>

240 \end{center}

241 \<close>

243 lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:

244 assumes "continuous V f norm"

245 assumes ineq: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"

246 shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"

247 proof -

248 interpret continuous V f norm by fact

249 show ?thesis

250 proof (rule fn_norm_leastB [folded B_def fn_norm_def])

251 fix b assume b: "b \<in> B V f"

252 show "b \<le> c"

253 proof cases

254 assume "b = 0"

255 with ge show ?thesis by simp

256 next

257 assume "b \<noteq> 0"

258 with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"

259 and x_neq: "x \<noteq> 0" and x: "x \<in> V"

260 by (auto simp add: B_def divide_inverse)

261 note b_rep

262 also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"

263 proof (rule mult_right_mono)

264 have "0 < \<parallel>x\<parallel>" using x x_neq ..

265 then show "0 \<le> inverse \<parallel>x\<parallel>" by simp

266 from x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by (rule ineq)

267 qed

268 also have "\<dots> = c"

269 proof -

270 from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp

271 then show ?thesis by simp

272 qed

273 finally show ?thesis .

274 qed

275 qed (insert \<open>continuous V f norm\<close>, simp_all add: continuous_def)

276 qed

278 end