author  huffman 
Thu, 09 Nov 2006 00:19:16 +0100  
changeset 21257  b7f090c5057d 
parent 21239  d4fbe2c87ef1 
child 21282  dd647b4d7952 
permissions  rwrr 
10751  1 
(* Title : Lim.thy 
14477  2 
ID : $Id$ 
10751  3 
Author : Jacques D. Fleuriot 
4 
Copyright : 1998 University of Cambridge 

14477  5 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 
10751  6 
*) 
7 

21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

8 
header{* Limits and Continuity *} 
10751  9 

15131  10 
theory Lim 
15360  11 
imports SEQ 
15131  12 
begin 
14477  13 

14 
text{*Standard and Nonstandard Definitions*} 

10751  15 

19765  16 
definition 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

17 
LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

18 
("((_)/  (_)/ > (_))" [60, 0, 60] 60) 
19765  19 
"f  a > L = 
20563  20 
(\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x  a) < s 
21 
> norm (f x  L) < r)" 

10751  22 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

23 
NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

24 
("((_)/  (_)/ NS> (_))" [60, 0, 60] 60) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

25 
"f  a NS> L = 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

26 
(\<forall>x. (x \<noteq> star_of a & x @= star_of a > ( *f* f) x @= star_of L))" 
10751  27 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

28 
isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" 
19765  29 
"isCont f a = (f  a > (f a))" 
10751  30 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

31 
isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" 
15228  32 
{*NS definition dispenses with limit notions*} 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

33 
"isNSCont f a = (\<forall>y. y @= star_of a > 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

34 
( *f* f) y @= star_of (f a))" 
10751  35 

20752  36 
isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" 
37 
"isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x  y) < s \<longrightarrow> norm (f x  f y) < r)" 

10751  38 

20752  39 
isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" 
19765  40 
"isNSUCont f = (\<forall>x y. x @= y > ( *f* f) x @= ( *f* f) y)" 
10751  41 

42 

20755  43 
subsection {* Limits of Functions *} 
14477  44 

20755  45 
subsubsection {* Purely standard proofs *} 
14477  46 

47 
lemma LIM_eq: 

48 
"f  a > L = 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

49 
(\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (xa) < s > norm (f x  L) < r)" 
14477  50 
by (simp add: LIM_def diff_minus) 
51 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

52 
lemma LIM_I: 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

53 
"(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (xa) < s > norm (f x  L) < r) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

54 
==> f  a > L" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

55 
by (simp add: LIM_eq) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

56 

14477  57 
lemma LIM_D: 
58 
"[ f  a > L; 0<r ] 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

59 
==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (xa) < s > norm (f x  L) < r" 
14477  60 
by (simp add: LIM_eq) 
61 

21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

62 
lemma LIM_offset: "f  a > L \<Longrightarrow> (\<lambda>x. f (x + k))  a  k > L" 
20756  63 
apply (rule LIM_I) 
64 
apply (drule_tac r="r" in LIM_D, safe) 

65 
apply (rule_tac x="s" in exI, safe) 

66 
apply (drule_tac x="x + k" in spec) 

67 
apply (simp add: compare_rls) 

68 
done 

69 

21239  70 
lemma LIM_offset_zero: "f  a > L \<Longrightarrow> (\<lambda>h. f (a + h))  0 > L" 
71 
by (drule_tac k="a" in LIM_offset, simp add: add_commute) 

72 

73 
lemma LIM_offset_zero_cancel: "(\<lambda>h. f (a + h))  0 > L \<Longrightarrow> f  a > L" 

74 
by (drule_tac k=" a" in LIM_offset, simp) 

75 

15228  76 
lemma LIM_const [simp]: "(%x. k)  x > k" 
14477  77 
by (simp add: LIM_def) 
78 

79 
lemma LIM_add: 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

80 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
14477  81 
assumes f: "f  a > L" and g: "g  a > M" 
82 
shows "(%x. f x + g(x))  a > (L + M)" 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

83 
proof (rule LIM_I) 
14477  84 
fix r :: real 
20409  85 
assume r: "0 < r" 
14477  86 
from LIM_D [OF f half_gt_zero [OF r]] 
87 
obtain fs 

88 
where fs: "0 < fs" 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

89 
and fs_lt: "\<forall>x. x \<noteq> a & norm (xa) < fs > norm (f x  L) < r/2" 
14477  90 
by blast 
91 
from LIM_D [OF g half_gt_zero [OF r]] 

92 
obtain gs 

93 
where gs: "0 < gs" 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

94 
and gs_lt: "\<forall>x. x \<noteq> a & norm (xa) < gs > norm (g x  M) < r/2" 
14477  95 
by blast 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

96 
show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> norm (xa) < s \<longrightarrow> norm (f x + g x  (L + M)) < r" 
14477  97 
proof (intro exI conjI strip) 
98 
show "0 < min fs gs" by (simp add: fs gs) 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

99 
fix x :: 'a 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

