author  nipkow 
Wed, 02 Mar 2005 12:06:15 +0100  
changeset 15561  045a07ac35a7 
parent 15546  5188ce7316b7 
child 16733  236dfafbeb63 
permissions  rwrr 
10751  1 
(* Title : Series.thy 
2 
Author : Jacques D. Fleuriot 

3 
Copyright : 1998 University of Cambridge 

14416  4 

5 
Converted to Isar and polished by lcp 

15539  6 
Converted to setsum and polished yet more by TNN 
10751  7 
*) 
8 

14416  9 
header{*Finite Summation and Infinite Series*} 
10751  10 

15131  11 
theory Series 
15140  12 
imports SEQ Lim 
15131  13 
begin 
15561  14 

15539  15 
declare atLeastLessThan_iff[iff] 
15561  16 
declare setsum_op_ivl_Suc[simp] 
10751  17 

18 
constdefs 

15543  19 
sums :: "(nat => real) => real => bool" (infixr "sums" 80) 
15536  20 
"f sums s == (%n. setsum f {0..<n}) > s" 
10751  21 

14416  22 
summable :: "(nat=>real) => bool" 
23 
"summable f == (\<exists>s. f sums s)" 

24 

25 
suminf :: "(nat=>real) => real" 

15539  26 
"suminf f == SOME s. f sums s" 
14416  27 

15546  28 
syntax 
29 
"_suminf" :: "idt => real => real" ("\<Sum>_. _" [0, 10] 10) 

30 
translations 

31 
"\<Sum>i. b" == "suminf (%i. b)" 

32 

14416  33 

15539  34 
lemma sumr_diff_mult_const: 
35 
"setsum f {0..<n}  (real n*r) = setsum (%i. f i  r) {0..<n::nat}" 

15536  36 
by (simp add: diff_minus setsum_addf real_of_nat_def) 
37 

15542  38 
lemma real_setsum_nat_ivl_bounded: 
39 
"(!!p. p < n \<Longrightarrow> f(p) \<le> K) 

40 
\<Longrightarrow> setsum f {0..<n::nat} \<le> real n * K" 

41 
using setsum_bounded[where A = "{0..<n}"] 

42 
by (auto simp:real_of_nat_def) 

14416  43 

15539  44 
(* Generalize from real to some algebraic structure? *) 
45 
lemma sumr_minus_one_realpow_zero [simp]: 

15543  46 
"(\<Sum>i=0..<2*n. (1) ^ Suc i) = (0::real)" 
15251  47 
by (induct "n", auto) 
14416  48 

15539  49 
(* FIXME this is an awful lemma! *) 
50 
lemma sumr_one_lb_realpow_zero [simp]: 

51 
"(\<Sum>n=Suc 0..<n. f(n) * (0::real) ^ n) = 0" 

15251  52 
apply (induct "n") 
14416  53 
apply (case_tac [2] "n", auto) 
54 
done 

55 

15543  56 
lemma sumr_group: 
15539  57 
"(\<Sum>m=0..<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {0 ..< n * k}" 
15543  58 
apply (subgoal_tac "k = 0  0 < k", auto) 
15251  59 
apply (induct "n") 
15539  60 
apply (simp_all add: setsum_add_nat_ivl add_commute) 
14416  61 
done 
15539  62 

14416  63 

64 
subsection{* Infinite Sums, by the Properties of Limits*} 

65 

66 
(* 

67 
suminf is the sum 

68 
*) 

69 
lemma sums_summable: "f sums l ==> summable f" 

70 
by (simp add: sums_def summable_def, blast) 

71 

72 
lemma summable_sums: "summable f ==> f sums (suminf f)" 

73 
apply (simp add: summable_def suminf_def) 

74 
apply (blast intro: someI2) 

75 
done 

76 

77 
lemma summable_sumr_LIMSEQ_suminf: 

15539  78 
"summable f ==> (%n. setsum f {0..<n}) > (suminf f)" 
14416  79 
apply (simp add: summable_def suminf_def sums_def) 
80 
apply (blast intro: someI2) 

81 
done 

82 

83 
(* 

84 
sum is unique 

85 
*) 

86 
lemma sums_unique: "f sums s ==> (s = suminf f)" 

