author  huffman 
Sun, 31 May 2009 21:59:33 0700  
changeset 31349  2261c8781f73 
parent 31336  e17f13cd1280 
child 31353  14a58e2ca374 
permissions  rwrr 
10751  1 
(* Title : SEQ.thy 
2 
Author : Jacques D. Fleuriot 

3 
Copyright : 1998 University of Cambridge 

4 
Description : Convergence of sequences and series 

15082  5 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 
22608  6 
Additional contributions by Jeremy Avigad and Brian Huffman 
15082  7 
*) 
10751  8 

22631
7ae5a6ab7bd6
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
huffman
parents:
22629
diff
changeset

9 
header {* Sequences and Convergence *} 
17439  10 

15131  11 
theory SEQ 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

12 
imports Limits 
15131  13 
begin 
10751  14 

19765  15 
definition 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

16 
sequentially :: "nat filter" where 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

17 
"sequentially = Abs_filter (\<lambda>P. \<exists>N. \<forall>n\<ge>N. P n)" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

18 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

19 
definition 
22608  20 
Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where 
21 
{*Standard definition of sequence converging to zero*} 

28562  22 
[code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)" 
22608  23 

24 
definition 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

25 
LIMSEQ :: "[nat \<Rightarrow> 'a::metric_space, 'a] \<Rightarrow> bool" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset

26 
("((_)/ > (_))" [60, 60] 60) where 
15082  27 
{*Standard definition of convergence of sequence*} 
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

28 
[code del]: "X > L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)" 
10751  29 

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

30 
definition 
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

31 
lim :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a" where 
15082  32 
{*Standard definition of limit using choice operator*} 
20682  33 
"lim X = (THE L. X > L)" 
10751  34 

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

35 
definition 
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

36 
convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where 
15082  37 
{*Standard definition of convergence*} 
20682  38 
"convergent X = (\<exists>L. X > L)" 
10751  39 

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

40 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset

41 
Bseq :: "(nat => 'a::real_normed_vector) => bool" where 
15082  42 
{*Standard definition for bounded sequence*} 
28562  43 
[code del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)" 
10751  44 

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

45 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21139
diff
changeset

46 
monoseq :: "(nat=>real)=>bool" where 
30730  47 
{*Definition of monotonicity. 
48 
The use of disjunction here complicates proofs considerably. 

49 
One alternative is to add a Boolean argument to indicate the direction. 

50 
Another is to develop the notions of increasing and decreasing first.*} 

28562  51 
[code del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n)  (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))" 
10751  52 

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

53 
definition 
30730  54 
incseq :: "(nat=>real)=>bool" where 
55 
{*Increasing sequence*} 

56 
[code del]: "incseq X = (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)" 

57 

58 
definition 

59 
decseq :: "(nat=>real)=>bool" where 

60 
{*Increasing sequence*} 

61 
[code del]: "decseq X = (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)" 

62 

63 
definition 

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

64 
subseq :: "(nat => nat) => bool" where 
15082  65 
{*Definition of subsequence*} 
28562  66 
[code del]: "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))" 
10751  67 

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

68 
definition 
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

69 
Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where 
15082  70 
{*Standard definition of the Cauchy condition*} 
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

71 
[code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)" 
10751  72 

15082  73 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

74 
subsection {* Sequentially *} 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

75 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

76 
lemma eventually_sequentially: 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

77 
"eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

78 
unfolding sequentially_def 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

79 
apply (rule eventually_Abs_filter) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

80 
apply simp 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

81 
apply (clarify, rule_tac x=N in exI, simp) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

82 
apply (clarify, rename_tac M N) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

83 
apply (rule_tac x="max M N" in exI, simp) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

84 
done 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

85 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

86 
lemma Zseq_conv_Zfun: "Zseq X \<longleftrightarrow> Zfun X sequentially" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

87 
unfolding Zseq_def Zfun_def eventually_sequentially .. 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

88 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

89 
lemma LIMSEQ_conv_tendsto: "(X > L) \<longleftrightarrow> tendsto X L sequentially" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

90 
unfolding LIMSEQ_def tendsto_def eventually_sequentially .. 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

91 

22608  92 
subsection {* Bounded Sequences *} 
93 

26312  94 
lemma BseqI': assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X" 
22608  95 
unfolding Bseq_def 
96 
proof (intro exI conjI allI) 

97 
show "0 < max K 1" by simp 

98 
next 

99 
fix n::nat 

100 
have "norm (X n) \<le> K" by (rule K) 

101 
thus "norm (X n) \<le> max K 1" by simp 

102 
qed 

103 

104 
lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 

105 
unfolding Bseq_def by auto 

106 

26312  107 
lemma BseqI2': assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X" 
108 
proof (rule BseqI') 

22608  109 
let ?A = "norm ` X ` {..N}" 
110 
have 1: "finite ?A" by simp 

111 
fix n::nat 

112 
show "norm (X n) \<le> max K (Max ?A)" 

113 
proof (cases rule: linorder_le_cases) 

114 
assume "n \<ge> N" 

115 
hence "norm (X n) \<le> K" using K by simp 

116 
thus "norm (X n) \<le> max K (Max ?A)" by simp 

117 
next 

118 
assume "n \<le> N" 

119 
hence "norm (X n) \<in> ?A" by simp 

26757
e775accff967
thms Max_ge, Min_le: dropped superfluous premise
haftmann
parents:
26312
diff
changeset

120 
with 1 have "norm (X n) \<le> Max ?A" by (rule Max_ge) 
22608  121 
thus "norm (X n) \<le> max K (Max ?A)" by simp 
122 
qed 

123 
qed 

124 

125 
lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))" 

126 
unfolding Bseq_def by auto 

127 

128 
lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X" 

129 
apply (erule BseqE) 