100 
assume "x \<noteq> a \<and> norm (xa) < min fs gs" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

101 
hence "x \<noteq> a \<and> norm (xa) < fs \<and> norm (xa) < gs" by simp 
14477  102 
with fs_lt gs_lt 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

103 
have "norm (f x  L) < r/2" and "norm (g x  M) < r/2" by blast+ 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

104 
hence "norm (f x  L) + norm (g x  M) < r" by arith 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

105 
thus "norm (f x + g x  (L + M)) < r" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

106 
by (blast intro: norm_diff_triangle_ineq order_le_less_trans) 
14477  107 
qed 
108 
qed 

109 

21257  110 
lemma LIM_add_zero: 
111 
"\<lbrakk>f  a > 0; g  a > 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x)  a > 0" 

112 
by (drule (1) LIM_add, simp) 

113 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

114 
lemma minus_diff_minus: 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

115 
fixes a b :: "'a::ab_group_add" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

116 
shows "( a)  ( b) =  (a  b)" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

117 
by simp 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

118 

14477  119 
lemma LIM_minus: "f  a > L ==> (%x. f(x))  a > L" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

120 
by (simp only: LIM_eq minus_diff_minus norm_minus_cancel) 
14477  121 

122 
lemma LIM_add_minus: 

123 
"[ f  x > l; g  x > m ] ==> (%x. f(x) + g(x))  x > (l + m)" 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

124 
by (intro LIM_add LIM_minus) 
14477  125 

126 
lemma LIM_diff: 

127 
"[ f  x > l; g  x > m ] ==> (%x. f(x)  g(x))  x > lm" 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

128 
by (simp only: diff_minus LIM_add LIM_minus) 
14477  129 

21239  130 
lemma LIM_zero: "f  a > l \<Longrightarrow> (\<lambda>x. f x  l)  a > 0" 
131 
by (simp add: LIM_def) 

132 

133 
lemma LIM_zero_cancel: "(\<lambda>x. f x  l)  a > 0 \<Longrightarrow> f  a > l" 

134 
by (simp add: LIM_def) 

135 

21257  136 
lemma LIM_imp_LIM: 
137 
assumes f: "f  a > l" 

138 
assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x  m) \<le> norm (f x  l)" 

139 
shows "g  a > m" 

140 
apply (rule LIM_I, drule LIM_D [OF f], safe) 

141 
apply (rule_tac x="s" in exI, safe) 

142 
apply (drule_tac x="x" in spec, safe) 

143 
apply (erule (1) order_le_less_trans [OF le]) 

144 
done 

145 

146 
lemma LIM_norm: "f  a > l \<Longrightarrow> (\<lambda>x. norm (f x))  a > norm l" 

147 
by (erule LIM_imp_LIM, simp add: norm_triangle_ineq3) 

148 

149 
lemma LIM_norm_zero: "f  a > 0 \<Longrightarrow> (\<lambda>x. norm (f x))  a > 0" 

150 
by (drule LIM_norm, simp) 

151 

152 
lemma LIM_norm_zero_cancel: "(\<lambda>x. norm (f x))  a > 0 \<Longrightarrow> f  a > 0" 

153 
by (erule LIM_imp_LIM, simp) 

154 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

155 
lemma LIM_const_not_eq: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

156 
fixes a :: "'a::real_normed_div_algebra" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

157 
shows "k \<noteq> L ==> ~ ((%x. k)  a > L)" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

158 
apply (simp add: LIM_eq) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

159 
apply (rule_tac x="norm (k  L)" in exI, simp, safe) 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

160 
apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

161 
done 
14477  162 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

163 
lemma LIM_const_eq: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

164 
fixes a :: "'a::real_normed_div_algebra" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

165 
shows "(%x. k)  a > L ==> k = L" 
14477  166 
apply (rule ccontr) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

167 
apply (blast dest: LIM_const_not_eq) 
14477  168 
done 
169 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

170 
lemma LIM_unique: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

171 
fixes a :: "'a::real_normed_div_algebra" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

172 
shows "[ f  a > L; f  a > M ] ==> L = M" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

173 
apply (drule LIM_diff, assumption) 
14477  174 
apply (auto dest!: LIM_const_eq) 
175 
done 

176 

177 
lemma LIM_mult_zero: 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

178 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" 
14477  179 
assumes f: "f  a > 0" and g: "g  a > 0" 
180 
shows "(%x. f(x) * g(x))  a > 0" 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

181 
proof (rule LIM_I, simp) 
14477  182 
fix r :: real 
183 
assume r: "0<r" 

184 
from LIM_D [OF f zero_less_one] 

185 
obtain fs 

186 
where fs: "0 < fs" 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

187 
and fs_lt: "\<forall>x. x \<noteq> a & norm (xa) < fs > norm (f x) < 1" 
14477  188 
by auto 
189 
from LIM_D [OF g r] 

190 
obtain gs 

