author  nipkow 
Mon, 21 Feb 2005 15:04:10 +0100  
changeset 15539  333a88244569 
parent 15537  5538d3244b4d 
child 15542  ee6cd48cf840 
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 

15536  33 
(* 
14416  34 
lemma sumr_add: "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)" 
15047  35 
by (simp add: setsum_addf) 
14416  36 

15047  37 
lemma sumr_mult: "r * sumr m n (f::nat=>real) = sumr m n (%n. r * f n)" 
38 
by (simp add: setsum_mult) 

14416  39 

40 
lemma sumr_split_add [rule_format]: 

15047  41 
"n < p > sumr 0 n f + sumr n p f = sumr 0 p (f::nat=>real)" 
15251  42 
apply (induct "p", auto) 
14416  43 
apply (rename_tac k) 
44 
apply (subgoal_tac "n=k", auto) 

45 
done 

15536  46 

47 
lemma sumr_split_add: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> 

48 
setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}" 

49 
by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un) 

14416  50 

15047  51 
lemma sumr_split_add_minus: 
15537  52 
fixes f :: "nat \<Rightarrow> 'a::ab_group_add" 
53 
shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> 

54 
setsum f {m..<p}  setsum f {m..<n} = setsum f {n..<p}" 

55 
using sumr_split_add [of m n p f,symmetric] 

14416  56 
apply (simp add: add_ac) 
57 
done 

15539  58 
*) 
14416  59 

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

15536  62 
by (simp add: diff_minus setsum_addf real_of_nat_def) 
63 

64 
(* 

15047  65 
lemma sumr_rabs: "abs(sumr m n (f::nat=>real)) \<le> sumr m n (%i. abs(f i))" 
66 
by (simp add: setsum_abs) 

14416  67 

15047  68 
lemma sumr_rabs_ge_zero [iff]: "0 \<le> sumr m n (%n. abs (f n))" 
69 
by (simp add: setsum_abs_ge_zero) 

14416  70 

15047  71 
text{*Just a congruence rule*} 
72 
lemma sumr_fun_eq: 

73 
"(\<forall>r. m \<le> r & r < n > f r = g r) ==> sumr m n f = sumr m n g" 

74 
by (auto intro: setsum_cong) 

14416  75 

15047  76 
lemma sumr_less_bounds_zero [simp]: "n < m ==> sumr m n f = 0" 
77 
by (simp add: atLeastLessThan_empty) 

14416  78 

79 
lemma sumr_minus: "sumr m n (%i.  f i) =  sumr m n f" 

15047  80 
by (simp add: Finite_Set.setsum_negf) 
15539  81 

82 
lemma sumr_shift_bounds: 

83 
"setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}" 

84 
by (induct "n", auto) 

15536  85 
*) 
14416  86 

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

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

15251  90 
by (induct "n", auto) 
14416  91 

15539  92 
(* 
93 
lemma sumr_interval_const2: 

94 
"[\<forall>n\<ge>m. f n = r; m \<le> k] 

95 
==> sumr m k f = (real (k  m) * r)" 

96 
apply (induct "k", auto) 

15251  97 
apply (drule_tac x = k in spec) 
14416  98 
apply (auto dest!: le_imp_less_or_eq) 
15047  99 
apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split) 
14416  100 
done 
15539  101 
*) 
102 
(* FIXME split in tow steps 

103 
lemma setsum_nat_set_real_const: 

104 
"(\<And>n. n\<in>A \<Longrightarrow> f n = r) \<Longrightarrow> setsum f A = real(card A) * r" (is "PROP ?P") 

105 
proof (cases "finite A") 

106 
case True 

107 
thus "PROP ?P" 

108 
proof induct 

109 
case empty thus ?case by simp 

110 
next 

111 
case insert thus ?case by(simp add: left_distrib real_of_nat_Suc) 

112 
qed 

113 
next 

114 
case False thus "PROP ?P" by (simp add: setsum_def) 

115 
qed 

116 
*) 

14416  117 

