author | nipkow |
Mon, 21 Feb 2005 15:04:10 +0100 | |
changeset 15539 | 333a88244569 |
parent 15537 | 5538d3244b4d |
child 15542 | ee6cd48cf840 |
permissions | -rw-r--r-- |
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 (x0-y0)" |
|
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{*Cauchy-type 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 |