191 
where gs: "0 < gs" 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

192 
and gs_lt: "\<forall>x. x \<noteq> a & norm (xa) < gs > norm (g x) < r" 
14477  193 
by auto 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

194 
show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> norm (xa) < s \<longrightarrow> norm (f x * g x) < r)" 
14477  195 
proof (intro exI conjI strip) 
196 
show "0 < min fs gs" by (simp add: fs gs) 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

197 
fix x :: 'a 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

198 
assume "x \<noteq> a \<and> norm (xa) < min fs gs" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

199 
hence "x \<noteq> a \<and> norm (xa) < fs \<and> norm (xa) < gs" by simp 
14477  200 
with fs_lt gs_lt 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

201 
have "norm (f x) < 1" and "norm (g x) < r" by blast+ 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

202 
hence "norm (f x) * norm (g x) < 1*r" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

203 
by (rule mult_strict_mono' [OF _ _ norm_ge_zero norm_ge_zero]) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

204 
thus "norm (f x * g x) < r" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

205 
by (simp add: order_le_less_trans [OF norm_mult_ineq]) 
14477  206 
qed 
207 
qed 

208 

209 
lemma LIM_self: "(%x. x)  a > a" 

210 
by (auto simp add: LIM_def) 

211 

212 
text{*Limits are equal for functions equal except at limit point*} 

213 
lemma LIM_equal: 

214 
"[ \<forall>x. x \<noteq> a > (f x = g x) ] ==> (f  a > l) = (g  a > l)" 

215 
by (simp add: LIM_def) 

216 

20796  217 
lemma LIM_cong: 
218 
"\<lbrakk>a = b; \<And>x. x \<noteq> b \<Longrightarrow> f x = g x; l = m\<rbrakk> 

219 
\<Longrightarrow> (f  a > l) = (g  b > m)" 

220 
by (simp add: LIM_def) 

221 

14477  222 
text{*Two uses in Hyperreal/Transcendental.ML*} 
223 
lemma LIM_trans: 

224 
"[ (%x. f(x) + g(x))  a > 0; g  a > l ] ==> f  a > l" 

225 
apply (drule LIM_add, assumption) 

226 
apply (auto simp add: add_assoc) 

227 
done 

228 

21239  229 
lemma LIM_compose: 
230 
assumes g: "g  l > g l" 

231 
assumes f: "f  a > l" 

232 
shows "(\<lambda>x. g (f x))  a > g l" 

233 
proof (rule LIM_I) 

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

235 
obtain s where s: "0 < s" 

236 
and less_r: "\<And>y. \<lbrakk>y \<noteq> l; norm (y  l) < s\<rbrakk> \<Longrightarrow> norm (g y  g l) < r" 

237 
using LIM_D [OF g r] by fast 

238 
obtain t where t: "0 < t" 

239 
and less_s: "\<And>x. \<lbrakk>x \<noteq> a; norm (x  a) < t\<rbrakk> \<Longrightarrow> norm (f x  l) < s" 

240 
using LIM_D [OF f s] by fast 

241 

242 
show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> norm (x  a) < t \<longrightarrow> norm (g (f x)  g l) < r" 

243 
proof (rule exI, safe) 

244 
show "0 < t" using t . 

245 
next 

246 
fix x assume "x \<noteq> a" and "norm (x  a) < t" 

247 
hence "norm (f x  l) < s" by (rule less_s) 

248 
thus "norm (g (f x)  g l) < r" 

249 
using r less_r by (case_tac "f x = l", simp_all) 

250 
qed 

251 
qed 

252 

253 
lemma LIM_o: "\<lbrakk>g  l > g l; f  a > l\<rbrakk> \<Longrightarrow> (g \<circ> f)  a > g l" 

254 
unfolding o_def by (rule LIM_compose) 

255 

20755  256 
subsubsection {* Purely nonstandard proofs *} 
14477  257 

20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

258 
lemma NSLIM_I: 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

259 
"(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

260 
\<Longrightarrow> f  a NS> L" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

261 
by (simp add: NSLIM_def) 
14477  262 

20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

263 
lemma NSLIM_D: 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

264 
"\<lbrakk>f  a NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

265 
\<Longrightarrow> starfun f x \<approx> star_of L" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

266 
by (simp add: NSLIM_def) 
14477  267 

20755  268 
text{*Proving properties of limits using nonstandard definition. 
269 
The properties hold for standard limits as well!*} 

270 

271 
lemma NSLIM_mult: 

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

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

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

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

276 

20794  277 
lemma starfun_scaleR [simp]: 
278 
"starfun (\<lambda>x. f x *# g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))" 

279 
by transfer (rule refl) 

280 

281 
lemma NSLIM_scaleR: 

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

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

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

285 

20755  286 
lemma NSLIM_add: 
287 
"[ f  x NS> l; g  x NS> m ] 

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

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

290 

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

292 
by (simp add: NSLIM_def) 

293 

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

295 
by (simp add: NSLIM_def) 

296 

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

298 
by (simp only: NSLIM_add NSLIM_minus) 

299 

300 
lemma NSLIM_inverse: 

301 
fixes L :: "'a::real_normed_div_algebra" 

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

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

304 
apply (simp add: NSLIM_def, clarify) 

305 
apply (drule spec) 

306 
apply (auto simp add: star_of_approx_inverse) 

307 
done 

308 

309 
lemma NSLIM_zero: 

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

311 
proof  

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

313 
by (rule NSLIM_add_minus [OF f NSLIM_const]) 

314 
thus ?thesis by simp 

315 
qed 

316 

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

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

319 
apply (auto simp add: diff_minus add_assoc) 

320 
done 

321 

322 
lemma NSLIM_const_not_eq: 

323 
fixes a :: real (* TODO: generalize to real_normed_div_algebra *) 

324 
shows "k \<noteq> L ==> ~ ((%x. k)  a NS> L)" 

325 
apply (simp add: NSLIM_def) 

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

327 
apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym] 