26312  130 
apply (rule_tac N="k" and K="K" in BseqI2') 
22608  131 
apply clarify 
132 
apply (drule_tac x="n  k" in spec, simp) 

133 
done 

134 

135 

136 
subsection {* Sequences That Converge to Zero *} 

137 

138 
lemma ZseqI: 

139 
"(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n) < r) \<Longrightarrow> Zseq X" 

140 
unfolding Zseq_def by simp 

141 

142 
lemma ZseqD: 

143 
"\<lbrakk>Zseq X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n) < r" 

144 
unfolding Zseq_def by simp 

145 

146 
lemma Zseq_zero: "Zseq (\<lambda>n. 0)" 

147 
unfolding Zseq_def by simp 

148 

149 
lemma Zseq_const_iff: "Zseq (\<lambda>n. k) = (k = 0)" 

150 
unfolding Zseq_def by force 

151 

152 
lemma Zseq_norm_iff: "Zseq (\<lambda>n. norm (X n)) = Zseq (\<lambda>n. X n)" 

153 
unfolding Zseq_def by simp 

154 

155 
lemma Zseq_imp_Zseq: 

156 
assumes X: "Zseq X" 

157 
assumes Y: "\<And>n. norm (Y n) \<le> norm (X n) * K" 

158 
shows "Zseq (\<lambda>n. Y n)" 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

159 
using assms unfolding Zseq_conv_Zfun by (rule Zfun_imp_Zfun) 
22608  160 

161 
lemma Zseq_le: "\<lbrakk>Zseq Y; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zseq X" 

162 
by (erule_tac K="1" in Zseq_imp_Zseq, simp) 

163 

164 
lemma Zseq_add: 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

165 
"Zseq X \<Longrightarrow> Zseq Y \<Longrightarrow> Zseq (\<lambda>n. X n + Y n)" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

166 
unfolding Zseq_conv_Zfun by (rule Zfun_add) 
22608  167 

168 
lemma Zseq_minus: "Zseq X \<Longrightarrow> Zseq (\<lambda>n.  X n)" 

169 
unfolding Zseq_def by simp 

170 

171 
lemma Zseq_diff: "\<lbrakk>Zseq X; Zseq Y\<rbrakk> \<Longrightarrow> Zseq (\<lambda>n. X n  Y n)" 

172 
by (simp only: diff_minus Zseq_add Zseq_minus) 

173 

174 
lemma (in bounded_linear) Zseq: 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

175 
"Zseq X \<Longrightarrow> Zseq (\<lambda>n. f (X n))" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

176 
unfolding Zseq_conv_Zfun by (rule Zfun) 
22608  177 

23127  178 
lemma (in bounded_bilinear) Zseq: 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

179 
"Zseq X \<Longrightarrow> Zseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

180 
unfolding Zseq_conv_Zfun by (rule Zfun) 
22608  181 

182 
lemma (in bounded_bilinear) Zseq_prod_Bseq: 

183 
assumes X: "Zseq X" 

184 
assumes Y: "Bseq Y" 

185 
shows "Zseq (\<lambda>n. X n ** Y n)" 

186 
proof  

187 
obtain K where K: "0 \<le> K" 

188 
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" 

189 
using nonneg_bounded by fast 

190 
obtain B where B: "0 < B" 

191 
and norm_Y: "\<And>n. norm (Y n) \<le> B" 

192 
using Y [unfolded Bseq_def] by fast 

193 
from X show ?thesis 

194 
proof (rule Zseq_imp_Zseq) 

195 
fix n::nat 

196 
have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K" 

197 
by (rule norm_le) 

198 
also have "\<dots> \<le> norm (X n) * B * K" 

199 
by (intro mult_mono' order_refl norm_Y norm_ge_zero 

200 
mult_nonneg_nonneg K) 

201 
also have "\<dots> = norm (X n) * (B * K)" 

202 
by (rule mult_assoc) 

203 
finally show "norm (X n ** Y n) \<le> norm (X n) * (B * K)" . 

204 
qed 

205 
qed 

206 

207 
lemma (in bounded_bilinear) Bseq_prod_Zseq: 

208 
assumes X: "Bseq X" 

209 
assumes Y: "Zseq Y" 

210 
shows "Zseq (\<lambda>n. X n ** Y n)" 

211 
proof  

212 
obtain K where K: "0 \<le> K" 

213 
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" 

214 
using nonneg_bounded by fast 

215 
obtain B where B: "0 < B" 

216 
and norm_X: "\<And>n. norm (X n) \<le> B" 

217 
using X [unfolded Bseq_def] by fast 

218 
from Y show ?thesis 

219 
proof (rule Zseq_imp_Zseq) 

220 
fix n::nat 

221 
have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K" 

222 
by (rule norm_le) 

223 
also have "\<dots> \<le> B * norm (Y n) * K" 

224 
by (intro mult_mono' order_refl norm_X norm_ge_zero 

225 
mult_nonneg_nonneg K) 

226 
also have "\<dots> = norm (Y n) * (B * K)" 

227 
by (simp only: mult_ac) 

228 
finally show "norm (X n ** Y n) \<le> norm (Y n) * (B * K)" . 

229 
qed 

230 
qed 

231 

23127  232 
lemma (in bounded_bilinear) Zseq_left: 
22608  233 
"Zseq X \<Longrightarrow> Zseq (\<lambda>n. X n ** a)" 
234 
by (rule bounded_linear_left [THEN bounded_linear.Zseq]) 

235 

23127  236 
lemma (in bounded_bilinear) Zseq_right: 
22608  237 
"Zseq X \<Longrightarrow> Zseq (\<lambda>n. a ** X n)" 
238 
by (rule bounded_linear_right [THEN bounded_linear.Zseq]) 

239 

23127  240 
lemmas Zseq_mult = mult.Zseq 
241 
lemmas Zseq_mult_right = mult.Zseq_right 

242 
lemmas Zseq_mult_left = mult.Zseq_left 

22608  243 

244 

20696  245 
subsection {* Limits of Sequences *} 
246 

15082  247 
lemma LIMSEQ_iff: 
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

248 
fixes L :: "'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

249 
shows "(X > L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n  L) < r)" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

250 
unfolding LIMSEQ_def dist_norm .. 
22608  251 

252 
lemma LIMSEQ_Zseq_iff: "((\<lambda>n. X n) > L) = Zseq (\<lambda>n. X n  L)" 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

253 
by (simp only: LIMSEQ_iff Zseq_def) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

254 

e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

255 
lemma metric_LIMSEQ_I: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

256 
"(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X > L" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

257 
by (simp add: LIMSEQ_def) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

258 

e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

259 
lemma metric_LIMSEQ_D: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

260 
"\<lbrakk>X > L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

261 
by (simp add: LIMSEQ_def) 
15082  262 

20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset

263 
lemma LIMSEQ_I: 
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

264 
fixes L :: "'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

265 
shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n  L) < r) \<Longrightarrow> X > L" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

266 
by (simp add: LIMSEQ_iff) 
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset

267 

93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset

268 
lemma LIMSEQ_D: 
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

269 
fixes L :: "'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

270 
shows "\<lbrakk>X > L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n  L) < r" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

271 
by (simp add: LIMSEQ_iff) 
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset

272 

22608  273 
lemma LIMSEQ_const: "(\<lambda>n. k) > k" 
20696  274 
by (simp add: LIMSEQ_def) 
275 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

276 
lemma LIMSEQ_const_iff: "(\<lambda>n. k) > l \<longleftrightarrow> k = l" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

277 
apply (safe intro!: LIMSEQ_const) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

278 
apply (rule ccontr) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

279 
apply (drule_tac r="dist k l" in metric_LIMSEQ_D) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

280 
apply (simp add: zero_less_dist_iff) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

281 
apply auto 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

282 
done 
22608  283 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

284 
lemma LIMSEQ_norm: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

285 
fixes a :: "'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

286 
shows "X > a \<Longrightarrow> (\<lambda>n. norm (X n)) > norm a" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

287 
unfolding LIMSEQ_conv_tendsto by (rule tendsto_norm) 
20696  288 

22615  289 
lemma LIMSEQ_ignore_initial_segment: 
290 
"f > a \<Longrightarrow> (\<lambda>n. f (n + k)) > a" 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

291 
apply (rule metric_LIMSEQ_I) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

292 
apply (drule (1) metric_LIMSEQ_D) 
22615  293 
apply (erule exE, rename_tac N) 
294 
apply (rule_tac x=N in exI) 

295 
apply simp 

296 
done 

20696  297 

22615  298 
lemma LIMSEQ_offset: 
299 
"(\<lambda>n. f (n + k)) > a \<Longrightarrow> f > a" 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

300 
apply (rule metric_LIMSEQ_I) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

301 
apply (drule (1) metric_LIMSEQ_D) 
22615  302 
apply (erule exE, rename_tac N) 
303 
apply (rule_tac x="N + k" in exI) 

304 
apply clarify 

305 
apply (drule_tac x="n  k" in spec) 

306 
apply (simp add: le_diff_conv2) 

20696  307 
done 
308 

22615  309 
lemma LIMSEQ_Suc: "f > l \<Longrightarrow> (\<lambda>n. f (Suc n)) > l" 
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset

310 
by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp) 
22615  311 

312 
lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) > l \<Longrightarrow> f > l" 

30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29803
diff
changeset

313 
by (rule_tac k="Suc 0" in LIMSEQ_offset, simp) 
22615  314 

315 
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) > l = f > l" 

316 
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc) 

317 

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

318 
lemma LIMSEQ_linear: "\<lbrakk> X > x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) > x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

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

320 
by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

321 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

322 
lemma LIMSEQ_add: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

323 
fixes a b :: "'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

