author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44714  a8990b5d7365 
child 50087  635d73673b5e 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32877
diff
changeset

1 
(* Title: HOL/SEQ.thy 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32877
diff
changeset

2 
Author: Jacques D. Fleuriot, University of Cambridge 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32877
diff
changeset

3 
Author: Lawrence C Paulson 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32877
diff
changeset

4 
Author: Jeremy Avigad 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32877
diff
changeset

5 
Author: Brian Huffman 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32877
diff
changeset

6 

69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32877
diff
changeset

7 
Convergence of sequences and series. 
15082  8 
*) 
10751  9 

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

10 
header {* Sequences and Convergence *} 
17439  11 

15131  12 
theory SEQ 
36822  13 
imports Limits RComplete 
15131  14 
begin 
10751  15 

41972  16 
subsection {* Monotone sequences and subsequences *} 
10751  17 

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

18 
definition 
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

19 
monoseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where 
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

20 
{*Definition of monotonicity. 
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

21 
The use of disjunction here complicates proofs considerably. 
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

22 
One alternative is to add a Boolean argument to indicate the direction. 
30730  23 
Another is to develop the notions of increasing and decreasing first.*} 
37767  24 
"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  25 

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

26 
definition 
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

27 
incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where 
30730  28 
{*Increasing sequence*} 
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

29 
"incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)" 
30730  30 

31 
definition 

41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

32 
decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where 
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

33 
{*Decreasing sequence*} 
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

34 
"decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)" 
30730  35 

36 
definition 

41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

37 
subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where 
15082  38 
{*Definition of subsequence*} 
41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

39 
"subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)" 
10751  40 

41972  41 
lemma incseq_mono: "mono f \<longleftrightarrow> incseq f" 
42 
unfolding mono_def incseq_def by auto 

43 

44 
lemma incseq_SucI: 

45 
"(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X" 

46 
using lift_Suc_mono_le[of X] 

47 
by (auto simp: incseq_def) 

48 

49 
lemma incseqD: "\<And>i j. incseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f i \<le> f j" 

50 
by (auto simp: incseq_def) 

51 

52 
lemma incseq_SucD: "incseq A \<Longrightarrow> A i \<le> A (Suc i)" 

53 
using incseqD[of A i "Suc i"] by auto 

54 

55 
lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))" 

56 
by (auto intro: incseq_SucI dest: incseq_SucD) 

57 

58 
lemma incseq_const[simp, intro]: "incseq (\<lambda>x. k)" 

59 
unfolding incseq_def by auto 

60 

61 
lemma decseq_SucI: 

62 
"(\<And>n. X (Suc n) \<le> X n) \<Longrightarrow> decseq X" 

63 
using order.lift_Suc_mono_le[OF dual_order, of X] 

64 
by (auto simp: decseq_def) 

65 

66 
lemma decseqD: "\<And>i j. decseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f j \<le> f i" 

67 
by (auto simp: decseq_def) 

68 

69 
lemma decseq_SucD: "decseq A \<Longrightarrow> A (Suc i) \<le> A i" 

70 
using decseqD[of A i "Suc i"] by auto 

71 

72 
lemma decseq_Suc_iff: "decseq f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)" 

73 
by (auto intro: decseq_SucI dest: decseq_SucD) 

74 

75 
lemma decseq_const[simp, intro]: "decseq (\<lambda>x. k)" 

76 
unfolding decseq_def by auto 

77 

78 
lemma monoseq_iff: "monoseq X \<longleftrightarrow> incseq X \<or> decseq X" 

79 
unfolding monoseq_def incseq_def decseq_def .. 

80 

81 
lemma monoseq_Suc: 

82 
"monoseq X \<longleftrightarrow> (\<forall>n. X n \<le> X (Suc n)) \<or> (\<forall>n. X (Suc n) \<le> X n)" 

83 
unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff .. 

84 

85 
lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X" 

86 
by (simp add: monoseq_def) 

87 

88 
lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X" 

89 
by (simp add: monoseq_def) 

90 

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

92 
by (simp add: monoseq_Suc) 

93 

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

95 
by (simp add: monoseq_Suc) 

96 

97 
lemma monoseq_minus: 

98 
fixes a :: "nat \<Rightarrow> 'a::ordered_ab_group_add" 

99 
assumes "monoseq a" 

100 
shows "monoseq (\<lambda> n.  a n)" 

101 
proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n") 

102 
case True 

103 
hence "\<forall> m. \<forall> n \<ge> m.  a n \<le>  a m" by auto 

104 
thus ?thesis by (rule monoI2) 

105 
next 

106 
case False 

107 
hence "\<forall> m. \<forall> n \<ge> m.  a m \<le>  a n" using `monoseq a`[unfolded monoseq_def] by auto 

108 
thus ?thesis by (rule monoI1) 

109 
qed 

110 

111 
text{*Subsequence (alternative definition, (e.g. Hoskins)*} 

112 

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

114 
apply (simp add: subseq_def) 

115 
apply (auto dest!: less_imp_Suc_add) 

116 
apply (induct_tac k) 

117 
apply (auto intro: less_trans) 

118 
done 

119 

120 
text{* for any sequence, there is a monotonic subsequence *} 

121 
lemma seq_monosub: 

122 
fixes s :: "nat => 'a::linorder" 

123 
shows "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))" 

124 
proof cases 

125 
let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)" 

