author  huffman 
Sun, 20 May 2007 03:18:50 +0200  
changeset 23040  d329182b5966 
parent 23012  496b42cf588d 
child 23069  cdfff0241c12 
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 
22641
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
22637
diff
changeset

11 
imports SEQ 
15131  12 
begin 
14477  13 

22641
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
22637
diff
changeset

14 
text{*Standard 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 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21399
diff
changeset

24 
isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where 
19765  25 
"isCont f a = (f  a > (f a))" 
10751  26 

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

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

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

31 

20755  32 
subsection {* Limits of Functions *} 
14477  33 

20755  34 
subsubsection {* Purely standard proofs *} 
14477  35 

36 
lemma LIM_eq: 

37 
"f  a > L = 

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

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

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

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

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

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

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

45 

14477  46 
lemma LIM_D: 
47 
"[ 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

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

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

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

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

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

56 
apply (simp add: compare_rls) 

57 
done 

58 

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

61 

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

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

64 

15228  65 
lemma LIM_const [simp]: "(%x. k)  x > k" 
14477  66 
by (simp add: LIM_def) 
67 

68 
lemma LIM_add: 

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

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

72 
proof (rule LIM_I) 
14477  73 
fix r :: real 
20409  74 
assume r: "0 < r" 
14477  75 
from LIM_D [OF f half_gt_zero [OF r]] 
76 
obtain fs 

77 
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

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

81 
obtain gs 

82 
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

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

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

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

89 
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

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

92 
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

93 
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

94 
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

95 
by (blast intro: norm_diff_triangle_ineq order_le_less_trans) 
14477  96 
qed 
97 
qed 

98 

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

101 
by (drule (1) LIM_add, simp) 

102 

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

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

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

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

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

107 

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

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

111 
lemma LIM_add_minus: 

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

113 
by (intro LIM_add LIM_minus) 
14477  114 

115 
lemma LIM_diff: 

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

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

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

121 

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

123 
by (simp add: LIM_def) 

124 

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

127 

21257  128 
lemma LIM_imp_LIM: 
129 
assumes f: "f  a > l" 

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

131 
shows "g  a > m" 

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

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

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

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

136 
done 

137 

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

139 
by (erule LIM_imp_LIM, simp add: norm_triangle_ineq3) 

140 

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

142 
by (drule LIM_norm, simp) 

143 

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

145 
by (erule LIM_imp_LIM, simp) 

146 

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

149 

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

150 
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

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

152 

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

153 
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

154 
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

155 

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

156 
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

157 
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

158 

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

159 
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

160 
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

161 

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

162 
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

163 
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

164 
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

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

166 
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

167 
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

168 
done 
14477  169 

21786  170 
lemmas LIM_not_zero = LIM_const_not_eq [where L = 0] 
171 

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

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

173 
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

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

176 
apply (blast dest: LIM_const_not_eq) 
14477  177 
done 
178 

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

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

180 
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

181 
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

182 
apply (drule LIM_diff, assumption) 
14477  183 
apply (auto dest!: LIM_const_eq) 
184 
done 

185 

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

187 
by (auto simp add: LIM_def) 

188 

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

190 
lemma LIM_equal: 

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

192 
by (simp add: LIM_def) 

193 

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

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

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

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

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

201 
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

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

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

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

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

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

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

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

209 

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

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

213 
apply (drule LIM_add, assumption) 

214 
apply (auto simp add: add_assoc) 

215 
done 

216 

21239  217 
lemma LIM_compose: 
218 
assumes g: "g  l > g l" 

219 
assumes f: "f  a > l" 

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

221 
proof (rule LIM_I) 

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

223 
obtain s where s: "0 < s" 

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

225 
using LIM_D [OF g r] by fast 

226 
obtain t where t: "0 < t" 

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

228 
using LIM_D [OF f s] by fast 

229 

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

231 
proof (rule exI, safe) 

232 
show "0 < t" using t . 

233 
next 

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

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

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

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

238 
qed 

239 
qed 

240 

23040  241 
lemma LIM_compose2: 
242 
assumes f: "f  a > b" 

243 
assumes g: "g  b > c" 

244 
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x  a) < d \<longrightarrow> f x \<noteq> b" 

245 
shows "(\<lambda>x. g (f x))  a > c" 

246 
proof (rule LIM_I) 

247 
fix r :: real 

248 
assume r: "0 < r" 

249 
obtain s where s: "0 < s" 

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

251 
using LIM_D [OF g r] by fast 