324 
shows "\<lbrakk>X > a; Y > b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n + Y n) > a + b" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

325 
unfolding LIMSEQ_conv_tendsto by (rule tendsto_add) 
22608  326 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

327 
lemma LIMSEQ_minus: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

328 
fixes a :: "'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

329 
shows "X > a \<Longrightarrow> (\<lambda>n.  X n) >  a" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

330 
unfolding LIMSEQ_conv_tendsto by (rule tendsto_minus) 
22608  331 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

332 
lemma LIMSEQ_minus_cancel: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

333 
fixes a :: "'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

334 
shows "(\<lambda>n.  X n) >  a \<Longrightarrow> X > a" 
22608  335 
by (drule LIMSEQ_minus, simp) 
336 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

337 
lemma LIMSEQ_diff: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

338 
fixes a b :: "'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

339 
shows "\<lbrakk>X > a; Y > b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n  Y n) > a  b" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

340 
unfolding LIMSEQ_conv_tendsto by (rule tendsto_diff) 
22608  341 

342 
lemma LIMSEQ_unique: "\<lbrakk>X > a; X > b\<rbrakk> \<Longrightarrow> a = b" 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

343 
apply (rule ccontr) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

344 
apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

345 
apply (drule_tac r="dist a b / 2" in metric_LIMSEQ_D, simp add: zero_less_dist_iff) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

346 
apply (clarify, rename_tac M N) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

347 
apply (subgoal_tac "dist a b < dist a b / 2 + dist a b / 2", simp) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

348 
apply (subgoal_tac "dist a b \<le> dist (X (max M N)) a + dist (X (max M N)) b") 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

349 
apply (erule le_less_trans, rule add_strict_mono, simp, simp) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

350 
apply (subst dist_commute, rule dist_triangle) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

351 
done 
22608  352 

353 
lemma (in bounded_linear) LIMSEQ: 

354 
"X > a \<Longrightarrow> (\<lambda>n. f (X n)) > f a" 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

355 
unfolding LIMSEQ_conv_tendsto by (rule tendsto) 
22608  356 

357 
lemma (in bounded_bilinear) LIMSEQ: 

358 
"\<lbrakk>X > a; Y > b\<rbrakk> \<Longrightarrow> (\<lambda>n. X n ** Y n) > a ** b" 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
31336
diff
changeset

359 
unfolding LIMSEQ_conv_tendsto by (rule tendsto) 
22608  360 

361 
lemma LIMSEQ_mult: 

362 
fixes a b :: "'a::real_normed_algebra" 

363 
shows "[ X > a; Y > b ] ==> (%n. X n * Y n) > a * b" 

23127  364 
by (rule mult.LIMSEQ) 
22608  365 

366 
lemma inverse_diff_inverse: 

367 
"\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk> 

368 
\<Longrightarrow> inverse a  inverse b =  (inverse a * (a  b) * inverse b)" 

29667  369 
by (simp add: algebra_simps) 
22608  370 

371 
lemma Bseq_inverse_lemma: 

372 
fixes x :: "'a::real_normed_div_algebra" 

373 
shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r" 

374 
apply (subst nonzero_norm_inverse, clarsimp) 

375 
apply (erule (1) le_imp_inverse_le) 

376 
done 

377 

378 
lemma Bseq_inverse: 

379 
fixes a :: "'a::real_normed_div_algebra" 

380 
assumes X: "X > a" 

381 
assumes a: "a \<noteq> 0" 

382 
shows "Bseq (\<lambda>n. inverse (X n))" 

383 
proof  

384 
from a have "0 < norm a" by simp 

385 
hence "\<exists>r>0. r < norm a" by (rule dense) 

386 
then obtain r where r1: "0 < r" and r2: "r < norm a" by fast 

387 
obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (X n  a) < r" 

388 
using LIMSEQ_D [OF X r1] by fast 

389 
show ?thesis 

26312  390 
proof (rule BseqI2' [rule_format]) 
22608  391 
fix n assume n: "N \<le> n" 
392 
hence 1: "norm (X n  a) < r" by (rule N) 

393 
hence 2: "X n \<noteq> 0" using r2 by auto 

394 
hence "norm (inverse (X n)) = inverse (norm (X n))" 

395 
by (rule nonzero_norm_inverse) 

396 
also have "\<dots> \<le> inverse (norm a  r)" 

397 
proof (rule le_imp_inverse_le) 

398 
show "0 < norm a  r" using r2 by simp 

399 
next 

400 
have "norm a  norm (X n) \<le> norm (a  X n)" 

401 
by (rule norm_triangle_ineq2) 

402 
also have "\<dots> = norm (X n  a)" 

403 
by (rule norm_minus_commute) 

404 
also have "\<dots> < r" using 1 . 

405 
finally show "norm a  r \<le> norm (X n)" by simp 

406 
qed 

407 
finally show "norm (inverse (X n)) \<le> inverse (norm a  r)" . 

408 
qed 

409 
qed 

410 

411 
lemma LIMSEQ_inverse_lemma: 

412 
fixes a :: "'a::real_normed_div_algebra" 

413 
shows "\<lbrakk>X > a; a \<noteq> 0; \<forall>n. X n \<noteq> 0\<rbrakk> 

414 
\<Longrightarrow> (\<lambda>n. inverse (X n)) > inverse a" 

415 
apply (subst LIMSEQ_Zseq_iff) 

416 
apply (simp add: inverse_diff_inverse nonzero_imp_inverse_nonzero) 

417 
apply (rule Zseq_minus) 

418 
apply (rule Zseq_mult_left) 

23127  419 
apply (rule mult.Bseq_prod_Zseq) 
22608  420 
apply (erule (1) Bseq_inverse) 
421 
apply (simp add: LIMSEQ_Zseq_iff) 

422 
done 

423 

424 
lemma LIMSEQ_inverse: 

425 
fixes a :: "'a::real_normed_div_algebra" 

426 
assumes X: "X > a" 

427 
assumes a: "a \<noteq> 0" 

428 
shows "(\<lambda>n. inverse (X n)) > inverse a" 

429 
proof  

430 
from a have "0 < norm a" by simp 

431 
then obtain k where "\<forall>n\<ge>k. norm (X n  a) < norm a" 

432 
using LIMSEQ_D [OF X] by fast 

433 
hence "\<forall>n\<ge>k. X n \<noteq> 0" by auto 

434 
hence k: "\<forall>n. X (n + k) \<noteq> 0" by simp 

435 

436 
from X have "(\<lambda>n. X (n + k)) > a" 

437 
by (rule LIMSEQ_ignore_initial_segment) 

438 
hence "(\<lambda>n. inverse (X (n + k))) > inverse a" 

439 
using a k by (rule LIMSEQ_inverse_lemma) 

440 
thus "(\<lambda>n. inverse (X n)) > inverse a" 

441 
by (rule LIMSEQ_offset) 

442 
qed 

443 

444 
lemma LIMSEQ_divide: 

445 
fixes a b :: "'a::real_normed_field" 

446 
shows "\<lbrakk>X > a; Y > b; b \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. X n / Y n) > a / b" 

447 
by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse) 

448 

449 
lemma LIMSEQ_pow: 

31017  450 
fixes a :: "'a::{power, real_normed_algebra}" 
22608  451 
shows "X > a \<Longrightarrow> (\<lambda>n. (X n) ^ m) > a ^ m" 
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
30242
diff
changeset

452 
by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult) 
22608  453 

454 
lemma LIMSEQ_setsum: 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

455 
fixes L :: "'a \<Rightarrow> 'b::real_normed_vector" 
22608  456 
assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n > L n" 
457 
shows "(\<lambda>m. \<Sum>n\<in>S. X n m) > (\<Sum>n\<in>S. L n)" 

