author  huffman 
Sat, 04 Nov 2006 00:12:06 +0100  
changeset 21165  8fb49f668511 
parent 21141  f0b5e6254a1f 
child 21239  d4fbe2c87ef1 
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 

15228  70 
lemma LIM_const [simp]: "(%x. k)  x > k" 
14477  71 
by (simp add: LIM_def) 
72 

73 
lemma LIM_add: 

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

74 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
14477  75 
assumes f: "f  a > L" and g: "g  a > M" 
76 
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

77 
proof (rule LIM_I) 
14477  78 
fix r :: real 
20409  79 
assume r: "0 < r" 
14477  80 
from LIM_D [OF f half_gt_zero [OF r]] 
81 
obtain fs 

82 
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

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

86 
obtain gs 

87 
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

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

90 
show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> norm (xa) < s \<longrightarrow> norm (f x + g x  (L + M)) < r" 
14477  91 
proof (intro exI conjI strip) 
92 
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

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

94 
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

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

97 
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

98 
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

99 
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

100 
by (blast intro: norm_diff_triangle_ineq order_le_less_trans) 
14477  101 
qed 
102 
qed 

103 

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

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

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

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

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

108 

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

110 
by (simp only: LIM_eq minus_diff_minus norm_minus_cancel) 
14477  111 

112 
lemma LIM_add_minus: 

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

114 
by (intro LIM_add LIM_minus) 
14477  115 

116 
lemma LIM_diff: 

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

118 
by (simp only: diff_minus LIM_add LIM_minus) 
14477  119 

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

120 
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

121 
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

122 
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

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

124 
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

125 
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

126 
done 
14477  127 

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

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

129 
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

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

132 
apply (blast dest: LIM_const_not_eq) 
14477  133 
done 
134 

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

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

136 
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

137 
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

138 
apply (drule LIM_diff, assumption) 
14477  139 
apply (auto dest!: LIM_const_eq) 
140 
done 

141 

142 
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

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

146 
proof (rule LIM_I, simp) 
14477  147 
fix r :: real 
148 
assume r: "0<r" 

149 
from LIM_D [OF f zero_less_one] 

150 
obtain fs 

151 
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

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

155 
obtain gs 

156 
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

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

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

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

163 
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

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

166 
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

167 
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

168 
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

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

170 
by (simp add: order_le_less_trans [OF norm_mult_ineq]) 
14477  171 
qed 
172 
qed 

173 

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

175 
by (auto simp add: LIM_def) 

176 

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

178 
lemma LIM_equal: 

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

180 
by (simp add: LIM_def) 

181 

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

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

185 
by (simp add: LIM_def) 

186 

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

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

190 
apply (drule LIM_add, assumption) 

191 
apply (auto simp add: add_assoc) 

192 
done 

193 

20755  194 
subsubsection {* Purely nonstandard proofs *} 
14477  195 

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

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

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

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

199 
by (simp add: NSLIM_def) 
14477  200 

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

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

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

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

204 
by (simp add: NSLIM_def) 
14477  205 

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

208 

209 
lemma NSLIM_mult: 

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

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

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

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

214 

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

217 
by transfer (rule refl) 

218 

219 
lemma NSLIM_scaleR: 

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

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

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

223 

20755  224 
lemma NSLIM_add: 
225 
"[ f  x NS> l; g  x NS> m ] 

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

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

228 

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

230 
by (simp add: NSLIM_def) 

231 

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

233 
by (simp add: NSLIM_def) 

234 

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

236 
by (simp only: NSLIM_add NSLIM_minus) 

237 

238 
lemma NSLIM_inverse: 

239 
fixes L :: "'a::real_normed_div_algebra" 

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

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

242 
apply (simp add: NSLIM_def, clarify) 

243 
apply (drule spec) 

244 
apply (auto simp add: star_of_approx_inverse) 

245 
done 

246 

247 
lemma NSLIM_zero: 

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

249 
proof  

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

251 
by (rule NSLIM_add_minus [OF f NSLIM_const]) 

252 
thus ?thesis by simp 

253 
qed 

254 

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

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

257 
apply (auto simp add: diff_minus add_assoc) 

258 
done 

259 

260 
lemma NSLIM_const_not_eq: 

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

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

263 
apply (simp add: NSLIM_def) 

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

265 
apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym] 

266 
simp add: hypreal_epsilon_not_zero) 

267 
done 

268 

269 
lemma NSLIM_not_zero: 

270 
fixes a :: real 

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

272 
by (rule NSLIM_const_not_eq) 

273 

274 
lemma NSLIM_const_eq: 

275 
fixes a :: real 

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

277 
apply (rule ccontr) 

278 
apply (blast dest: NSLIM_const_not_eq) 

279 
done 

280 

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

282 
lemma NSLIM_unique: 

283 
fixes a :: real 

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

285 
apply (drule NSLIM_minus) 

286 
apply (drule NSLIM_add, assumption) 

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

288 
apply (simp add: diff_def [symmetric]) 

289 
done 

290 

291 
lemma NSLIM_mult_zero: 

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

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

294 
by (drule NSLIM_mult, auto) 