328 
simp add: hypreal_epsilon_not_zero) 

329 
done 

330 

331 
lemma NSLIM_not_zero: 

332 
fixes a :: real 

333 
shows "k \<noteq> 0 ==> ~ ((%x. k)  a NS> 0)" 

334 
by (rule NSLIM_const_not_eq) 

335 

336 
lemma NSLIM_const_eq: 

337 
fixes a :: real 

338 
shows "(%x. k)  a NS> L ==> k = L" 

339 
apply (rule ccontr) 

340 
apply (blast dest: NSLIM_const_not_eq) 

341 
done 

342 

343 
text{* can actually be proved more easily by unfolding the definition!*} 

344 
lemma NSLIM_unique: 

345 
fixes a :: real 

346 
shows "[ f  a NS> L; f  a NS> M ] ==> L = M" 

347 
apply (drule NSLIM_minus) 

348 
apply (drule NSLIM_add, assumption) 

349 
apply (auto dest!: NSLIM_const_eq [symmetric]) 

350 
apply (simp add: diff_def [symmetric]) 

351 
done 

352 

353 
lemma NSLIM_mult_zero: 

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

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

356 
by (drule NSLIM_mult, auto) 

357 

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

359 
by (simp add: NSLIM_def) 

360 

361 
subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *} 

362 

20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

363 
lemma LIM_NSLIM: 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

364 
assumes f: "f  a > L" shows "f  a NS> L" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

365 
proof (rule NSLIM_I) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

366 
fix x 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

367 
assume neq: "x \<noteq> star_of a" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

368 
assume approx: "x \<approx> star_of a" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

369 
have "starfun f x  star_of L \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

370 
proof (rule InfinitesimalI2) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

371 
fix r::real assume r: "0 < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

372 
from LIM_D [OF f r] 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

373 
obtain s where s: "0 < s" and 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

374 
less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x  a) < s\<rbrakk> \<Longrightarrow> norm (f x  L) < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

375 
by fast 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

376 
from less_r have less_r': 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

377 
"\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x  star_of a) < star_of s\<rbrakk> 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

378 
\<Longrightarrow> hnorm (starfun f x  star_of L) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

379 
by transfer 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

380 
from approx have "x  star_of a \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

381 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

382 
hence "hnorm (x  star_of a) < star_of s" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

383 
using s by (rule InfinitesimalD2) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

384 
with neq show "hnorm (starfun f x  star_of L) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

385 
by (rule less_r') 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

386 
qed 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

387 
thus "starfun f x \<approx> star_of L" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

388 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

389 
qed 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

390 

20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

391 
lemma NSLIM_LIM: 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

392 
assumes f: "f  a NS> L" shows "f  a > L" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

393 
proof (rule LIM_I) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

394 
fix r::real assume r: "0 < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

395 
have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x  star_of a) < s 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

396 
\<longrightarrow> hnorm (starfun f x  star_of L) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

397 
proof (rule exI, safe) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

398 
show "0 < epsilon" by (rule hypreal_epsilon_gt_zero) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

399 
next 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

400 
fix x assume neq: "x \<noteq> star_of a" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

401 
assume "hnorm (x  star_of a) < epsilon" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

402 
with Infinitesimal_epsilon 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

403 
have "x  star_of a \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

404 
by (rule hnorm_less_Infinitesimal) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

405 
hence "x \<approx> star_of a" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

406 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

407 
with f neq have "starfun f x \<approx> star_of L" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

408 
by (rule NSLIM_D) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

409 
hence "starfun f x  star_of L \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

410 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

411 
thus "hnorm (starfun f x  star_of L) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

412 
using r by (rule InfinitesimalD2) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

413 
qed 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

414 
thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x  a) < s \<longrightarrow> norm (f x  L) < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

415 
by transfer 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

416 
qed 
14477  417 