458 
proof (cases "finite S") 

459 
case True 

460 
thus ?thesis using n 

461 
proof (induct) 

462 
case empty 

463 
show ?case 

464 
by (simp add: LIMSEQ_const) 

465 
next 

466 
case insert 

467 
thus ?case 

468 
by (simp add: LIMSEQ_add) 

469 
qed 

470 
next 

471 
case False 

472 
thus ?thesis 

473 
by (simp add: LIMSEQ_const) 

474 
qed 

475 

476 
lemma LIMSEQ_setprod: 

477 
fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}" 

478 
assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n > L n" 

479 
shows "(\<lambda>m. \<Prod>n\<in>S. X n m) > (\<Prod>n\<in>S. L n)" 

480 
proof (cases "finite S") 

481 
case True 

482 
thus ?thesis using n 

483 
proof (induct) 

484 
case empty 

485 
show ?case 

486 
by (simp add: LIMSEQ_const) 

487 
next 

488 
case insert 

489 
thus ?case 

490 
by (simp add: LIMSEQ_mult) 

491 
qed 

492 
next 

493 
case False 

494 
thus ?thesis 

495 
by (simp add: setprod_def LIMSEQ_const) 

496 
qed 

497 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

498 
lemma LIMSEQ_add_const: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

499 
fixes a :: "'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

500 
shows "f > a ==> (%n.(f n + b)) > a + b" 
22614  501 
by (simp add: LIMSEQ_add LIMSEQ_const) 
502 

503 
(* FIXME: delete *) 

504 
lemma LIMSEQ_add_minus: 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

505 
fixes a b :: "'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

506 
shows "[ X > a; Y > b ] ==> (%n. X n + Y n) > a + b" 
22614  507 
by (simp only: LIMSEQ_add LIMSEQ_minus) 
508 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

509 
lemma LIMSEQ_diff_const: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

510 
fixes a b :: "'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

511 
shows "f > a ==> (%n.(f n  b)) > a  b" 
22614  512 
by (simp add: LIMSEQ_diff LIMSEQ_const) 
513 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

514 
lemma LIMSEQ_diff_approach_zero: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

515 
fixes L :: "'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

516 
shows "g > L ==> (%x. f x  g x) > 0 ==> f > L" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

517 
by (drule (1) LIMSEQ_add, simp) 
22614  518 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

519 
lemma LIMSEQ_diff_approach_zero2: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

520 
fixes L :: "'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

521 
shows "f > L ==> (%x. f x  g x) > 0 ==> g > L"; 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

522 
by (drule (1) LIMSEQ_diff, simp) 
22614  523 

524 
text{*A sequence tends to zero iff its abs does*} 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

525 
lemma LIMSEQ_norm_zero: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

526 
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

527 
shows "((\<lambda>n. norm (X n)) > 0) \<longleftrightarrow> (X > 0)" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

528 
by (simp add: LIMSEQ_iff) 
22614  529 

530 
lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) > 0) = (f > (0::real))" 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

531 
by (simp add: LIMSEQ_iff) 
22614  532 

533 
lemma LIMSEQ_imp_rabs: "f > (l::real) ==> (%n. \<bar>f n\<bar>) > \<bar>l\<bar>" 

534 
by (drule LIMSEQ_norm, simp) 

535 

536 
text{*An unbounded sequence's inverse tends to 0*} 

537 

538 
lemma LIMSEQ_inverse_zero: 

22974  539 
"\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) > 0" 
540 
apply (rule LIMSEQ_I) 

541 
apply (drule_tac x="inverse r" in spec, safe) 

542 
apply (rule_tac x="N" in exI, safe) 

543 
apply (drule_tac x="n" in spec, safe) 

22614  544 
apply (frule positive_imp_inverse_positive) 
22974  545 
apply (frule (1) less_imp_inverse_less) 
546 
apply (subgoal_tac "0 < X n", simp) 

547 
apply (erule (1) order_less_trans) 

22614  548 
done 
549 

550 
text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*} 

551 

552 
lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) > 0" 

553 
apply (rule LIMSEQ_inverse_zero, safe) 

22974  554 
apply (cut_tac x = r in reals_Archimedean2) 
22614  555 
apply (safe, rule_tac x = n in exI) 
556 
apply (auto simp add: real_of_nat_Suc) 

557 
done 

558 

559 
text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to 

560 
infinity is now easily proved*} 

561 

562 
lemma LIMSEQ_inverse_real_of_nat_add: 

563 
"(%n. r + inverse(real(Suc n))) > r" 

564 
by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) 

565 

566 
lemma LIMSEQ_inverse_real_of_nat_add_minus: 

567 
"(%n. r + inverse(real(Suc n))) > r" 

568 
by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) 

569 

570 
lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: 

571 
"(%n. r*( 1 + inverse(real(Suc n)))) > r" 

572 
by (cut_tac b=1 in 

573 
LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto) 

574 

22615  575 
lemma LIMSEQ_le_const: 
576 
"\<lbrakk>X > (x::real); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x" 

577 
apply (rule ccontr, simp only: linorder_not_le) 

578 
apply (drule_tac r="a  x" in LIMSEQ_D, simp) 

579 
apply clarsimp 

580 
apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI1) 

581 
apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI2) 

582 
apply simp 

583 
done 

584 

585 
lemma LIMSEQ_le_const2: 

586 
"\<lbrakk>X > (x::real); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a" 

587 
apply (subgoal_tac " a \<le>  x", simp) 

588 
apply (rule LIMSEQ_le_const) 

589 
apply (erule LIMSEQ_minus) 

590 
apply simp 

591 
done 

592 

593 
lemma LIMSEQ_le: 

594 
"\<lbrakk>X > x; Y > y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)" 

595 
apply (subgoal_tac "0 \<le> y  x", simp) 

596 
apply (rule LIMSEQ_le_const) 

597 
apply (erule (1) LIMSEQ_diff) 

598 
apply (simp add: le_diff_eq) 

599 
done 

600 

15082  601 

20696  602 
subsection {* Convergence *} 
15082  603 

604 
lemma limI: "X > L ==> lim X = L" 

605 
apply (simp add: lim_def) 

606 
apply (blast intro: LIMSEQ_unique) 

607 
done 

608 

609 
lemma convergentD: "convergent X ==> \<exists>L. (X > L)" 

610 
by (simp add: convergent_def) 

611 

612 
lemma convergentI: "(X > L) ==> convergent X" 

613 
by (auto simp add: convergent_def) 

614 

615 
lemma convergent_LIMSEQ_iff: "convergent X = (X > lim X)" 

20682  616 
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def) 
15082  617 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

618 
lemma convergent_minus_iff: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

619 
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

620 
shows "convergent X \<longleftrightarrow> convergent (\<lambda>n.  X n)" 
20696  621 
apply (simp add: convergent_def) 
622 
apply (auto dest: LIMSEQ_minus) 

623 
apply (drule LIMSEQ_minus, auto) 

624 
done 

625 

30196
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

626 
text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *} 
20696  627 

30196
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

628 
lemma nat_function_unique: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

629 
unfolding Ex1_def 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

630 
apply (rule_tac x="nat_rec e f" in exI) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

631 
apply (rule conjI)+ 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

632 
apply (rule def_nat_rec_0, simp) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

633 
apply (rule allI, rule def_nat_rec_Suc, simp) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

634 
apply (rule allI, rule impI, rule ext) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

635 
apply (erule conjE) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

636 
apply (induct_tac x) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

637 
apply (simp add: nat_rec_0) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

638 
apply (erule_tac x="n" in allE) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

639 
apply (simp) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

640 
done 
20696  641 

15082  642 
text{*Subsequence (alternative definition, (e.g. Hoskins)*} 
643 

644 
lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))" 

