author  huffman 
Wed, 08 Nov 2006 02:13:02 +0100  
changeset 21239  d4fbe2c87ef1 
parent 21165  8fb49f668511 
child 21257  b7f090c5057d 
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 

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

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

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

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

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

114 

14477  115 
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

116 
by (simp only: LIM_eq minus_diff_minus norm_minus_cancel) 
14477  117 

118 
lemma LIM_add_minus: 

119 
"[ 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

120 
by (intro LIM_add LIM_minus) 
14477  121 

122 
lemma LIM_diff: 

123 
"[ 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

124 
by (simp only: diff_minus LIM_add LIM_minus) 
14477  125 

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

128 

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

130 
by (simp add: LIM_def) 

131 

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

132 
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

133 
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

134 
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

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

136 
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

137 
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

138 
done 
14477  139 

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

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

141 
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

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

144 
apply (blast dest: LIM_const_not_eq) 
14477  145 
done 
146 

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

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

148 
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

149 
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

150 
apply (drule LIM_diff, assumption) 
14477  151 
apply (auto dest!: LIM_const_eq) 
152 
done 

153 

154 
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

155 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" 
14477  156 
assumes f: "f  a > 0" and g: "g  a > 0" 
157 
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

158 
proof (rule LIM_I, simp) 
14477  159 
fix r :: real 
160 
assume r: "0<r" 

161 
from LIM_D [OF f zero_less_one] 

162 
obtain fs 

163 
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

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

167 
obtain gs 

168 
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

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

171 
show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> norm (xa) < s \<longrightarrow> norm (f x * g x) < r)" 
14477  172 
proof (intro exI conjI strip) 
173 
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

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

175 
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

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

178 
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

179 
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

180 
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

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

182 
by (simp add: order_le_less_trans [OF norm_mult_ineq]) 
14477  183 
qed 
184 
qed 

185 

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

187 
by (auto simp add: LIM_def) 

188 

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

190 
lemma LIM_equal: 

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

192 
by (simp add: LIM_def) 

193 

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

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

197 
by (simp add: LIM_def) 

198 

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

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

202 
apply (drule LIM_add, assumption) 

203 
apply (auto simp add: add_assoc) 

204 
done 

205 

21239  206 
lemma LIM_compose: 
207 
assumes g: "g  l > g l" 

208 
assumes f: "f  a > l" 

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

210 
proof (rule LIM_I) 

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

212 
obtain s where s: "0 < s" 

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

214 
using LIM_D [OF g r] by fast 

215 
obtain t where t: "0 < t" 

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

217 
using LIM_D [OF f s] by fast 

218 

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

220 
proof (rule exI, safe) 

221 
show "0 < t" using t . 

222 
next 

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

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

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

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

227 
qed 

228 
qed 

229 

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

231 
unfolding o_def by (rule LIM_compose) 

232 

20755  233 
subsubsection {* Purely nonstandard proofs *} 
14477  234 

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

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

236 
"(\<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

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

238 
by (simp add: NSLIM_def) 
14477  239 

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

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

241 
"\<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

242 
\<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

243 
by (simp add: NSLIM_def) 
14477  244 

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

247 

248 
lemma NSLIM_mult: 

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

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

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

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

253 

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

256 
by transfer (rule refl) 

257 

258 
lemma NSLIM_scaleR: 

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

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

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

262 

20755  263 
lemma NSLIM_add: 
264 
"[ f  x NS> l; g  x NS> m ] 

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

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

267 

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

269 
by (simp add: NSLIM_def) 

270 

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

272 
by (simp add: NSLIM_def) 

273 

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

275 
by (simp only: NSLIM_add NSLIM_minus) 

276 

277 
lemma NSLIM_inverse: 

278 
fixes L :: "'a::real_normed_div_algebra" 

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

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

281 
apply (simp add: NSLIM_def, clarify) 

282 
apply (drule spec) 

283 
apply (auto simp add: star_of_approx_inverse) 

284 
done 

285 

286 
lemma NSLIM_zero: 

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

288 
proof  

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

290 
by (rule NSLIM_add_minus [OF f NSLIM_const]) 

291 
thus ?thesis by simp 

292 
qed 

293 

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

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

296 
apply (auto simp add: diff_minus add_assoc) 

297 
done 

298 

299 
lemma NSLIM_const_not_eq: 

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

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

302 
apply (simp add: NSLIM_def) 

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

