author  nipkow 
Fri, 18 Feb 2005 15:20:27 +0100  
changeset 15537  5538d3244b4d 
parent 15536  3ce1cb7a24f0 
child 15539  333a88244569 
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 

10751  6 
*) 
7 

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

15131  10 
theory Series 
15140  11 
imports SEQ Lim 
15131  12 
begin 
10751  13 

15536  14 
declare atLeastLessThan_empty[simp]; 
15 

15047  16 
syntax sumr :: "[nat,nat,(nat=>real)] => real" 
17 
translations 

18 
"sumr m n f" => "setsum (f::nat=>real) (atLeastLessThan m n)" 

10751  19 

20 
constdefs 

14416  21 
sums :: "[nat=>real,real] => bool" (infixr "sums" 80) 
15536  22 
"f sums s == (%n. setsum f {0..<n}) > s" 
10751  23 

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

26 

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

28 
"suminf f == (@s. f sums s)" 

29 

30 

15047  31 
lemma sumr_Suc [simp]: 
15536  32 
"setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))" 
33 
by (simp add: atLeastLessThanSuc add_commute) 

14416  34 

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

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

14416  41 

42 
lemma sumr_split_add [rule_format]: 

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

47 
done 

15536  48 
*) 
49 

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

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

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

14416  53 

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

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

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

14416  59 
apply (simp add: add_ac) 
60 
done 

61 

15536  62 
lemma sumr_diff_mult_const: "sumr 0 n f  (real n*r) = sumr 0 n (%i. f i  r)" 
63 
by (simp add: diff_minus setsum_addf real_of_nat_def) 

64 

65 
(* 

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

14416  68 

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

14416  71 

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

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

75 
by (auto intro: setsum_cong) 

14416  76 

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

14416  79 

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

15047  81 
by (simp add: Finite_Set.setsum_negf) 
15536  82 
*) 
14416  83 

84 
lemma sumr_shift_bounds: "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))" 

15251  85 
by (induct "n", auto) 
14416  86 

87 
lemma sumr_minus_one_realpow_zero [simp]: "sumr 0 (2*n) (%i. (1) ^ Suc i) = 0" 

15251  88 
by (induct "n", auto) 
14416  89 

15251  90 
lemma sumr_interval_const: 
91 
"\<lbrakk>\<forall>n. m \<le> Suc n > f n = r; m \<le> k\<rbrakk> \<Longrightarrow> sumr m k f = (real(km) * r)" 

92 
apply (induct "k", auto) 

93 
apply (drule_tac x = k in spec) 

14416  94 
apply (auto dest!: le_imp_less_or_eq) 
15047  95 
apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split) 
14416  96 
done 
97 

15251  98 
lemma sumr_interval_const2: 
15360  99 
"[\<forall>n\<ge>m. f n = r; m \<le> k] 
15251  100 
==> sumr m k f = (real (k  m) * r)" 
101 
apply (induct "k", auto) 

102 
apply (drule_tac x = k in spec) 

14416  103 
apply (auto dest!: le_imp_less_or_eq) 
15047  104 
apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split) 
14416  105 
done 
106 

15047  107 

15251  108 
lemma sumr_le: 
15360  109 
"[\<forall>n\<ge>m. 0 \<le> f n; m < k] ==> sumr 0 m f \<le> sumr 0 k f" 
15251  110 
apply (induct "k") 
14416  111 
apply (auto simp add: less_Suc_eq_le) 
15251  112 
apply (drule_tac x = k in spec, safe) 
14416  113 
apply (drule le_imp_less_or_eq, safe) 
15047  114 
apply (arith) 
14416  115 
apply (drule_tac a = "sumr 0 m f" in order_refl [THEN add_mono], auto) 
116 
done 

117 

118 
lemma sumr_le2 [rule_format (no_asm)]: 

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

15251  120 
apply (induct "n") 
14416  121 
apply (auto intro: add_mono simp add: le_def) 
122 
done 

123 