645 
apply (simp add: subseq_def) 

646 
apply (auto dest!: less_imp_Suc_add) 

647 
apply (induct_tac k) 

648 
apply (auto intro: less_trans) 

649 
done 

650 

651 
lemma monoseq_Suc: 

652 
"monoseq X = ((\<forall>n. X n \<le> X (Suc n)) 

653 
 (\<forall>n. X (Suc n) \<le> X n))" 

654 
apply (simp add: monoseq_def) 

655 
apply (auto dest!: le_imp_less_or_eq) 

656 
apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add) 

657 
apply (induct_tac "ka") 

658 
apply (auto intro: order_trans) 

18585  659 
apply (erule contrapos_np) 
15082  660 
apply (induct_tac "k") 
661 
apply (auto intro: order_trans) 

662 
done 

663 

15360  664 
lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X" 
15082  665 
by (simp add: monoseq_def) 
666 

15360  667 
lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X" 
15082  668 
by (simp add: monoseq_def) 
669 

670 
lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X" 

671 
by (simp add: monoseq_Suc) 

672 

673 
lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X" 

674 
by (simp add: monoseq_Suc) 

675 

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

676 
lemma monoseq_minus: assumes "monoseq a" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

677 
shows "monoseq (\<lambda> n.  a n)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

678 
proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

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

680 
hence "\<forall> m. \<forall> n \<ge> m.  a n \<le>  a m" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

681 
thus ?thesis by (rule monoI2) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

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

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

684 
hence "\<forall> m. \<forall> n \<ge> m.  a m \<le>  a n" using `monoseq a`[unfolded monoseq_def] by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

685 
thus ?thesis by (rule monoI1) 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

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

687 

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

688 
lemma monoseq_le: assumes "monoseq a" and "a > x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

689 
shows "((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or> 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

690 
((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

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

692 
{ fix x n fix a :: "nat \<Rightarrow> real" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

693 
assume "a > x" and "\<forall> m. \<forall> n \<ge> m. a m \<le> a n" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

694 
hence monotone: "\<And> m n. m \<le> n \<Longrightarrow> a m \<le> a n" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

695 
have "a n \<le> x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

696 
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

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

698 
hence "0 < a n  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

699 
from `a > x`[THEN LIMSEQ_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

700 
obtain no where "\<And>n'. no \<le> n' \<Longrightarrow> norm (a n'  x) < a n  x" by blast 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

701 
hence "norm (a (max no n)  x) < a n  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

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

703 
{ fix n' have "n \<le> n' \<Longrightarrow> x < a n'" using monotone[where m=n and n=n'] and `x < a n` by auto } 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

704 
hence "x < a (max no n)" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

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

706 
have "a (max no n) < a n" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

707 
with monotone[where m=n and n="max no n"] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

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

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

710 
} note top_down = this 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

711 
{ fix x n m fix a :: "nat \<Rightarrow> real" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

712 
assume "a > x" and "monoseq a" and "a m < x" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

713 
have "a n \<le> x \<and> (\<forall> m. \<forall> n \<ge> m. a m \<le> a n)" 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

714 
proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

715 
case True with top_down and `a > x` show ?thesis by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

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

717 
case False with `monoseq a`[unfolded monoseq_def] have "\<forall> m. \<forall> n \<ge> m.  a m \<le>  a n" by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

718 
hence " a m \<le>  x" using top_down[OF LIMSEQ_minus[OF `a > x`]] by blast 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

719 
hence False using `a m < 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

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

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

722 
} note when_decided = this 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

723 

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

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

725 
proof (cases "\<exists> m. a m \<noteq> x") 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

726 
case True then obtain m where "a m \<noteq> 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

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

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

729 
case True with when_decided[OF `a > x` `monoseq a`, where m2=m] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

730 
show ?thesis by blast 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

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

732 
case False hence " a m <  x" using `a m \<noteq> 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

733 
with when_decided[OF LIMSEQ_minus[OF `a > x`] monoseq_minus[OF `monoseq a`], where m2=m] 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

734 
show ?thesis by auto 
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

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

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

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

738 

30196
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

739 
text{* for any sequence, there is a mootonic subsequence *} 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

740 
lemma seq_monosub: "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

741 
proof 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

742 
{assume H: "\<forall>n. \<exists>p >n. \<forall> m\<ge>p. s m \<le> s p" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

743 
let ?P = "\<lambda> p n. p > n \<and> (\<forall>m \<ge> p. s m \<le> s p)" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

744 
from nat_function_unique[of "SOME p. ?P p 0" "\<lambda>p n. SOME p. ?P p n"] 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

745 
obtain f where f: "f 0 = (SOME p. ?P p 0)" "\<forall>n. f (Suc n) = (SOME p. ?P p (f n))" by blast 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

746 
have "?P (f 0) 0" unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p 0"] 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

747 
using H apply  
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

748 
apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

749 
unfolding order_le_less by blast 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

750 
hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+ 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

751 
{fix n 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

752 
have "?P (f (Suc n)) (f n)" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

753 
unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"] 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

754 
using H apply  
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

755 
apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

756 
unfolding order_le_less by blast 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

757 
hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+} 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

758 
note fSuc = this 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

759 
{fix p q assume pq: "p \<ge> f q" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

760 
have "s p \<le> s(f(q))" using f0(2)[rule_format, of p] pq fSuc 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

761 
by (cases q, simp_all) } 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

762 
note pqth = this 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

763 
{fix q 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

764 
have "f (Suc q) > f q" apply (induct q) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

765 
using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))} 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

766 
note fss = this 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

767 
from fss have th1: "subseq f" unfolding subseq_Suc_iff .. 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

768 
{fix a b 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

769 
have "f a \<le> f (a + b)" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

770 
proof(induct b) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

771 
case 0 thus ?case by simp 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

772 
next 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

773 
case (Suc b) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

774 
from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

775 
qed} 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

776 
note fmon0 = this 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

777 
have "monoseq (\<lambda>n. s (f n))" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

778 
proof 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

779 
{fix n 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

780 
have "s (f n) \<ge> s (f (Suc n))" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

781 
proof(cases n) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

782 
case 0 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

783 
assume n0: "n = 0" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

784 
from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

785 
from f0(2)[rule_format, OF th0] show ?thesis using n0 by simp 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

786 
next 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

787 
case (Suc m) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

788 
assume m: "n = Suc m" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

789 
from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

790 
from m fSuc(2)[rule_format, OF th0] show ?thesis by simp 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

791 
qed} 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

792 
thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

793 
qed 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

794 
with th1 have ?thesis by blast} 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

795 
moreover 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

796 
{fix N assume N: "\<forall>p >N. \<exists> m\<ge>p. s m > s p" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

797 
{fix p assume p: "p \<ge> Suc N" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

798 
hence pN: "p > N" by arith with N obtain m where m: "m \<ge> p" "s m > s p" by blast 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

799 
have "m \<noteq> p" using m(2) by auto 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

800 
with m have "\<exists>m>p. s p < s m" by  (rule exI[where x=m], auto)} 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

801 
note th0 = this 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

802 
let ?P = "\<lambda>m x. m > x \<and> s x < s m" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

803 
from nat_function_unique[of "SOME x. ?P x (Suc N)" "\<lambda>m x. SOME y. ?P y x"] 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

804 
obtain f where f: "f 0 = (SOME x. ?P x (Suc N))" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

805 
"\<forall>n. f (Suc n) = (SOME m. ?P m (f n))" by blast 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

806 
have "?P (f 0) (Suc N)" unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

807 
using N apply  
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

808 
apply (erule allE[where x="Suc N"], clarsimp) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

809 
apply (rule_tac x="m" in exI) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

810 
apply auto 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

811 
apply (subgoal_tac "Suc N \<noteq> m") 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

812 
apply simp 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

813 
apply (rule ccontr, simp) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

814 
done 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

815 
hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+ 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

816 
{fix n 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

817 
have "f n > N \<and> ?P (f (Suc n)) (f n)" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

818 
unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"] 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

819 
proof (induct n) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

820 
case 0 thus ?case 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

821 
using f0 N apply auto 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

822 
apply (erule allE[where x="f 0"], clarsimp) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

823 
apply (rule_tac x="m" in exI, simp) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

824 
by (subgoal_tac "f 0 \<noteq> m", auto) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

825 
next 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

826 
case (Suc n) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

827 
from Suc.hyps have Nfn: "N < f n" by blast 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

828 
from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

829 
with Nfn have mN: "m > N" by arith 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

830 
note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]] 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

831 

6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

832 
from key have th0: "f (Suc n) > N" by simp 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

833 
from N[rule_format, OF th0] 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

834 
obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

835 
have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

836 
hence "m' > f (Suc n)" using m'(1) by simp 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

837 
with key m'(2) show ?case by auto 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

838 
qed} 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