15228  418 
theorem LIM_NSLIM_iff: "(f  x > L) = (f  x NS> L)" 
14477  419 
by (blast intro: LIM_NSLIM NSLIM_LIM) 
420 

20755  421 
subsubsection {* Derived theorems about @{term LIM} *} 
14477  422 

15228  423 
lemma LIM_mult2: 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

424 
fixes l m :: "'a::real_normed_algebra" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

425 
shows "[ f  x > l; g  x > m ] 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

426 
==> (%x. f(x) * g(x))  x > (l * m)" 
14477  427 
by (simp add: LIM_NSLIM_iff NSLIM_mult) 
428 

20794  429 
lemma LIM_scaleR: 
430 
"[ f  x > l; g  x > m ] 

431 
==> (%x. f(x) *# g(x))  x > (l *# m)" 

432 
by (simp add: LIM_NSLIM_iff NSLIM_scaleR) 

433 

15228  434 
lemma LIM_add2: 
435 
"[ f  x > l; g  x > m ] ==> (%x. f(x) + g(x))  x > (l + m)" 

14477  436 
by (simp add: LIM_NSLIM_iff NSLIM_add) 
437 

438 
lemma LIM_const2: "(%x. k)  x > k" 

439 
by (simp add: LIM_NSLIM_iff) 

440 

441 
lemma LIM_minus2: "f  a > L ==> (%x. f(x))  a > L" 

442 
by (simp add: LIM_NSLIM_iff NSLIM_minus) 

443 

444 
lemma LIM_add_minus2: "[ f  x > l; g  x > m ] ==> (%x. f(x) + g(x))  x > (l + m)" 

445 
by (simp add: LIM_NSLIM_iff NSLIM_add_minus) 

446 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

447 
lemma LIM_inverse: 
20653
24cda2c5fd40
removed division_by_zero class requirements from several lemmas
huffman
parents:
20635
diff
changeset

448 
fixes L :: "'a::real_normed_div_algebra" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

449 
shows "[ f  a > L; L \<noteq> 0 ] 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

450 
==> (%x. inverse(f(x)))  a > (inverse L)" 
14477  451 
by (simp add: LIM_NSLIM_iff NSLIM_inverse) 
452 

453 
lemma LIM_zero2: "f  a > l ==> (%x. f(x) + l)  a > 0" 

454 
by (simp add: LIM_NSLIM_iff NSLIM_zero) 

455 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

456 
lemma LIM_unique2: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

457 
fixes a :: real 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

458 
shows "[ f  a > L; f  a > M ] ==> L = M" 
14477  459 
by (simp add: LIM_NSLIM_iff NSLIM_unique) 
460 

461 
(* we can use the corresponding thm LIM_mult2 *) 

462 
(* for standard definition of limit *) 

463 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

464 
lemma LIM_mult_zero2: 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

465 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

466 
shows "[ f  x > 0; g  x > 0 ] ==> (%x. f(x)*g(x))  x > 0" 
14477  467 
by (drule LIM_mult2, auto) 
468 

469 

20755  470 
subsection {* Continuity *} 
14477  471 

21239  472 
subsubsection {* Purely standard proofs *} 
473 

474 
lemma LIM_isCont_iff: "(f  a > f a) = ((\<lambda>h. f (a + h))  0 > f a)" 

475 
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) 

476 

477 
lemma isCont_iff: "isCont f x = (\<lambda>h. f (x + h))  0 > f x" 

478 
by (simp add: isCont_def LIM_isCont_iff) 

479 

480 
lemma isCont_Id: "isCont (\<lambda>x. x) a" 

481 
unfolding isCont_def by (rule LIM_self) 

482 

483 
lemma isCont_const [simp]: "isCont (%x. k) a" 

484 
unfolding isCont_def by (rule LIM_const) 

485 

486 
lemma isCont_add: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a" 

487 
unfolding isCont_def by (rule LIM_add) 

488 

489 
lemma isCont_minus: "isCont f a \<Longrightarrow> isCont (\<lambda>x.  f x) a" 

490 
unfolding isCont_def by (rule LIM_minus) 

491 

492 
lemma isCont_diff: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x  g x) a" 

493 
unfolding isCont_def by (rule LIM_diff) 

494 

495 
lemma isCont_mult: 

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

497 
shows "[ isCont f a; isCont g a ] ==> isCont (%x. f(x) * g(x)) a" 

498 
unfolding isCont_def by (rule LIM_mult2) 

499 

500 
lemma isCont_inverse: 

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

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

503 
unfolding isCont_def by (rule LIM_inverse) 

504 

505 
lemma isCont_LIM_compose: 

506 
"\<lbrakk>isCont g l; f  a > l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x))  a > g l" 

507 
unfolding isCont_def by (rule LIM_compose) 

508 

509 
lemma isCont_o2: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. g (f x)) a" 

510 
unfolding isCont_def by (rule LIM_compose) 

511 

512 
lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a" 

513 
unfolding o_def by (rule isCont_o2) 