15539  118 
(* 
119 
lemma sumr_le: 

120 
"[\<forall>n\<ge>m. 0 \<le> (f n::real); m < k] ==> setsum f {0..<m} \<le> setsum f {0..<k::nat}" 

121 
apply (induct "k") 

122 
apply (auto simp add: less_Suc_eq_le) 

123 
apply (drule_tac x = k in spec, safe) 

124 
apply (drule le_imp_less_or_eq, safe) 

125 
apply (arith) 

126 
apply (drule_tac a = "sumr 0 m f" in order_refl [THEN add_mono], auto) 

14416  127 
done 
128 

15251  129 
lemma sumr_le: 
15360  130 
"[\<forall>n\<ge>m. 0 \<le> f n; m < k] ==> sumr 0 m f \<le> sumr 0 k f" 
15251  131 
apply (induct "k") 
14416  132 
apply (auto simp add: less_Suc_eq_le) 
15251  133 
apply (drule_tac x = k in spec, safe) 
14416  134 
apply (drule le_imp_less_or_eq, safe) 
15047  135 
apply (arith) 
14416  136 
apply (drule_tac a = "sumr 0 m f" in order_refl [THEN add_mono], auto) 
137 
done 

138 

139 
lemma sumr_le2 [rule_format (no_asm)]: 

140 
"(\<forall>r. m \<le> r & r < n > f r \<le> g r) > sumr m n f \<le> sumr m n g" 

15251  141 
apply (induct "n") 
14416  142 
apply (auto intro: add_mono simp add: le_def) 
143 
done 

15539  144 
*) 
14416  145 

15539  146 
(* 
15360  147 
lemma sumr_ge_zero: "(\<forall>n\<ge>m. 0 \<le> f n) > 0 \<le> sumr m n f" 
15251  148 
apply (induct "n", auto) 
14416  149 
apply (drule_tac x = n in spec, arith) 
150 
done 

15539  151 
*) 
14416  152 

15539  153 
(* 
14416  154 
lemma rabs_sumr_rabs_cancel [simp]: 
15229  155 
"abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))" 
15251  156 
by (induct "n", simp_all add: add_increasing) 
14416  157 

158 
lemma sumr_zero [rule_format]: 

15360  159 
"\<forall>n \<ge> N. f n = 0 ==> N \<le> m > sumr m n f = 0" 
15251  160 
by (induct "n", auto) 
15539  161 
*) 
14416  162 

163 
lemma Suc_le_imp_diff_ge2: 

15539  164 
"[\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m] ==> setsum f {m..<n} = 0" 
165 
apply (rule setsum_0') 

14416  166 
apply (case_tac "n", auto) 
15539  167 
apply(erule_tac x = "a  1" in allE) 
168 
apply (simp split:nat_diff_split) 

14416  169 
done 
170 

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

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

15251  174 
apply (induct "n") 
14416  175 
apply (case_tac [2] "n", auto) 
176 
done 

15536  177 
(* 
14416  178 
lemma sumr_diff: "sumr m n f  sumr m n g = sumr m n (%n. f n  g n)" 
15536  179 
by (simp add: diff_minus setsum_addf setsum_negf) 
180 
*) 

15539  181 
(* 
14416  182 
lemma sumr_subst [rule_format (no_asm)]: 
183 
"(\<forall>p. m \<le> p & p < m+n > (f p = g p)) > sumr m n f = sumr m n g" 

15251  184 
by (induct "n", auto) 
15539  185 
*) 
14416  186 

15539  187 
lemma setsum_bounded: 
188 
assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{comm_semiring_1_cancel, pordered_ab_semigroup_add})" 

189 
shows "setsum f A \<le> of_nat(card A) * K" 

190 
proof (cases "finite A") 

191 
case True 

192 
thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp 

193 
next 

194 
case False thus ?thesis by (simp add: setsum_def) 

195 
qed 

196 
(* 

14416  197 
lemma sumr_bound [rule_format (no_asm)]: 
198 
"(\<forall>p. m \<le> p & p < m + n > (f(p) \<le> K)) 

15539  199 
> setsum f {m..<m+n::nat} \<le> (real n * K)" 
15251  200 
apply (induct "n") 
14416  201 
apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc) 
202 
done 