126 
assume *: "\<forall>n. \<exists>p. ?P p n" 

127 
def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)" 

128 
have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp 

129 
have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc .. 

130 
have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto 

131 
have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto 

132 
then have "subseq f" unfolding subseq_Suc_iff by auto 

133 
moreover have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc 

134 
proof (intro disjI2 allI) 

135 
fix n show "s (f (Suc n)) \<le> s (f n)" 

136 
proof (cases n) 

137 
case 0 with P_Suc[of 0] P_0 show ?thesis by auto 

138 
next 

139 
case (Suc m) 

140 
from P_Suc[of n] Suc have "f (Suc m) \<le> f (Suc (Suc m))" by simp 

141 
with P_Suc Suc show ?thesis by simp 

142 
qed 

143 
qed 

144 
ultimately show ?thesis by auto 

145 
next 

146 
let "?P p m" = "m < p \<and> s m < s p" 

147 
assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))" 

148 
then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less) 

149 
def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)" 

150 
have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp 

151 
have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc .. 

152 
have P_0: "?P (f 0) (Suc N)" 

153 
unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto 

154 
{ fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)" 

155 
unfolding f_Suc some_eq_ex[of "\<lambda>p. ?P p (f i)"] using N[of "f i"] . } 

156 
note P' = this 