514 

515 
subsubsection {* Nonstandard proofs *} 

516 

14477  517 
lemma isNSContD: "[ isNSCont f a; y \<approx> hypreal_of_real a ] ==> ( *f* f) y \<approx> hypreal_of_real (f a)" 
518 
by (simp add: isNSCont_def) 

519 

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

521 
by (simp add: isNSCont_def NSLIM_def) 

522 

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

524 
apply (simp add: isNSCont_def NSLIM_def, auto) 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

525 
apply (case_tac "y = star_of a", auto) 
14477  526 
done 
527 

15228  528 
text{*NS continuity can be defined using NS Limit in 
529 
similar fashion to standard def of continuity*} 

14477  530 
lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f  a NS> (f a))" 
531 
by (blast intro: isNSCont_NSLIM NSLIM_isNSCont) 

532 

15228  533 
text{*Hence, NS continuity can be given 
534 
in terms of standard limit*} 

14477  535 
lemma isNSCont_LIM_iff: "(isNSCont f a) = (f  a > (f a))" 
536 
by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff) 

537 

15228  538 
text{*Moreover, it's trivial now that NS continuity 
539 
is equivalent to standard continuity*} 

14477  540 
lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)" 
541 
apply (simp add: isCont_def) 

542 
apply (rule isNSCont_LIM_iff) 

543 
done 

544 

15228  545 
text{*Standard continuity ==> NS continuity*} 
14477  546 
lemma isCont_isNSCont: "isCont f a ==> isNSCont f a" 
547 
by (erule isNSCont_isCont_iff [THEN iffD2]) 

548 

15228  549 
text{*NS continuity ==> Standard continuity*} 
14477  550 
lemma isNSCont_isCont: "isNSCont f a ==> isCont f a" 
551 
by (erule isNSCont_isCont_iff [THEN iffD1]) 

552 

553 
text{*Alternative definition of continuity*} 

554 
(* Prove equivalence between NS limits  *) 

555 
(* seems easier than using standard def *) 

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

557 
apply (simp add: NSLIM_def, auto) 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

558 
apply (drule_tac x = "star_of a + x" in spec) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

559 
apply (drule_tac [2] x = " star_of a + x" in spec, safe, simp) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

560 
apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]]) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

561 
apply (erule_tac [3] approx_minus_iff2 [THEN iffD1]) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

562 
prefer 2 apply (simp add: add_commute diff_def [symmetric]) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

563 
apply (rule_tac x = x in star_cases) 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

564 
apply (rule_tac [2] x = x in star_cases) 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

565 
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num) 
14477  566 
done 
567 

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

569 
by (rule NSLIM_h_iff) 

570 

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

572 
by (simp add: isNSCont_def) 

573 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

574 
lemma isNSCont_inverse: 
20653
24cda2c5fd40
removed division_by_zero class requirements from several lemmas
huffman
parents:
20635
diff
changeset

575 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

576 
shows "[ isNSCont f x; f x \<noteq> 0 ] ==> isNSCont (%x. inverse (f x)) x" 
14477  577 
by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff) 
578 

15228  579 
lemma isNSCont_const [simp]: "isNSCont (%x. k) a" 
14477  580 
by (simp add: isNSCont_def) 
581 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

582 
lemma isNSCont_abs [simp]: "isNSCont abs (a::real)" 
14477  583 
apply (simp add: isNSCont_def) 
584 
apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs) 

585 
done 

586 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

587 
lemma isCont_abs [simp]: "isCont abs (a::real)" 
14477  588 
by (auto simp add: isNSCont_isCont_iff [symmetric]) 
15228  589 

14477  590 

591 
(**************************************************************** 

592 
(%* Leave as commented until I add topology theory or remove? *%) 

593 
(%* 

594 
Elementary topology proof for a characterisation of 

595 
continuity now: a function f is continuous if and only 

596 
if the inverse image, {x. f(x) \<in> A}, of any open set A 

597 
is always an open set 

598 
*%) 

599 
Goal "[ isNSopen A; \<forall>x. isNSCont f x ] 

600 
==> isNSopen {x. f x \<in> A}" 

601 
by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1])); 

602 
by (dtac (mem_monad_approx RS approx_sym); 

603 
by (dres_inst_tac [("x","a")] spec 1); 

604 
by (dtac isNSContD 1 THEN assume_tac 1) 

605 
by (dtac bspec 1 THEN assume_tac 1) 

606 
by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1); 

607 
by (blast_tac (claset() addIs [starfun_mem_starset]); 

608 
qed "isNSCont_isNSopen"; 

609 

610 
Goalw [isNSCont_def] 

611 
"\<forall>A. isNSopen A > isNSopen {x. f x \<in> A} \ 

612 
\ ==> isNSCont f x"; 

613 
by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS 

614 
(approx_minus_iff RS iffD2)],simpset() addsimps 

615 
[Infinitesimal_def,SReal_iff])); 

