author  nipkow 
Mon, 21 Feb 2005 19:23:46 +0100  
changeset 15542  ee6cd48cf840 
parent 15539  333a88244569 
child 15543  0024472afce7 
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 
10751  14 

15539  15 
(* FIXME why not globally? *) 
15536  16 
declare atLeastLessThan_empty[simp]; 
15539  17 
declare atLeastLessThan_iff[iff] 
10751  18 

19 
constdefs 

14416  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]: 

45 
"setsum (%i. (1) ^ Suc i) {0..<2*n} = (0::real)" 

15251  46 
by (induct "n", auto) 
14416  47 

15542  48 
(* FIXME get rid of this one! *) 
14416  49 
lemma Suc_le_imp_diff_ge2: 
15539  50 
"[\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m] ==> setsum f {m..<n} = 0" 
51 
apply (rule setsum_0') 

14416  52 
apply (case_tac "n", auto) 
15539  53 
apply(erule_tac x = "a  1" in allE) 
54 
apply (simp split:nat_diff_split) 

14416  55 
done 
56 

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

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

15251  60 
apply (induct "n") 
14416  61 
apply (case_tac [2] "n", auto) 
62 
done 

63 

15539  64 
(* FIXME a bit specialized for [simp]! *) 
14416  65 
lemma sumr_group [simp]: 
15539  66 
"(\<Sum>m=0..<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {0 ..< n * k}" 
67 
apply (subgoal_tac "k = 0  0 < k", auto simp:setsum_0') 

15251  68 
apply (induct "n") 
15539  69 
apply (simp_all add: setsum_add_nat_ivl add_commute) 
14416  70 
done 
15539  71 

14416  72 

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

74 

75 
(* 

76 
suminf is the sum 

77 
*) 

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

79 
by (simp add: sums_def summable_def, blast) 

80 

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

82 
apply (simp add: summable_def suminf_def) 

83 
apply (blast intro: someI2) 

84 
done 

85 

86 
lemma summable_sumr_LIMSEQ_suminf: 

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

90 
done 

91 

92 
(* 

93 
sum is unique 

94 
*) 

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

96 
apply (frule sums_summable [THEN summable_sums]) 

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

98 
done 

99 

100 
lemma series_zero: 

15539  101 
"(\<forall>m. n \<le> m > f(m) = 0) ==> f sums (setsum f {0..<n})" 
15537  102 
apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe) 
14416  103 
apply (rule_tac x = n in exI) 
15542  104 
apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong) 
14416  105 
done 
106 

15539  107 

14416  108 
lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)" 
15536  109 
by (auto simp add: sums_def setsum_mult [symmetric] 
14416  110 
intro!: LIMSEQ_mult intro: LIMSEQ_const) 
111 

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

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

114 

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

15536  116 
by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff) 
14416  117 

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

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

120 

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

122 
by (auto intro!: sums_unique sums_mult summable_sums) 

123 

124 
lemma suminf_diff: 

125 
"[ summable f; summable g ] 

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

127 
by (auto intro!: sums_diff sums_unique summable_sums) 

128 

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

15536  130 
by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf) 
14416  131 

132 
lemma sums_group: 

15539  133 
"[summable f; 0 < k ] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)" 
14416  134 
apply (drule summable_sums) 
135 
apply (auto simp add: sums_def LIMSEQ_def) 

136 
apply (drule_tac x = r in spec, safe) 

137 
apply (rule_tac x = no in exI, safe) 

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

139 
apply (auto dest!: not_leE) 

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

141 
done 

142 

143 
lemma sumr_pos_lt_pair_lemma: 

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

15251  146 
apply (induct "no", auto) 
147 
apply (drule_tac x = "Suc no" in spec) 

15539  148 
apply (simp add: add_ac) 
14416  149 
done 
10751  150 

151 

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

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

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

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

158 
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

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

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

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

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

165 
apply (safe, simp) 

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

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

14416  169 
prefer 3 apply assumption 
15539  170 
apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans) 
14416  171 
apply simp_all 
15539  172 
apply (subgoal_tac "suminf f \<le> setsum f {0..< Suc (Suc 0) * (Suc no) + n}") 
14416  173 
apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans) 
15539  174 
prefer 3 apply simp 
14416  175 
apply (drule_tac [2] x = 0 in spec) 
176 
prefer 2 apply simp 

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

14416  179 
apply (auto simp add: linorder_not_less [symmetric]) 
180 
done 

181 

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

182 
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

183 
great as any partial sum.*} 
14416  184 

185 
lemma series_pos_le: 

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

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

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

192 
apply (rule setsum_mono2) 

193 
apply auto 

14416  194 
done 
195 

196 
lemma series_pos_less: 

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

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

201 
done 

202 

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

203 
text{*Sum of a geometric progression.*} 
14416  204 

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

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

210 
apply (simp add: right_distrib diff_minus mult_commute) 
14416  211 
done 
212 

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

214 
apply (case_tac "x = 1") 

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

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

216 
simp add: sumr_geometric sums_def diff_minus add_divide_distrib) 
14416  217 
apply (subgoal_tac "1 / (1 + x) = 0/ (x  1) +  1/ (x  1) ") 
218 
apply (erule ssubst) 

219 
apply (rule LIMSEQ_add, rule LIMSEQ_divide) 

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

220 
apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2) 
14416  221 
done 
222 

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

223 
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

224 

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

14416  227 
by (simp add: summable_def sums_def convergent_def) 
228 

229 
lemma summable_Cauchy: 

230 
"summable f = 

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

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

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

15360  238 
apply (drule_tac x = n in spec, simp) 
14416  239 
apply (drule_tac x = m in spec) 
15539  240 
apply(simp add: setsum_diff[symmetric]) 
15537  241 
apply(subst abs_minus_commute) 
15539  242 
apply(simp add: setsum_diff[symmetric]) 
243 
apply(simp add: setsum_diff[symmetric]) 