157 
{ fix i have "N < f i \<and> ?P (f (Suc i)) (f i)" 

158 
by (induct i) (insert P_0 P', auto) } 

159 
then have "subseq f" "monoseq (\<lambda>x. s (f x))" 

160 
unfolding subseq_Suc_iff monoseq_Suc by (auto simp: not_le intro: less_imp_le) 

161 
then show ?thesis by auto 

162 
qed 

163 

164 
lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n" 

165 
proof(induct n) 

166 
case 0 thus ?case by simp 

167 
next 

168 
case (Suc n) 

169 
from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps 

170 
have "n < f (Suc n)" by arith 

171 
thus ?case by arith 

172 
qed 

173 

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

175 
by (simp add: incseq_def monoseq_def) 

176 

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

178 
by (simp add: decseq_def monoseq_def) 

179 

180 
lemma decseq_eq_incseq: 

181 
fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n.  X n)" 

182 
by (simp add: decseq_def incseq_def) 

183 

184 
subsection {* Defintions of limits *} 

185 

44206
5e4a1664106e
localeize some constant definitions, so complete_space can inherit from metric_space
huffman
parents:
44205
diff
changeset

186 
abbreviation (in topological_space) 
5e4a1664106e
localeize some constant definitions, so complete_space can inherit from metric_space
huffman
parents:
44205
diff
changeset

187 
LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool" 
41972  188 
("((_)/ > (_))" [60, 60] 60) where 
189 
"X > L \<equiv> (X > L) sequentially" 

190 

191 
definition 

44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44194
diff
changeset

192 
lim :: "(nat \<Rightarrow> 'a::t2_space) \<Rightarrow> 'a" where 
41972  193 
{*Standard definition of limit using choice operator*} 
194 
"lim X = (THE L. X > L)" 

195 

44206
5e4a1664106e
localeize some constant definitions, so complete_space can inherit from metric_space
huffman
parents:
44205
diff
changeset

196 
definition (in topological_space) convergent :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where 
41972  197 
"convergent X = (\<exists>L. X > L)" 
198 

199 
definition 

200 
Bseq :: "(nat => 'a::real_normed_vector) => bool" where 

201 
{*Standard definition for bounded sequence*} 

202 
"Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)" 

203 

44206
5e4a1664106e
localeize some constant definitions, so complete_space can inherit from metric_space
huffman
parents:
44205
diff
changeset

204 
definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where 
37767  205 
"Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)" 
10751  206 

15082  207 

22608  208 
subsection {* Bounded Sequences *} 
209 

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

213 
show "0 < max K 1" by simp 

214 
next 

215 
fix n::nat 

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

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

218 
qed 

219 

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

221 
unfolding Bseq_def by auto 

222 

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

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

227 
fix n::nat 

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

229 
proof (cases rule: linorder_le_cases) 

230 
assume "n \<ge> N" 

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

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

233 
next 

234 
assume "n \<le> N" 

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

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

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

239 
qed 

240 

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

242 
unfolding Bseq_def by auto 

243 

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

245 
apply (erule BseqE) 

26312  246 
apply (rule_tac N="k" and K="K" in BseqI2') 
22608  247 
apply clarify 
248 
apply (drule_tac x="n  k" in spec, simp) 

249 
done 

250 

31355  251 
lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially" 
252 
unfolding Bfun_def eventually_sequentially 

253 
apply (rule iffI) 

32064  254 
apply (simp add: Bseq_def) 
255 
apply (auto intro: BseqI2') 

31355  256 
done 
257 

22608  258 

20696  259 
subsection {* Limits of Sequences *} 
260 

32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

261 
lemma [trans]: "X=Y ==> Y > z ==> X > z" 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

262 
by simp 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

263 

36660
1cc4ab4b7ff7
make (X > L) an abbreviation for (X > L) sequentially
huffman
parents:
36657
diff
changeset

264 
lemma LIMSEQ_def: "X > L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)" 
1cc4ab4b7ff7
make (X > L) an abbreviation for (X > L) sequentially
huffman
parents:
36657
diff
changeset

265 
unfolding tendsto_iff eventually_sequentially .. 
31392  266 

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

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

269 
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

270 
unfolding LIMSEQ_def dist_norm .. 
22608  271 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33042
diff
changeset

272 
lemma LIMSEQ_iff_nz: "X > L = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)" 
36660
1cc4ab4b7ff7
make (X > L) an abbreviation for (X > L) sequentially
huffman
parents:
36657
diff
changeset

273 
unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33042
diff
changeset

274 

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

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

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

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

278 

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

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

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

281 
by (simp add: LIMSEQ_def) 
15082  282 

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

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

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

285 
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

286 
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

287 

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

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

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

290 
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

291 
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

292 

36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

293 
lemma LIMSEQ_const_iff: 
44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44194
diff
changeset

294 
fixes k l :: "'a::t2_space" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

295 
shows "(\<lambda>n. k) > l \<longleftrightarrow> k = l" 
44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44194
diff
changeset

296 
using trivial_limit_sequentially by (rule tendsto_const_iff) 
22608  297 

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

36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

300 
apply (rule topological_tendstoI) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

301 
apply (drule (2) topological_tendstoD) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

302 
apply (simp only: eventually_sequentially) 
22615  303 
apply (erule exE, rename_tac N) 
304 
apply (rule_tac x=N in exI) 

305 
apply simp 

306 
done 

20696  307 

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

36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

310 
apply (rule topological_tendstoI) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

311 
apply (drule (2) topological_tendstoD) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

312 
apply (simp only: eventually_sequentially) 
22615  313 
apply (erule exE, rename_tac N) 
314 
apply (rule_tac x="N + k" in exI) 

315 
apply clarify 

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

317 
apply (simp add: le_diff_conv2) 

20696  318 
done 
319 

22615  320 
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

321 
by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp) 
22615  322 

323 
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

324 
by (rule_tac k="Suc 0" in LIMSEQ_offset, simp) 
22615  325 

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

327 
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc) 

328 

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

329 
lemma LIMSEQ_linear: "\<lbrakk> X > x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) > x" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

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

331 
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

332 

36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

333 
lemma LIMSEQ_unique: 
44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44194
diff
changeset

334 
fixes a b :: "'a::t2_space" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

335 
shows "\<lbrakk>X > a; X > b\<rbrakk> \<Longrightarrow> a = b" 
44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44194
diff
changeset

336 
using trivial_limit_sequentially by (rule tendsto_unique) 
22608  337 

32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

338 
lemma increasing_LIMSEQ: 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

339 
fixes f :: "nat \<Rightarrow> real" 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

340 
assumes inc: "!!n. f n \<le> f (Suc n)" 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

341 
and bdd: "!!n. f n \<le> l" 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

342 
and en: "!!e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e" 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

343 
shows "f > l" 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

344 
proof (auto simp add: LIMSEQ_def) 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

345 
fix e :: real 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

346 
assume e: "0 < e" 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

347 
then obtain N where "l \<le> f N + e/2" 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

348 
by (metis half_gt_zero e en that) 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

349 
hence N: "l < f N + e" using e 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

350 
by simp 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

351 
{ fix k 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

352 
have [simp]: "!!n. \<bar>f n  l\<bar> = l  f n" 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

353 
by (simp add: bdd) 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

354 
have "\<bar>f (N+k)  l\<bar> < e" 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

355 
proof (induct k) 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

356 
case 0 show ?case using N 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32877
diff
changeset

357 
by simp 
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

358 
next 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

359 
case (Suc k) thus ?case using N inc [of "N+k"] 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32877
diff
changeset

360 
by simp 
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

361 
qed 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

362 
} note 1 = this 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

363 
{ fix n 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

364 
have "N \<le> n \<Longrightarrow> \<bar>f n  l\<bar> < e" using 1 [of "nN"] 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

365 
by simp 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

366 
} note [intro] = this 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

367 
show " \<exists>no. \<forall>n\<ge>no. dist (f n) l < e" 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

368 
by (auto simp add: dist_real_def) 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

369 
qed 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
32707
diff
changeset

370 

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

31355  380 
shows "\<lbrakk>X > a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))" 
36660
1cc4ab4b7ff7
make (X > L) an abbreviation for (X > L) sequentially
huffman
parents:
36657
diff
changeset

381 
unfolding Bseq_conv_Bfun by (rule Bfun_inverse) 
22608  382 

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

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

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

385 
shows "g > L ==> (%x. f x  g x) > 0 ==> f > L" 
44313  386 
by (drule (1) tendsto_add, simp) 
22614  387 

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

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

389 
fixes L :: "'a::real_normed_vector" 
35292
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
35216
diff
changeset

390 
shows "f > L ==> (%x. f x  g x) > 0 ==> g > L" 
44313  391 
by (drule (1) tendsto_diff, simp) 
22614  392 

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

394 

395 
lemma LIMSEQ_inverse_zero: 

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

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

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

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

22614  401 
apply (frule positive_imp_inverse_positive) 
22974  402 
apply (frule (1) less_imp_inverse_less) 
403 
apply (subgoal_tac "0 < X n", simp) 

404 
apply (erule (1) order_less_trans) 

22614  405 
done 
406 

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

408 

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

410 
apply (rule LIMSEQ_inverse_zero, safe) 

22974  411 
apply (cut_tac x = r in reals_Archimedean2) 
22614  412 
apply (safe, rule_tac x = n in exI) 
413 
apply (auto simp add: real_of_nat_Suc) 

414 
done 

415 

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

417 
infinity is now easily proved*} 