295 

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

297 
by (simp add: NSLIM_def) 

298 

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

300 

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

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

302 
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

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

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

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

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

307 
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

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

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

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

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

312 
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

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

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

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

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

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

318 
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

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

320 
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

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

322 
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

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

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

325 
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

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

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

328 

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

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

330 
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

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

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

333 
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

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

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

336 
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

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

338 
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

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

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

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

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

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

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

345 
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

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

347 
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

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

349 
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

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

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

352 
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

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

354 
qed 
14477  355 

15228  356 
theorem LIM_NSLIM_iff: "(f  x > L) = (f  x NS> L)" 
14477  357 
by (blast intro: LIM_NSLIM NSLIM_LIM) 
358 

20755  359 
subsubsection {* Derived theorems about @{term LIM} *} 
14477  360 

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

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

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

364 
==> (%x. f(x) * g(x))  x > (l * m)" 
14477  365 
by (simp add: LIM_NSLIM_iff NSLIM_mult) 
366 

20794  367 
lemma LIM_scaleR: 
368 
"[ f  x > l; g  x > m ] 

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

370 
by (simp add: LIM_NSLIM_iff NSLIM_scaleR) 

371 

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

14477  374 
by (simp add: LIM_NSLIM_iff NSLIM_add) 
375 

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

377 
by (simp add: LIM_NSLIM_iff) 

378 

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

380 
by (simp add: LIM_NSLIM_iff NSLIM_minus) 

381 

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

383 
by (simp add: LIM_NSLIM_iff NSLIM_add_minus) 

384 

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

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

386 
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

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

388 
==> (%x. inverse(f(x)))  a > (inverse L)" 
14477  389 
by (simp add: LIM_NSLIM_iff NSLIM_inverse) 
390 

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

392 
by (simp add: LIM_NSLIM_iff NSLIM_zero) 

393 

394 
lemma LIM_zero_cancel: "(%x. f(x)  l)  x > 0 ==> f  x > l" 

395 
apply (drule_tac g = "%x. l" and M = l in LIM_add) 

396 
apply (auto simp add: diff_minus add_assoc) 

397 
done 

398 

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

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

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

401 
shows "[ f  a > L; f  a > M ] ==> L = M" 
14477  402 
by (simp add: LIM_NSLIM_iff NSLIM_unique) 
403 

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

405 
(* for standard definition of limit *) 

406 

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

407 
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

408 
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

409 
shows "[ f  x > 0; g  x > 0 ] ==> (%x. f(x)*g(x))  x > 0" 
14477  410 
by (drule LIM_mult2, auto) 
411 

412 

20755  413 
subsection {* Continuity *} 
14477  414 

415 
lemma isNSContD: "[ isNSCont f a; y \<approx> hypreal_of_real a ] ==> ( *f* f) y \<approx> hypreal_of_real (f a)" 

416 
by (simp add: isNSCont_def) 

417 

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

419 
by (simp add: isNSCont_def NSLIM_def) 

420 

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

422 
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

423 
apply (case_tac "y = star_of a", auto) 
14477  424 
done 
425 

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

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

430 

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

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

435 

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

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

440 
apply (rule isNSCont_LIM_iff) 

441 
done 

442 

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

446 

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

450 

451 
text{*Alternative definition of continuity*} 

452 
(* Prove equivalence between NS limits  *) 

453 
(* seems easier than using standard def *) 

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

455 
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

456 
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

457 
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

458 
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

459 
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

460 
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

461 
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

462 
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

463 
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num) 
14477  464 
done 
465 

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

467 
by (rule NSLIM_h_iff) 

468 

469 
lemma LIM_isCont_iff: "(f  a > f a) = ((%h. f(a + h))  0 > f(a))" 

470 
by (simp add: LIM_NSLIM_iff NSLIM_isCont_iff) 

471 

472 
lemma isCont_iff: "(isCont f x) = ((%h. f(x + h))  0 > f(x))" 

473 
by (simp add: isCont_def LIM_isCont_iff) 

474 

15228  475 
text{*Immediate application of nonstandard criterion for continuity can offer 
476 
very simple proofs of some standard property of continuous functions*} 

14477  477 
text{*sum continuous*} 
478 
lemma isCont_add: "[ isCont f a; isCont g a ] ==> isCont (%x. f(x) + g(x)) a" 

479 
by (auto intro: approx_add simp add: isNSCont_isCont_iff [symmetric] isNSCont_def) 

480 

481 
text{*mult continuous*} 

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

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

483 
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

484 
shows "[ isCont f a; isCont g a ] ==> isCont (%x. f(x) * g(x)) a" 
15228  485 
by (auto intro!: starfun_mult_HFinite_approx 
486 
simp del: starfun_mult [symmetric] 

14477  487 
simp add: isNSCont_isCont_iff [symmetric] isNSCont_def) 
488 

15228  489 
text{*composition of continuous functions 
490 
Note very short straightforard proof!*} 

14477  491 
lemma isCont_o: "[ isCont f a; isCont g (f a) ] ==> isCont (g o f) a" 
492 
by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_def starfun_o [symmetric]) 