87 
apply (frule sums_summable [THEN summable_sums]) 

88 
apply (auto intro!: LIMSEQ_unique simp add: sums_def) 

89 
done 

90 

91 
lemma series_zero: 

15539  92 
"(\<forall>m. n \<le> m > f(m) = 0) ==> f sums (setsum f {0..<n})" 
15537  93 
apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe) 
14416  94 
apply (rule_tac x = n in exI) 
15542  95 
apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong) 
14416  96 
done 
97 

15539  98 

14416  99 
lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)" 
15536  100 
by (auto simp add: sums_def setsum_mult [symmetric] 
14416  101 
intro!: LIMSEQ_mult intro: LIMSEQ_const) 
102 

103 
lemma sums_divide: "x sums x' ==> (%n. x(n)/c) sums (x'/c)" 

104 
by (simp add: real_divide_def sums_mult mult_commute [of _ "inverse c"]) 

105 

106 
lemma sums_diff: "[ x sums x0; y sums y0 ] ==> (%n. x n  y n) sums (x0y0)" 

15536  107 
by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff) 
14416  108 

15546  109 
lemma suminf_mult: "summable f ==> suminf f * c = (\<Sum>n. f n * c)" 
14416  110 
by (auto intro!: sums_unique sums_mult summable_sums simp add: mult_commute) 
111 

15546  112 
lemma suminf_mult2: "summable f ==> c * suminf f = (\<Sum>n. c * f n)" 
14416  113 
by (auto intro!: sums_unique sums_mult summable_sums) 
114 

115 
lemma suminf_diff: 

116 
"[ summable f; summable g ] 

15546  117 
==> suminf f  suminf g = (\<Sum>n. f n  g n)" 
14416  118 
by (auto intro!: sums_diff sums_unique summable_sums) 
119 

120 
lemma sums_minus: "x sums x0 ==> (%n.  x n) sums  x0" 

15536  121 
by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf) 
14416  122 

123 
lemma sums_group: 

15539  124 
"[summable f; 0 < k ] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)" 
14416  125 
apply (drule summable_sums) 
15543  126 
apply (auto simp add: sums_def LIMSEQ_def sumr_group) 
14416  127 
apply (drule_tac x = r in spec, safe) 
128 
apply (rule_tac x = no in exI, safe) 

129 
apply (drule_tac x = "n*k" in spec) 

130 
apply (auto dest!: not_leE) 

131 
apply (drule_tac j = no in less_le_trans, auto) 

132 
done 

133 

134 
lemma sumr_pos_lt_pair_lemma: 

15539  135 
"[\<forall>d.  f (n + (d + d)) < (f (Suc (n + (d + d))) :: real) ] 
136 
==> setsum f {0..<n+Suc(Suc 0)} \<le> setsum f {0..<Suc(Suc 0) * Suc no + n}" 

15251  137 
apply (induct "no", auto) 
138 
apply (drule_tac x = "Suc no" in spec) 

15539  139 
apply (simp add: add_ac) 
14416  140 
done 
10751  141 

142 

14416  143 
lemma sumr_pos_lt_pair: 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

144 
"[summable f; 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

145 
\<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))] 
15539  146 
==> setsum f {0..<n} < suminf f" 
14416  147 
apply (drule summable_sums) 
148 
apply (auto simp add: sums_def LIMSEQ_def) 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

149 
apply (drule_tac x = "f (n) + f (n + 1)" in spec) 
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

150 
apply (auto iff: real_0_less_add_iff) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

151 
{*legacy proof: not necessarily better!*} 
14416  152 
apply (rule_tac [2] ccontr, drule_tac [2] linorder_not_less [THEN iffD1]) 
153 
apply (frule_tac [2] no=no in sumr_pos_lt_pair_lemma) 

154 
apply (drule_tac x = 0 in spec, simp) 

155 
apply (rotate_tac 1, drule_tac x = "Suc (Suc 0) * (Suc no) + n" in spec) 

156 
apply (safe, simp) 

15539  157 
apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \<le> 
158 
setsum f {0 ..< Suc (Suc 0) * (Suc no) + n}") 

159 
apply (rule_tac [2] y = "setsum f {0..<n+ Suc (Suc 0)}" in order_trans) 