15360  124 
lemma sumr_ge_zero: "(\<forall>n\<ge>m. 0 \<le> f n) > 0 \<le> sumr m n f" 
15251  125 
apply (induct "n", auto) 
14416  126 
apply (drule_tac x = n in spec, arith) 
127 
done 

128 

15536  129 
(* FIXME generalize *) 
14416  130 
lemma rabs_sumr_rabs_cancel [simp]: 
15229  131 
"abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))" 
15251  132 
by (induct "n", simp_all add: add_increasing) 
14416  133 

134 
lemma sumr_zero [rule_format]: 

15360  135 
"\<forall>n \<ge> N. f n = 0 ==> N \<le> m > sumr m n f = 0" 
15251  136 
by (induct "n", auto) 
14416  137 

138 
lemma Suc_le_imp_diff_ge2: 

15360  139 
"[\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m] ==> sumr m n f = 0" 
14416  140 
apply (rule sumr_zero) 
141 
apply (case_tac "n", auto) 

142 
done 

143 

144 
lemma sumr_one_lb_realpow_zero [simp]: "sumr (Suc 0) n (%n. f(n) * 0 ^ n) = 0" 

15251  145 
apply (induct "n") 
14416  146 
apply (case_tac [2] "n", auto) 
147 
done 

15536  148 
(* 
14416  149 
lemma sumr_diff: "sumr m n f  sumr m n g = sumr m n (%n. f n  g n)" 
15536  150 
by (simp add: diff_minus setsum_addf setsum_negf) 
151 
*) 

14416  152 
lemma sumr_subst [rule_format (no_asm)]: 
153 
"(\<forall>p. m \<le> p & p < m+n > (f p = g p)) > sumr m n f = sumr m n g" 

15251  154 
by (induct "n", auto) 
14416  155 

156 
lemma sumr_bound [rule_format (no_asm)]: 

157 
"(\<forall>p. m \<le> p & p < m + n > (f(p) \<le> K)) 

158 
> (sumr m (m + n) f \<le> (real n * K))" 

15251  159 
apply (induct "n") 
14416  160 
apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc) 
161 
done 

162 

163 
lemma sumr_bound2 [rule_format (no_asm)]: 

164 
"(\<forall>p. 0 \<le> p & p < n > (f(p) \<le> K)) 

165 
> (sumr 0 n f \<le> (real n * K))" 

15251  166 
apply (induct "n") 
15047  167 
apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc add_commute) 
14416  168 
done 
169 

170 
lemma sumr_group [simp]: 

171 
"sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f" 

172 
apply (subgoal_tac "k = 0  0 < k", auto) 

15251  173 
apply (induct "n") 
14416  174 
apply (simp_all add: sumr_split_add add_commute) 
175 
done 

176 

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

178 

179 
(* 

180 
suminf is the sum 

181 
*) 

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

183 
by (simp add: sums_def summable_def, blast) 

184 

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

186 
apply (simp add: summable_def suminf_def) 

187 
apply (blast intro: someI2) 

188 
done 

189 

190 
lemma summable_sumr_LIMSEQ_suminf: 

191 
"summable f ==> (%n. sumr 0 n f) > (suminf f)" 

192 
apply (simp add: summable_def suminf_def sums_def) 

193 
apply (blast intro: someI2) 

194 
done 

195 

196 
(* 

197 
sum is unique 

198 
*) 

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

200 
apply (frule sums_summable [THEN summable_sums]) 

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

202 
done 

203 

204 
(* 

205 
Goalw [sums_def,LIMSEQ_def] 

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

207 
by safe 

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

209 
by (safe THEN ftac le_imp_less_or_eq 1) 

210 
by safe 

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

212 
by (ALLGOALS (Asm_simp_tac)); 

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

214 
by Auto_tac 

215 
qed "series_zero"; 

216 
next one was called series_zero2 

217 
**********************) 

218 

219 
lemma series_zero: 

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

15537  221 
apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe) 
14416  222 
apply (rule_tac x = n in exI) 
15537  223 
apply (clarsimp simp:sumr_split_add_minus) 
14416  224 
apply (drule sumr_interval_const2, auto) 
225 
done 