616 
by (dres_inst_tac [("x","{z. abs(z + f(x)) < ya}")] spec 1); 

617 
by (etac (isNSopen_open_interval RSN (2,impE)); 

618 
by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def])); 

619 
by (dres_inst_tac [("x","x")] spec 1); 

620 
by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad], 

621 
simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus])); 

622 
qed "isNSopen_isNSCont"; 

623 

624 
Goal "(\<forall>x. isNSCont f x) = \ 

625 
\ (\<forall>A. isNSopen A > isNSopen {x. f(x) \<in> A})"; 

626 
by (blast_tac (claset() addIs [isNSCont_isNSopen, 

627 
isNSopen_isNSCont]); 

628 
qed "isNSCont_isNSopen_iff"; 

629 

630 
(%* Standard version of same theorem *%) 

631 
Goal "(\<forall>x. isCont f x) = \ 

632 
\ (\<forall>A. isopen A > isopen {x. f(x) \<in> A})"; 

633 
by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff], 

634 
simpset() addsimps [isNSopen_isopen_iff RS sym, 

635 
isNSCont_isCont_iff RS sym])); 

636 
qed "isCont_isopen_iff"; 

637 
*******************************************************************) 

638 

20755  639 
subsection {* Uniform Continuity *} 
640 

14477  641 
lemma isNSUContD: "[ isNSUCont f; x \<approx> y] ==> ( *f* f) x \<approx> ( *f* f) y" 
642 
by (simp add: isNSUCont_def) 

643 

644 
lemma isUCont_isCont: "isUCont f ==> isCont f x" 

645 
by (simp add: isUCont_def isCont_def LIM_def, meson) 

646 

20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

647 
lemma isUCont_isNSUCont: 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

648 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

649 
assumes f: "isUCont f" shows "isNSUCont f" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

650 
proof (unfold isNSUCont_def, safe) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

651 
fix x y :: "'a star" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

652 
assume approx: "x \<approx> y" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

653 
have "starfun f x  starfun f y \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

654 
proof (rule InfinitesimalI2) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

655 
fix r::real assume r: "0 < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

656 
with f obtain s where s: "0 < s" and 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

657 
less_r: "\<And>x y. norm (x  y) < s \<Longrightarrow> norm (f x  f y) < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

658 
by (auto simp add: isUCont_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

659 
from less_r have less_r': 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

660 
"\<And>x y. hnorm (x  y) < star_of s 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

661 
\<Longrightarrow> hnorm (starfun f x  starfun f y) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

662 
by transfer 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

663 
from approx have "x  y \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

664 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

665 
hence "hnorm (x  y) < star_of s" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

666 
using s by (rule InfinitesimalD2) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

667 
thus "hnorm (starfun f x  starfun f y) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

668 
by (rule less_r') 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

669 
qed 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

670 
thus "starfun f x \<approx> starfun f y" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

671 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

672 
qed 
14477  673 

674 
lemma isNSUCont_isUCont: 

20754
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

675 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

676 
assumes f: "isNSUCont f" shows "isUCont f" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

677 
proof (unfold isUCont_def, safe) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

678 
fix r::real assume r: "0 < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

679 
have "\<exists>s>0. \<forall>x y. hnorm (x  y) < s 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

680 
\<longrightarrow> hnorm (starfun f x  starfun f y) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

681 
proof (rule exI, safe) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

682 
show "0 < epsilon" by (rule hypreal_epsilon_gt_zero) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

683 
next 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

684 
fix x y :: "'a star" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

685 
assume "hnorm (x  y) < epsilon" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

686 
with Infinitesimal_epsilon 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

687 
have "x  y \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

688 
by (rule hnorm_less_Infinitesimal) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

689 
hence "x \<approx> y" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

690 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

691 
with f have "starfun f x \<approx> starfun f y" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

692 
by (simp add: isNSUCont_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

693 
hence "starfun f x  starfun f y \<in> Infinitesimal" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

694 
by (unfold approx_def) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

695 
thus "hnorm (starfun f x  starfun f y) < star_of r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

696 
using r by (rule InfinitesimalD2) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

697 
qed 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

698 
thus "\<exists>s>0. \<forall>x y. norm (x  y) < s \<longrightarrow> norm (f x  f y) < r" 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

699 
by transfer 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

700 
qed 
14477  701 

21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

702 
subsection {* Relation of LIM and LIMSEQ *} 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

703 

5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

704 
lemma LIMSEQ_SEQ_conv1: 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

705 
fixes a :: "'a::real_normed_vector" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

706 
assumes X: "X  a > L" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

707 
shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

708 
proof (safe intro!: LIMSEQ_I) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

709 
fix S :: "nat \<Rightarrow> 'a" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

710 
fix r :: real 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

711 
assume rgz: "0 < r" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

712 
assume as: "\<forall>n. S n \<noteq> a" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

713 
assume S: "S > a" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

714 
from LIM_D [OF X rgz] obtain s 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

715 
where sgz: "0 < s" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

716 
and aux: "\<And>x. \<lbrakk>x \<noteq> a; norm (x  a) < s\<rbrakk> \<Longrightarrow> norm (X x  L) < r" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

717 
by fast 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

718 
from LIMSEQ_D [OF S sgz] 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

719 
obtain no where "\<forall>n\<ge>no. norm (S n  a) < s" by fast 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

720 
hence "\<forall>n\<ge>no. norm (X (S n)  L) < r" by (simp add: aux as) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

721 
thus "\<exists>no. \<forall>n\<ge>no. norm (X (S n)  L) < r" .. 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

722 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

723 

5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

724 
lemma LIMSEQ_SEQ_conv2: 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

725 
fixes a :: real 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

726 
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

727 
shows "X  a > L" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

728 
proof (rule ccontr) 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

729 
assume "\<not> (X  a > L)" 
20563  730 
hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x  a) < s > norm (X x  L) < r)" by (unfold LIM_def) 
731 
hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x  a\<bar> < s > norm (X x  L) < r)" by simp 

