author  huffman 
Thu, 12 Feb 2009 20:36:41 0800  
changeset 29885  379e43e513c2 
parent 29803  c56a5571f60a 
child 30273  ecd6f0ca62ea 
permissions  rwrr 
10751  1 
(* Title : Lim.thy 
2 
Author : Jacques D. Fleuriot 

3 
Copyright : 1998 University of Cambridge 

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

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

7 
header{* Limits and Continuity *} 
10751  8 

15131  9 
theory Lim 
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
28952
diff
changeset

10 
imports SEQ 
15131  11 
begin 
14477  12 

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

13 
text{*Standard Definitions*} 
10751  14 

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

16 
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

17 
("((_)/  (_)/ > (_))" [60, 0, 60] 60) where 
28562  18 
[code del]: "f  a > L = 
20563  19 
(\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x  a) < s 
20 
> norm (f x  L) < r)" 

10751  21 

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

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

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

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

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

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

30 

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

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

35 
lemma LIM_eq: 

36 
"f  a > L = 

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

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

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

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

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

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

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

44 

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

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

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

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

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

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

29667  55 
apply (simp add: algebra_simps) 
20756  56 
done 
57 

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

60 

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

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

63 

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

67 
lemma LIM_add: 

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

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

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

76 
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

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

80 
obtain gs 

81 
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

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

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

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

88 
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

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

91 
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

92 
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

93 
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

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

97 

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

100 
by (drule (1) LIM_add, simp) 

101 

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

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

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

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

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

106 

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

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

110 
lemma LIM_add_minus: 

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

112 
by (intro LIM_add LIM_minus) 
14477  113 

114 
lemma LIM_diff: 

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

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

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

120 

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

122 
by (simp add: LIM_def) 

123 

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

126 

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

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

130 
shows "g  a > m" 

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

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

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

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

135 
done 

136 

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

138 
by (erule LIM_imp_LIM, simp add: norm_triangle_ineq3) 

139 

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

141 
by (drule LIM_norm, simp) 

142 

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

144 
by (erule LIM_imp_LIM, simp) 

145 

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

148 

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

149 
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

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

151 

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

152 
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

153 
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

154 

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

155 
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

156 
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

157 

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

158 
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

159 
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

160 

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

161 
lemma LIM_const_not_eq: 
23076
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

162 
fixes a :: "'a::real_normed_algebra_1" 
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

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

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

165 
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

166 
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

167 
done 
14477  168 

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

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

171 
lemma LIM_const_eq: 
23076
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

172 
fixes a :: "'a::real_normed_algebra_1" 
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

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

175 
apply (blast dest: LIM_const_not_eq) 
14477  176 
done 
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_unique: 
23076
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

179 
fixes a :: "'a::real_normed_algebra_1" 
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

180 
shows "\<lbrakk>f  a > L; f  a > M\<rbrakk> \<Longrightarrow> L = M" 
1b2acb3ccb29
generalize uniqueness of limits to class real_normed_algebra_1
huffman
parents:
23069
diff
changeset

181 
apply (drule (1) LIM_diff) 
14477  182 
apply (auto dest!: LIM_const_eq) 
183 
done 

184 

23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23040
diff
changeset

185 
lemma LIM_ident [simp]: "(\<lambda>x. x)  a > a" 
14477  186 
by (auto simp add: LIM_def) 
187 

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

189 
lemma LIM_equal: 

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

191 
by (simp add: LIM_def) 

192 

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

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

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

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

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

200 
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

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

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

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

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

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

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

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

208 

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

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

212 
apply (drule LIM_add, assumption) 

213 
apply (auto simp add: add_assoc) 

214 
done 

215 

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

218 
assumes f: "f  a > l" 

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

220 
proof (rule LIM_I) 

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

222 
obtain s where s: "0 < s" 

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

224 
using LIM_D [OF g r] by fast 

225 
obtain t where t: "0 < t" 

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

227 
using LIM_D [OF f s] by fast 

228 

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

230 
proof (rule exI, safe) 

231 
show "0 < t" using t . 

232 
next 

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

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

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

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

237 
qed 

238 
qed 

239 

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

242 
assumes g: "g  b > c" 

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

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

245 
proof (rule LIM_I) 

246 
fix r :: real 

247 
assume r: "0 < r" 

248 
obtain s where s: "0 < s" 

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

250 
using LIM_D [OF g r] by fast 

251 
obtain t where t: "0 < t" 

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

253 
using LIM_D [OF f s] by fast 

254 
obtain d where d: "0 < d" 

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

256 
using inj by fast 

257 

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

259 
proof (safe intro!: exI) 

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

261 
next 

262 
fix x 

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

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

265 
using neq_b less_s by simp_all 

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

267 
by (rule less_r) 

268 
qed 

269 
qed 

270 

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

273 

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

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

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

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

277 
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

278 
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

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

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

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

282 
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

283 
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

284 
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

285 
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

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

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

288 

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

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

290 

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

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

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

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

294 
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

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

296 
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

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

298 
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

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

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

301 
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

302 
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

303 
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

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