14416  160 
prefer 3 apply assumption 
15539  161 
apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans) 
14416  162 
apply simp_all 
15539  163 
apply (subgoal_tac "suminf f \<le> setsum f {0..< Suc (Suc 0) * (Suc no) + n}") 
14416  164 
apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans) 
15539  165 
prefer 3 apply simp 
14416  166 
apply (drule_tac [2] x = 0 in spec) 
167 
prefer 2 apply simp 

15539  168 
apply (subgoal_tac "0 \<le> setsum f {0 ..< Suc (Suc 0) * Suc no + n} +  suminf f") 
169 
apply (simp add: abs_if) 

14416  170 
apply (auto simp add: linorder_not_less [symmetric]) 
171 
done 

172 

15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

173 
text{*A summable series of positive terms has limit that is at least as 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

174 
great as any partial sum.*} 
14416  175 

176 
lemma series_pos_le: 

15539  177 
"[ summable f; \<forall>m \<ge> n. 0 \<le> f(m) ] ==> setsum f {0..<n} \<le> suminf f" 
14416  178 
apply (drule summable_sums) 
179 
apply (simp add: sums_def) 

15539  180 
apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const) 
181 
apply (erule LIMSEQ_le, blast) 

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

183 
apply (rule setsum_mono2) 

184 
apply auto 

14416  185 
done 
186 

187 
lemma series_pos_less: 

15539  188 
"[ summable f; \<forall>m \<ge> n. 0 < f(m) ] ==> setsum f {0..<n} < suminf f" 
189 
apply (rule_tac y = "setsum f {0..<Suc n}" in order_less_le_trans) 

14416  190 
apply (rule_tac [2] series_pos_le, auto) 
191 
apply (drule_tac x = m in spec, auto) 

192 
done 

193 

15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

194 
text{*Sum of a geometric progression.*} 
14416  195 

15539  196 
lemma sumr_geometric: 
197 
"x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = (x ^ n  1) / (x  1::real)" 

15251  198 
apply (induct "n", auto) 
14416  199 
apply (rule_tac c1 = "x  1" in real_mult_right_cancel [THEN iffD1]) 
15539  200 
apply (auto simp add: mult_assoc left_distrib) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

201 
apply (simp add: right_distrib diff_minus mult_commute) 
14416  202 
done 
203 

204 
lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1  x))" 

205 
apply (case_tac "x = 1") 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

206 
apply (auto dest!: LIMSEQ_rabs_realpow_zero2 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

207 
simp add: sumr_geometric sums_def diff_minus add_divide_distrib) 
14416  208 
apply (subgoal_tac "1 / (1 + x) = 0/ (x  1) +  1/ (x  1) ") 
209 
apply (erule ssubst) 

210 
apply (rule LIMSEQ_add, rule LIMSEQ_divide) 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

211 
apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2) 
14416  212 
done 
213 

15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

214 
text{*Cauchytype criterion for convergence of series (c.f. Harrison)*} 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

215 

15539  216 
lemma summable_convergent_sumr_iff: 
217 
"summable f = convergent (%n. setsum f {0..<n})" 

14416  218 
by (simp add: summable_def sums_def convergent_def) 
219 

220 
lemma summable_Cauchy: 

221 
"summable f = 

15539  222 
(\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(setsum f {m..<n}) < e)" 
15537  223 
apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus[symmetric]) 
15539  224 
apply (drule_tac [!] spec, auto) 
14416  225 
apply (rule_tac x = M in exI) 
226 
apply (rule_tac [2] x = N in exI, auto) 

227 
apply (cut_tac [!] m = m and n = n in less_linear, auto) 

228 
apply (frule le_less_trans [THEN less_imp_le], assumption) 

15360  229 
apply (drule_tac x = n in spec, simp) 
14416  230 
apply (drule_tac x = m in spec) 
15539  231 
apply(simp add: setsum_diff[symmetric]) 
15537  232 
apply(subst abs_minus_commute) 
15539  233 
apply(simp add: setsum_diff[symmetric]) 
234 
apply(simp add: setsum_diff[symmetric]) 

14416  235 
done 
236 

15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

237 
text{*Comparison test*} 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

238 