839 
note fSuc = this 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

840 
{fix n 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

841 
have "f n \<ge> Suc N \<and> f(Suc n) > f n \<and> s(f n) < s(f(Suc n))" using fSuc[of n] by auto 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

842 
hence "f n \<ge> Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+} 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

843 
note thf = this 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

844 
have sqf: "subseq f" unfolding subseq_Suc_iff using thf by simp 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

845 
have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc using thf 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

846 
apply  
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

847 
apply (rule disjI1) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

848 
apply auto 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

849 
apply (rule order_less_imp_le) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

850 
apply blast 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

851 
done 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

852 
then have ?thesis using sqf by blast} 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

853 
ultimately show ?thesis unfolding linorder_not_less[symmetric] by blast 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

854 
qed 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

855 

6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

856 
lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n" 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

857 
proof(induct n) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

858 
case 0 thus ?case by simp 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

859 
next 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

860 
case (Suc n) 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

861 
from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

862 
have "n < f (Suc n)" by arith 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

863 
thus ?case by arith 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

864 
qed 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

865 

30730  866 
lemma LIMSEQ_subseq_LIMSEQ: 
867 
"\<lbrakk> X > L; subseq f \<rbrakk> \<Longrightarrow> (X o f) > L" 

868 
apply (auto simp add: LIMSEQ_def) 

869 
apply (drule_tac x=r in spec, clarify) 

870 
apply (rule_tac x=no in exI, clarify) 

871 
apply (blast intro: seq_suble le_trans dest!: spec) 

872 
done 

873 

30196
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

874 
subsection {* Bounded Monotonic Sequences *} 
6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

875 

6ffaa79c352c
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
chaieb
parents:
30082
diff
changeset

876 

20696  877 
text{*Bounded Sequence*} 
15082  878 

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

879 
lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)" 
15082  880 
by (simp add: Bseq_def) 
881 

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

882 
lemma BseqI: "[ 0 < K; \<forall>n. norm (X n) \<le> K ] ==> Bseq X" 
15082  883 
by (auto simp add: Bseq_def) 
884 

885 
lemma lemma_NBseq_def: 

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

886 
"(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

887 
(\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" 
15082  888 
apply auto 
889 
prefer 2 apply force 

890 
apply (cut_tac x = K in reals_Archimedean2, clarify) 

891 
apply (rule_tac x = n in exI, clarify) 

892 
apply (drule_tac x = na in spec) 

893 
apply (auto simp add: real_of_nat_Suc) 

894 
done 

895 

896 
text{* alternative definition for Bseq *} 

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

897 
lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" 
15082  898 
apply (simp add: Bseq_def) 
899 
apply (simp (no_asm) add: lemma_NBseq_def) 

900 
done 

901 

902 
lemma lemma_NBseq_def2: 

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

903 
"(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))" 
15082  904 
apply (subst lemma_NBseq_def, auto) 
905 
apply (rule_tac x = "Suc N" in exI) 

906 
apply (rule_tac [2] x = N in exI) 

907 
apply (auto simp add: real_of_nat_Suc) 

908 
prefer 2 apply (blast intro: order_less_imp_le) 

909 
apply (drule_tac x = n in spec, simp) 

910 
done 

911 

912 
(* yet another definition for Bseq *) 

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

913 
lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))" 
15082  914 
by (simp add: Bseq_def lemma_NBseq_def2) 
915 

20696  916 
subsubsection{*Upper Bounds and Lubs of Bounded Sequences*} 
15082  917 

918 
lemma Bseq_isUb: 

919 
"!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U" 

22998  920 
by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff) 
15082  921 

922 

923 
text{* Use completeness of reals (supremum property) 

924 
to show that any bounded sequence has a least upper bound*} 

925 

926 
lemma Bseq_isLub: 

927 
"!!(X::nat=>real). Bseq X ==> 

928 
\<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U" 

929 
by (blast intro: reals_complete Bseq_isUb) 

930 

20696  931 
subsubsection{*A Bounded and Monotonic Sequence Converges*} 
15082  932 

933 
lemma lemma_converg1: 

15360  934 
"!!(X::nat=>real). [ \<forall>m. \<forall> n \<ge> m. X m \<le> X n; 
15082  935 
isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma) 
15360  936 
] ==> \<forall>n \<ge> ma. X n = X ma" 
15082  937 
apply safe 
938 
apply (drule_tac y = "X n" in isLubD2) 

939 
apply (blast dest: order_antisym)+ 

940 
done 

941 

942 
text{* The best of both worlds: Easier to prove this result as a standard 

943 
theorem and then use equivalence to "transfer" it into the 

944 
equivalent nonstandard form if needed!*} 

945 

946 
lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n > X n = X m ==> \<exists>L. (X > L)" 

947 
apply (simp add: LIMSEQ_def) 

948 
apply (rule_tac x = "X m" in exI, safe) 

949 
apply (rule_tac x = m in exI, safe) 

950 
apply (drule spec, erule impE, auto) 

951 
done 

952 

953 
lemma lemma_converg2: 

954 
"!!(X::nat=>real). 

955 
[ \<forall>m. X m ~= U; isLub UNIV {x. \<exists>n. X n = x} U ] ==> \<forall>m. X m < U" 

956 
apply safe 

957 
apply (drule_tac y = "X m" in isLubD2) 

958 
apply (auto dest!: order_le_imp_less_or_eq) 

959 
done 

960 

961 
lemma lemma_converg3: "!!(X ::nat=>real). \<forall>m. X m \<le> U ==> isUb UNIV {x. \<exists>n. X n = x} U" 

962 
by (rule setleI [THEN isUbI], auto) 

963 

964 
text{* FIXME: @{term "U  T < U"} is redundant *} 

965 
lemma lemma_converg4: "!!(X::nat=> real). 

966 
[ \<forall>m. X m ~= U; 

967 
isLub UNIV {x. \<exists>n. X n = x} U; 

968 
0 < T; 

969 
U +  T < U 

970 
] ==> \<exists>m. U + T < X m & X m < U" 

971 
apply (drule lemma_converg2, assumption) 

972 
apply (rule ccontr, simp) 

973 
apply (simp add: linorder_not_less) 

974 
apply (drule lemma_converg3) 

975 
apply (drule isLub_le_isUb, assumption) 

976 
apply (auto dest: order_less_le_trans) 

977 
done 

978 

979 
text{*A standard proof of the theorem for monotone increasing sequence*} 

980 

981 
lemma Bseq_mono_convergent: 

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

982 
"[ Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n ] ==> convergent (X::nat=>real)" 
15082  983 
apply (simp add: convergent_def) 
984 
apply (frule Bseq_isLub, safe) 