305 
qed 
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 

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

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

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

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

311 

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

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

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

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

315 

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

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

317 

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

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

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

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

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

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

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

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

325 
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

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

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

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

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

330 
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

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

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

333 
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

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

335 
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

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

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

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

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

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

341 
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

342 
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

343 
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

344 
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

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

346 
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

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

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

349 
qed 
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 

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

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

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

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

355 

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

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

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

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

359 

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

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

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

362 
apply (drule LIM_zero) 
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 (rule LIM_zero_cancel) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

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

366 
apply (rule LIM_add_zero) 
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 (erule (1) LIM_prod_zero) 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

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

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

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

372 

23127  373 
lemmas LIM_mult = mult.LIM 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

374 

23127  375 
lemmas LIM_mult_zero = mult.LIM_prod_zero 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

376 

23127  377 
lemmas LIM_mult_left_zero = mult.LIM_left_zero 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

378 

23127  379 
lemmas LIM_mult_right_zero = mult.LIM_right_zero 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

380 

23127  381 
lemmas LIM_scaleR = scaleR.LIM 
21282
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

382 

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

384 

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

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

386 
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

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

388 
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

389 
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

390 

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

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

392 

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

395 
assumes r: "0 < r" 

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

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

398 
proof  

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

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

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

402 
by (simp only: norm_minus_commute) 

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

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

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

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

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

408 
by (rule less_imp_inverse_less, simp) 

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

410 
by (simp add: nonzero_norm_inverse 0) 

411 
from less1 less2 r2 norm_ge_zero 

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

413 
by (rule mult_strict_mono) 

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

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

416 
qed 

417 

418 
lemma LIM_inverse_fun: 

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

420 
shows "inverse  a > inverse a" 

421 
proof (rule LIM_equal2) 

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

423 
next 

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

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

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

427 
by (simp add: nonzero_inverse_mult_distrib 

428 
nonzero_imp_inverse_nonzero 

429 
nonzero_inverse_inverse_eq mult_assoc) 

430 
next 

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

432 
apply (rule LIM_I) 

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

434 
apply (simp add: LIM_inverse_lemma) 

435 
done 

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

23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23040
diff
changeset

437 
by (intro LIM_mult LIM_ident LIM_const) 
22637  438 
hence "(\<lambda>x. inverse a * x)  a > 1" 
439 
by (simp add: a) 

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

441 
by (rule LIM_compose) 

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

443 
by simp 

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

445 
by (intro LIM_mult LIM_const) 

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

447 
by simp 

448 
qed 

449 

450 
lemma LIM_inverse: 

451 
fixes L :: "'a::real_normed_div_algebra" 

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

453 
by (rule LIM_inverse_fun [THEN LIM_compose]) 

454 

29885  455 
lemma LIM_sgn: 
456 
"\<lbrakk>f  a > l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x))  a > sgn l" 

457 
unfolding sgn_div_norm 

458 
by (simp add: LIM_scaleR LIM_inverse LIM_norm) 

459 

14477  460 

20755  461 
subsection {* Continuity *} 
14477  462 

21239  463 
subsubsection {* Purely standard proofs *} 
464 

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

466 
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) 

467 

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

469 
by (simp add: isCont_def LIM_isCont_iff) 

470 

23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23040
diff
changeset

471 
lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a" 
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23040
diff
changeset

472 
unfolding isCont_def by (rule LIM_ident) 
21239  473 

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

475 
unfolding isCont_def by (rule LIM_const) 
21239  476 

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

479 

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

480 
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

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

482 

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

484 
unfolding isCont_def by (rule LIM_add) 
21239  485 

486 
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

487 
unfolding isCont_def by (rule LIM_minus) 
21239  488 

489 
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

490 
unfolding isCont_def by (rule LIM_diff) 
21239  491 

492 
lemma isCont_mult: 

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

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

495 
unfolding isCont_def by (rule LIM_mult) 
21239  496 

497 
lemma isCont_inverse: 

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

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

500 
unfolding isCont_def by (rule LIM_inverse) 
21239  501 

502 
lemma isCont_LIM_compose: 

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

504 
unfolding isCont_def by (rule LIM_compose) 
21239  505 

23040  506 
lemma isCont_LIM_compose2: 
507 
assumes f [unfolded isCont_def]: "isCont f a" 

508 
assumes g: "g  f a > l" 

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

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

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

512 

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

514 
unfolding isCont_def by (rule LIM_compose) 
21239  515 

516 
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

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

518 

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

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

520 
unfolding isCont_def by (rule cont) 
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 
lemma (in bounded_bilinear) isCont: 
dd647b4d7952
added bounded_linear and bounded_bilinear locales
huffman
parents:
21257
diff
changeset

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

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

525 

23127  526 
lemmas isCont_scaleR = scaleR.isCont 
21239  527 

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

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

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

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

531 

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

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

533 
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

534 
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

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

536 

29885  537 
lemma isCont_sgn: 
538 
"\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a" 

539 
unfolding isCont_def by (rule LIM_sgn) 

540 

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

