1 (* Title : Series.thy |
1 (* Title : Series.thy |
2 Author : Jacques D. Fleuriot |
2 Author : Jacques D. Fleuriot |
3 Copyright : 1998 University of Cambridge |
3 Copyright : 1998 University of Cambridge |
4 |
4 |
5 Converted to Isar and polished by lcp |
5 Converted to Isar and polished by lcp |
|
6 Converted to setsum and polished yet more by TNN |
6 *) |
7 *) |
7 |
8 |
8 header{*Finite Summation and Infinite Series*} |
9 header{*Finite Summation and Infinite Series*} |
9 |
10 |
10 theory Series |
11 theory Series |
11 imports SEQ Lim |
12 imports SEQ Lim |
12 begin |
13 begin |
13 |
14 |
|
15 (* FIXME why not globally? *) |
14 declare atLeastLessThan_empty[simp]; |
16 declare atLeastLessThan_empty[simp]; |
15 |
17 declare atLeastLessThan_iff[iff] |
16 syntax sumr :: "[nat,nat,(nat=>real)] => real" |
|
17 translations |
|
18 "sumr m n f" => "setsum (f::nat=>real) (atLeastLessThan m n)" |
|
19 |
18 |
20 constdefs |
19 constdefs |
21 sums :: "[nat=>real,real] => bool" (infixr "sums" 80) |
20 sums :: "[nat=>real,real] => bool" (infixr "sums" 80) |
22 "f sums s == (%n. setsum f {0..<n}) ----> s" |
21 "f sums s == (%n. setsum f {0..<n}) ----> s" |
23 |
22 |
24 summable :: "(nat=>real) => bool" |
23 summable :: "(nat=>real) => bool" |
25 "summable f == (\<exists>s. f sums s)" |
24 "summable f == (\<exists>s. f sums s)" |
26 |
25 |
27 suminf :: "(nat=>real) => real" |
26 suminf :: "(nat=>real) => real" |
28 "suminf f == (@s. f sums s)" |
27 "suminf f == SOME s. f sums s" |
29 |
28 |
30 |
29 lemma setsum_Suc[simp]: |
31 lemma sumr_Suc [simp]: |
|
32 "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))" |
30 "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))" |
33 by (simp add: atLeastLessThanSuc add_commute) |
31 by (simp add: atLeastLessThanSuc add_commute) |
34 |
32 |
35 (* |
33 (* |
36 lemma sumr_add: "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)" |
34 lemma sumr_add: "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)" |
77 lemma sumr_less_bounds_zero [simp]: "n < m ==> sumr m n f = 0" |
76 lemma sumr_less_bounds_zero [simp]: "n < m ==> sumr m n f = 0" |
78 by (simp add: atLeastLessThan_empty) |
77 by (simp add: atLeastLessThan_empty) |
79 |
78 |
80 lemma sumr_minus: "sumr m n (%i. - f i) = - sumr m n f" |
79 lemma sumr_minus: "sumr m n (%i. - f i) = - sumr m n f" |
81 by (simp add: Finite_Set.setsum_negf) |
80 by (simp add: Finite_Set.setsum_negf) |
82 *) |
81 |
83 |
82 lemma sumr_shift_bounds: |
84 lemma sumr_shift_bounds: "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))" |
83 "setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}" |
85 by (induct "n", auto) |
84 by (induct "n", auto) |
86 |
85 *) |
87 lemma sumr_minus_one_realpow_zero [simp]: "sumr 0 (2*n) (%i. (-1) ^ Suc i) = 0" |
86 |
|
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)" |
88 by (induct "n", auto) |
90 by (induct "n", auto) |
89 |
91 |
90 lemma sumr_interval_const: |
92 (* |
91 "\<lbrakk>\<forall>n. m \<le> Suc n --> f n = r; m \<le> k\<rbrakk> \<Longrightarrow> sumr m k f = (real(k-m) * r)" |
93 lemma sumr_interval_const2: |
92 apply (induct "k", auto) |
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) |
93 apply (drule_tac x = k in spec) |
97 apply (drule_tac x = k in spec) |
94 apply (auto dest!: le_imp_less_or_eq) |
98 apply (auto dest!: le_imp_less_or_eq) |
95 apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split) |
99 apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split) |
96 done |
100 done |
97 |
101 *) |
98 lemma sumr_interval_const2: |
102 (* FIXME split in tow steps |
99 "[|\<forall>n\<ge>m. f n = r; m \<le> k|] |
103 lemma setsum_nat_set_real_const: |
100 ==> sumr m k f = (real (k - m) * r)" |
104 "(\<And>n. n\<in>A \<Longrightarrow> f n = r) \<Longrightarrow> setsum f A = real(card A) * r" (is "PROP ?P") |
101 apply (induct "k", auto) |
105 proof (cases "finite A") |
102 apply (drule_tac x = k in spec) |
106 case True |
103 apply (auto dest!: le_imp_less_or_eq) |
107 thus "PROP ?P" |
104 apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split) |
108 proof induct |
105 done |
109 case empty thus ?case by simp |
106 |
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 *) |
|
117 |
|
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) |
|
127 done |
107 |
128 |
108 lemma sumr_le: |
129 lemma sumr_le: |
109 "[|\<forall>n\<ge>m. 0 \<le> f n; m < k|] ==> sumr 0 m f \<le> sumr 0 k f" |
130 "[|\<forall>n\<ge>m. 0 \<le> f n; m < k|] ==> sumr 0 m f \<le> sumr 0 k f" |
110 apply (induct "k") |
131 apply (induct "k") |
111 apply (auto simp add: less_Suc_eq_le) |
132 apply (auto simp add: less_Suc_eq_le) |
118 lemma sumr_le2 [rule_format (no_asm)]: |
139 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" |
140 "(\<forall>r. m \<le> r & r < n --> f r \<le> g r) --> sumr m n f \<le> sumr m n g" |
120 apply (induct "n") |
141 apply (induct "n") |
121 apply (auto intro: add_mono simp add: le_def) |
142 apply (auto intro: add_mono simp add: le_def) |
122 done |
143 done |
123 |
144 *) |
|
145 |
|
146 (* |
124 lemma sumr_ge_zero: "(\<forall>n\<ge>m. 0 \<le> f n) --> 0 \<le> sumr m n f" |
147 lemma sumr_ge_zero: "(\<forall>n\<ge>m. 0 \<le> f n) --> 0 \<le> sumr m n f" |
125 apply (induct "n", auto) |
148 apply (induct "n", auto) |
126 apply (drule_tac x = n in spec, arith) |
149 apply (drule_tac x = n in spec, arith) |
127 done |
150 done |
128 |
151 *) |
129 (* FIXME generalize *) |
152 |
|
153 (* |
130 lemma rabs_sumr_rabs_cancel [simp]: |
154 lemma rabs_sumr_rabs_cancel [simp]: |
131 "abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))" |
155 "abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))" |
132 by (induct "n", simp_all add: add_increasing) |
156 by (induct "n", simp_all add: add_increasing) |
133 |
157 |
134 lemma sumr_zero [rule_format]: |
158 lemma sumr_zero [rule_format]: |
135 "\<forall>n \<ge> N. f n = 0 ==> N \<le> m --> sumr m n f = 0" |
159 "\<forall>n \<ge> N. f n = 0 ==> N \<le> m --> sumr m n f = 0" |
136 by (induct "n", auto) |
160 by (induct "n", auto) |
|
161 *) |
137 |
162 |
138 lemma Suc_le_imp_diff_ge2: |
163 lemma Suc_le_imp_diff_ge2: |
139 "[|\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m|] ==> sumr m n f = 0" |
164 "[|\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m|] ==> setsum f {m..<n} = 0" |
140 apply (rule sumr_zero) |
165 apply (rule setsum_0') |
141 apply (case_tac "n", auto) |
166 apply (case_tac "n", auto) |
142 done |
167 apply(erule_tac x = "a - 1" in allE) |
143 |
168 apply (simp split:nat_diff_split) |
144 lemma sumr_one_lb_realpow_zero [simp]: "sumr (Suc 0) n (%n. f(n) * 0 ^ n) = 0" |
169 done |
|
170 |
|
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" |
145 apply (induct "n") |
174 apply (induct "n") |
146 apply (case_tac [2] "n", auto) |
175 apply (case_tac [2] "n", auto) |
147 done |
176 done |
148 (* |
177 (* |
149 lemma sumr_diff: "sumr m n f - sumr m n g = sumr m n (%n. f n - g n)" |
178 lemma sumr_diff: "sumr m n f - sumr m n g = sumr m n (%n. f n - g n)" |
150 by (simp add: diff_minus setsum_addf setsum_negf) |
179 by (simp add: diff_minus setsum_addf setsum_negf) |
151 *) |
180 *) |
|
181 (* |
152 lemma sumr_subst [rule_format (no_asm)]: |
182 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" |
183 "(\<forall>p. m \<le> p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g" |
154 by (induct "n", auto) |
184 by (induct "n", auto) |
155 |
185 *) |
|
186 |
|
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 (* |
156 lemma sumr_bound [rule_format (no_asm)]: |
197 lemma sumr_bound [rule_format (no_asm)]: |
157 "(\<forall>p. m \<le> p & p < m + n --> (f(p) \<le> K)) |
198 "(\<forall>p. m \<le> p & p < m + n --> (f(p) \<le> K)) |
158 --> (sumr m (m + n) f \<le> (real n * K))" |
199 --> setsum f {m..<m+n::nat} \<le> (real n * K)" |
159 apply (induct "n") |
200 apply (induct "n") |
160 apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc) |
201 apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc) |
161 done |
202 done |
162 |
203 *) |
|
204 (* FIXME should be generalized |
163 lemma sumr_bound2 [rule_format (no_asm)]: |
205 lemma sumr_bound2 [rule_format (no_asm)]: |
164 "(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K)) |
206 "(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K)) |
165 --> (sumr 0 n f \<le> (real n * K))" |
207 --> setsum f {0..<n::nat} \<le> (real n * K)" |
166 apply (induct "n") |
208 apply (induct "n") |
167 apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc add_commute) |
209 apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc add_commute) |
168 done |
210 done |
169 |
211 *) |
|
212 (* FIXME a bit specialized for [simp]! *) |
170 lemma sumr_group [simp]: |
213 lemma sumr_group [simp]: |
171 "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f" |
214 "(\<Sum>m=0..<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {0 ..< n * k}" |
172 apply (subgoal_tac "k = 0 | 0 < k", auto) |
215 apply (subgoal_tac "k = 0 | 0 < k", auto simp:setsum_0') |
173 apply (induct "n") |
216 apply (induct "n") |
174 apply (simp_all add: sumr_split_add add_commute) |
217 apply (simp_all add: setsum_add_nat_ivl add_commute) |
175 done |
218 done |
|
219 (* FIXME setsum_0[simp] *) |
|
220 |
176 |
221 |
177 subsection{* Infinite Sums, by the Properties of Limits*} |
222 subsection{* Infinite Sums, by the Properties of Limits*} |
178 |
223 |
179 (*---------------------- |
224 (*---------------------- |
180 suminf is the sum |
225 suminf is the sum |
214 by Auto_tac |
259 by Auto_tac |
215 qed "series_zero"; |
260 qed "series_zero"; |
216 next one was called series_zero2 |
261 next one was called series_zero2 |
217 **********************) |
262 **********************) |
218 |
263 |
|
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??? *) |
219 lemma series_zero: |
281 lemma series_zero: |
220 "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (sumr 0 n f)" |
282 "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})" |
221 apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe) |
283 apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe) |
222 apply (rule_tac x = n in exI) |
284 apply (rule_tac x = n in exI) |
223 apply (clarsimp simp:sumr_split_add_minus) |
285 apply (clarsimp simp add:setsum_diff[symmetric] setsum_0' Ball_def) |
224 apply (drule sumr_interval_const2, auto) |
286 done |
225 done |
287 |
226 |
288 |
227 lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)" |
289 lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)" |
228 by (auto simp add: sums_def setsum_mult [symmetric] |
290 by (auto simp add: sums_def setsum_mult [symmetric] |
229 intro!: LIMSEQ_mult intro: LIMSEQ_const) |
291 intro!: LIMSEQ_mult intro: LIMSEQ_const) |
230 |
292 |
247 |
309 |
248 lemma sums_minus: "x sums x0 ==> (%n. - x n) sums - x0" |
310 lemma sums_minus: "x sums x0 ==> (%n. - x n) sums - x0" |
249 by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf) |
311 by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf) |
250 |
312 |
251 lemma sums_group: |
313 lemma sums_group: |
252 "[|summable f; 0 < k |] ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)" |
314 "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)" |
253 apply (drule summable_sums) |
315 apply (drule summable_sums) |
254 apply (auto simp add: sums_def LIMSEQ_def) |
316 apply (auto simp add: sums_def LIMSEQ_def) |
255 apply (drule_tac x = r in spec, safe) |
317 apply (drule_tac x = r in spec, safe) |
256 apply (rule_tac x = no in exI, safe) |
318 apply (rule_tac x = no in exI, safe) |
257 apply (drule_tac x = "n*k" in spec) |
319 apply (drule_tac x = "n*k" in spec) |
258 apply (auto dest!: not_leE) |
320 apply (auto dest!: not_leE) |
259 apply (drule_tac j = no in less_le_trans, auto) |
321 apply (drule_tac j = no in less_le_trans, auto) |
260 done |
322 done |
261 |
323 |
262 lemma sumr_pos_lt_pair_lemma: |
324 lemma sumr_pos_lt_pair_lemma: |
263 "[|\<forall>d. - f (n + (d + d)) < f (Suc (n + (d + d)))|] |
325 "[|\<forall>d. - f (n + (d + d)) < (f (Suc (n + (d + d))) :: real) |] |
264 ==> sumr 0 (n + Suc (Suc 0)) f \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f" |
326 ==> setsum f {0..<n+Suc(Suc 0)} \<le> setsum f {0..<Suc(Suc 0) * Suc no + n}" |
265 apply (induct "no", auto) |
327 apply (induct "no", auto) |
266 apply (drule_tac x = "Suc no" in spec) |
328 apply (drule_tac x = "Suc no" in spec) |
267 apply (simp add: add_ac) |
329 apply (simp add: add_ac) |
268 done |
330 done |
269 |
331 |
270 |
332 |
271 lemma sumr_pos_lt_pair: |
333 lemma sumr_pos_lt_pair: |
272 "[|summable f; |
334 "[|summable f; |
273 \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|] |
335 \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|] |
274 ==> sumr 0 n f < suminf f" |
336 ==> setsum f {0..<n} < suminf f" |
275 apply (drule summable_sums) |
337 apply (drule summable_sums) |
276 apply (auto simp add: sums_def LIMSEQ_def) |
338 apply (auto simp add: sums_def LIMSEQ_def) |
277 apply (drule_tac x = "f (n) + f (n + 1)" in spec) |
339 apply (drule_tac x = "f (n) + f (n + 1)" in spec) |
278 apply (auto iff: real_0_less_add_iff) |
340 apply (auto iff: real_0_less_add_iff) |
279 --{*legacy proof: not necessarily better!*} |
341 --{*legacy proof: not necessarily better!*} |
280 apply (rule_tac [2] ccontr, drule_tac [2] linorder_not_less [THEN iffD1]) |
342 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) |
343 apply (frule_tac [2] no=no in sumr_pos_lt_pair_lemma) |
282 apply (drule_tac x = 0 in spec, simp) |
344 apply (drule_tac x = 0 in spec, simp) |
283 apply (rotate_tac 1, drule_tac x = "Suc (Suc 0) * (Suc no) + n" in spec) |
345 apply (rotate_tac 1, drule_tac x = "Suc (Suc 0) * (Suc no) + n" in spec) |
284 apply (safe, simp) |
346 apply (safe, simp) |
285 apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \<le> sumr 0 (Suc (Suc 0) * (Suc no) + n) f") |
347 apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \<le> |
286 apply (rule_tac [2] y = "sumr 0 (n+ Suc (Suc 0)) f" in order_trans) |
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) |
287 prefer 3 apply assumption |
350 prefer 3 apply assumption |
288 apply (rule_tac [2] y = "sumr 0 n f + (f (n) + f (n + 1))" in order_trans) |
351 apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans) |
289 apply simp_all |
352 apply simp_all |
290 apply (subgoal_tac "suminf f \<le> sumr 0 (Suc (Suc 0) * (Suc no) + n) f") |
353 apply (subgoal_tac "suminf f \<le> setsum f {0..< Suc (Suc 0) * (Suc no) + n}") |
291 apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans) |
354 apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans) |
292 prefer 3 apply simp |
355 prefer 3 apply simp |
293 apply (drule_tac [2] x = 0 in spec) |
356 apply (drule_tac [2] x = 0 in spec) |
294 prefer 2 apply simp |
357 prefer 2 apply simp |
295 apply (subgoal_tac "0 \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f + - suminf f") |
358 apply (subgoal_tac "0 \<le> setsum f {0 ..< Suc (Suc 0) * Suc no + n} + - suminf f") |
296 apply (simp add: abs_if) |
359 apply (simp add: abs_if) |
297 apply (auto simp add: linorder_not_less [symmetric]) |
360 apply (auto simp add: linorder_not_less [symmetric]) |
298 done |
361 done |
299 |
362 |
300 text{*A summable series of positive terms has limit that is at least as |
363 text{*A summable series of positive terms has limit that is at least as |
301 great as any partial sum.*} |
364 great as any partial sum.*} |
302 |
365 |
303 lemma series_pos_le: |
366 lemma series_pos_le: |
304 "[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f" |
367 "[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> setsum f {0..<n} \<le> suminf f" |
305 apply (drule summable_sums) |
368 apply (drule summable_sums) |
306 apply (simp add: sums_def) |
369 apply (simp add: sums_def) |
307 apply (cut_tac k = "sumr 0 n f" in LIMSEQ_const) |
370 apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const) |
308 apply (erule LIMSEQ_le, blast) |
371 apply (erule LIMSEQ_le, blast) |
309 apply (rule_tac x = n in exI, clarify) |
372 apply (rule_tac x = n in exI, clarify) |
310 apply (drule le_imp_less_or_eq) |
373 apply (rule setsum_mono2) |
311 apply (auto intro: sumr_le) |
374 apply auto |
312 done |
375 done |
313 |
376 |
314 lemma series_pos_less: |
377 lemma series_pos_less: |
315 "[| summable f; \<forall>m \<ge> n. 0 < f(m) |] ==> sumr 0 n f < suminf f" |
378 "[| summable f; \<forall>m \<ge> n. 0 < f(m) |] ==> setsum f {0..<n} < suminf f" |
316 apply (rule_tac y = "sumr 0 (Suc n) f" in order_less_le_trans) |
379 apply (rule_tac y = "setsum f {0..<Suc n}" in order_less_le_trans) |
317 apply (rule_tac [2] series_pos_le, auto) |
380 apply (rule_tac [2] series_pos_le, auto) |
318 apply (drule_tac x = m in spec, auto) |
381 apply (drule_tac x = m in spec, auto) |
319 done |
382 done |
320 |
383 |
321 text{*Sum of a geometric progression.*} |
384 text{*Sum of a geometric progression.*} |
322 |
385 |
323 lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)" |
386 lemma sumr_geometric: |
|
387 "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = (x ^ n - 1) / (x - 1::real)" |
324 apply (induct "n", auto) |
388 apply (induct "n", auto) |
325 apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1]) |
389 apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1]) |
326 apply (auto simp add: mult_assoc left_distrib times_divide_eq) |
390 apply (auto simp add: mult_assoc left_distrib) |
327 apply (simp add: right_distrib diff_minus mult_commute) |
391 apply (simp add: right_distrib diff_minus mult_commute) |
328 done |
392 done |
329 |
393 |
330 lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))" |
394 lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))" |
331 apply (case_tac "x = 1") |
395 apply (case_tac "x = 1") |
337 apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2) |
401 apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2) |
338 done |
402 done |
339 |
403 |
340 text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*} |
404 text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*} |
341 |
405 |
342 lemma summable_convergent_sumr_iff: "summable f = convergent (%n. sumr 0 n f)" |
406 lemma summable_convergent_sumr_iff: |
|
407 "summable f = convergent (%n. setsum f {0..<n})" |
343 by (simp add: summable_def sums_def convergent_def) |
408 by (simp add: summable_def sums_def convergent_def) |
344 |
409 |
345 lemma summable_Cauchy: |
410 lemma summable_Cauchy: |
346 "summable f = |
411 "summable f = |
347 (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(sumr m n f) < e)" |
412 (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(setsum f {m..<n}) < e)" |
348 apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus[symmetric]) |
413 apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus[symmetric]) |
349 apply (drule_tac [!] spec, auto) |
414 apply (drule_tac [!] spec, auto) |
350 apply (rule_tac x = M in exI) |
415 apply (rule_tac x = M in exI) |
351 apply (rule_tac [2] x = N in exI, auto) |
416 apply (rule_tac [2] x = N in exI, auto) |
352 apply (cut_tac [!] m = m and n = n in less_linear, auto) |
417 apply (cut_tac [!] m = m and n = n in less_linear, auto) |
353 apply (frule le_less_trans [THEN less_imp_le], assumption) |
418 apply (frule le_less_trans [THEN less_imp_le], assumption) |
354 apply (drule_tac x = n in spec, simp) |
419 apply (drule_tac x = n in spec, simp) |
355 apply (drule_tac x = m in spec) |
420 apply (drule_tac x = m in spec) |
356 apply(simp add: sumr_split_add_minus) |
421 apply(simp add: setsum_diff[symmetric]) |
357 apply(subst abs_minus_commute) |
422 apply(subst abs_minus_commute) |
358 apply(simp add: sumr_split_add_minus) |
423 apply(simp add: setsum_diff[symmetric]) |
359 apply (simp add: sumr_split_add_minus) |
424 apply(simp add: setsum_diff[symmetric]) |
360 done |
425 done |
|
426 (* FIXME move ivl_ lemmas out of this theory *) |
361 |
427 |
362 text{*Comparison test*} |
428 text{*Comparison test*} |
363 |
429 |
364 lemma summable_comparison_test: |
430 lemma summable_comparison_test: |
365 "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] ==> summable f" |
431 "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] ==> summable f" |
465 |
531 |
466 text{*Differentiation of finite sum*} |
532 text{*Differentiation of finite sum*} |
467 |
533 |
468 lemma DERIV_sumr [rule_format (no_asm)]: |
534 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)) |
535 "(\<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)" |
536 --> DERIV (%x. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)" |
471 apply (induct "n") |
537 apply (induct "n") |
472 apply (auto intro: DERIV_add) |
538 apply (auto intro: DERIV_add) |
473 done |
539 done |
474 |
540 |
475 ML |
541 ML |
476 {* |
542 {* |
477 val sumr_Suc = thm"sumr_Suc"; |
|
478 val sums_def = thm"sums_def"; |
543 val sums_def = thm"sums_def"; |
479 val summable_def = thm"summable_def"; |
544 val summable_def = thm"summable_def"; |
480 val suminf_def = thm"suminf_def"; |
545 val suminf_def = thm"suminf_def"; |
481 |
546 |
482 val sumr_split_add = thm "sumr_split_add"; |
|
483 val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero"; |
547 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"; |
548 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"; |
549 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"; |
550 val sumr_group = thm "sumr_group"; |
493 val sums_summable = thm "sums_summable"; |
551 val sums_summable = thm "sums_summable"; |
494 val summable_sums = thm "summable_sums"; |
552 val summable_sums = thm "summable_sums"; |
495 val summable_sumr_LIMSEQ_suminf = thm "summable_sumr_LIMSEQ_suminf"; |
553 val summable_sumr_LIMSEQ_suminf = thm "summable_sumr_LIMSEQ_suminf"; |
496 val sums_unique = thm "sums_unique"; |
554 val sums_unique = thm "sums_unique"; |