418 

419 
lemma LIMSEQ_inverse_real_of_nat_add: 

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

44313  421 
using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto 
22614  422 

423 
lemma LIMSEQ_inverse_real_of_nat_add_minus: 

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

44710  425 
using tendsto_add [OF tendsto_const 
426 
tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] by auto 

22614  427 

428 
lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: 

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

44313  430 
using tendsto_mult [OF tendsto_const 
431 
LIMSEQ_inverse_real_of_nat_add_minus [of 1]] 

432 
by auto 

22614  433 

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

436 
apply (rule ccontr, simp only: linorder_not_le) 

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

438 
apply clarsimp 

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

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

441 
apply simp 

442 
done 

443 

444 
lemma LIMSEQ_le_const2: 

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

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

447 
apply (rule LIMSEQ_le_const) 

44313  448 
apply (erule tendsto_minus) 
22615  449 
apply simp 
450 
done 

451 

452 
lemma LIMSEQ_le: 

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

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

455 
apply (rule LIMSEQ_le_const) 

44313  456 
apply (erule (1) tendsto_diff) 
22615  457 
apply (simp add: le_diff_eq) 
458 
done 

459 

15082  460 

20696  461 
subsection {* Convergence *} 
15082  462 

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

464 
apply (simp add: lim_def) 

465 
apply (blast intro: LIMSEQ_unique) 

466 
done 

467 

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

469 
by (simp add: convergent_def) 

470 

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

472 
by (auto simp add: convergent_def) 

473 

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

20682  475 
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def) 
15082  476 

36625  477 
lemma convergent_const: "convergent (\<lambda>n. c)" 
44313  478 
by (rule convergentI, rule tendsto_const) 
36625  479 

480 
lemma convergent_add: 

481 
fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector" 

482 
assumes "convergent (\<lambda>n. X n)" 

483 
assumes "convergent (\<lambda>n. Y n)" 

484 
shows "convergent (\<lambda>n. X n + Y n)" 

44313  485 
using assms unfolding convergent_def by (fast intro: tendsto_add) 
36625  486 

487 
lemma convergent_setsum: 

488 
fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector" 

36647  489 
assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)" 
36625  490 
shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)" 
36647  491 
proof (cases "finite A") 
36650  492 
case True from this and assms show ?thesis 
36647  493 
by (induct A set: finite) (simp_all add: convergent_const convergent_add) 
494 
qed (simp add: convergent_const) 

36625  495 

496 
lemma (in bounded_linear) convergent: 

497 
assumes "convergent (\<lambda>n. X n)" 

498 
shows "convergent (\<lambda>n. f (X n))" 

44313  499 
using assms unfolding convergent_def by (fast intro: tendsto) 
36625  500 

501 
lemma (in bounded_bilinear) convergent: 

502 
assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)" 

503 
shows "convergent (\<lambda>n. X n ** Y n)" 

44313  504 
using assms unfolding convergent_def by (fast intro: tendsto) 
36625  505 

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

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

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

508 
shows "convergent X \<longleftrightarrow> convergent (\<lambda>n.  X n)" 
20696  509 
apply (simp add: convergent_def) 
44313  510 
apply (auto dest: tendsto_minus) 
511 
apply (drule tendsto_minus, auto) 

20696  512 
done 
513 

32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

514 
lemma lim_le: 
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

515 
fixes x :: real 
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

516 
assumes f: "convergent f" and fn_le: "!!n. f n \<le> x" 
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

517 
shows "lim f \<le> x" 
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

518 
proof (rule classical) 
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

519 
assume "\<not> lim f \<le> x" 
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

520 
hence 0: "0 < lim f  x" by arith 
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

521 
have 1: "f> lim f" 
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

522 
by (metis convergent_LIMSEQ_iff f) 
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

523 
thus ?thesis 
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

524 
proof (simp add: LIMSEQ_iff) 
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

525 
assume "\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>f n  lim f\<bar> < r" 
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

526 
hence "\<exists>no. \<forall>n\<ge>no. \<bar>f n  lim f\<bar> < lim f  x" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32877
diff
changeset

527 
by (metis 0) 
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

528 
from this obtain no where "\<forall>n\<ge>no. \<bar>f n  lim f\<bar> < lim f  x" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32877
diff
changeset

529 
by blast 
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

530 
thus "lim f \<le> x" 
37887  531 
by (metis 1 LIMSEQ_le_const2 fn_le) 
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

532 
qed 
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

533 
qed 
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

534 

41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

535 
lemma monoseq_le: 
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

536 
fixes a :: "nat \<Rightarrow> real" 
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

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

538 
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

