author  huffman 
Tue, 10 Apr 2007 22:01:19 +0200  
changeset 22627  2b093ba973bc 
parent 22613  2f119f54d150 
child 22631  7ae5a6ab7bd6 
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" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

18 
("((_)/  (_)/ > (_))" [60, 0, 60] 60) where 
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 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

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

24 
NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

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

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

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

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

29 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

30 
isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where 
19765  31 
"isCont f a = (f  a > (f a))" 
10751  32 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

33 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

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

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

37 
( *f* f) y @= star_of (f a))" 
10751  38 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

39 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

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

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

43 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

44 
isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where 
19765  45 
"isNSUCont f = (\<forall>x y. x @= y > ( *f* f) x @= ( *f* f) y)" 
10751  46 

47 

20755  48 
subsection {* Limits of Functions *} 
14477  49 

20755  50 
subsubsection {* Purely standard proofs *} 
14477  51 

52 
lemma LIM_eq: 

53 
"f  a > L = 

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

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

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

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

58 
"(!!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

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

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

61 

14477  62 
lemma LIM_D: 
63 
"[ 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

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

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

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

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

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

72 
apply (simp add: compare_rls) 

73 
done 

74 

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

77 

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

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

80 

15228  81 
lemma LIM_const [simp]: "(%x. k)  x > k" 
14477  82 
by (simp add: LIM_def) 
83 

84 
lemma LIM_add: 

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

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

88 
proof (rule LIM_I) 
14477  89 
fix r :: real 
20409  90 
assume r: "0 < r" 
14477  91 
from LIM_D [OF f half_gt_zero [OF r]] 
92 
obtain fs 

93 
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

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

97 
obtain gs 

98 
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

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

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

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

105 
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

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

108 
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

109 
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

110 
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

111 
by (blast intro: norm_diff_triangle_ineq order_le_less_trans) 
14477  112 
qed 
113 
qed 

114 

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

117 
by (drule (1) LIM_add, simp) 

118 

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

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

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

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

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

123 

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

125 
by (simp only: LIM_eq minus_diff_minus norm_minus_cancel) 
14477  126 

127 
lemma LIM_add_minus: 

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

129 
by (intro LIM_add LIM_minus) 
14477  130 

131 
lemma LIM_diff: 

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

133 
by (simp only: diff_minus LIM_add LIM_minus) 
14477  134 

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

137 

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

139 
by (simp add: LIM_def) 

140 

21399  141 
lemma LIM_zero_iff: "(\<lambda>x. f x  l)  a > 0 = f  a > l" 
142 
by (simp add: LIM_def) 

143 

21257  144 
lemma LIM_imp_LIM: 
145 
assumes f: "f  a > l" 

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

147 
shows "g  a > m" 

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

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

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

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

152 
done 

153 

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

155 
by (erule LIM_imp_LIM, simp add: norm_triangle_ineq3) 

156 

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

158 
by (drule LIM_norm, simp) 

159 

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

161 
by (erule LIM_imp_LIM, simp) 

162 

21399  163 
lemma LIM_norm_zero_iff: "(\<lambda>x. norm (f x))  a > 0 = f  a > 0" 
164 
by (rule iffI [OF LIM_norm_zero_cancel LIM_norm_zero]) 

165 

22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

166 
lemma LIM_rabs: "f  a > (l::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>)  a > \<bar>l\<bar>" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

167 
by (fold real_norm_def, rule LIM_norm) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

168 

2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

169 
lemma LIM_rabs_zero: "f  a > (0::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>)  a > 0" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

170 
by (fold real_norm_def, rule LIM_norm_zero) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

171 

2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

172 
lemma LIM_rabs_zero_cancel: "(\<lambda>x. \<bar>f x\<bar>)  a > (0::real) \<Longrightarrow> f  a > 0" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

173 
by (fold real_norm_def, rule LIM_norm_zero_cancel) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

174 

2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