985 
apply (case_tac "\<exists>m. X m = U", auto) 

986 
apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ) 

987 
(* second case *) 

988 
apply (rule_tac x = U in exI) 

989 
apply (subst LIMSEQ_iff, safe) 

990 
apply (frule lemma_converg2, assumption) 

991 
apply (drule lemma_converg4, auto) 

992 
apply (rule_tac x = m in exI, safe) 

993 
apply (subgoal_tac "X m \<le> X n") 

994 
prefer 2 apply blast 

995 
apply (drule_tac x=n and P="%m. X m < U" in spec, arith) 

996 
done 

997 

998 
lemma Bseq_minus_iff: "Bseq (%n. (X n)) = Bseq X" 

999 
by (simp add: Bseq_def) 

1000 

1001 
text{*Main monotonicity theorem*} 

1002 
lemma Bseq_monoseq_convergent: "[ Bseq X; monoseq X ] ==> convergent X" 

1003 
apply (simp add: monoseq_def, safe) 

1004 
apply (rule_tac [2] convergent_minus_iff [THEN ssubst]) 

1005 
apply (drule_tac [2] Bseq_minus_iff [THEN ssubst]) 

1006 
apply (auto intro!: Bseq_mono_convergent) 

1007 
done 

1008 

30730  1009 
subsubsection{*Increasing and Decreasing Series*} 
1010 

1011 
lemma incseq_imp_monoseq: "incseq X \<Longrightarrow> monoseq X" 

1012 
by (simp add: incseq_def monoseq_def) 

1013 

1014 
lemma incseq_le: assumes inc: "incseq X" and lim: "X > L" shows "X n \<le> L" 

1015 
using monoseq_le [OF incseq_imp_monoseq [OF inc] lim] 

1016 
proof 

1017 
assume "(\<forall>n. X n \<le> L) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n)" 

1018 
thus ?thesis by simp 

1019 
next 

1020 
assume "(\<forall>n. L \<le> X n) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X n \<le> X m)" 

1021 
hence const: "(!!m n. m \<le> n \<Longrightarrow> X n = X m)" using inc 

1022 
by (auto simp add: incseq_def intro: order_antisym) 

1023 
have X: "!!n. X n = X 0" 

1024 
by (blast intro: const [of 0]) 

1025 
have "X = (\<lambda>n. X 0)" 

1026 
by (blast intro: ext X) 

1027 
hence "L = X 0" using LIMSEQ_const [of "X 0"] 

1028 
by (auto intro: LIMSEQ_unique lim) 

1029 
thus ?thesis 

1030 
by (blast intro: eq_refl X) 

1031 
qed 

1032 

1033 
lemma decseq_imp_monoseq: "decseq X \<Longrightarrow> monoseq X" 

1034 
by (simp add: decseq_def monoseq_def) 

1035 

1036 
lemma decseq_eq_incseq: "decseq X = incseq (\<lambda>n.  X n)" 

1037 
by (simp add: decseq_def incseq_def) 

1038 

1039 

1040 
lemma decseq_le: assumes dec: "decseq X" and lim: "X > L" shows "L \<le> X n" 

1041 
proof  

1042 
have inc: "incseq (\<lambda>n.  X n)" using dec 

1043 
by (simp add: decseq_eq_incseq) 

1044 
have " X n \<le>  L" 

1045 
by (blast intro: incseq_le [OF inc] LIMSEQ_minus lim) 

1046 
thus ?thesis 

1047 
by simp 

1048 
qed 

1049 

20696  1050 
subsubsection{*A Few More Equivalence Theorems for Boundedness*} 
15082  1051 

1052 
text{*alternative formulation for boundedness*} 

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

1053 
lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + x) \<le> k)" 
15082  1054 
apply (unfold Bseq_def, safe) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1055 
apply (rule_tac [2] x = "k + norm x" in exI) 
15360  1056 
apply (rule_tac x = K in exI, simp) 
15221  1057 
apply (rule exI [where x = 0], auto) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1058 
apply (erule order_less_le_trans, simp) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1059 
apply (drule_tac x=n in spec, fold diff_def) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1060 
apply (drule order_trans [OF norm_triangle_ineq2]) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1061 
apply simp 
15082  1062 
done 
1063 

1064 
text{*alternative formulation for boundedness*} 

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

1065 
lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + X(N)) \<le> k)" 
15082  1066 
apply safe 
1067 
apply (simp add: Bseq_def, safe) 

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

1068 
apply (rule_tac x = "K + norm (X N)" in exI) 
15082  1069 
apply auto 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1070 
apply (erule order_less_le_trans, simp) 
15082  1071 
apply (rule_tac x = N in exI, safe) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1072 
apply (drule_tac x = n in spec) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1073 
apply (rule order_trans [OF norm_triangle_ineq], simp) 
15082  1074 
apply (auto simp add: Bseq_iff2) 
1075 
done 

1076 

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

1077 
lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f" 
15082  1078 
apply (simp add: Bseq_def) 
15221  1079 
apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset

1080 
apply (drule_tac x = n in spec, arith) 
15082  1081 
done 
1082 

1083 

20696  1084 
subsection {* Cauchy Sequences *} 
15082  1085 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1086 
lemma metric_CauchyI: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1087 
"(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1088 
by (simp add: Cauchy_def) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1089 

e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1090 
lemma metric_CauchyD: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1091 
"\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e" 
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset

1092 
by (simp add: Cauchy_def) 
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset

1093 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1094 
lemma Cauchy_iff: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1095 
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1096 
shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m  X n) < e)" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1097 
unfolding Cauchy_def dist_norm .. 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1098 

e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1099 
lemma CauchyI: 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1100 
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1101 
shows "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m  X n) < e) \<Longrightarrow> Cauchy X" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1102 
by (simp add: Cauchy_iff) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1103 

20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset

1104 
lemma CauchyD: 
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1105 
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1106 
shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m  X n) < e" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1107 
by (simp add: Cauchy_iff) 
20751
93271c59d211
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
huffman
parents:
20740
diff
changeset

1108 

30730  1109 
lemma Cauchy_subseq_Cauchy: 
1110 
"\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)" 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1111 
apply (auto simp add: Cauchy_def) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1112 
apply (drule_tac x=e in spec, clarify) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1113 
apply (rule_tac x=M in exI, clarify) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1114 
apply (blast intro: le_trans [OF _ seq_suble] dest!: spec) 
30730  1115 
done 
1116 

20696  1117 
subsubsection {* Cauchy Sequences are Bounded *} 
1118 

15082  1119 
text{*A Cauchy sequence is bounded  this is the standard 
1120 
proof mechanization rather than the nonstandard proof*} 

1121 

20563  1122 
lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M  X n) < (1::real) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1123 
==> \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1124 
apply (clarify, drule spec, drule (1) mp) 
20563  1125 
apply (simp only: norm_minus_commute) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1126 
apply (drule order_le_less_trans [OF norm_triangle_ineq2]) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1127 
apply simp 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1128 
done 
15082  1129 

1130 
lemma Cauchy_Bseq: "Cauchy X ==> Bseq X" 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1131 
apply (simp add: Cauchy_iff) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1132 
apply (drule spec, drule mp, rule zero_less_one, safe) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1133 
apply (drule_tac x="M" in spec, simp) 
15082  1134 
apply (drule lemmaCauchy) 
22608  1135 
apply (rule_tac k="M" in Bseq_offset) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

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

1137 
apply (rule_tac x="1 + norm (X M)" in exI) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1138 
apply (rule conjI, rule order_less_le_trans [OF zero_less_one], simp) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

1139 
apply (simp add: order_less_imp_le) 
15082  1140 
done 
1141 