14416  239 
lemma summable_comparison_test: 
15360  240 
"[ \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g ] ==> summable f" 
14416  241 
apply (auto simp add: summable_Cauchy) 
242 
apply (drule spec, auto) 

243 
apply (rule_tac x = "N + Na" in exI, auto) 

244 
apply (rotate_tac 2) 

245 
apply (drule_tac x = m in spec) 

246 
apply (auto, rotate_tac 2, drule_tac x = n in spec) 

15539  247 
apply (rule_tac y = "\<Sum>k=m..<n. abs(f k)" in order_le_less_trans) 
15536  248 
apply (rule setsum_abs) 
15539  249 
apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans) 
250 
apply (auto intro: setsum_mono simp add: abs_interval_iff) 

14416  251 
done 
252 

253 
lemma summable_rabs_comparison_test: 

15360  254 
"[ \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g ] 
14416  255 
==> summable (%k. abs (f k))" 
256 
apply (rule summable_comparison_test) 

15543  257 
apply (auto) 
14416  258 
done 
259 

15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

260 
text{*Limit comparison property for series (c.f. jrh)*} 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

261 

14416  262 
lemma summable_le: 
263 
"[\<forall>n. f n \<le> g n; summable f; summable g ] ==> suminf f \<le> suminf g" 

264 
apply (drule summable_sums)+ 

265 
apply (auto intro!: LIMSEQ_le simp add: sums_def) 

266 
apply (rule exI) 

15539  267 
apply (auto intro!: setsum_mono) 
14416  268 
done 
269 

270 
lemma summable_le2: 

271 
"[\<forall>n. abs(f n) \<le> g n; summable g ] 

272 
==> summable f & suminf f \<le> suminf g" 

273 
apply (auto intro: summable_comparison_test intro!: summable_le) 

274 
apply (simp add: abs_le_interval_iff) 

275 
done 

276 

15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

277 
text{*Absolute convergence imples normal convergence*} 
14416  278 
lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f" 
15536  279 
apply (auto simp add: summable_Cauchy) 
14416  280 
apply (drule spec, auto) 
281 
apply (rule_tac x = N in exI, auto) 

282 
apply (drule spec, auto) 

15539  283 
apply (rule_tac y = "\<Sum>n=m..<n. abs(f n)" in order_le_less_trans) 
15536  284 
apply (auto) 
14416  285 
done 
286 

15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

287 
text{*Absolute convergence of series*} 
14416  288 
lemma summable_rabs: 
15546  289 
"summable (%n. abs (f n)) ==> abs(suminf f) \<le> (\<Sum>n. abs(f n))" 
15536  290 
by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf) 
14416  291 

292 

293 
subsection{* The Ratio Test*} 

294 

295 
lemma rabs_ratiotest_lemma: "[ c \<le> 0; abs x \<le> c * abs y ] ==> x = (0::real)" 

296 
apply (drule order_le_imp_less_or_eq, auto) 

297 
apply (subgoal_tac "0 \<le> c * abs y") 

298 
apply (simp add: zero_le_mult_iff, arith) 

299 
done 

300 

301 
lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)" 

302 
apply (drule le_imp_less_or_eq) 

303 
apply (auto dest: less_imp_Suc_add) 

304 
done 

305 

306 
lemma le_Suc_ex_iff: "((k::nat) \<le> l) = (\<exists>n. l = k + n)" 

307 
by (auto simp add: le_Suc_ex) 

308 

309 
(*All this trouble just to get 0<c *) 

310 
lemma ratio_test_lemma2: 

15360  311 
"[ \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) ] 
14416  312 
==> 0 < c  summable f" 
313 
apply (simp (no_asm) add: linorder_not_le [symmetric]) 

314 
apply (simp add: summable_Cauchy) 

15543  315 
apply (safe, subgoal_tac "\<forall>n. N < n > f (n) = 0") 
316 
prefer 2 

317 
apply clarify 

318 
apply(erule_tac x = "n  1" in allE) 

319 
apply (simp add:diff_Suc split:nat.splits) 

320 
apply (blast intro: rabs_ratiotest_lemma) 

14416  321 
apply (rule_tac x = "Suc N" in exI, clarify) 
15543  322 
apply(simp cong:setsum_ivl_cong) 
14416  323 
done 
324 