539 
((\<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

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

541 
{ 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

542 
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

543 
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

544 
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

545 
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

546 
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

547 
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

548 
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

549 
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

550 
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

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

552 
{ 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

553 
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

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

555 
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

556 
with monotone[where m=n and n="max no n"] 
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32064
diff
changeset

557 
show False by (auto simp:max_def split:split_if_asm) 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

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

559 
} 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

560 
{ 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

561 
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

562 
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

563 
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

564 
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

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

566 
case False with `monoseq a`[unfolded monoseq_def] have "\<forall> m. \<forall> n \<ge> m.  a m \<le>  a n" by auto 
44313  567 
hence " a m \<le>  x" using top_down[OF tendsto_minus[OF `a > x`]] by blast 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

568 
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

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

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

571 
} 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

572 

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

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

574 
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

575 
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

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

577 
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

578 
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

579 
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

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

581 
case False hence " a m <  x" using `a m \<noteq> x` by auto 
44313  582 
with when_decided[OF tendsto_minus[OF `a > x`] monoseq_minus[OF `monoseq a`], where m2=m] 
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29667
diff
changeset

583 
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

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

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

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

587 

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

36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

590 
apply (rule topological_tendstoI) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

591 
apply (drule (2) topological_tendstoD) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

592 
apply (simp only: eventually_sequentially) 
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

593 
apply (clarify, rule_tac x=N in exI, clarsimp) 
30730  594 
apply (blast intro: seq_suble le_trans dest!: spec) 
595 
done 

596 

44208  597 
lemma convergent_subseq_convergent: 
598 
"\<lbrakk>convergent X; subseq f\<rbrakk> \<Longrightarrow> convergent (X o f)" 

599 
unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ) 

600 

601 

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

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

603 

20696  604 
text{*Bounded Sequence*} 
15082  605 

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

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

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

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

612 
lemma lemma_NBseq_def: 

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

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

614 
(\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" 
32064  615 
proof auto 
616 
fix K :: real 

617 
from reals_Archimedean2 obtain n :: nat where "K < real n" .. 

618 
then have "K \<le> real (Suc n)" by auto 

619 
assume "\<forall>m. norm (X m) \<le> K" 

620 
have "\<forall>m. norm (X m) \<le> real (Suc n)" 

621 
proof 

622 
fix m :: 'a 

623 
from `\<forall>m. norm (X m) \<le> K` have "norm (X m) \<le> K" .. 

624 
with `K \<le> real (Suc n)` show "norm (X m) \<le> real (Suc n)" by auto 

625 
qed 

626 
then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" .. 

627 
next 

628 
fix N :: nat 

629 
have "real (Suc N) > 0" by (simp add: real_of_nat_Suc) 

630 
moreover assume "\<forall>n. norm (X n) \<le> real (Suc N)" 

631 
ultimately show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" by blast 

632 
qed 

633 

15082  634 

635 
text{* alternative definition for Bseq *} 

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

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

639 
done 

640 

641 
lemma lemma_NBseq_def2: 

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

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

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

646 
apply (auto simp add: real_of_nat_Suc) 

647 
prefer 2 apply (blast intro: order_less_imp_le) 

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

649 
done 

650 

651 
(* yet another definition for Bseq *) 

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

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

20696  655 
subsubsection{*Upper Bounds and Lubs of Bounded Sequences*} 
15082  656 

657 
lemma Bseq_isUb: 

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

22998  659 
by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff) 
15082  660 

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

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

663 

664 
lemma Bseq_isLub: 

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

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

667 
by (blast intro: reals_complete Bseq_isUb) 

668 

20696  669 
subsubsection{*A Bounded and Monotonic Sequence Converges*} 
15082  670 

44714  671 
(* TODO: delete *) 
672 
(* FIXME: one use in NSA/HSEQ.thy *) 

15082  673 
lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n > X n = X m ==> \<exists>L. (X > L)" 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36660
diff
changeset

674 
unfolding tendsto_def eventually_sequentially 
15082  675 
apply (rule_tac x = "X m" in exI, safe) 
676 
apply (rule_tac x = m in exI, safe) 

677 
apply (drule spec, erule impE, auto) 

678 
done 

679 

44714  680 
text {* A monotone sequence converges to its least upper bound. *} 
15082  681 

44714  682 
lemma isLub_mono_imp_LIMSEQ: 
683 
fixes X :: "nat \<Rightarrow> real" 

684 
assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *) 

685 
assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n" 

686 
shows "X > u" 

687 
proof (rule LIMSEQ_I) 

688 
have 1: "\<forall>n. X n \<le> u" 

689 
using isLubD2 [OF u] by auto 

690 
have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y" 

691 
using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def) 

692 
hence 2: "\<forall>y<u. \<exists>n. y < X n" 

693 
by (metis not_le) 

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

695 
hence "u  r < u" by simp 

696 
hence "\<exists>m. u  r < X m" using 2 by simp 

697 
then obtain m where "u  r < X m" .. 

698 
with X have "\<forall>n\<ge>m. u  r < X n" 

699 
by (fast intro: less_le_trans) 

700 
hence "\<exists>m. \<forall>n\<ge>m. u  r < X n" .. 

701 
thus "\<exists>m. \<forall>n\<ge>m. norm (X n  u) < r" 

702 
using 1 by (simp add: diff_less_eq add_commute) 

