author  wenzelm 
Tue, 27 Nov 2012 20:01:57 +0100  
changeset 50249  3f0920f8a24e 
parent 41959  b460124855b8 
child 50322  b06b95a5fda2 
permissions  rwrr 
41959  1 
(* Title: HOL/NSA/HLim.thy 
41589  2 
Author: Jacques D. Fleuriot, University of Cambridge 
3 
Author: Lawrence C Paulson 

27468  4 
*) 
5 

6 
header{* Limits and Continuity (Nonstandard) *} 

7 

8 
theory HLim 

9 
imports Star Lim 

10 
begin 

11 

12 
text{*Nonstandard Definitions*} 

13 

14 
definition 

15 
NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" 

16 
("((_)/  (_)/ NS> (_))" [60, 0, 60] 60) where 

37765  17 
"f  a NS> L = 
27468  18 
(\<forall>x. (x \<noteq> star_of a & x @= star_of a > ( *f* f) x @= star_of L))" 
19 

20 
definition 

21 
isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where 

22 
{*NS definition dispenses with limit notions*} 

37765  23 
"isNSCont f a = (\<forall>y. y @= star_of a > 
27468  24 
( *f* f) y @= star_of (f a))" 
25 

26 
definition 

27 
isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where 

37765  28 
"isNSUCont f = (\<forall>x y. x @= y > ( *f* f) x @= ( *f* f) y)" 
27468  29 

30 

31 
subsection {* Limits of Functions *} 

32 

33 
lemma NSLIM_I: 

34 
"(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L) 

35 
\<Longrightarrow> f  a NS> L" 

36 
by (simp add: NSLIM_def) 

37 

38 
lemma NSLIM_D: 

39 
"\<lbrakk>f  a NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> 

40 
\<Longrightarrow> starfun f x \<approx> star_of L" 

41 
by (simp add: NSLIM_def) 

42 

43 
text{*Proving properties of limits using nonstandard definition. 

44 
The properties hold for standard limits as well!*} 

45 

46 
lemma NSLIM_mult: 

47 
fixes l m :: "'a::real_normed_algebra" 

48 
shows "[ f  x NS> l; g  x NS> m ] 

49 
==> (%x. f(x) * g(x))  x NS> (l * m)" 

50 
by (auto simp add: NSLIM_def intro!: approx_mult_HFinite) 

51 

52 
lemma starfun_scaleR [simp]: 

53 
"starfun (\<lambda>x. f x *\<^sub>R g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))" 

54 
by transfer (rule refl) 

55 

56 
lemma NSLIM_scaleR: 

57 
"[ f  x NS> l; g  x NS> m ] 

58 
==> (%x. f(x) *\<^sub>R g(x))  x NS> (l *\<^sub>R m)" 

59 
by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite) 

60 

61 
lemma NSLIM_add: 

62 
"[ f  x NS> l; g  x NS> m ] 

63 
==> (%x. f(x) + g(x))  x NS> (l + m)" 

64 
by (auto simp add: NSLIM_def intro!: approx_add) 

65 

66 
lemma NSLIM_const [simp]: "(%x. k)  x NS> k" 

67 
by (simp add: NSLIM_def) 

68 

69 
lemma NSLIM_minus: "f  a NS> L ==> (%x. f(x))  a NS> L" 

70 
by (simp add: NSLIM_def) 

71 

72 
lemma NSLIM_diff: 

73 
"\<lbrakk>f  x NS> l; g  x NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x  g x)  x NS> (l  m)" 

37887  74 
by (simp only: diff_minus NSLIM_add NSLIM_minus) 
27468  75 

76 
lemma NSLIM_add_minus: "[ f  x NS> l; g  x NS> m ] ==> (%x. f(x) + g(x))  x NS> (l + m)" 

77 
by (simp only: NSLIM_add NSLIM_minus) 

78 

79 
lemma NSLIM_inverse: 

80 
fixes L :: "'a::real_normed_div_algebra" 

81 
shows "[ f  a NS> L; L \<noteq> 0 ] 

82 
==> (%x. inverse(f(x)))  a NS> (inverse L)" 

83 
apply (simp add: NSLIM_def, clarify) 