175 
lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>)  a > (0::real) = f  a > 0" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

176 
by (fold real_norm_def, rule LIM_norm_zero_iff) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

177 

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

178 
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

179 
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

180 
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

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

182 
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

183 
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

184 
done 
14477  185 

21786  186 
lemmas LIM_not_zero = LIM_const_not_eq [where L = 0] 
187 

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

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

189 
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

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

192 
apply (blast dest: LIM_const_not_eq) 
14477  193 
done 
194 

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

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

196 
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

197 
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

198 
apply (drule LIM_diff, assumption) 
14477  199 
apply (auto dest!: LIM_const_eq) 
200 
done 

201 

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

203 
by (auto simp add: LIM_def) 

204 

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

206 
lemma LIM_equal: 

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

208 
by (simp add: LIM_def) 

209 

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

21399  212 
\<Longrightarrow> ((\<lambda>x. f x)  a > l) = ((\<lambda>x. g x)  b > m)" 
20796  213 
by (simp add: LIM_def) 
214 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

215 
lemma LIM_equal2: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

216 
assumes 1: "0 < R" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

217 
assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x  a) < R\<rbrakk> \<Longrightarrow> f x = g x" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

218 
shows "g  a > l \<Longrightarrow> f  a > l" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

219 
apply (unfold LIM_def, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

220 
apply (drule_tac x="r" in spec, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

221 
apply (rule_tac x="min s R" in exI, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

222 
apply (simp add: 1) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

223 
apply (simp add: 2) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

224 
done 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

225 

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

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

229 
apply (drule LIM_add, assumption) 

230 
apply (auto simp add: add_assoc) 

231 
done 

232 

21239  233 
lemma LIM_compose: 
234 
assumes g: "g  l > g l" 

235 
assumes f: "f  a > l" 

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

237 
proof (rule LIM_I) 

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

239 
obtain s where s: "0 < s" 

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

241 
using LIM_D [OF g r] by fast 

242 
obtain t where t: "0 < t" 

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

244 
using LIM_D [OF f s] by fast 

245 

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

247 
proof (rule exI, safe) 

248 
show "0 < t" using t . 

249 
next 

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

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

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

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

254 
qed 

255 
qed 

256 

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

258 
unfolding o_def by (rule LIM_compose) 

259 

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

260 
lemma real_LIM_sandwich_zero: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

261 
fixes f g :: "'a::real_normed_vector \<Rightarrow> real" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

262 
assumes f: "f  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

263 
assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

264 
assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

265 
shows "g  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

266 
proof (rule LIM_imp_LIM [OF f]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

267 
fix x assume x: "x \<noteq> a" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

268 
have "norm (g x  0) = g x" by (simp add: 1 x) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

269 
also have "g x \<le> f x" by (rule 2 [OF x]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

270 
also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

271 
also have "\<bar>f x\<bar> = norm (f x  0)" by simp 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

272 
finally show "norm (g x  0) \<le> norm (f x  0)" . 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

273 
qed 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

274 

22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21810
diff
changeset

275 
text {* Bounded Linear Operators *} 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

276 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

277 
lemma (in bounded_linear) cont: "f  a > f a" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

278 
proof (rule LIM_I) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

279 
fix r::real assume r: "0 < r" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

280 
obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

281 
using pos_bounded by fast 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

282 
show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x  a) < s \<longrightarrow> norm (f x  f a) < r" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

283 
proof (rule exI, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

284 
from r K show "0 < r / K" by (rule divide_pos_pos) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

285 
next 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

286 
fix x assume x: "norm (x  a) < r / K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

287 
have "norm (f x  f a) = norm (f (x  a))" by (simp only: diff) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

288 
also have "\<dots> \<le> norm (x  a) * K" by (rule norm_le) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

289 
also from K x have "\<dots> < r" by (simp only: pos_less_divide_eq) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

290 
finally show "norm (f x  f a) < r" . 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

291 
qed 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

292 
qed 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

293 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

294 
lemma (in bounded_linear) LIM: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

295 
"g  a > l \<Longrightarrow> (\<lambda>x. f (g x))  a > f l" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

296 
by (rule LIM_compose [OF cont]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

297 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

298 
lemma (in bounded_linear) LIM_zero: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

299 
"g  a > 0 \<Longrightarrow> (\<lambda>x. f (g x))  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

300 
by (drule LIM, simp only: zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

301 

22442
15d9ed9b5051
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
huffman
parents:
21810
diff
changeset

302 
text {* Bounded Bilinear Operators *} 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

303 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

304 
lemma (in bounded_bilinear) LIM_prod_zero: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

305 
assumes f: "f  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

306 
assumes g: "g  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

307 
shows "(\<lambda>x. f x ** g x)  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

308 
proof (rule LIM_I) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

309 
fix r::real assume r: "0 < r" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

310 
obtain K where K: "0 < K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

311 
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

312 
using pos_bounded by fast 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

313 
from K have K': "0 < inverse K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

314 
by (rule positive_imp_inverse_positive) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

315 
obtain s where s: "0 < s" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

316 
and norm_f: "\<And>x. \<lbrakk>x \<noteq> a; norm (x  a) < s\<rbrakk> \<Longrightarrow> norm (f x) < r" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

317 
using LIM_D [OF f r] by auto 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

318 
obtain t where t: "0 < t" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

319 
and norm_g: "\<And>x. \<lbrakk>x \<noteq> a; norm (x  a) < t\<rbrakk> \<Longrightarrow> norm (g x) < inverse K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

320 
using LIM_D [OF g K'] by auto 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

321 
show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x  a) < s \<longrightarrow> norm (f x ** g x  0) < r" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

322 
proof (rule exI, safe) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

323 
from s t show "0 < min s t" by simp 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

324 
next 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

325 
fix x assume x: "x \<noteq> a" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

326 
assume "norm (x  a) < min s t" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

327 
hence xs: "norm (x  a) < s" and xt: "norm (x  a) < t" by simp_all 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

328 
from x xs have 1: "norm (f x) < r" by (rule norm_f) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

329 
from x xt have 2: "norm (g x) < inverse K" by (rule norm_g) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

330 
have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" by (rule norm_le) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

331 
also from 1 2 K have "\<dots> < r * inverse K * K" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

332 
by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

333 
also from K have "r * inverse K * K = r" by simp 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

334 
finally show "norm (f x ** g x  0) < r" by simp 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

335 
qed 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

336 
qed 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

337 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

338 
lemma (in bounded_bilinear) LIM_left_zero: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

339 
"f  a > 0 \<Longrightarrow> (\<lambda>x. f x ** c)  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

340 
by (rule bounded_linear.LIM_zero [OF bounded_linear_left]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

341 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

342 
lemma (in bounded_bilinear) LIM_right_zero: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

343 
"f  a > 0 \<Longrightarrow> (\<lambda>x. c ** f x)  a > 0" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

344 
by (rule bounded_linear.LIM_zero [OF bounded_linear_right]) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

345 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

346 
lemma (in bounded_bilinear) LIM: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

347 
"\<lbrakk>f  a > L; g  a > M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x)  a > L ** M" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

348 
apply (drule LIM_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

349 
apply (drule LIM_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

350 
apply (rule LIM_zero_cancel) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

351 
apply (subst prod_diff_prod) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

352 
apply (rule LIM_add_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

353 
apply (rule LIM_add_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

354 
apply (erule (1) LIM_prod_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

355 
apply (erule LIM_left_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

356 
apply (erule LIM_right_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

357 
done 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

358 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

359 
lemmas LIM_mult = bounded_bilinear_mult.LIM 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

360 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

361 
lemmas LIM_mult_zero = bounded_bilinear_mult.LIM_prod_zero 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

362 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

363 
lemmas LIM_mult_left_zero = bounded_bilinear_mult.LIM_left_zero 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

364 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

365 
lemmas LIM_mult_right_zero = bounded_bilinear_mult.LIM_right_zero 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

366 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

367 
lemmas LIM_scaleR = bounded_bilinear_scaleR.LIM 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

368 

22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

369 
lemmas LIM_of_real = bounded_linear_of_real.LIM 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

370 

2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

371 
lemma LIM_power: 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

372 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

373 
assumes f: "f  a > l" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

374 
shows "(\<lambda>x. f x ^ n)  a > l ^ n" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

375 
by (induct n, simp, simp add: power_Suc LIM_mult f) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

376 

20755  377 
subsubsection {* Purely nonstandard proofs *} 
14477  378 

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

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

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

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

382 
by (simp add: NSLIM_def) 
14477  383 

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

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

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

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

387 
by (simp add: NSLIM_def) 
14477  388 

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

391 

392 
lemma NSLIM_mult: 

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

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

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

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

397 

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

400 
by transfer (rule refl) 

401 

402 
lemma NSLIM_scaleR: 

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

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

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

406 

20755  407 
lemma NSLIM_add: 
408 
"[ f  x NS> l; g  x NS> m ] 

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

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

411 

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

413 
by (simp add: NSLIM_def) 

414 

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

416 
by (simp add: NSLIM_def) 

417 

21786  418 
lemma NSLIM_diff: 
419 
"\<lbrakk>f  x NS> l; g  x NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x  g x)  x NS> (l  m)" 

420 
by (simp only: diff_def NSLIM_add NSLIM_minus) 

421 

20755  422 
lemma NSLIM_add_minus: "[ f  x NS> l; g  x NS> m ] ==> (%x. f(x) + g(x))  x NS> (l + m)" 
423 
by (simp only: NSLIM_add NSLIM_minus) 

424 

425 
lemma NSLIM_inverse: 

426 
fixes L :: "'a::real_normed_div_algebra" 

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

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

429 
apply (simp add: NSLIM_def, clarify) 

430 
apply (drule spec) 

431 
apply (auto simp add: star_of_approx_inverse) 

432 
done 

433 

434 
lemma NSLIM_zero: 

21786  435 
assumes f: "f  a NS> l" shows "(%x. f(x)  l)  a NS> 0" 
20755  436 
proof  
21786  437 
have "(\<lambda>x. f x  l)  a NS> l  l" 
438 
by (rule NSLIM_diff [OF f NSLIM_const]) 

20755  439 
thus ?thesis by simp 
440 
qed 

441 

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

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

444 
apply (auto simp add: diff_minus add_assoc) 

445 
done 

446 

447 
lemma NSLIM_const_not_eq: 

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

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

450 
apply (simp add: NSLIM_def) 

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

452 
apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym] 

453 
simp add: hypreal_epsilon_not_zero) 

454 
done 

455 

456 
lemma NSLIM_not_zero: 

457 
fixes a :: real 

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

459 
by (rule NSLIM_const_not_eq) 

460 

461 
lemma NSLIM_const_eq: 

462 
fixes a :: real 

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

464 
apply (rule ccontr) 

465 
apply (blast dest: NSLIM_const_not_eq) 

466 
done 

467 

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

469 
lemma NSLIM_unique: 

470 
fixes a :: real 

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

472 
apply (drule NSLIM_minus) 

473 
apply (drule NSLIM_add, assumption) 

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

475 
apply (simp add: diff_def [symmetric]) 

476 
done 

477 

478 
lemma NSLIM_mult_zero: 

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

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

481 
by (drule NSLIM_mult, auto) 

482 

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

484 
by (simp add: NSLIM_def) 

485 

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

487 

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

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

489 
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

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

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

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

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

494 
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

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

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

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

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

499 
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

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

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

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

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

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

505 
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

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

507 
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

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

509 
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

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

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

512 
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

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

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

515 

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

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

517 
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

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

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

520 
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

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

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

523 
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

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

525 
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

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

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

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

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

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

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

532 
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

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

534 
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

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

536 
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

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

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

539 
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

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

541 
qed 
14477  542 

15228  543 
theorem LIM_NSLIM_iff: "(f  x > L) = (f  x NS> L)" 
14477  544 
by (blast intro: LIM_NSLIM NSLIM_LIM) 
545 

20755  546 
subsubsection {* Derived theorems about @{term LIM} *} 
14477  547 

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

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

549 
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

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

551 
==> (%x. inverse(f(x)))  a > (inverse L)" 
14477  552 
by (simp add: LIM_NSLIM_iff NSLIM_inverse) 
553 

554 

20755  555 
subsection {* Continuity *} 
14477  556 

21239  557 
subsubsection {* Purely standard proofs *} 
558 

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

560 
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) 

561 

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

563 
by (simp add: isCont_def LIM_isCont_iff) 

564 

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

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

566 
unfolding isCont_def by (rule LIM_self) 
21239  567 

21786  568 
lemma isCont_const [simp]: "isCont (\<lambda>x. k) a" 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

569 
unfolding isCont_def by (rule LIM_const) 
21239  570 

21786  571 
lemma isCont_norm: "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a" 
572 
unfolding isCont_def by (rule LIM_norm) 

573 

22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

574 
lemma isCont_rabs: "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x :: real\<bar>) a" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

575 
unfolding isCont_def by (rule LIM_rabs) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

576 

21239  577 
lemma isCont_add: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a" 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

578 
unfolding isCont_def by (rule LIM_add) 
21239  579 

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

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

581 
unfolding isCont_def by (rule LIM_minus) 
21239  582 

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

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

584 
unfolding isCont_def by (rule LIM_diff) 
21239  585 

586 
lemma isCont_mult: 

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

21786  588 
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a" 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

589 
unfolding isCont_def by (rule LIM_mult) 
21239  590 

591 
lemma isCont_inverse: 

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

21786  593 
shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a" 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

594 
unfolding isCont_def by (rule LIM_inverse) 
21239  595 

596 
lemma isCont_LIM_compose: 

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

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

598 
unfolding isCont_def by (rule LIM_compose) 
21239  599 

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

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

601 
unfolding isCont_def by (rule LIM_compose) 
21239  602 

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

21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

604 
unfolding o_def by (rule isCont_o2) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

605 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

606 
lemma (in bounded_linear) isCont: "isCont f a" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

607 
unfolding isCont_def by (rule cont) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

608 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

609 
lemma (in bounded_bilinear) isCont: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

610 
"\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a" 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

611 
unfolding isCont_def by (rule LIM) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

612 

dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

613 
lemmas isCont_scaleR = bounded_bilinear_scaleR.isCont 
21239  614 

22627
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

615 
lemma isCont_of_real: 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

616 
"isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)) a" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

617 
unfolding isCont_def by (rule LIM_of_real) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

618 

2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

619 
lemma isCont_power: 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

620 
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

621 
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a" 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

622 
unfolding isCont_def by (rule LIM_power) 
2b093ba973bc
new LIM/isCont lemmas for abs, of_real, and power
huffman
parents:
22613
diff
changeset

623 

21239  624 
subsubsection {* Nonstandard proofs *} 
625 

21786  626 
lemma isNSContD: 
627 
"\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)" 

14477  628 
by (simp add: isNSCont_def) 
629 

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

631 
by (simp add: isNSCont_def NSLIM_def) 

632 

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

634 
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

635 
apply (case_tac "y = star_of a", auto) 
14477  636 
done 
637 

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

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

642 

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

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

647 

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

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

652 
apply (rule isNSCont_LIM_iff) 

653 
done 

654 

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

658 

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

662 

663 
text{*Alternative definition of continuity*} 

664 
(* Prove equivalence between NS limits  *) 

665 
(* seems easier than using standard def *) 

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

667 
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

668 
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

669 
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

670 
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

671 
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

672 
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

673 
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

674 
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

675 
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num) 
14477  676 
done 
677 

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

679 
by (rule NSLIM_h_iff) 

680 

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

682 
by (simp add: isNSCont_def) 

683 

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

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

685 
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

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

15228  689 
lemma isNSCont_const [simp]: "isNSCont (%x. k) a" 
14477  690 
by (simp add: isNSCont_def) 
691 

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

692 
lemma isNSCont_abs [simp]: "isNSCont abs (a::real)" 
14477  693 
apply (simp add: isNSCont_def) 
21810
b2d23672b003
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
huffman
parents:
21786
diff
changeset

694 
apply (auto intro: approx_hrabs simp add: starfun_rabs_hrabs) 
14477  695 
done 
696 

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

697 
lemma isCont_abs [simp]: "isCont abs (a::real)" 
14477  698 
by (auto simp add: isNSCont_isCont_iff [symmetric]) 
15228  699 

14477  700 

701 
(**************************************************************** 

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

703 
(%* 

704 
Elementary topology proof for a characterisation of 

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

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

707 
is always an open set 

708 
*%) 

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

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

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

712 
by (dtac (mem_monad_approx RS approx_sym); 

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

714 
by (dtac isNSContD 1 THEN assume_tac 1) 

715 
by (dtac bspec 1 THEN assume_tac 1) 

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

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

718 
qed "isNSCont_isNSopen"; 

719 

720 
Goalw [isNSCont_def] 

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

722 
\ ==> isNSCont f x"; 

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

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

725 
[Infinitesimal_def,SReal_iff])); 

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

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

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

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

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

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

732 
qed "isNSopen_isNSCont"; 

733 

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

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

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

737 
isNSopen_isNSCont]); 

738 
qed "isNSCont_isNSopen_iff"; 

739 

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

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

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

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

744 
simpset() addsimps [isNSopen_isopen_iff RS sym, 

745 
isNSCont_isCont_iff RS sym])); 

746 
qed "isCont_isopen_iff"; 

747 
*******************************************************************) 

748 

20755  749 
subsection {* Uniform Continuity *} 
750 

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

753 

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

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

756 

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

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

758 
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

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

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

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

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

763 
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

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

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

766 
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

767 
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

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

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

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

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

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

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

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

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

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

777 
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

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

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

780 
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

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

782 
qed 
14477  783 

784 
lemma isNSUCont_isUCont: 

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

785 
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

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

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

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

789 
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

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

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

792 
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

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

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

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

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

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

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

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

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

801 
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

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

803 
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

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

805 
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

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

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

808 
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

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

810 
qed 
14477  811 

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

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

813 

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

814 
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

815 
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

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

817 
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

818 
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

819 
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

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

821 
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

822 
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

823 
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

824 
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

825 
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

826 
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

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

828 
from LIMSEQ_D [OF S sgz] 
21733  829 
obtain no where "\<forall>n\<ge>no. norm (S n  a) < s" by blast 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

830 
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

831 
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

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

833 

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

834 
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

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

836 
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

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

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

839 
assume "\<not> (X  a > L)" 
20563  840 
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) 
841 
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 

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

843 
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

844 

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

846 
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

847 
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

848 
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

849 
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

850 
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

851 
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

852 
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

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

854 

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

855 
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

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

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

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

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

860 
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

861 
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

862 
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

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

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

865 
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

866 
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

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

868 
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

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

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

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

872 
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

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

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

875 

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

876 
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

877 
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

878 

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

879 
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

880 
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

881 

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

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

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

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

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

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

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

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

889 
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

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

891 
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

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

895 
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

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

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

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

899 

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

900 
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

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

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

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

904 
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

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

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

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

908 
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

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

910 

10751  911 
end 