15539  203 
*) 
204 
(* FIXME should be generalized 

14416  205 
lemma sumr_bound2 [rule_format (no_asm)]: 
206 
"(\<forall>p. 0 \<le> p & p < n > (f(p) \<le> K)) 

15539  207 
> setsum f {0..<n::nat} \<le> (real n * K)" 
15251  208 
apply (induct "n") 
15047  209 
apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc add_commute) 
14416  210 
done 
15539  211 
*) 
212 
(* FIXME a bit specialized for [simp]! *) 

14416  213 
lemma sumr_group [simp]: 
15539  214 
"(\<Sum>m=0..<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {0 ..< n * k}" 
215 
apply (subgoal_tac "k = 0  0 < k", auto simp:setsum_0') 

15251  216 
apply (induct "n") 
15539  217 
apply (simp_all add: setsum_add_nat_ivl add_commute) 
14416  218 
done 
15539  219 
(* FIXME setsum_0[simp] *) 
220 

14416  221 

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

223 

224 
(* 

225 
suminf is the sum 

226 
*) 

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

228 
by (simp add: sums_def summable_def, blast) 

229 

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

231 
apply (simp add: summable_def suminf_def) 

232 
apply (blast intro: someI2) 

233 
done 

234 

235 
lemma summable_sumr_LIMSEQ_suminf: 

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

239 
done 

240 

241 
(* 

242 
sum is unique 

243 
*) 

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

245 
apply (frule sums_summable [THEN summable_sums]) 

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

247 
done 

248 

249 
(* 

250 
Goalw [sums_def,LIMSEQ_def] 

251 
"(\<forall>m. n \<le> Suc m > f(m) = 0) ==> f sums (sumr 0 n f)" 

252 
by safe 

253 
by (res_inst_tac [("x","n")] exI 1); 

254 
by (safe THEN ftac le_imp_less_or_eq 1) 

255 
by safe 

256 
by (dres_inst_tac [("f","f")] sumr_split_add_minus 1); 

257 
by (ALLGOALS (Asm_simp_tac)); 

258 
by (dtac (conjI RS sumr_interval_const) 1); 

259 
by Auto_tac 

260 
qed "series_zero"; 

261 
next one was called series_zero2 

262 
**********************) 

263 

15539  264 
lemma ivl_subset[simp]: 
265 
"({i..<j} \<subseteq> {m..<n}) = (j \<le> i  m \<le> i & j \<le> (n::'a::linorder))" 

266 
apply(auto simp:linorder_not_le) 

267 
apply(rule ccontr) 

268 
apply(frule subsetCE[where c = n]) 

269 
apply(auto simp:linorder_not_le) 

270 
done 

271 

272 
lemma ivl_diff[simp]: 

273 
"i \<le> n \<Longrightarrow> {i..<m}  {i..<n} = {n..<(m::'a::linorder)}" 

274 
by(auto) 

275 

276 

277 
(* FIXME the last step should work w/o Ball_def, ideally just with 

278 
setsum_0 and setsum_cong. Currently the simplifier does not simplify 

279 
the premise x:{i..<j} that ball_cong (or a modified version of setsum_0') 

280 
generates. FIX simplifier??? *) 

14416  281 
lemma series_zero: 
15539  282 
"(\<forall>m. n \<le> m > f(m) = 0) ==> f sums (setsum f {0..<n})" 
15537  283 
apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe) 
14416  284 
apply (rule_tac x = n in exI) 
15539  285 
apply (clarsimp simp add:setsum_diff[symmetric] setsum_0' Ball_def) 
14416  286 
done 
287 

15539  288 

14416  289 
lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)" 
15536  290 
by (auto simp add: sums_def setsum_mult [symmetric] 
14416  291 
intro!: LIMSEQ_mult intro: LIMSEQ_const) 
292 

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

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

295 

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

15536  297 
by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff) 
14416  298 

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

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

301 

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

303 
by (auto intro!: sums_unique sums_mult summable_sums) 

304 

305 
lemma suminf_diff: 

306 
"[ summable f; summable g ] 

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