226 

227 
lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)" 

15536  228 
by (auto simp add: sums_def setsum_mult [symmetric] 
14416  229 
intro!: LIMSEQ_mult intro: LIMSEQ_const) 
230 

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

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

233 

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

15536  235 
by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff) 
14416  236 

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

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

239 

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

241 
by (auto intro!: sums_unique sums_mult summable_sums) 

242 

243 
lemma suminf_diff: 

244 
"[ summable f; summable g ] 

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

246 
by (auto intro!: sums_diff sums_unique summable_sums) 

247 

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

15536  249 
by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf) 
14416  250 

251 
lemma sums_group: 

252 
"[summable f; 0 < k ] ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)" 

253 
apply (drule summable_sums) 

254 
apply (auto simp add: sums_def LIMSEQ_def) 

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

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

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

258 
apply (auto dest!: not_leE) 

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

260 
done 

261 

262 
lemma sumr_pos_lt_pair_lemma: 

263 
"[\<forall>d.  f (n + (d + d)) < f (Suc (n + (d + d)))] 

264 
==> sumr 0 (n + Suc (Suc 0)) f \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f" 

15251  265 
apply (induct "no", auto) 
266 
apply (drule_tac x = "Suc no" in spec) 

14416  267 
apply (simp add: add_ac) 
268 
done 

10751  269 

270 

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

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

273 
\<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))] 
14416  274 
==> sumr 0 n f < suminf f" 
275 
apply (drule summable_sums) 

276 
apply (auto simp add: sums_def LIMSEQ_def) 

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

277 
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

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

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

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

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

284 
apply (safe, simp) 

285 
apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \<le> sumr 0 (Suc (Suc 0) * (Suc no) + n) f") 

286 
apply (rule_tac [2] y = "sumr 0 (n+ Suc (Suc 0)) f" in order_trans) 

287 
prefer 3 apply assumption 

288 
apply (rule_tac [2] y = "sumr 0 n f + (f (n) + f (n + 1))" in order_trans) 

289 
apply simp_all 

290 
apply (subgoal_tac "suminf f \<le> sumr 0 (Suc (Suc 0) * (Suc no) + n) f") 

291 
apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans) 

292 
prefer 3 apply simp 

293 
apply (drule_tac [2] x = 0 in spec) 

294 
prefer 2 apply simp 

295 
apply (subgoal_tac "0 \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f +  suminf f") 

296 
apply (simp add: abs_if) 

297 
apply (auto simp add: linorder_not_less [symmetric]) 

298 
done 

299 

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

300 
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

301 
great as any partial sum.*} 
14416  302 

303 
lemma series_pos_le: 

15360  304 
"[ summable f; \<forall>m \<ge> n. 0 \<le> f(m) ] ==> sumr 0 n f \<le> suminf f" 
14416  305 
apply (drule summable_sums) 
306 
apply (simp add: sums_def) 

307 
apply (cut_tac k = "sumr 0 n f" in LIMSEQ_const) 

308 
apply (erule LIMSEQ_le, blast) 

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

310 
apply (drule le_imp_less_or_eq) 

311 
apply (auto intro: sumr_le) 

312 
done 

313 

314 
lemma series_pos_less: 

15360  315 
"[ summable f; \<forall>m \<ge> n. 0 < f(m) ] ==> sumr 0 n f < suminf f" 
14416  316 
apply (rule_tac y = "sumr 0 (Suc n) f" in order_less_le_trans) 
317 
apply (rule_tac [2] series_pos_le, auto) 

318 
apply (drule_tac x = m in spec, auto) 

319 
done 

320 

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

321 
text{*Sum of a geometric progression.*} 
14416  322 

323 
lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n  1) / (x  1)" 

15251  324 
apply (induct "n", auto) 
14416  325 
apply (rule_tac c1 = "x  1" in real_mult_right_cancel [THEN iffD1]) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