84 
apply (drule spec) 

85 
apply (auto simp add: star_of_approx_inverse) 

86 
done 

87 

88 
lemma NSLIM_zero: 

89 
assumes f: "f  a NS> l" shows "(%x. f(x)  l)  a NS> 0" 

90 
proof  

91 
have "(\<lambda>x. f x  l)  a NS> l  l" 

92 
by (rule NSLIM_diff [OF f NSLIM_const]) 

93 
thus ?thesis by simp 

94 
qed 

95 

96 
lemma NSLIM_zero_cancel: "(%x. f(x)  l)  x NS> 0 ==> f  x NS> l" 

97 
apply (drule_tac g = "%x. l" and m = l in NSLIM_add) 

98 
apply (auto simp add: diff_minus add_assoc) 

99 
done 

100 

101 
lemma NSLIM_const_not_eq: 

102 
fixes a :: "'a::real_normed_algebra_1" 

103 
shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k)  a NS> L" 

104 
apply (simp add: NSLIM_def) 

105 
apply (rule_tac x="star_of a + of_hypreal epsilon" in exI) 

106 
apply (simp add: hypreal_epsilon_not_zero approx_def) 

107 
done 

108 

109 
lemma NSLIM_not_zero: 

110 
fixes a :: "'a::real_normed_algebra_1" 

111 
shows "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>x. k)  a NS> 0" 

112 
by (rule NSLIM_const_not_eq) 

113 

114 
lemma NSLIM_const_eq: 

115 
fixes a :: "'a::real_normed_algebra_1" 

116 
shows "(\<lambda>x. k)  a NS> L \<Longrightarrow> k = L" 

117 
apply (rule ccontr) 

118 
apply (blast dest: NSLIM_const_not_eq) 

119 
done 

120 

121 
lemma NSLIM_unique: 

122 
fixes a :: "'a::real_normed_algebra_1" 

123 
shows "\<lbrakk>f  a NS> L; f  a NS> M\<rbrakk> \<Longrightarrow> L = M" 

124 
apply (drule (1) NSLIM_diff) 

125 
apply (auto dest!: NSLIM_const_eq) 

126 
done 

127 

128 
lemma NSLIM_mult_zero: 

129 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" 

130 
shows "[ f  x NS> 0; g  x NS> 0 ] ==> (%x. f(x)*g(x))  x NS> 0" 

131 
by (drule NSLIM_mult, auto) 

132 

133 
lemma NSLIM_self: "(%x. x)  a NS> a" 

134 
by (simp add: NSLIM_def) 

135 

50249  136 
subsubsection {* Equivalence of @{term filter_lim} and @{term NSLIM} *} 
27468  137 

138 
lemma LIM_NSLIM: 

139 
assumes f: "f  a > L" shows "f  a NS> L" 

140 
proof (rule NSLIM_I) 

141 
fix x 

142 
assume neq: "x \<noteq> star_of a" 

143 
assume approx: "x \<approx> star_of a" 

144 
have "starfun f x  star_of L \<in> Infinitesimal" 

145 
proof (rule InfinitesimalI2) 

146 
fix r::real assume r: "0 < r" 

147 
from LIM_D [OF f r] 

148 
obtain s where s: "0 < s" and 

149 
less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x  a) < s\<rbrakk> \<Longrightarrow> norm (f x  L) < r" 

150 
by fast 

151 
from less_r have less_r': 

152 
"\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x  star_of a) < star_of s\<rbrakk> 

153 
\<Longrightarrow> hnorm (starfun f x  star_of L) < star_of r" 

154 
by transfer 

155 
from approx have "x  star_of a \<in> Infinitesimal" 

156 
by (unfold approx_def) 

157 
hence "hnorm (x  star_of a) < star_of s" 

158 
using s by (rule InfinitesimalD2) 

159 
with neq show "hnorm (starfun f x  star_of L) < star_of r" 

160 
by (rule less_r') 

161 
qed 

162 
thus "starfun f x \<approx> star_of L" 

163 
by (unfold approx_def) 

164 
qed 

165 

166 
lemma NSLIM_LIM: 

167 
assumes f: "f  a NS> L" shows "f  a > L" 

168 
proof (rule LIM_I) 

169 
fix r::real assume r: "0 < r" 

170 
have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x  star_of a) < s 