493 

494 
lemma isCont_o2: "[ isCont f a; isCont g (f a) ] ==> isCont (%x. g (f x)) a" 

495 
by (auto dest: isCont_o simp add: o_def) 

496 

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

498 
by (simp add: isNSCont_def) 

499 

500 
lemma isCont_minus: "isCont f a ==> isCont (%x.  f x) a" 

501 
by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_minus) 

502 

503 
lemma isCont_inverse: 

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

504 
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

505 
shows "[ isCont f x; f x \<noteq> 0 ] ==> isCont (%x. inverse (f x)) x" 
14477  506 
apply (simp add: isCont_def) 
507 
apply (blast intro: LIM_inverse) 

508 
done 

509 

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

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

511 
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

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

515 
lemma isCont_diff: 

516 
"[ isCont f a; isCont g a ] ==> isCont (%x. f(x)  g(x)) a" 

517 
apply (simp add: diff_minus) 

518 
apply (auto intro: isCont_add isCont_minus) 

519 
done 

520 

21140  521 
lemma isCont_Id: "isCont (\<lambda>x. x) a" 
522 
by (simp only: isCont_def LIM_self) 

523 

15228  524 
lemma isCont_const [simp]: "isCont (%x. k) a" 
14477  525 
by (simp add: isCont_def) 
526 

15228  527 
lemma isNSCont_const [simp]: "isNSCont (%x. k) a" 
14477  528 
by (simp add: isNSCont_def) 
529 

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

530 
lemma isNSCont_abs [simp]: "isNSCont abs (a::real)" 
14477  531 
apply (simp add: isNSCont_def) 
532 
apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs) 

533 
done 

534 

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

535 
lemma isCont_abs [simp]: "isCont abs (a::real)" 
14477  536 
by (auto simp add: isNSCont_isCont_iff [symmetric]) 
15228  537 

14477  538 

539 
(**************************************************************** 

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

541 
(%* 

542 
Elementary topology proof for a characterisation of 

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

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

545 
is always an open set 

546 
*%) 

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

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

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

550 
by (dtac (mem_monad_approx RS approx_sym); 

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

552 
by (dtac isNSContD 1 THEN assume_tac 1) 

553 
by (dtac bspec 1 THEN assume_tac 1) 

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

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

556 
qed "isNSCont_isNSopen"; 

557 

558 
Goalw [isNSCont_def] 

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

560 
\ ==> isNSCont f x"; 

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

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

563 
[Infinitesimal_def,SReal_iff])); 

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

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

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

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

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

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

570 
qed "isNSopen_isNSCont"; 

571 

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

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

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

575 
isNSopen_isNSCont]); 

576 
qed "isNSCont_isNSopen_iff"; 

577 

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

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

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

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

582 
simpset() addsimps [isNSopen_isopen_iff RS sym, 

583 
isNSCont_isCont_iff RS sym])); 

584 
qed "isCont_isopen_iff"; 

585 
*******************************************************************) 

586 

20755  587 
subsection {* Uniform Continuity *} 
588 

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

591 

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

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

594 

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

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

596 
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

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

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

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

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

601 
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

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

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

604 
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

605 
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

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

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

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

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

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

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

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

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

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

615 
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

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

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

618 
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

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

620 
qed 
14477  621 

622 
lemma isNSUCont_isUCont: 

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

623 
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

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

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

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

627 
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

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

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

630 
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

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

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

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

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

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

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

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

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

639 
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

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

641 
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

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

643 
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

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

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

646 
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

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

648 
qed 
14477  649 

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

651 
assumes g: "isCont g l" 
20805  652 
assumes f: "f  a > l" 
653 
shows "(\<lambda>x. g (f x))  a > g l" 

654 
proof (rule LIM_I) 

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

656 
obtain s where s: "0 < s" 

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

658 
using LIM_D [OF g [unfolded isCont_def] r] by fast 

659 
obtain t where t: "0 < t" 

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

661 
using LIM_D [OF f s] by fast 

662 

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

664 
proof (rule exI, safe) 

665 
show "0 < t" using t . 

666 
next 

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

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

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

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

671 
qed 

672 
qed 

673 

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

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

675 

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

676 
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

677 
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

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

679 
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

680 
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

681 
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

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

683 
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

684 
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

685 
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

686 
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

687 
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

688 
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

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

690 
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

691 
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

692 
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

693 
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

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

695 

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

696 
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

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

698 
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

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

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

701 
assume "\<not> (X  a > L)" 
20563  702 
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) 
703 
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 

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

705 
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

706 

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

708 
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

709 
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

710 
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

711 
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

712 
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

713 
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

714 
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

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

716 

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

717 
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

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

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

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

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

722 
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

723 
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

724 
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

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

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

727 
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

728 
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

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

730 
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

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

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

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

734 
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

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

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

737 

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

738 
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

739 
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

740 

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

741 
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

742 
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

743 

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

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

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

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

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

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

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

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

751 
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

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

753 
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

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

757 
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

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

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

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

761 

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

762 
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

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

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

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

766 
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

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

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

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

770 
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

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

772 

10751  773 
end 