326 
apply (auto simp add: mult_assoc left_distrib times_divide_eq) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

327 
apply (simp add: right_distrib diff_minus mult_commute) 
14416  328 
done 
329 

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

331 
apply (case_tac "x = 1") 

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

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

333 
simp add: sumr_geometric sums_def diff_minus add_divide_distrib) 
14416  334 
apply (subgoal_tac "1 / (1 + x) = 0/ (x  1) +  1/ (x  1) ") 
335 
apply (erule ssubst) 

336 
apply (rule LIMSEQ_add, rule LIMSEQ_divide) 

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

337 
apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2) 
14416  338 
done 
339 

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

340 
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

341 

14416  342 
lemma summable_convergent_sumr_iff: "summable f = convergent (%n. sumr 0 n f)" 
343 
by (simp add: summable_def sums_def convergent_def) 

344 

345 
lemma summable_Cauchy: 

346 
"summable f = 

15360  347 
(\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(sumr m n f) < e)" 
15537  348 
apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus[symmetric]) 
14416  349 
apply (drule_tac [!] spec, auto) 
350 
apply (rule_tac x = M in exI) 

351 
apply (rule_tac [2] x = N in exI, auto) 

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

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

15360  354 
apply (drule_tac x = n in spec, simp) 
14416  355 
apply (drule_tac x = m in spec) 
15537  356 
apply(simp add: sumr_split_add_minus) 
357 
apply(subst abs_minus_commute) 

358 
apply(simp add: sumr_split_add_minus) 

359 
apply (simp add: sumr_split_add_minus) 

14416  360 
done 
361 

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

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

363 

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

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

369 
apply (rotate_tac 2) 

370 
apply (drule_tac x = m in spec) 

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

372 
apply (rule_tac y = "sumr m n (%k. abs (f k))" in order_le_less_trans) 

15536  373 
apply (rule setsum_abs) 
14416  374 
apply (rule_tac y = "sumr m n g" in order_le_less_trans) 
375 
apply (auto intro: sumr_le2 simp add: abs_interval_iff) 

376 
done 

377 

378 
lemma summable_rabs_comparison_test: 

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

382 
apply (auto simp add: abs_idempotent) 

383 
done 

384 

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

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

386 

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

389 
apply (drule summable_sums)+ 

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

391 
apply (rule exI) 

392 
apply (auto intro!: sumr_le2) 

393 
done 

394 

395 
lemma summable_le2: 

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

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

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

399 
apply (simp add: abs_le_interval_iff) 

400 
done 

401 

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

402 
text{*Absolute convergence imples normal convergence*} 
14416  403 
lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f" 
15536  404 
apply (auto simp add: summable_Cauchy) 
14416  405 
apply (drule spec, auto) 
406 
apply (rule_tac x = N in exI, auto) 

407 
apply (drule spec, auto) 

408 
apply (rule_tac y = "sumr m n (%n. abs (f n))" in order_le_less_trans) 

15536  409 
apply (auto) 
14416  410 
done 
411 

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

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

15536  415 
by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf) 
14416  416 

417 

418 
subsection{* The Ratio Test*} 

419 

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

421 
apply (drule order_le_imp_less_or_eq, auto) 

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

423 
apply (simp add: zero_le_mult_iff, arith) 

424 
done 

425 

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

427 
apply (drule le_imp_less_or_eq) 

428 
apply (auto dest: less_imp_Suc_add) 

429 
done 

430 

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

432 
by (auto simp add: le_Suc_ex) 

433 

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

435 
lemma ratio_test_lemma2: 

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

439 
apply (simp add: summable_Cauchy) 

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

441 
prefer 2 apply (blast intro: rabs_ratiotest_lemma) 

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

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

444 
done 

445 

446 
lemma ratio_test: 

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

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

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

451 
in summable_comparison_test) 
14416  452 
apply (rule_tac x = N in exI, safe) 
453 
apply (drule le_Suc_ex_iff [THEN iffD1]) 

454 
apply (auto simp add: power_add realpow_not_zero) 

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