252 
obtain t where t: "0 < t" 

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

254 
using LIM_D [OF f s] by fast 

255 
obtain d where d: "0 < d" 

256 
and neq_b: "\<And>x. \<lbrakk>x \<noteq> a; norm (x  a) < d\<rbrakk> \<Longrightarrow> f x \<noteq> b" 

257 
using inj by fast 

258 

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

260 
proof (safe intro!: exI) 

261 
show "0 < min d t" using d t by simp 

262 
next 

263 
fix x 

264 
assume "x \<noteq> a" and "norm (x  a) < min d t" 

265 
hence "f x \<noteq> b" and "norm (f x  b) < s" 

266 
using neq_b less_s by simp_all 

267 
thus "norm (g (f x)  c) < r" 

268 
by (rule less_r) 

269 
qed 

270 
qed 

271 

21239  272 
lemma LIM_o: "\<lbrakk>g  l > g l; f  a > l\<rbrakk> \<Longrightarrow> (g \<circ> f)  a > g l" 
273 
unfolding o_def by (rule LIM_compose) 

274 

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

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

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

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

278 
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

279 
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

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

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

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

283 
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

284 
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

285 
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

286 
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

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

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

289 

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

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

291 

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

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

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

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

295 
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

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

297 
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

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

299 
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

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

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

302 
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

303 
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

304 
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

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

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

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

308 

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

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

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

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

312 

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

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

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

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

316 

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

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

318 

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

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

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

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

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

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

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

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

326 
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

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

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

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

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

331 
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

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

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

334 
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

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

336 
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

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

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

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

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

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

342 
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

343 
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

344 
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

345 
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

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

347 
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

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

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

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

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

352 

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

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

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

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

356 

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

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

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

359 
by (rule bounded_linear.LIM_zero [OF bounded_linear_right]) 
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 
lemma (in bounded_bilinear) LIM: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

373 

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

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

375 

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

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

377 

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

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

379 

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

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

381 

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

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

383 

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

384 
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

385 

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

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

387 
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

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

389 
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

390 
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

391 

22641
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
22637
diff
changeset

392 
subsubsection {* Derived theorems about @{term LIM} *} 
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
22637
diff
changeset

393 

22637  394 
lemma LIM_inverse_lemma: 
395 
fixes x :: "'a::real_normed_div_algebra" 

396 
assumes r: "0 < r" 

397 
assumes x: "norm (x  1) < min (1/2) (r/2)" 

398 
shows "norm (inverse x  1) < r" 

399 
proof  

400 
from r have r2: "0 < r/2" by simp 

401 
from x have 0: "x \<noteq> 0" by clarsimp 

402 
from x have x': "norm (1  x) < min (1/2) (r/2)" 

403 
by (simp only: norm_minus_commute) 

404 
hence less1: "norm (1  x) < r/2" by simp 

405 
have "norm (1::'a)  norm x \<le> norm (1  x)" by (rule norm_triangle_ineq2) 

406 
also from x' have "norm (1  x) < 1/2" by simp 

407 
finally have "1/2 < norm x" by simp 

408 
hence "inverse (norm x) < inverse (1/2)" 

409 
by (rule less_imp_inverse_less, simp) 

410 
hence less2: "norm (inverse x) < 2" 

411 
by (simp add: nonzero_norm_inverse 0) 

412 
from less1 less2 r2 norm_ge_zero 

413 
have "norm (1  x) * norm (inverse x) < (r/2) * 2" 

414 
by (rule mult_strict_mono) 

415 
thus "norm (inverse x  1) < r" 

416 
by (simp only: norm_mult [symmetric] left_diff_distrib, simp add: 0) 

417 
qed 

418 

419 
lemma LIM_inverse_fun: 

420 
assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)" 

421 
shows "inverse  a > inverse a" 

422 
proof (rule LIM_equal2) 

423 
from a show "0 < norm a" by simp 

424 
next 

425 
fix x assume "norm (x  a) < norm a" 

426 
hence "x \<noteq> 0" by auto 

427 
with a show "inverse x = inverse (inverse a * x) * inverse a" 

428 
by (simp add: nonzero_inverse_mult_distrib 

429 
nonzero_imp_inverse_nonzero 

430 
nonzero_inverse_inverse_eq mult_assoc) 

431 
next 

432 
have 1: "inverse  1 > inverse (1::'a)" 

433 
apply (rule LIM_I) 

434 
apply (rule_tac x="min (1/2) (r/2)" in exI) 

435 
apply (simp add: LIM_inverse_lemma) 