304 
apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym] 

305 
simp add: hypreal_epsilon_not_zero) 

306 
done 

307 

308 
lemma NSLIM_not_zero: 

309 
fixes a :: real 

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

311 
by (rule NSLIM_const_not_eq) 

312 

313 
lemma NSLIM_const_eq: 

314 
fixes a :: real 

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

316 
apply (rule ccontr) 

317 
apply (blast dest: NSLIM_const_not_eq) 

318 
done 

319 

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

321 
lemma NSLIM_unique: 

322 
fixes a :: real 

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

324 
apply (drule NSLIM_minus) 

325 
apply (drule NSLIM_add, assumption) 

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

327 
apply (simp add: diff_def [symmetric]) 

328 
done 

329 

330 
lemma NSLIM_mult_zero: 

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

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

333 
by (drule NSLIM_mult, auto) 

334 

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

336 
by (simp add: NSLIM_def) 

337 

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

339 

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

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

341 
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

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

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

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

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

346 
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

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

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

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

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

351 
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

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

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

354 
"\<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

355 
\<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

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

357 
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

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

359 
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

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

361 
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

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

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

364 
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

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

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

367 

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

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

369 
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

370 
proof (rule LIM_I) 
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 
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

373 
\<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

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

375 
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

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

377 
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

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

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

380 
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 (rule hnorm_less_Infinitesimal) 
9c053a494dc6
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
huffman
parents:
20752
diff
changeset

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

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

384 
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

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

386 
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

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

388 
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

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

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

391 
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

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

393 
qed 
14477  394 

15228  395 
theorem LIM_NSLIM_iff: "(f  x > L) = (f  x NS> L)" 
14477  396 
by (blast intro: LIM_NSLIM NSLIM_LIM) 
397 

20755  398 
subsubsection {* Derived theorems about @{term LIM} *} 
14477  399 

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

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

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

403 
==> (%x. f(x) * g(x))  x > (l * m)" 
14477  404 
by (simp add: LIM_NSLIM_iff NSLIM_mult) 
405 

20794  406 
lemma LIM_scaleR: 
407 
"[ f  x > l; g  x > m ] 

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

409 
by (simp add: LIM_NSLIM_iff NSLIM_scaleR) 

410 

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

14477  413 
by (simp add: LIM_NSLIM_iff NSLIM_add) 
414 

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

416 
by (simp add: LIM_NSLIM_iff) 

417 

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

419 
by (simp add: LIM_NSLIM_iff NSLIM_minus) 

420 

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

422 
by (simp add: LIM_NSLIM_iff NSLIM_add_minus) 

423 

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

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

425 
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

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

427 
==> (%x. inverse(f(x)))  a > (inverse L)" 
14477  428 
by (simp add: LIM_NSLIM_iff NSLIM_inverse) 
429 

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

431 
by (simp add: LIM_NSLIM_iff NSLIM_zero) 

432 

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

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

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

435 
shows "[ f  a > L; f  a > M ] ==> L = M" 
14477  436 
by (simp add: LIM_NSLIM_iff NSLIM_unique) 
437 

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

439 
(* for standard definition of limit *) 

440 

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

441 
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

442 
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

443 
shows "[ f  x > 0; g  x > 0 ] ==> (%x. f(x)*g(x))  x > 0" 
14477  444 
by (drule LIM_mult2, auto) 
445 

446 

20755  447 
subsection {* Continuity *} 
14477  448 

21239  449 
subsubsection {* Purely standard proofs *} 
450 

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

452 
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) 

453 

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

455 
by (simp add: isCont_def LIM_isCont_iff) 

456 

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

458 
unfolding isCont_def by (rule LIM_self) 

459 

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

461 
unfolding isCont_def by (rule LIM_const) 

462 

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

464 
unfolding isCont_def by (rule LIM_add) 

465 

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

467 
unfolding isCont_def by (rule LIM_minus) 

468 

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

470 
unfolding isCont_def by (rule LIM_diff) 

471 

472 
lemma isCont_mult: 

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

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

475 
unfolding isCont_def by (rule LIM_mult2) 

476 

477 
lemma isCont_inverse: 

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

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

480 
unfolding isCont_def by (rule LIM_inverse) 

481 

482 
lemma isCont_LIM_compose: 

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

484 
unfolding isCont_def by (rule LIM_compose) 

485 

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

487 
unfolding isCont_def by (rule LIM_compose) 