703 
qed 

15082  704 

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

706 

707 
lemma Bseq_mono_convergent: 

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

708 
"[ Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n ] ==> convergent (X::nat=>real)" 
44714  709 
proof  
710 
assume "Bseq X" 

711 
then obtain u where u: "isLub UNIV {x. \<exists>n. X n = x} u" 

712 
using Bseq_isLub by fast 

713 
assume "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n" 

714 
with u have "X > u" 

715 
by (rule isLub_mono_imp_LIMSEQ) 

716 
thus "convergent X" 

717 
by (rule convergentI) 

718 
qed 

15082  719 

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

721 
by (simp add: Bseq_def) 

722 

723 
text{*Main monotonicity theorem*} 

41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

724 
lemma Bseq_monoseq_convergent: "[ Bseq X; monoseq X ] ==> convergent (X::nat\<Rightarrow>real)" 
15082  725 
apply (simp add: monoseq_def, safe) 
726 
apply (rule_tac [2] convergent_minus_iff [THEN ssubst]) 

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

728 
apply (auto intro!: Bseq_mono_convergent) 

729 
done 

730 

30730  731 
subsubsection{*Increasing and Decreasing Series*} 
732 

41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

733 
lemma incseq_le: 
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

734 
fixes X :: "nat \<Rightarrow> real" 
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

735 
assumes inc: "incseq X" and lim: "X > L" shows "X n \<le> L" 
30730  736 
using monoseq_le [OF incseq_imp_monoseq [OF inc] lim] 
737 
proof 

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

739 
thus ?thesis by simp 

740 
next 

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

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

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

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

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

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

44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44313
diff
changeset

747 
by (blast intro: X) 
44313  748 
hence "L = X 0" using tendsto_const [of "X 0" sequentially] 
749 
by (auto intro: LIMSEQ_unique lim) 

30730  750 
thus ?thesis 
751 
by (blast intro: eq_refl X) 

752 
qed 

753 

41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

754 
lemma decseq_le: 
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

755 
fixes X :: "nat \<Rightarrow> real" assumes dec: "decseq X" and lim: "X > L" shows "L \<le> X n" 
30730  756 
proof  
757 
have inc: "incseq (\<lambda>n.  X n)" using dec 

758 
by (simp add: decseq_eq_incseq) 

759 
have " X n \<le>  L" 

44313  760 
by (blast intro: incseq_le [OF inc] tendsto_minus lim) 
30730  761 
thus ?thesis 
762 
by simp 

763 
qed 

764 

20696  765 
subsubsection{*A Few More Equivalence Theorems for Boundedness*} 
15082  766 

767 
text{*alternative formulation for boundedness*} 

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

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

770 
apply (rule_tac [2] x = "k + norm x" in exI) 
15360  771 
apply (rule_tac x = K in exI, simp) 
15221  772 
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

773 
apply (erule order_less_le_trans, simp) 
37887  774 
apply (drule_tac x=n in spec, fold diff_minus) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20408
diff
changeset

775 
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

776 
apply simp 
15082  777 
done 
778 

779 
text{*alternative formulation for boundedness*} 

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

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

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

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

785 
apply (erule order_less_le_trans, simp) 
15082  786 
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

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

788 
apply (rule order_trans [OF norm_triangle_ineq], simp) 
15082  789 
apply (auto simp add: Bseq_iff2) 
790 
done 

791 

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

792 
lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f" 
15082  793 
apply (simp add: Bseq_def) 
15221  794 
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

795 
apply (drule_tac x = n in spec, arith) 
15082  796 
done 
797 

798 

20696  799 
subsection {* Cauchy Sequences *} 
15082  800 

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

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

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

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

804 

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

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

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

807 
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

808 

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

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

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

811 
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

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

813 

35292
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
35216
diff
changeset

814 
lemma Cauchy_iff2: 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
35216
diff
changeset

815 
"Cauchy X = 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
35216
diff
changeset

816 
(\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m  X n\<bar> < inverse(real (Suc j))))" 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
35216
diff
changeset

817 
apply (simp add: Cauchy_iff, auto) 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
35216
diff
changeset

818 
apply (drule reals_Archimedean, safe) 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
35216
diff
changeset

819 
apply (drule_tac x = n in spec, auto) 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
35216
diff
changeset

820 
apply (rule_tac x = M in exI, auto) 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
35216
diff
changeset

821 
apply (drule_tac x = m in spec, simp) 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
35216
diff
changeset

822 
apply (drule_tac x = na in spec, auto) 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
35216
diff
changeset

823 
done 
e4a431b6d9b7
Replaced Integration by MultivariateAnalysis/Real_Integration
hoelzl
parents:
35216
diff
changeset

824 

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

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

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

827 
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

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

829 

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

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

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

832 
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

833 
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

834 

30730  835 
lemma Cauchy_subseq_Cauchy: 
836 
"\<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

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

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

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

840 
apply (blast intro: le_trans [OF _ seq_suble] dest!: spec) 
30730  841 
done 
842 

20696  843 
subsubsection {* Cauchy Sequences are Bounded *} 
844 

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

847 

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

849 
==> \<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

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

852 
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

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

854 
done 
15082  855 

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

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

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

858 
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