455 
apply (induct_tac "na", auto simp add: times_divide_eq) 
14416  456 
apply (rule_tac y = "c*abs (f (N + n))" in order_trans) 
457 
apply (auto intro: mult_right_mono simp add: summable_def) 

458 
apply (simp add: mult_ac) 

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

459 
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

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

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

462 
apply (auto intro!: geometric_sums) 
14416  463 
done 
464 

465 

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

466 
text{*Differentiation of finite sum*} 
14416  467 

468 
lemma DERIV_sumr [rule_format (no_asm)]: 

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

470 
> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)" 

15251  471 
apply (induct "n") 
14416  472 
apply (auto intro: DERIV_add) 
473 
done 

474 

475 
ML 

476 
{* 

477 
val sumr_Suc = thm"sumr_Suc"; 

478 
val sums_def = thm"sums_def"; 

479 
val summable_def = thm"summable_def"; 

480 
val suminf_def = thm"suminf_def"; 

481 

482 
val sumr_split_add = thm "sumr_split_add"; 

483 
val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero"; 

484 
val sumr_le2 = thm "sumr_le2"; 

485 
val rabs_sumr_rabs_cancel = thm "rabs_sumr_rabs_cancel"; 

486 
val sumr_zero = thm "sumr_zero"; 

487 
val Suc_le_imp_diff_ge2 = thm "Suc_le_imp_diff_ge2"; 

488 
val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero"; 

489 
val sumr_subst = thm "sumr_subst"; 

490 
val sumr_bound = thm "sumr_bound"; 

491 
val sumr_bound2 = thm "sumr_bound2"; 

492 
val sumr_group = thm "sumr_group"; 

493 
val sums_summable = thm "sums_summable"; 

494 
val summable_sums = thm "summable_sums"; 

495 
val summable_sumr_LIMSEQ_suminf = thm "summable_sumr_LIMSEQ_suminf"; 

496 
val sums_unique = thm "sums_unique"; 

497 
val series_zero = thm "series_zero"; 

498 
val sums_mult = thm "sums_mult"; 

499 
val sums_divide = thm "sums_divide"; 

500 
val sums_diff = thm "sums_diff"; 

501 
val suminf_mult = thm "suminf_mult"; 

502 
val suminf_mult2 = thm "suminf_mult2"; 

503 
val suminf_diff = thm "suminf_diff"; 

504 
val sums_minus = thm "sums_minus"; 

505 
val sums_group = thm "sums_group"; 

506 
val sumr_pos_lt_pair_lemma = thm "sumr_pos_lt_pair_lemma"; 

507 
val sumr_pos_lt_pair = thm "sumr_pos_lt_pair"; 

508 
val series_pos_le = thm "series_pos_le"; 

509 
val series_pos_less = thm "series_pos_less"; 

510 
val sumr_geometric = thm "sumr_geometric"; 

511 
val geometric_sums = thm "geometric_sums"; 

512 
val summable_convergent_sumr_iff = thm "summable_convergent_sumr_iff"; 

513 
val summable_Cauchy = thm "summable_Cauchy"; 

514 
val summable_comparison_test = thm "summable_comparison_test"; 

515 
val summable_rabs_comparison_test = thm "summable_rabs_comparison_test"; 

516 
val summable_le = thm "summable_le"; 

517 
val summable_le2 = thm "summable_le2"; 

518 
val summable_rabs_cancel = thm "summable_rabs_cancel"; 

519 
val summable_rabs = thm "summable_rabs"; 

520 
val rabs_ratiotest_lemma = thm "rabs_ratiotest_lemma"; 

521 
val le_Suc_ex = thm "le_Suc_ex"; 

522 
val le_Suc_ex_iff = thm "le_Suc_ex_iff"; 

523 
val ratio_test_lemma2 = thm "ratio_test_lemma2"; 

524 
val ratio_test = thm "ratio_test"; 

525 
val DERIV_sumr = thm "DERIV_sumr"; 

526 
*} 

527 

528 
end 