488 

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

490 
unfolding o_def by (rule isCont_o2) 

491 

492 
subsubsection {* Nonstandard proofs *} 

493 

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

496 

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

498 
by (simp add: isNSCont_def NSLIM_def) 

499 

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

501 
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

502 
apply (case_tac "y = star_of a", auto) 
14477  503 
done 
504 

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

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

509 

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

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

514 

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

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

519 
apply (rule isNSCont_LIM_iff) 

520 
done 

521 

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

525 

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

529 

530 
text{*Alternative definition of continuity*} 

531 
(* Prove equivalence between NS limits  *) 

532 
(* seems easier than using standard def *) 

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

534 
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

535 
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

536 
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

537 
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

538 
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

539 
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

540 
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

541 
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

542 
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num) 
14477  543 
done 
544 

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

546 
by (rule NSLIM_h_iff) 

547 

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

549 
by (simp add: isNSCont_def) 

550 

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

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

552 
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

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

15228  556 
lemma isNSCont_const [simp]: "isNSCont (%x. k) a" 
14477  557 
by (simp add: isNSCont_def) 
558 

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

559 
lemma isNSCont_abs [simp]: "isNSCont abs (a::real)" 
14477  560 
apply (simp add: isNSCont_def) 
561 
apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs) 

562 
done 

563 

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

564 
lemma isCont_abs [simp]: "isCont abs (a::real)" 
14477  565 
by (auto simp add: isNSCont_isCont_iff [symmetric]) 
15228  566 

14477  567 

568 
(**************************************************************** 

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

570 
(%* 

571 
Elementary topology proof for a characterisation of 

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

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

574 
is always an open set 

575 
*%) 

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

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

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

579 
by (dtac (mem_monad_approx RS approx_sym); 

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

581 
by (dtac isNSContD 1 THEN assume_tac 1) 

582 
by (dtac bspec 1 THEN assume_tac 1) 

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

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

585 
qed "isNSCont_isNSopen"; 

586 

587 
Goalw [isNSCont_def] 

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

589 
\ ==> isNSCont f x"; 

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

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

592 
[Infinitesimal_def,SReal_iff])); 

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

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

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

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

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

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

599 
qed "isNSopen_isNSCont"; 

600 

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

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

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

604 
isNSopen_isNSCont]); 

605 
qed "isNSCont_isNSopen_iff"; 

606 

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

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

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

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

611 
simpset() addsimps [isNSopen_isopen_iff RS sym, 

612 
isNSCont_isCont_iff RS sym])); 

613 
qed "isCont_isopen_iff"; 

614 
*******************************************************************) 

615 

20755  616 
subsection {* Uniform Continuity *} 
617 

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

620 

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

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

623 

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

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

625 
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

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

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

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

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

630 
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

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

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

633 
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

634 
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

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

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

637 
"\<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

638 
\<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

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

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

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

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

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

644 
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

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

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

647 
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

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

649 
qed 
14477  650 

651 
lemma isNSUCont_isUCont: 

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

652 
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

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

654 
proof (unfold isUCont_def, safe) 
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 
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

657 
\<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

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

659 
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

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

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

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

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

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

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

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

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

668 
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

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

670 
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

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

672 
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

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

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

675 
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

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

677 
qed 
14477  678 

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

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

680 

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

681 
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

682 
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

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

684 
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

685 
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

686 
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

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

688 
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

689 
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

690 
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

691 
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

692 
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

693 
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

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

695 
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

696 
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

697 
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

698 
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

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

700 

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

701 
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

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

703 
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

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

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

706 
assume "\<not> (X  a > L)" 
20563  707 
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) 
708 
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 

709 
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) 

710 
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

711 

20563  712 
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

713 
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

714 
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

715 
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

716 
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

717 
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

718 
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

719 
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

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

721 

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

722 
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

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

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

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

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

727 
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

728 
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

729 
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

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

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

732 
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

733 
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

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

735 
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

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

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

738 
"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

739 
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

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

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

742 

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

743 
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

744 
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

745 

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

746 
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

747 
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

748 

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

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

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

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

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

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

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

755 
(* 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

756 
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

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

758 
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

759 
} 
20563  760 
then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n)  L) \<ge> r)" by simp 
761 
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

762 
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

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

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

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

766 

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

767 
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

768 
"(\<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

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

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

771 
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

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

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

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

775 
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

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

777 

10751  778 
end 