859 
apply (drule_tac x="M" in spec, simp) 
15082  860 
apply (drule lemmaCauchy) 
22608  861 
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

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

863 
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

864 
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

865 
apply (simp add: order_less_imp_le) 
15082  866 
done 
867 

20696  868 
subsubsection {* Cauchy Sequences are Convergent *} 
15082  869 

44206
5e4a1664106e
localeize some constant definitions, so complete_space can inherit from metric_space
huffman
parents:
44205
diff
changeset

870 
class complete_space = metric_space + 
33042  871 
assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X" 
20830
65ba80cae6df
add axclass banach for complete normed vector spaces
huffman
parents:
20829
diff
changeset

872 

33042  873 
class banach = real_normed_vector + complete_space 
31403  874 

22629  875 
theorem LIMSEQ_imp_Cauchy: 
876 
assumes X: "X > a" shows "Cauchy X" 

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

877 
proof (rule metric_CauchyI) 
22629  878 
fix e::real assume "0 < e" 
879 
hence "0 < e/2" by simp 

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

880 
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

881 
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

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

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

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

887 
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

888 
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

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

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

891 
finally show "dist (X m) (X n) < e" . 
22629  892 
qed 
893 
qed 

894 

20691  895 
lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X" 
22629  896 
unfolding convergent_def 
897 
by (erule exE, erule LIMSEQ_imp_Cauchy) 

20691  898 

31403  899 
lemma Cauchy_convergent_iff: 
900 
fixes X :: "nat \<Rightarrow> 'a::complete_space" 

901 
shows "Cauchy X = convergent X" 

902 
by (fast intro: Cauchy_convergent convergent_Cauchy) 

903 

22629  904 
text {* 
905 
Proof that Cauchy sequences converge based on the one from 

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

907 
*} 

908 

909 
text {* 

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

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

912 
*} 

913 

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

915 
by (simp add: isUbI setleI) 

916 

27681  917 
locale real_Cauchy = 
22629  918 
fixes X :: "nat \<Rightarrow> real" 
919 
assumes X: "Cauchy X" 

920 
fixes S :: "real set" 

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

922 

27681  923 
lemma real_CauchyI: 
924 
assumes "Cauchy X" 

925 
shows "real_Cauchy X" 

28823  926 
proof qed (fact assms) 
27681  927 

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

930 

931 
lemma (in real_Cauchy) bound_isUb: 

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

933 
shows "isUb UNIV S x" 

934 
proof (rule isUb_UNIV_I) 

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

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

937 
by (simp add: S_def) 

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

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

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

941 
finally show "y \<le> x" 

942 
by (rule order_less_imp_le) 

943 
qed 

944 

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

946 
proof (rule reals_complete) 

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

32064  948 
using CauchyD [OF X zero_less_one] by auto 
22629  949 
hence N: "\<forall>n\<ge>N. norm (X n  X N) < 1" by simp 
950 
show "\<exists>x. x \<in> S" 

951 
proof 

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

32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

953 
by (simp add: abs_diff_less_iff) 
22629  954 
thus "X N  1 \<in> S" by (rule mem_S) 
955 
qed 

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

957 
proof 

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

32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

959 
by (simp add: abs_diff_less_iff) 
22629  960 
thus "isUb UNIV S (X N + 1)" 
961 
by (rule bound_isUb) 

962 
qed 

963 
qed 

964 

965 
lemma (in real_Cauchy) isLub_imp_LIMSEQ: 

966 
assumes x: "isLub UNIV S x" 

967 
shows "X > x" 

968 
proof (rule LIMSEQ_I) 

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

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

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

32064  972 
using CauchyD [OF X r] by auto 
22629  973 
hence "\<forall>n\<ge>N. norm (X n  X N) < r/2" by simp 
974 
hence N: "\<forall>n\<ge>N. X N  r/2 < X n \<and> X n < X N + r/2" 

32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

975 
by (simp only: real_norm_def abs_diff_less_iff) 
22629  976 

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

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

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

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

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

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

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

986 
proof (intro exI allI impI) 

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

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

32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
32436
diff
changeset

990 
by (simp add: abs_diff_less_iff) 
22629  991 
qed 
992 
qed 

993 

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

995 
proof  

996 
obtain x where "isLub UNIV S x" 

997 
using isLub_ex by fast 

998 
hence "X > x" 

999 
by (rule isLub_imp_LIMSEQ) 

1000 
thus ?thesis .. 

1001 
qed 

1002 

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

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

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

1005 
shows "Cauchy X \<Longrightarrow> convergent X" 
27681  1006 
unfolding convergent_def 
1007 
by (rule real_Cauchy.LIMSEQ_ex) 

1008 
(rule real_CauchyI) 

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

1009 

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

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

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

1012 

15082  1013 

20696  1014 
subsection {* Power Sequences *} 
15082  1015 

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

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

1018 
also fact that bounded and monotonic sequence converges.*} 

1019 

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

1020 
lemma Bseq_realpow: "[ 0 \<le> (x::real); x \<le> 1 ] ==> Bseq (%n. x ^ n)" 
15082  1021 
apply (simp add: Bseq_def) 
1022 
apply (rule_tac x = 1 in exI) 

1023 
apply (simp add: power_abs) 

22974  1024 
apply (auto dest: power_mono) 
15082  1025 
done 
1026 