308 
by (auto intro!: sums_diff sums_unique summable_sums) 

309 

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

15536  311 
by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf) 
14416  312 

313 
lemma sums_group: 

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

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

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

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

320 
apply (auto dest!: not_leE) 

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

322 
done 

323 

324 
lemma sumr_pos_lt_pair_lemma: 

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

15251  327 
apply (induct "no", auto) 
328 
apply (drule_tac x = "Suc no" in spec) 

15539  329 
apply (simp add: add_ac) 
14416  330 
done 
10751  331 

332 

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

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

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

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

339 
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

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

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

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

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

346 
apply (safe, simp) 

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

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

14416  350 
prefer 3 apply assumption 
15539  351 
apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans) 
14416  352 
apply simp_all 
15539  353 
apply (subgoal_tac "suminf f \<le> setsum f {0..< Suc (Suc 0) * (Suc no) + n}") 
14416  354 
apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans) 
15539  355 
prefer 3 apply simp 
14416  356 
apply (drule_tac [2] x = 0 in spec) 
357 
prefer 2 apply simp 

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

14416  360 
apply (auto simp add: linorder_not_less [symmetric]) 
361 
done 

362 

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

363 
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

364 
great as any partial sum.*} 
14416  365 

366 
lemma series_pos_le: 

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

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

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

373 
apply (rule setsum_mono2) 

374 
apply auto 

14416  375 
done 
376 

377 
lemma series_pos_less: 

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

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

382 
done 

383 

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

384 
text{*Sum of a geometric progression.*} 
14416  385 

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

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

391 
apply (simp add: right_distrib diff_minus mult_commute) 
14416  392 
done 
393 

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

395 
apply (case_tac "x = 1") 

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

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

397 
simp add: sumr_geometric sums_def diff_minus add_divide_distrib) 
14416  398 
apply (subgoal_tac "1 / (1 + x) = 0/ (x  1) +  1/ (x  1) ") 
399 
apply (erule ssubst) 

400 
apply (rule LIMSEQ_add, rule LIMSEQ_divide) 

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

401 
apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2) 
14416  402 
done 
403 

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

404 
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

405 

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

14416  408 
by (simp add: summable_def sums_def convergent_def) 
409 

410 
lemma summable_Cauchy: 

411 
"summable f = 

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

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

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

15360  419 
apply (drule_tac x = n in spec, simp) 
14416  420 
apply (drule_tac x = m in spec) 
15539  421 
apply(simp add: setsum_diff[symmetric]) 
15537  422 
apply(subst abs_minus_commute) 
15539  423 
apply(simp add: setsum_diff[symmetric]) 
424 
apply(simp add: setsum_diff[symmetric]) 

14416  425 
done 
15539  426 
(* FIXME move ivl_ lemmas out of this theory *) 
14416  427 

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

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

429 

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

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

435 
apply (rotate_tac 2) 

436 
apply (drule_tac x = m in spec) 

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

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

14416  442 
done 
443 

444 
lemma summable_rabs_comparison_test: 

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

448 
apply (auto simp add: abs_idempotent) 

449 
done 

450 

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

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

452 

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

455 
apply (drule summable_sums)+ 

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

457 
apply (rule exI) 

15539  458 
apply (auto intro!: setsum_mono) 
14416  459 
done 
460 

461 
lemma summable_le2: 

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

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

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

465 
apply (simp add: abs_le_interval_iff) 

466 
done 

467 

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

468 
text{*Absolute convergence imples normal convergence*} 
14416  469 
lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f" 
15536  470 
apply (auto simp add: summable_Cauchy) 
14416  471 
apply (drule spec, auto) 
472 
apply (rule_tac x = N in exI, auto) 

473 
apply (drule spec, auto) 

15539  474 
apply (rule_tac y = "\<Sum>n=m..<n. abs(f n)" in order_le_less_trans) 
15536  475 
apply (auto) 
14416  476 
done 
477 

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

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

15536  481 
by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf) 
14416  482 

483 

484 
subsection{* The Ratio Test*} 

485 

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