541 
lemma isCont_abs [simp]: "isCont abs (a::real)" 
23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
23040
diff
changeset

542 
by (rule isCont_rabs [OF isCont_ident]) 
15228  543 

29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

544 
lemma isCont_setsum: fixes A :: "nat set" assumes "finite A" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

545 
shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

546 
using `finite A` 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

547 
proof induct 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

548 
case (insert a F) show "isCont (\<lambda> x. \<Sum> i \<in> (insert a F). f i x) x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

549 
unfolding setsum_insert[OF `finite F` `a \<notin> F`] by (rule isCont_add, auto simp add: insert) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

550 
qed auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

551 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

552 
lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

553 
and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

554 
shows "0 \<le> f x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

555 
proof (rule ccontr) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

556 
assume "\<not> 0 \<le> f x" hence "f x < 0" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

557 
hence "0 <  f x / 2" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

558 
from isCont[unfolded isCont_def, THEN LIM_D, OF this] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

559 
obtain s where "s > 0" and s_D: "\<And>x'. \<lbrakk> x' \<noteq> x ; \<bar> x'  x \<bar> < s \<rbrakk> \<Longrightarrow> \<bar> f x'  f x \<bar> <  f x / 2" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

560 

c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

561 
let ?x = "x  min (s / 2) ((x  b) / 2)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

562 
have "?x < x" and "\<bar> ?x  x \<bar> < s" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

563 
using `b < x` and `0 < s` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

564 
have "b < ?x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

565 
proof (cases "s < x  b") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

566 
case True thus ?thesis using `0 < s` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

567 
next 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

568 
case False hence "s / 2 \<ge> (x  b) / 2" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

569 
from inf_absorb2[OF this, unfolded inf_real_def] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

570 
have "?x = (x + b) / 2" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

571 
thus ?thesis using `b < x` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

572 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

573 
hence "0 \<le> f ?x" using all_le `?x < x` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

574 
moreover have "\<bar>f ?x  f x\<bar> <  f x / 2" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

575 
using s_D[OF _ `\<bar> ?x  x \<bar> < s`] `?x < x` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

576 
hence "f ?x  f x <  f x / 2" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

577 
hence "f ?x < f x / 2" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

578 
hence "f ?x < 0" using `f x < 0` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

579 
thus False using `0 \<le> f ?x` by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

580 
qed 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

581 

14477  582 

20755  583 
subsection {* Uniform Continuity *} 
584 

14477  585 
lemma isUCont_isCont: "isUCont f ==> isCont f x" 
23012  586 
by (simp add: isUCont_def isCont_def LIM_def, force) 
14477  587 

23118  588 
lemma isUCont_Cauchy: 
589 
"\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))" 

590 
unfolding isUCont_def 

591 
apply (rule CauchyI) 

592 
apply (drule_tac x=e in spec, safe) 

593 
apply (drule_tac e=s in CauchyD, safe) 

594 
apply (rule_tac x=M in exI, simp) 

595 
done 

596 

597 
lemma (in bounded_linear) isUCont: "isUCont f" 

598 
unfolding isUCont_def 

599 
proof (intro allI impI) 

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

601 
obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K" 

602 
using pos_bounded by fast 

603 
show "\<exists>s>0. \<forall>x y. norm (x  y) < s \<longrightarrow> norm (f x  f y) < r" 

604 
proof (rule exI, safe) 

605 
from r K show "0 < r / K" by (rule divide_pos_pos) 

606 
next 

607 
fix x y :: 'a 

608 
assume xy: "norm (x  y) < r / K" 

609 
have "norm (f x  f y) = norm (f (x  y))" by (simp only: diff) 

610 
also have "\<dots> \<le> norm (x  y) * K" by (rule norm_le) 

611 
also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq) 

612 
finally show "norm (f x  f y) < r" . 

613 
qed 

614 
qed 

615 

616 
lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))" 

617 
by (rule isUCont [THEN isUCont_Cauchy]) 

618 

14477  619 

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

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

621 

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

622 
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

623 
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

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

625 
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

626 
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

627 
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

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

629 
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

630 
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

631 
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

632 
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

633 
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

634 
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

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

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

638 
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

639 
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

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

641 

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

642 
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

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

644 
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

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

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

647 
assume "\<not> (X  a > L)" 
20563  648 
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) 
649 
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 

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

651 
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

652 

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

654 
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

655 
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

656 
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

657 
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

658 
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

659 
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

660 
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

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

662 

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

663 
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

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

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

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

667 
(* choose no such that inverse (real (Suc n)) < e *) 
23441  668 
then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

669 
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

670 
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

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

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

673 
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

674 
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

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

676 
also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))" 
23441  677 
using mlen by auto 
21165
8fb49f668511
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
huffman
parents:
21141
diff
changeset

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

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

680 
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

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

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

683 

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

684 
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

685 
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

686 

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

687 
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

688 
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

689 

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

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

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

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

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

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

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

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

697 
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

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

699 
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

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

703 
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

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

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

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

707 

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

708 
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

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

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

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

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

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

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

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

718 

10751  719 
end 