732 
hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x  a\<bar> < s \<and> norm (X x  L) \<ge> r)" by (simp add: linorder_not_less) 

733 
then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x  a\<bar> < s \<and> norm (X x  L) \<ge> r))" by auto 

19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

734 

20563  735 
let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x  a\<bar> < inverse (real (Suc n)) \<and> norm (X x  L) \<ge> r" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

736 
have "\<And>n. \<exists>x. x\<noteq>a \<and> \<bar>x  a\<bar> < inverse (real (Suc n)) \<and> norm (X x  L) \<ge> r" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

737 
using rdef by simp 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

738 
hence F: "\<And>n. ?F n \<noteq> a \<and> \<bar>?F n  a\<bar> < inverse (real (Suc n)) \<and> norm (X (?F n)  L) \<ge> r" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

739 
by (rule someI_ex) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

740 
hence F1: "\<And>n. ?F n \<noteq> a" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

741 
and F2: "\<And>n. \<bar>?F n  a\<bar> < inverse (real (Suc n))" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

742 
and F3: "\<And>n. norm (X (?F n)  L) \<ge> r" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

743 
by fast+ 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

744 

19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

745 
have "?F > a" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

746 
proof (rule LIMSEQ_I, unfold real_norm_def) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

747 
fix e::real 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

748 
assume "0 < e" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

749 
(* choose no such that inverse (real (Suc n)) < e *) 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

750 
have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean) 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

751 
then obtain m where nodef: "inverse (real (Suc m)) < e" by auto 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

752 
show "\<exists>no. \<forall>n. no \<le> n > \<bar>?F n  a\<bar> < e" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

753 
proof (intro exI allI impI) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

754 
fix n 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

755 
assume mlen: "m \<le> n" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

756 
have "\<bar>?F n  a\<bar> < inverse (real (Suc n))" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

757 
by (rule F2) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

758 
also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

759 
by auto 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

760 
also from nodef have 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

761 
"inverse (real (Suc m)) < e" . 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

762 
finally show "\<bar>?F n  a\<bar> < e" . 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

763 
qed 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

764 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

765 

5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

766 
moreover have "\<forall>n. ?F n \<noteq> a" 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

767 
by (rule allI) (rule F1) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

768 

19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

769 
moreover from prems have "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

770 
ultimately have "(\<lambda>n. X (?F n)) > L" by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

771 

5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

772 
moreover have "\<not> ((\<lambda>n. X (?F n)) > L)" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

773 
proof  
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

774 
{ 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

775 
fix no::nat 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

776 
obtain n where "n = no + 1" by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

777 
then have nolen: "no \<le> n" by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

778 
(* We prove this by showing that for any m there is an n\<ge>m such that X (?F n)  L \<ge> r *) 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

779 
have "norm (X (?F n)  L) \<ge> r" 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

780 
by (rule F3) 
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

781 
with nolen have "\<exists>n. no \<le> n \<and> norm (X (?F n)  L) \<ge> r" by fast 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

782 
} 
20563  783 
then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n)  L) \<ge> r)" by simp 
784 
with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n)  L) \<ge> e)" by auto 

19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

785 
thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less) 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

786 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

787 
ultimately show False by simp 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

788 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

789 

5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

790 
lemma LIMSEQ_SEQ_conv: 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

791 
"(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > (a::real) \<longrightarrow> (\<lambda>n. X (S n)) > L) = 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

792 
(X  a > L)" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

793 
proof 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

794 
assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

795 
show "X  a > L" by (rule LIMSEQ_SEQ_conv2) 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

796 
next 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

797 
assume "(X  a > L)" 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

798 
show "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S > a \<longrightarrow> (\<lambda>n. X (S n)) > L" by (rule LIMSEQ_SEQ_conv1) 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

799 
qed 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

800 

10751  801 
end 