171 
\<longrightarrow> hnorm (starfun f x  star_of L) < star_of r" 

172 
proof (rule exI, safe) 

173 
show "0 < epsilon" by (rule hypreal_epsilon_gt_zero) 

174 
next 

175 
fix x assume neq: "x \<noteq> star_of a" 

176 
assume "hnorm (x  star_of a) < epsilon" 

177 
with Infinitesimal_epsilon 

178 
have "x  star_of a \<in> Infinitesimal" 

179 
by (rule hnorm_less_Infinitesimal) 

180 
hence "x \<approx> star_of a" 

181 
by (unfold approx_def) 

182 
with f neq have "starfun f x \<approx> star_of L" 

183 
by (rule NSLIM_D) 

184 
hence "starfun f x  star_of L \<in> Infinitesimal" 

185 
by (unfold approx_def) 

186 
thus "hnorm (starfun f x  star_of L) < star_of r" 

187 
using r by (rule InfinitesimalD2) 

188 
qed 

189 
thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x  a) < s \<longrightarrow> norm (f x  L) < r" 

190 
by transfer 

191 
qed 

192 

193 
theorem LIM_NSLIM_iff: "(f  x > L) = (f  x NS> L)" 

194 
by (blast intro: LIM_NSLIM NSLIM_LIM) 

195 

196 

197 
subsection {* Continuity *} 

198 

199 
lemma isNSContD: 

200 
"\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)" 

201 
by (simp add: isNSCont_def) 

202 

203 
lemma isNSCont_NSLIM: "isNSCont f a ==> f  a NS> (f a) " 

204 
by (simp add: isNSCont_def NSLIM_def) 

205 

206 
lemma NSLIM_isNSCont: "f  a NS> (f a) ==> isNSCont f a" 

207 
apply (simp add: isNSCont_def NSLIM_def, auto) 

208 
apply (case_tac "y = star_of a", auto) 

209 
done 

210 

211 
text{*NS continuity can be defined using NS Limit in 

212 
similar fashion to standard def of continuity*} 

213 
lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f  a NS> (f a))" 

214 
by (blast intro: isNSCont_NSLIM NSLIM_isNSCont) 

215 

216 
text{*Hence, NS continuity can be given 

217 
in terms of standard limit*} 

218 
lemma isNSCont_LIM_iff: "(isNSCont f a) = (f  a > (f a))" 

219 
by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff) 

220 

221 
text{*Moreover, it's trivial now that NS continuity 

222 
is equivalent to standard continuity*} 

223 
lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)" 

224 
apply (simp add: isCont_def) 

225 
apply (rule isNSCont_LIM_iff) 

226 
done 

227 

228 
text{*Standard continuity ==> NS continuity*} 

229 
lemma isCont_isNSCont: "isCont f a ==> isNSCont f a" 

230 
by (erule isNSCont_isCont_iff [THEN iffD2]) 

231 

232 
text{*NS continuity ==> Standard continuity*} 

233 
lemma isNSCont_isCont: "isNSCont f a ==> isCont f a" 

234 
by (erule isNSCont_isCont_iff [THEN iffD1]) 

235 

236 
text{*Alternative definition of continuity*} 

237 

238 
(* Prove equivalence between NS limits  *) 

239 
(* seems easier than using standard def *) 

240 
lemma NSLIM_h_iff: "(f  a NS> L) = ((%h. f(a + h))  0 NS> L)" 

241 
apply (simp add: NSLIM_def, auto) 

242 
apply (drule_tac x = "star_of a + x" in spec) 

243 
apply (drule_tac [2] x = " star_of a + x" in spec, safe, simp) 

244 
apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]]) 

245 
apply (erule_tac [3] approx_minus_iff2 [THEN iffD1]) 

37887  246 
prefer 2 apply (simp add: add_commute diff_minus [symmetric]) 
27468  247 
apply (rule_tac x = x in star_cases) 
248 
apply (rule_tac [2] x = x in star_cases) 

249 
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num) 

250 
done 

251 