20696  1142 
subsubsection {* Cauchy Sequences are Convergent *} 
15082  1143 

20830
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

1144 
axclass banach \<subseteq> real_normed_vector 
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

1145 
Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X" 
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

1146 

22629  1147 
theorem LIMSEQ_imp_Cauchy: 
1148 
assumes X: "X > a" shows "Cauchy X" 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1149 
proof (rule metric_CauchyI) 
22629  1150 
fix e::real assume "0 < e" 
1151 
hence "0 < e/2" by simp 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1152 
with X have "\<exists>N. \<forall>n\<ge>N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1153 
then obtain N where N: "\<forall>n\<ge>N. dist (X n) a < e/2" .. 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1154 
show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e" 
22629  1155 
proof (intro exI allI impI) 
1156 
fix m assume "N \<le> m" 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1157 
hence m: "dist (X m) a < e/2" using N by fast 
22629  1158 
fix n assume "N \<le> n" 
31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1159 
hence n: "dist (X n) a < e/2" using N by fast 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1160 
have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a" 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1161 
by (rule dist_triangle2) 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1162 
also from m n have "\<dots> < e" by simp 
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1163 
finally show "dist (X m) (X n) < e" . 
22629  1164 
qed 
1165 
qed 

1166 

20691  1167 
lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X" 
22629  1168 
unfolding convergent_def 
1169 
by (erule exE, erule LIMSEQ_imp_Cauchy) 

20691  1170 

22629  1171 
text {* 
1172 
Proof that Cauchy sequences converge based on the one from 

1173 
http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html 

1174 
*} 

1175 

1176 
text {* 

1177 
If sequence @{term "X"} is Cauchy, then its limit is the lub of 

1178 
@{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"} 

1179 
*} 

1180 

1181 
lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u" 

1182 
by (simp add: isUbI setleI) 

1183 

1184 
lemma real_abs_diff_less_iff: 

1185 
"(\<bar>x  a\<bar> < (r::real)) = (a  r < x \<and> x < a + r)" 

1186 
by auto 

1187 

27681  1188 
locale real_Cauchy = 
22629  1189 
fixes X :: "nat \<Rightarrow> real" 
1190 
assumes X: "Cauchy X" 

1191 
fixes S :: "real set" 

1192 
defines S_def: "S \<equiv> {x::real. \<exists>N. \<forall>n\<ge>N. x < X n}" 

1193 

27681  1194 
lemma real_CauchyI: 
1195 
assumes "Cauchy X" 

1196 
shows "real_Cauchy X" 

28823  1197 
proof qed (fact assms) 
27681  1198 

22629  1199 
lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" 
1200 
by (unfold S_def, auto) 

1201 

1202 
lemma (in real_Cauchy) bound_isUb: 

1203 
assumes N: "\<forall>n\<ge>N. X n < x" 

1204 
shows "isUb UNIV S x" 

1205 
proof (rule isUb_UNIV_I) 

1206 
fix y::real assume "y \<in> S" 

1207 
hence "\<exists>M. \<forall>n\<ge>M. y < X n" 

1208 
by (simp add: S_def) 

1209 
then obtain M where "\<forall>n\<ge>M. y < X n" .. 

1210 
hence "y < X (max M N)" by simp 

1211 
also have "\<dots> < x" using N by simp 

1212 
finally show "y \<le> x" 

1213 
by (rule order_less_imp_le) 

1214 
qed 

1215 

1216 
lemma (in real_Cauchy) isLub_ex: "\<exists>u. isLub UNIV S u" 

1217 
proof (rule reals_complete) 

1218 
obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m  X n) < 1" 

1219 
using CauchyD [OF X zero_less_one] by fast 

1220 
hence N: "\<forall>n\<ge>N. norm (X n  X N) < 1" by simp 

1221 
show "\<exists>x. x \<in> S" 

1222 
proof 

1223 
from N have "\<forall>n\<ge>N. X N  1 < X n" 

1224 
by (simp add: real_abs_diff_less_iff) 

1225 
thus "X N  1 \<in> S" by (rule mem_S) 

1226 
qed 

1227 
show "\<exists>u. isUb UNIV S u" 

1228 
proof 

1229 
from N have "\<forall>n\<ge>N. X n < X N + 1" 

1230 
by (simp add: real_abs_diff_less_iff) 

1231 
thus "isUb UNIV S (X N + 1)" 

1232 
by (rule bound_isUb) 

1233 
qed 

1234 
qed 

1235 

1236 
lemma (in real_Cauchy) isLub_imp_LIMSEQ: 

1237 
assumes x: "isLub UNIV S x" 

1238 
shows "X > x" 

1239 
proof (rule LIMSEQ_I) 

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

1241 
hence r: "0 < r/2" by simp 

1242 
obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n  X m) < r/2" 

1243 
using CauchyD [OF X r] by fast 

1244 
hence "\<forall>n\<ge>N. norm (X n  X N) < r/2" by simp 

1245 
hence N: "\<forall>n\<ge>N. X N  r/2 < X n \<and> X n < X N + r/2" 

1246 
by (simp only: real_norm_def real_abs_diff_less_iff) 

1247 

1248 
from N have "\<forall>n\<ge>N. X N  r/2 < X n" by fast 

1249 
hence "X N  r/2 \<in> S" by (rule mem_S) 

23482  1250 
hence 1: "X N  r/2 \<le> x" using x isLub_isUb isUbD by fast 
22629  1251 

1252 
from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast 

1253 
hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb) 

23482  1254 
hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast 
22629  1255 

1256 
show "\<exists>N. \<forall>n\<ge>N. norm (X n  x) < r" 

1257 
proof (intro exI allI impI) 

1258 
fix n assume n: "N \<le> n" 

23482  1259 
from N n have "X n < X N + r/2" and "X N  r/2 < X n" by simp+ 
1260 
thus "norm (X n  x) < r" using 1 2 

22629  1261 
by (simp add: real_abs_diff_less_iff) 
1262 
qed 

1263 
qed 

1264 

1265 
lemma (in real_Cauchy) LIMSEQ_ex: "\<exists>x. X > x" 

1266 
proof  

1267 
obtain x where "isLub UNIV S x" 

1268 
using isLub_ex by fast 

1269 
hence "X > x" 

1270 
by (rule isLub_imp_LIMSEQ) 

1271 
thus ?thesis .. 

1272 
qed 

1273 

20830
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

1274 
lemma real_Cauchy_convergent: 
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

1275 
fixes X :: "nat \<Rightarrow> real" 
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

1276 
shows "Cauchy X \<Longrightarrow> convergent X" 
27681  1277 
unfolding convergent_def 
1278 
by (rule real_Cauchy.LIMSEQ_ex) 

1279 
(rule real_CauchyI) 

20830
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

1280 

65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

1281 
instance real :: banach 
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

1282 
by intro_classes (rule real_Cauchy_convergent) 
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

1283 

65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

1284 
lemma Cauchy_convergent_iff: 
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

1285 
fixes X :: "nat \<Rightarrow> 'a::banach" 
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

1286 
shows "Cauchy X = convergent X" 
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

1287 
by (fast intro: Cauchy_convergent convergent_Cauchy) 
15082  1288 

30730  1289 
lemma convergent_subseq_convergent: 
1290 
fixes X :: "nat \<Rightarrow> 'a::banach" 

1291 
shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)" 

31336
e17f13cd1280
generalize constants in SEQ.thy to class metric_space
huffman
parents:
31017
diff
changeset

1292 
by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric]) 
30730  1293 

15082  1294 

20696  1295 
subsection {* Power Sequences *} 
15082  1296 

1297 
text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term 

1298 
"x<1"}. Proof will use (NS) Cauchy equivalence for convergence and 