436 
done 

437 
have "(\<lambda>x. inverse a * x)  a > inverse a * a" 

438 
by (intro LIM_mult LIM_self LIM_const) 

439 
hence "(\<lambda>x. inverse a * x)  a > 1" 

440 
by (simp add: a) 

441 
with 1 have "(\<lambda>x. inverse (inverse a * x))  a > inverse 1" 

442 
by (rule LIM_compose) 

443 
hence "(\<lambda>x. inverse (inverse a * x))  a > 1" 

444 
by simp 

445 
hence "(\<lambda>x. inverse (inverse a * x) * inverse a)  a > 1 * inverse a" 

446 
by (intro LIM_mult LIM_const) 

447 
thus "(\<lambda>x. inverse (inverse a * x) * inverse a)  a > inverse a" 

448 
by simp 

449 
qed 

450 

451 
lemma LIM_inverse: 

452 
fixes L :: "'a::real_normed_div_algebra" 

453 
shows "\<lbrakk>f  a > L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x))  a > inverse L" 

454 
by (rule LIM_inverse_fun [THEN LIM_compose]) 

455 

14477  456 

20755  457 
subsection {* Continuity *} 
14477  458 

21239  459 
subsubsection {* Purely standard proofs *} 
460 

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

462 
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) 

463 

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

465 
by (simp add: isCont_def LIM_isCont_iff) 

466 

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

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

468 
unfolding isCont_def by (rule LIM_self) 
21239  469 

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

471 
unfolding isCont_def by (rule LIM_const) 
21239  472 

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

475 

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

476 
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

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

478 

21239  479 
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

480 
unfolding isCont_def by (rule LIM_add) 
21239  481 

482 
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

483 
unfolding isCont_def by (rule LIM_minus) 
21239  484 

485 
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

486 
unfolding isCont_def by (rule LIM_diff) 
21239  487 

488 
lemma isCont_mult: 

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

21786  490 
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

491 
unfolding isCont_def by (rule LIM_mult) 
21239  492 

493 
lemma isCont_inverse: 

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

21786  495 
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

496 
unfolding isCont_def by (rule LIM_inverse) 
21239  497 

498 
lemma isCont_LIM_compose: 

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

500 
unfolding isCont_def by (rule LIM_compose) 
21239  501 

23040  502 
lemma isCont_LIM_compose2: 
503 
assumes f [unfolded isCont_def]: "isCont f a" 

504 
assumes g: "g  f a > l" 

505 
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x  a) < d \<longrightarrow> f x \<noteq> f a" 

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

507 
by (rule LIM_compose2 [OF f g inj]) 

508 

21239  509 
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

510 
unfolding isCont_def by (rule LIM_compose) 
21239  511 

512 
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

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

514 

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

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

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

517 

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

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

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

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

521 

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

522 
lemmas isCont_scaleR = bounded_bilinear_scaleR.isCont 
21239  523 

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

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

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

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

527 

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

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

529 
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

530 
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

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

532 

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

533 
lemma isCont_abs [simp]: "isCont abs (a::real)" 
22641
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
22637
diff
changeset

534 
by (rule isCont_rabs [OF isCont_Id]) 
15228  535 

14477  536 

20755  537 
subsection {* Uniform Continuity *} 
538 

14477  539 
lemma isUCont_isCont: "isUCont f ==> isCont f x" 
23012  540 
by (simp add: isUCont_def isCont_def LIM_def, force) 
14477  541 

542 

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

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

544 

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

545 
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

546 
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

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

548 
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

549 
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

550 
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

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

552 
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

553 
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

554 
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

555 
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

556 
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

557 
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

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

559 
from LIMSEQ_D [OF S sgz] 
21733  560 
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

561 
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

562 
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

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

564 

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

565 
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

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

567 
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

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

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

570 
assume "\<not> (X  a > L)" 
20563  571 
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) 
572 
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 

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

574 
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

575 

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

577 
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

578 
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

579 
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

580 
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

581 
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

582 
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

583 
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

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

585 

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

586 
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

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

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

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

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

591 
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

592 
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

593 
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

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

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

596 
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

597 
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

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

599 
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

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

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

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

603 
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

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

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

606 

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

607 
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

608 
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

609 

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

610 
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

611 
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

612 

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

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

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

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

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

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

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

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

620 
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

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

622 
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

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

626 
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

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

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

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

630 

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

631 
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

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

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

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

635 
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

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

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

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

639 
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

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

641 

10751  642 
end 