252 
lemma NSLIM_isCont_iff: "(f  a NS> f a) = ((%h. f(a + h))  0 NS> f a)" 

253 
by (rule NSLIM_h_iff) 

254 

255 
lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x.  f x) a" 

256 
by (simp add: isNSCont_def) 

257 

258 
lemma isNSCont_inverse: 

259 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra" 

260 
shows "[ isNSCont f x; f x \<noteq> 0 ] ==> isNSCont (%x. inverse (f x)) x" 

261 
by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff) 

262 

263 
lemma isNSCont_const [simp]: "isNSCont (%x. k) a" 

264 
by (simp add: isNSCont_def) 

265 

266 
lemma isNSCont_abs [simp]: "isNSCont abs (a::real)" 

267 
apply (simp add: isNSCont_def) 

268 
apply (auto intro: approx_hrabs simp add: starfun_rabs_hrabs) 

269 
done 

270 

271 

272 
subsection {* Uniform Continuity *} 

273 

274 
lemma isNSUContD: "[ isNSUCont f; x \<approx> y] ==> ( *f* f) x \<approx> ( *f* f) y" 

275 
by (simp add: isNSUCont_def) 

276 

277 
lemma isUCont_isNSUCont: 

278 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 

279 
assumes f: "isUCont f" shows "isNSUCont f" 

280 
proof (unfold isNSUCont_def, safe) 

281 
fix x y :: "'a star" 

282 
assume approx: "x \<approx> y" 

283 
have "starfun f x  starfun f y \<in> Infinitesimal" 

284 
proof (rule InfinitesimalI2) 

285 
fix r::real assume r: "0 < r" 

286 
with f obtain s where s: "0 < s" and 

287 
less_r: "\<And>x y. norm (x  y) < s \<Longrightarrow> norm (f x  f y) < r" 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
28562
diff
changeset

288 
by (auto simp add: isUCont_def dist_norm) 
27468  289 
from less_r have less_r': 
290 
"\<And>x y. hnorm (x  y) < star_of s 

291 
\<Longrightarrow> hnorm (starfun f x  starfun f y) < star_of r" 

292 
by transfer 

293 
from approx have "x  y \<in> Infinitesimal" 

294 
by (unfold approx_def) 

295 
hence "hnorm (x  y) < star_of s" 

296 
using s by (rule InfinitesimalD2) 

297 
thus "hnorm (starfun f x  starfun f y) < star_of r" 

298 
by (rule less_r') 

299 
qed 

300 
thus "starfun f x \<approx> starfun f y" 

301 
by (unfold approx_def) 

302 
qed 

303 

304 
lemma isNSUCont_isUCont: 

305 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 

306 
assumes f: "isNSUCont f" shows "isUCont f" 

31338
d41a8ba25b67
generalize constants from Lim.thy to class metric_space
huffman
parents:
28562
diff
changeset

307 
proof (unfold isUCont_def dist_norm, safe) 
27468  308 
fix r::real assume r: "0 < r" 
309 
have "\<exists>s>0. \<forall>x y. hnorm (x  y) < s 

310 
\<longrightarrow> hnorm (starfun f x  starfun f y) < star_of r" 

311 
proof (rule exI, safe) 

312 
show "0 < epsilon" by (rule hypreal_epsilon_gt_zero) 

313 
next 

314 
fix x y :: "'a star" 

315 
assume "hnorm (x  y) < epsilon" 

316 
with Infinitesimal_epsilon 

317 
have "x  y \<in> Infinitesimal" 

318 
by (rule hnorm_less_Infinitesimal) 

319 
hence "x \<approx> y" 

320 
by (unfold approx_def) 

321 
with f have "starfun f x \<approx> starfun f y" 

322 
by (simp add: isNSUCont_def) 

323 
hence "starfun f x  starfun f y \<in> Infinitesimal" 

324 
by (unfold approx_def) 

325 
thus "hnorm (starfun f x  starfun f y) < star_of r" 

326 
using r by (rule InfinitesimalD2) 

327 
qed 

328 
thus "\<exists>s>0. \<forall>x y. norm (x  y) < s \<longrightarrow> norm (f x  f y) < r" 

329 
by transfer 

330 
qed 

331 

332 
end 