14416  244 
done 
245 

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

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

247 

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

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

253 
apply (rotate_tac 2) 

254 
apply (drule_tac x = m in spec) 

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

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

14416  260 
done 
261 

262 
lemma summable_rabs_comparison_test: 

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

266 
apply (auto simp add: abs_idempotent) 

267 
done 

268 

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

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

270 

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

273 
apply (drule summable_sums)+ 

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

275 
apply (rule exI) 

15539  276 
apply (auto intro!: setsum_mono) 
14416  277 
done 
278 

279 
lemma summable_le2: 

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

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

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

283 
apply (simp add: abs_le_interval_iff) 

284 
done 

285 

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

286 
text{*Absolute convergence imples normal convergence*} 
14416  287 
lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f" 
15536  288 
apply (auto simp add: summable_Cauchy) 
14416  289 
apply (drule spec, auto) 
290 
apply (rule_tac x = N in exI, auto) 

291 
apply (drule spec, auto) 

15539  292 
apply (rule_tac y = "\<Sum>n=m..<n. abs(f n)" in order_le_less_trans) 
15536  293 
apply (auto) 
14416  294 
done 
295 

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

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

15536  299 
by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf) 
14416  300 

301 

302 
subsection{* The Ratio Test*} 

303 

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

305 
apply (drule order_le_imp_less_or_eq, auto) 

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

307 
apply (simp add: zero_le_mult_iff, arith) 

308 
done 

309 

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

311 
apply (drule le_imp_less_or_eq) 

312 
apply (auto dest: less_imp_Suc_add) 

313 
done 

314 

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

316 
by (auto simp add: le_Suc_ex) 

317 

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

319 
lemma ratio_test_lemma2: 

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

323 
apply (simp add: summable_Cauchy) 

324 
apply (safe, subgoal_tac "\<forall>n. N \<le> n > f (Suc n) = 0") 

325 
prefer 2 apply (blast intro: rabs_ratiotest_lemma) 

326 
apply (rule_tac x = "Suc N" in exI, clarify) 

327 
apply (drule_tac n=n in Suc_le_imp_diff_ge2, auto) 

328 
done 

329 

330 
lemma ratio_test: 

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

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

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

335 
in summable_comparison_test) 
14416  336 
apply (rule_tac x = N in exI, safe) 
337 
apply (drule le_Suc_ex_iff [THEN iffD1]) 

338 
apply (auto simp add: power_add realpow_not_zero) 

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

342 
apply (simp add: mult_ac) 

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

343 
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

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

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

346 
apply (auto intro!: geometric_sums) 
14416  347 
done 
348 

349 

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

350 
text{*Differentiation of finite sum*} 
14416  351 

352 
lemma DERIV_sumr [rule_format (no_asm)]: 

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

15539  354 
> DERIV (%x. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)" 
15251  355 
apply (induct "n") 
14416  356 
apply (auto intro: DERIV_add) 
357 
done 

358 

359 
ML 

360 
{* 

361 
val sums_def = thm"sums_def"; 

362 
val summable_def = thm"summable_def"; 

363 
val suminf_def = thm"suminf_def"; 

364 

365 
val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero"; 

366 
val Suc_le_imp_diff_ge2 = thm "Suc_le_imp_diff_ge2"; 

367 
val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero"; 

368 
val sumr_group = thm "sumr_group"; 

369 
val sums_summable = thm "sums_summable"; 

370 
val summable_sums = thm "summable_sums"; 

371 
val summable_sumr_LIMSEQ_suminf = thm "summable_sumr_LIMSEQ_suminf"; 

372 
val sums_unique = thm "sums_unique"; 

373 
val series_zero = thm "series_zero"; 

374 
val sums_mult = thm "sums_mult"; 

375 
val sums_divide = thm "sums_divide"; 

376 
val sums_diff = thm "sums_diff"; 

377 
val suminf_mult = thm "suminf_mult"; 

378 
val suminf_mult2 = thm "suminf_mult2"; 

379 
val suminf_diff = thm "suminf_diff"; 

380 
val sums_minus = thm "sums_minus"; 

381 
val sums_group = thm "sums_group"; 

382 
val sumr_pos_lt_pair_lemma = thm "sumr_pos_lt_pair_lemma"; 

383 
val sumr_pos_lt_pair = thm "sumr_pos_lt_pair"; 

384 
val series_pos_le = thm "series_pos_le"; 

385 
val series_pos_less = thm "series_pos_less"; 

386 
val sumr_geometric = thm "sumr_geometric"; 

387 
val geometric_sums = thm "geometric_sums"; 

388 
val summable_convergent_sumr_iff = thm "summable_convergent_sumr_iff"; 

389 
val summable_Cauchy = thm "summable_Cauchy"; 

390 
val summable_comparison_test = thm "summable_comparison_test"; 

391 
val summable_rabs_comparison_test = thm "summable_rabs_comparison_test"; 

392 
val summable_le = thm "summable_le"; 

393 
val summable_le2 = thm "summable_le2"; 

394 
val summable_rabs_cancel = thm "summable_rabs_cancel"; 

395 
val summable_rabs = thm "summable_rabs"; 

396 
val rabs_ratiotest_lemma = thm "rabs_ratiotest_lemma"; 

397 
val le_Suc_ex = thm "le_Suc_ex"; 

398 
val le_Suc_ex_iff = thm "le_Suc_ex_iff"; 

399 
val ratio_test_lemma2 = thm "ratio_test_lemma2"; 

400 
val ratio_test = thm "ratio_test"; 

401 
val DERIV_sumr = thm "DERIV_sumr"; 

402 
*} 

403 

404 
end 