325 
lemma ratio_test: 

15360  326 
"[ c < 1; \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) ] 
14416  327 
==> summable f" 
328 
apply (frule ratio_test_lemma2, auto) 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

329 
apply (rule_tac g = "%n. (abs (f N) / (c ^ N))*c ^ n" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

330 
in summable_comparison_test) 
14416  331 
apply (rule_tac x = N in exI, safe) 
332 
apply (drule le_Suc_ex_iff [THEN iffD1]) 

333 
apply (auto simp add: power_add realpow_not_zero) 

15539  334 
apply (induct_tac "na", auto) 
14416  335 
apply (rule_tac y = "c*abs (f (N + n))" in order_trans) 
336 
apply (auto intro: mult_right_mono simp add: summable_def) 

337 
apply (simp add: mult_ac) 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

338 
apply (rule_tac x = "abs (f N) * (1/ (1  c)) / (c ^ N)" in exI) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

339 
apply (rule sums_divide) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

340 
apply (rule sums_mult) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

341 
apply (auto intro!: geometric_sums) 
14416  342 
done 
343 

344 

15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

345 
text{*Differentiation of finite sum*} 
14416  346 

347 
lemma DERIV_sumr [rule_format (no_asm)]: 

348 
"(\<forall>r. m \<le> r & r < (m + n) > DERIV (%x. f r x) x :> (f' r x)) 

15539  349 
> DERIV (%x. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)" 
15251  350 
apply (induct "n") 
14416  351 
apply (auto intro: DERIV_add) 
352 
done 

353 

354 
ML 

355 
{* 

356 
val sums_def = thm"sums_def"; 

357 
val summable_def = thm"summable_def"; 

358 
val suminf_def = thm"suminf_def"; 

359 

360 
val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero"; 

361 
val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero"; 

362 
val sumr_group = thm "sumr_group"; 

363 
val sums_summable = thm "sums_summable"; 

364 
val summable_sums = thm "summable_sums"; 

365 
val summable_sumr_LIMSEQ_suminf = thm "summable_sumr_LIMSEQ_suminf"; 

366 
val sums_unique = thm "sums_unique"; 

367 
val series_zero = thm "series_zero"; 

368 
val sums_mult = thm "sums_mult"; 

369 
val sums_divide = thm "sums_divide"; 

370 
val sums_diff = thm "sums_diff"; 

371 
val suminf_mult = thm "suminf_mult"; 

372 
val suminf_mult2 = thm "suminf_mult2"; 

373 
val suminf_diff = thm "suminf_diff"; 

374 
val sums_minus = thm "sums_minus"; 

375 
val sums_group = thm "sums_group"; 

376 
val sumr_pos_lt_pair_lemma = thm "sumr_pos_lt_pair_lemma"; 

377 
val sumr_pos_lt_pair = thm "sumr_pos_lt_pair"; 

378 
val series_pos_le = thm "series_pos_le"; 

379 
val series_pos_less = thm "series_pos_less"; 

380 
val sumr_geometric = thm "sumr_geometric"; 

381 
val geometric_sums = thm "geometric_sums"; 

382 
val summable_convergent_sumr_iff = thm "summable_convergent_sumr_iff"; 

383 
val summable_Cauchy = thm "summable_Cauchy"; 

384 
val summable_comparison_test = thm "summable_comparison_test"; 

385 
val summable_rabs_comparison_test = thm "summable_rabs_comparison_test"; 

386 
val summable_le = thm "summable_le"; 

387 
val summable_le2 = thm "summable_le2"; 

388 
val summable_rabs_cancel = thm "summable_rabs_cancel"; 

389 
val summable_rabs = thm "summable_rabs"; 

390 
val rabs_ratiotest_lemma = thm "rabs_ratiotest_lemma"; 

391 
val le_Suc_ex = thm "le_Suc_ex"; 

392 
val le_Suc_ex_iff = thm "le_Suc_ex_iff"; 

393 
val ratio_test_lemma2 = thm "ratio_test_lemma2"; 

394 
val ratio_test = thm "ratio_test"; 

395 
val DERIV_sumr = thm "DERIV_sumr"; 

396 
*} 

397 

398 
end 