487 
apply (drule order_le_imp_less_or_eq, auto) 

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

489 
apply (simp add: zero_le_mult_iff, arith) 

490 
done 

491 

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

493 
apply (drule le_imp_less_or_eq) 

494 
apply (auto dest: less_imp_Suc_add) 

495 
done 

496 

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

498 
by (auto simp add: le_Suc_ex) 

499 

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

501 
lemma ratio_test_lemma2: 

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

505 
apply (simp add: summable_Cauchy) 

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

507 
prefer 2 apply (blast intro: rabs_ratiotest_lemma) 

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

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

510 
done 

511 

512 
lemma ratio_test: 

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

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

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

517 
in summable_comparison_test) 
14416  518 
apply (rule_tac x = N in exI, safe) 
519 
apply (drule le_Suc_ex_iff [THEN iffD1]) 

520 
apply (auto simp add: power_add realpow_not_zero) 

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

524 
apply (simp add: mult_ac) 

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

525 
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

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

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

528 
apply (auto intro!: geometric_sums) 
14416  529 
done 
530 

531 

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

532 
text{*Differentiation of finite sum*} 
14416  533 

534 
lemma DERIV_sumr [rule_format (no_asm)]: 

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

15539  536 
> DERIV (%x. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)" 
15251  537 
apply (induct "n") 
14416  538 
apply (auto intro: DERIV_add) 
539 
done 

540 

541 
ML 

542 
{* 

543 
val sums_def = thm"sums_def"; 

544 
val summable_def = thm"summable_def"; 

545 
val suminf_def = thm"suminf_def"; 

546 

547 
val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero"; 

548 
val Suc_le_imp_diff_ge2 = thm "Suc_le_imp_diff_ge2"; 

549 
val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero"; 

550 
val sumr_group = thm "sumr_group"; 

551 
val sums_summable = thm "sums_summable"; 

552 
val summable_sums = thm "summable_sums"; 

553 
val summable_sumr_LIMSEQ_suminf = thm "summable_sumr_LIMSEQ_suminf"; 

554 
val sums_unique = thm "sums_unique"; 

555 
val series_zero = thm "series_zero"; 

556 
val sums_mult = thm "sums_mult"; 

557 
val sums_divide = thm "sums_divide"; 

558 
val sums_diff = thm "sums_diff"; 

559 
val suminf_mult = thm "suminf_mult"; 

560 
val suminf_mult2 = thm "suminf_mult2"; 

561 
val suminf_diff = thm "suminf_diff"; 

562 
val sums_minus = thm "sums_minus"; 

563 
val sums_group = thm "sums_group"; 

564 
val sumr_pos_lt_pair_lemma = thm "sumr_pos_lt_pair_lemma"; 

565 
val sumr_pos_lt_pair = thm "sumr_pos_lt_pair"; 

566 
val series_pos_le = thm "series_pos_le"; 

567 
val series_pos_less = thm "series_pos_less"; 

568 
val sumr_geometric = thm "sumr_geometric"; 

569 
val geometric_sums = thm "geometric_sums"; 

570 
val summable_convergent_sumr_iff = thm "summable_convergent_sumr_iff"; 

571 
val summable_Cauchy = thm "summable_Cauchy"; 

572 
val summable_comparison_test = thm "summable_comparison_test"; 

573 
val summable_rabs_comparison_test = thm "summable_rabs_comparison_test"; 

574 
val summable_le = thm "summable_le"; 

575 
val summable_le2 = thm "summable_le2"; 

576 
val summable_rabs_cancel = thm "summable_rabs_cancel"; 

577 
val summable_rabs = thm "summable_rabs"; 

578 
val rabs_ratiotest_lemma = thm "rabs_ratiotest_lemma"; 

579 
val le_Suc_ex = thm "le_Suc_ex"; 

580 
val le_Suc_ex_iff = thm "le_Suc_ex_iff"; 

581 
val ratio_test_lemma2 = thm "ratio_test_lemma2"; 

582 
val ratio_test = thm "ratio_test"; 

583 
val DERIV_sumr = thm "DERIV_sumr"; 

584 
*} 

585 

586 
end 