author  nipkow 
Tue, 22 Feb 2005 10:54:30 +0100  
changeset 15543  0024472afce7 
parent 15542  ee6cd48cf840 
child 15546  5188ce7316b7 
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 
15543  14 
thm atLeastLessThan_empty 
15539  15 
(* FIXME why not globally? *) 
15536  16 
declare atLeastLessThan_empty[simp]; 
15539  17 
declare atLeastLessThan_iff[iff] 
10751  18 

19 
constdefs 

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

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

25 

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

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

15539  29 
lemma setsum_Suc[simp]: 
15536  30 
"setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))" 
31 
by (simp add: atLeastLessThanSuc add_commute) 

14416  32 

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

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

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

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

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

41 
by (auto simp:real_of_nat_def) 

14416  42 

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

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

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

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

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

54 

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

14416  62 

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

64 

65 
(* 

66 
suminf is the sum 

67 
*) 

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

69 
by (simp add: sums_def summable_def, blast) 

70 

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

72 
apply (simp add: summable_def suminf_def) 

73 
apply (blast intro: someI2) 

74 
done 

75 

76 
lemma summable_sumr_LIMSEQ_suminf: 

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

80 
done 

81 

82 
(* 

83 
sum is unique 

84 
*) 

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

86 
apply (frule sums_summable [THEN summable_sums]) 

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

88 
done 

89 

90 
lemma series_zero: 

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

15539  97 

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

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

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

104 

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

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

108 
lemma suminf_mult: "summable f ==> suminf f * c = suminf(%n. f n * c)" 

109 
by (auto intro!: sums_unique sums_mult summable_sums simp add: mult_commute) 

110 

111 
lemma suminf_mult2: "summable f ==> c * suminf f = suminf(%n. c * f n)" 

112 
by (auto intro!: sums_unique sums_mult summable_sums) 

113 

114 
lemma suminf_diff: 

115 
"[ summable f; summable g ] 

116 
==> suminf f  suminf g = suminf(%n. f n  g n)" 

117 
by (auto intro!: sums_diff sums_unique summable_sums) 

118 

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

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

122 
lemma sums_group: 

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

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

129 
apply (auto dest!: not_leE) 

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

131 
done 

132 

133 
lemma sumr_pos_lt_pair_lemma: 

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

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

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

141 

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

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

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

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

148 
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

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

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

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

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

155 
apply (safe, simp) 

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

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

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

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

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

171 

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

172 
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

173 
great as any partial sum.*} 
14416  174 

175 
lemma series_pos_le: 

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

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

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

182 
apply (rule setsum_mono2) 

183 
apply auto 

14416  184 
done 
185 

186 
lemma series_pos_less: 

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

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

191 
done 

192 

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

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

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

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

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

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

204 
apply (case_tac "x = 1") 

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

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

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

209 
apply (rule LIMSEQ_add, rule LIMSEQ_divide) 

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

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

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

213 
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

214 

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

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

219 
lemma summable_Cauchy: 

220 
"summable f = 

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

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

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

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

14416  234 
done 
235 

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

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

237 

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

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

243 
apply (rotate_tac 2) 

244 
apply (drule_tac x = m in spec) 

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

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

14416  250 
done 
251 

252 
lemma summable_rabs_comparison_test: 

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

15543  256 
apply (auto) 
14416  257 
done 
258 

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

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

260 

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

263 
apply (drule summable_sums)+ 

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

265 
apply (rule exI) 

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

269 
lemma summable_le2: 

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

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

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

273 
apply (simp add: abs_le_interval_iff) 

274 
done 

275 

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

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

281 
apply (drule spec, auto) 

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

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

286 
text{*Absolute convergence of series*} 
14416  287 
lemma summable_rabs: 
288 
"summable (%n. abs (f n)) ==> abs(suminf f) \<le> suminf (%n. abs(f n))" 

15536  289 
by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf) 
14416  290 

291 

292 
subsection{* The Ratio Test*} 

293 

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

295 
apply (drule order_le_imp_less_or_eq, auto) 

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

297 
apply (simp add: zero_le_mult_iff, arith) 

298 
done 

299 

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

301 
apply (drule le_imp_less_or_eq) 

302 
apply (auto dest: less_imp_Suc_add) 

303 
done 

304 

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

306 
by (auto simp add: le_Suc_ex) 

307 

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

309 
lemma ratio_test_lemma2: 

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

313 
apply (simp add: summable_Cauchy) 

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

316 
apply clarify 

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

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

319 
apply (blast intro: rabs_ratiotest_lemma) 

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

324 
lemma ratio_test: 

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

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

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

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

332 
apply (auto simp add: power_add realpow_not_zero) 

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

336 
apply (simp add: mult_ac) 

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

337 
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

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

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

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

343 

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

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

346 
lemma DERIV_sumr [rule_format (no_asm)]: 

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

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

352 

353 
ML 

354 
{* 

355 
val sums_def = thm"sums_def"; 

356 
val summable_def = thm"summable_def"; 

357 
val suminf_def = thm"suminf_def"; 

358 

359 
val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero"; 

360 
val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero"; 

361 
val sumr_group = thm "sumr_group"; 

362 
val sums_summable = thm "sums_summable"; 

363 
val summable_sums = thm "summable_sums"; 

364 
val summable_sumr_LIMSEQ_suminf = thm "summable_sumr_LIMSEQ_suminf"; 

365 
val sums_unique = thm "sums_unique"; 

366 
val series_zero = thm "series_zero"; 

367 
val sums_mult = thm "sums_mult"; 

368 
val sums_divide = thm "sums_divide"; 

369 
val sums_diff = thm "sums_diff"; 

370 
val suminf_mult = thm "suminf_mult"; 

371 
val suminf_mult2 = thm "suminf_mult2"; 

372 
val suminf_diff = thm "suminf_diff"; 

373 
val sums_minus = thm "sums_minus"; 

374 
val sums_group = thm "sums_group"; 

375 
val sumr_pos_lt_pair_lemma = thm "sumr_pos_lt_pair_lemma"; 

376 
val sumr_pos_lt_pair = thm "sumr_pos_lt_pair"; 

377 
val series_pos_le = thm "series_pos_le"; 

378 
val series_pos_less = thm "series_pos_less"; 

379 
val sumr_geometric = thm "sumr_geometric"; 

380 
val geometric_sums = thm "geometric_sums"; 

381 
val summable_convergent_sumr_iff = thm "summable_convergent_sumr_iff"; 

382 
val summable_Cauchy = thm "summable_Cauchy"; 

383 
val summable_comparison_test = thm "summable_comparison_test"; 

384 
val summable_rabs_comparison_test = thm "summable_rabs_comparison_test"; 

385 
val summable_le = thm "summable_le"; 

386 
val summable_le2 = thm "summable_le2"; 

387 
val summable_rabs_cancel = thm "summable_rabs_cancel"; 

388 
val summable_rabs = thm "summable_rabs"; 

389 
val rabs_ratiotest_lemma = thm "rabs_ratiotest_lemma"; 

390 
val le_Suc_ex = thm "le_Suc_ex"; 

391 
val le_Suc_ex_iff = thm "le_Suc_ex_iff"; 

392 
val ratio_test_lemma2 = thm "ratio_test_lemma2"; 

393 
val ratio_test = thm "ratio_test"; 

394 
val DERIV_sumr = thm "DERIV_sumr"; 

395 
*} 

396 

397 
end 