41367
1b65137d598c
generalized monoseq, decseq and incseq; simplified proof for seq_monosub
hoelzl
parents:
40811
diff
changeset

1027 
lemma monoseq_realpow: fixes x :: real shows "[ 0 \<le> x; x \<le> 1 ] ==> monoseq (%n. x ^ n)" 
15082  1028 
apply (clarify intro!: mono_SucI2) 
1029 
apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto) 

1030 
done 

1031 

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

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

1033 
"[ 0 \<le> (x::real); x \<le> 1 ] ==> convergent (%n. x ^ n)" 
15082  1034 
by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) 
1035 

22628  1036 
lemma LIMSEQ_inverse_realpow_zero_lemma: 
1037 
fixes x :: real 

1038 
assumes x: "0 \<le> x" 

1039 
shows "real n * x + 1 \<le> (x + 1) ^ n" 

1040 
apply (induct n) 

1041 
apply simp 

1042 
apply simp 

1043 
apply (rule order_trans) 

1044 
prefer 2 

1045 
apply (erule mult_left_mono) 

1046 
apply (rule add_increasing [OF x], simp) 

1047 
apply (simp add: real_of_nat_Suc) 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23127
diff
changeset

1048 
apply (simp add: ring_distribs) 
22628  1049 
apply (simp add: mult_nonneg_nonneg x) 
1050 
done 

1051 

1052 
lemma LIMSEQ_inverse_realpow_zero: 

1053 
"1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) > 0" 

1054 
proof (rule LIMSEQ_inverse_zero [rule_format]) 

1055 
fix y :: real 

1056 
assume x: "1 < x" 

1057 
hence "0 < x  1" by simp 

1058 
hence "\<forall>y. \<exists>N::nat. y < real N * (x  1)" 

1059 
by (rule reals_Archimedean3) 

1060 
hence "\<exists>N::nat. y < real N * (x  1)" .. 

1061 
then obtain N::nat where "y < real N * (x  1)" .. 

1062 
also have "\<dots> \<le> real N * (x  1) + 1" by simp 

1063 
also have "\<dots> \<le> (x  1 + 1) ^ N" 

1064 
by (rule LIMSEQ_inverse_realpow_zero_lemma, cut_tac x, simp) 

1065 
also have "\<dots> = x ^ N" by simp 

1066 
finally have "y < x ^ N" . 

1067 
hence "\<forall>n\<ge>N. y < x ^ n" 

1068 
apply clarify 

1069 
apply (erule order_less_le_trans) 

1070 
apply (erule power_increasing) 

1071 
apply (rule order_less_imp_le [OF x]) 

1072 
done 

1073 
thus "\<exists>N. \<forall>n\<ge>N. y < x ^ n" .. 

1074 
qed 

1075 

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

1076 
lemma LIMSEQ_realpow_zero: 
22628  1077 
"\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) > 0" 
1078 
proof (cases) 

1079 
assume "x = 0" 

44313  1080 
hence "(\<lambda>n. x ^ Suc n) > 0" by (simp add: tendsto_const) 
22628  1081 
thus ?thesis by (rule LIMSEQ_imp_Suc) 
1082 
next 

1083 
assume "0 \<le> x" and "x \<noteq> 0" 

1084 
hence x0: "0 < x" by simp 

1085 
assume x1: "x < 1" 

1086 
from x0 x1 have "1 < inverse x" 

36776
c137ae7673d3
remove a couple of redundant lemmas; simplify some proofs
huffman
parents:
36663
diff
changeset

1087 
by (rule one_less_inverse) 
22628  1088 
hence "(\<lambda>n. inverse (inverse x ^ n)) > 0" 
1089 
by (rule LIMSEQ_inverse_realpow_zero) 

1090 
thus ?thesis by (simp add: power_inverse) 

1091 
qed 

15082  1092 

20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset

1093 
lemma LIMSEQ_power_zero: 
31017  1094 
fixes x :: "'a::{real_normed_algebra_1}" 
20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset

1095 
shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) > 0" 
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset

1096 
apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero]) 
44313  1097 
apply (simp only: tendsto_Zfun_iff, erule Zfun_le) 
22974  1098 
apply (simp add: power_abs norm_power_ineq) 
20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset

1099 
done 
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset

1100 

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

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

1102 
"1 < (x::real) ==> (%n. a / (x ^ n)) > 0" 
44313  1103 
using tendsto_mult [OF tendsto_const [of a] 
1104 
LIMSEQ_realpow_zero [of "inverse x"]] 

15082  1105 
apply (auto simp add: divide_inverse power_inverse) 
1106 
apply (simp add: inverse_eq_divide pos_divide_less_eq) 

1107 
done 

1108 

15102  1109 
text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*} 
15082  1110 

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

1111 
lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) > 0" 
20685
fee8c75e3b5d
added lemmas about LIMSEQ and norm; simplified some proofs
huffman
parents:
20682
diff
changeset

1112 
by (rule LIMSEQ_realpow_zero [OF abs_ge_zero]) 
15082  1113 

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

1114 
lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) > 0" 
44313  1115 
apply (rule tendsto_rabs_zero_cancel) 
15082  1116 
apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs) 
1117 
done 

1118 

10751  1119 
end 