author | paulson |
Tue, 16 Jan 2001 12:20:52 +0100 | |
changeset 10919 | 144ede948e58 |
parent 10784 | 27e4d90b35b5 |
child 11468 | 02cd5d5bc497 |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : Series.ML |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
4 |
: 1999 University of Edinburgh |
|
5 |
Description : Finite summation and infinite series |
|
6 |
*) |
|
7 |
||
8 |
Goal "sumr (Suc n) n f = #0"; |
|
9 |
by (induct_tac "n" 1); |
|
10 |
by (Auto_tac); |
|
11 |
qed "sumr_Suc_zero"; |
|
12 |
Addsimps [sumr_Suc_zero]; |
|
13 |
||
14 |
Goal "sumr m m f = #0"; |
|
15 |
by (induct_tac "m" 1); |
|
16 |
by (Auto_tac); |
|
17 |
qed "sumr_eq_bounds"; |
|
18 |
Addsimps [sumr_eq_bounds]; |
|
19 |
||
20 |
Goal "sumr m (Suc m) f = f(m)"; |
|
21 |
by (Auto_tac); |
|
22 |
qed "sumr_Suc_eq"; |
|
23 |
Addsimps [sumr_Suc_eq]; |
|
24 |
||
25 |
Goal "sumr (m+k) k f = #0"; |
|
26 |
by (induct_tac "k" 1); |
|
27 |
by (Auto_tac); |
|
28 |
qed "sumr_add_lbound_zero"; |
|
29 |
Addsimps [sumr_add_lbound_zero]; |
|
30 |
||
31 |
Goal "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)"; |
|
32 |
by (induct_tac "n" 1); |
|
33 |
by (auto_tac (claset(),simpset() addsimps real_add_ac)); |
|
34 |
qed "sumr_add"; |
|
35 |
||
36 |
Goal "r * sumr m n f = sumr m n (%n. r * f n)"; |
|
37 |
by (induct_tac "n" 1); |
|
38 |
by (Auto_tac); |
|
39 |
by (auto_tac (claset(),simpset() addsimps |
|
40 |
[real_add_mult_distrib2])); |
|
41 |
qed "sumr_mult"; |
|
42 |
||
43 |
Goal "n < p --> sumr 0 n f + sumr n p f = sumr 0 p f"; |
|
44 |
by (induct_tac "p" 1); |
|
45 |
by (auto_tac (claset() addSDs [CLAIM "n < Suc na ==> n <= na", |
|
46 |
leI] addDs [le_anti_sym], simpset())); |
|
47 |
qed_spec_mp "sumr_split_add"; |
|
48 |
||
49 |
Goal "n < p ==> sumr 0 p f + \ |
|
50 |
\ - sumr 0 n f = sumr n p f"; |
|
51 |
by (dres_inst_tac [("f1","f")] (sumr_split_add RS sym) 1); |
|
52 |
by (asm_simp_tac (simpset() addsimps real_add_ac) 1); |
|
53 |
qed "sumr_split_add_minus"; |
|
54 |
||
55 |
Goal "abs(sumr m n f) <= sumr m n (%i. abs(f i))"; |
|
56 |
by (induct_tac "n" 1); |
|
57 |
by (auto_tac (claset() addIs [abs_triangle_ineq RS order_trans, |
|
58 |
real_add_le_mono1], |
|
59 |
simpset())); |
|
60 |
qed "sumr_rabs"; |
|
61 |
||
62 |
Goal "!!f g. (ALL r. m <= r & r < n --> f r = g r) \ |
|
63 |
\ --> sumr m n f = sumr m n g"; |
|
64 |
by (induct_tac "n" 1); |
|
65 |
by (Auto_tac); |
|
66 |
qed_spec_mp "sumr_fun_eq"; |
|
67 |
||
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10784
diff
changeset
|
68 |
Goal "sumr 0 n (%i. r) = real n * r"; |
10751 | 69 |
by (induct_tac "n" 1); |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
70 |
by (auto_tac (claset(), |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
71 |
simpset() addsimps [real_add_mult_distrib,real_of_nat_zero, |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
72 |
real_of_nat_Suc])); |
10751 | 73 |
qed "sumr_const"; |
74 |
Addsimps [sumr_const]; |
|
75 |
||
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10784
diff
changeset
|
76 |
Goal "sumr 0 n f + -(real n * r) = sumr 0 n (%i. f i + -r)"; |
10751 | 77 |
by (full_simp_tac (simpset() addsimps [sumr_add RS sym, |
78 |
real_minus_mult_eq2] delsimps [real_minus_mult_eq2 RS sym]) 1); |
|
79 |
qed "sumr_add_mult_const"; |
|
80 |
||
81 |
Goalw [real_diff_def] |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10784
diff
changeset
|
82 |
"sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"; |
10751 | 83 |
by (full_simp_tac (simpset() addsimps [sumr_add_mult_const]) 1); |
84 |
qed "sumr_diff_mult_const"; |
|
85 |
||
86 |
Goal "n < m --> sumr m n f = #0"; |
|
87 |
by (induct_tac "n" 1); |
|
88 |
by (auto_tac (claset() addDs [less_imp_le], simpset())); |
|
89 |
qed_spec_mp "sumr_less_bounds_zero"; |
|
90 |
Addsimps [sumr_less_bounds_zero]; |
|
91 |
||
92 |
Goal "sumr m n (%i. - f i) = - sumr m n f"; |
|
93 |
by (induct_tac "n" 1); |
|
94 |
by (case_tac "Suc n <= m" 2); |
|
95 |
by (auto_tac (claset(),simpset() addsimps |
|
96 |
[real_minus_add_distrib])); |
|
97 |
qed "sumr_minus"; |
|
98 |
||
99 |
Goal "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"; |
|
100 |
by (induct_tac "n" 1); |
|
101 |
by (Auto_tac); |
|
102 |
qed "sumr_shift_bounds"; |
|
103 |
||
104 |
Goal "sumr 0 (#2*n) (%i. (#-1) ^ Suc i) = #0"; |
|
105 |
by (induct_tac "n" 1); |
|
106 |
by (Auto_tac); |
|
107 |
qed "sumr_minus_one_realpow_zero"; |
|
108 |
Addsimps [sumr_minus_one_realpow_zero]; |
|
109 |
||
110 |
Goal "m < Suc n ==> Suc n - m = Suc (n - m)"; |
|
111 |
by (dtac less_imp_Suc_add 1); |
|
112 |
by (Auto_tac); |
|
113 |
val Suc_diff_n = result(); |
|
114 |
||
115 |
Goal "(ALL n. m <= Suc n --> f n = r) & m <= na \ |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10784
diff
changeset
|
116 |
\ --> sumr m na f = (real (na - m) * r)"; |
10751 | 117 |
by (induct_tac "na" 1); |
118 |
by (Step_tac 1); |
|
119 |
by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq]) 2); |
|
120 |
by (Step_tac 1); |
|
121 |
by (dres_inst_tac [("x","n")] spec 3); |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
122 |
by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset())); |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
123 |
by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib, Suc_diff_n, |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
124 |
real_of_nat_Suc]) 1); |
10751 | 125 |
qed_spec_mp "sumr_interval_const"; |
126 |
||
127 |
Goal "(ALL n. m <= n --> f n = r) & m <= na \ |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10784
diff
changeset
|
128 |
\ --> sumr m na f = (real (na - m) * r)"; |
10751 | 129 |
by (induct_tac "na" 1); |
130 |
by (Step_tac 1); |
|
131 |
by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq]) 2); |
|
132 |
by (Step_tac 1); |
|
133 |
by (dres_inst_tac [("x","n")] spec 3); |
|
134 |
by (auto_tac (claset() addSDs [le_imp_less_or_eq], |
|
135 |
simpset())); |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
136 |
by (asm_simp_tac (simpset() addsimps [Suc_diff_n, real_add_mult_distrib, |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
137 |
real_of_nat_Suc]) 1); |
10751 | 138 |
qed_spec_mp "sumr_interval_const2"; |
139 |
||
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
140 |
Goal "(ALL n. m <= n --> #0 <= f n) & m < k --> sumr 0 m f <= sumr 0 k f"; |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
141 |
by (induct_tac "k" 1); |
10751 | 142 |
by (Step_tac 1); |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
143 |
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [less_Suc_eq_le]))); |
10751 | 144 |
by (ALLGOALS(dres_inst_tac [("x","n")] spec)); |
145 |
by (Step_tac 1); |
|
146 |
by (dtac le_imp_less_or_eq 1 THEN Step_tac 1); |
|
147 |
by (dtac real_add_le_mono 2); |
|
148 |
by (dres_inst_tac [("i","sumr 0 m f")] (order_refl RS real_add_le_mono) 1); |
|
149 |
by (Auto_tac); |
|
150 |
qed_spec_mp "sumr_le"; |
|
151 |
||
152 |
Goal "!!f g. (ALL r. m <= r & r < n --> f r <= g r) \ |
|
153 |
\ --> sumr m n f <= sumr m n g"; |
|
154 |
by (induct_tac "n" 1); |
|
155 |
by (auto_tac (claset() addIs [real_add_le_mono], |
|
156 |
simpset() addsimps [le_def])); |
|
157 |
qed_spec_mp "sumr_le2"; |
|
158 |
||
159 |
Goal "(ALL n. #0 <= f n) --> #0 <= sumr m n f"; |
|
160 |
by (induct_tac "n" 1); |
|
161 |
by Auto_tac; |
|
162 |
by (dres_inst_tac [("x","n")] spec 1); |
|
163 |
by (arith_tac 1); |
|
164 |
qed_spec_mp "sumr_ge_zero"; |
|
165 |
||
166 |
Goal "(ALL n. m <= n --> #0 <= f n) --> #0 <= sumr m n f"; |
|
167 |
by (induct_tac "n" 1); |
|
168 |
by Auto_tac; |
|
169 |
by (dres_inst_tac [("x","n")] spec 1); |
|
170 |
by (arith_tac 1); |
|
171 |
qed_spec_mp "sumr_ge_zero2"; |
|
172 |
||
173 |
Goal "#0 <= sumr m n (%n. abs (f n))"; |
|
174 |
by (induct_tac "n" 1); |
|
175 |
by Auto_tac; |
|
176 |
by (arith_tac 1); |
|
177 |
qed "sumr_rabs_ge_zero"; |
|
178 |
Addsimps [sumr_rabs_ge_zero]; |
|
179 |
AddSIs [sumr_rabs_ge_zero]; |
|
180 |
||
181 |
Goal "abs (sumr m n (%n. abs (f n))) = (sumr m n (%n. abs (f n)))"; |
|
182 |
by (induct_tac "n" 1); |
|
183 |
by (Auto_tac THEN arith_tac 1); |
|
184 |
qed "rabs_sumr_rabs_cancel"; |
|
185 |
Addsimps [rabs_sumr_rabs_cancel]; |
|
186 |
||
187 |
Goal "ALL n. N <= n --> f n = #0 \ |
|
188 |
\ ==> ALL m n. N <= m --> sumr m n f = #0"; |
|
189 |
by (Step_tac 1); |
|
190 |
by (induct_tac "n" 1); |
|
191 |
by (Auto_tac); |
|
192 |
qed "sumr_zero"; |
|
193 |
||
194 |
Goal "Suc N <= n --> N <= n - 1"; |
|
195 |
by (induct_tac "n" 1); |
|
196 |
by (Auto_tac); |
|
197 |
qed_spec_mp "Suc_le_imp_diff_ge"; |
|
198 |
||
199 |
Goal "ALL n. N <= n --> f (Suc n) = #0 \ |
|
200 |
\ ==> ALL m n. Suc N <= m --> sumr m n f = #0"; |
|
201 |
by (rtac sumr_zero 1 THEN Step_tac 1); |
|
202 |
by (subgoal_tac "0 < n" 1); |
|
203 |
by (dtac Suc_le_imp_diff_ge 1); |
|
204 |
by (Auto_tac); |
|
205 |
qed "Suc_le_imp_diff_ge2"; |
|
206 |
||
207 |
(* proved elsewhere? *) |
|
208 |
Goal "(0 < n) = (EX m. n = Suc m)"; |
|
209 |
by (induct_tac "n" 1); |
|
210 |
by (Auto_tac); |
|
211 |
qed "gt_zero_eq_Ex"; |
|
212 |
||
213 |
Goal "sumr 1 n (%n. f(n) * #0 ^ n) = #0"; |
|
214 |
by (induct_tac "n" 1); |
|
215 |
by (auto_tac (claset(),simpset() addsimps [gt_zero_eq_Ex])); |
|
216 |
qed "sumr_one_lb_realpow_zero"; |
|
217 |
Addsimps [sumr_one_lb_realpow_zero]; |
|
218 |
||
219 |
Goalw [real_diff_def] "sumr m n f - sumr m n g = sumr m n (%n. f n - g n)"; |
|
220 |
by (simp_tac (simpset() addsimps [sumr_add RS sym,sumr_minus]) 1); |
|
221 |
qed "sumr_diff"; |
|
222 |
||
223 |
Goal "(ALL p. (m <= p & p < m + n --> (f p = g p))) --> sumr m n f = sumr m n g"; |
|
224 |
by (induct_tac "n" 1); |
|
225 |
by (Auto_tac); |
|
226 |
qed_spec_mp "sumr_subst"; |
|
227 |
||
228 |
Goal "(ALL p. m <= p & p < m + n --> (f(p) <= K)) \ |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10784
diff
changeset
|
229 |
\ --> (sumr m (m + n) f <= (real n * K))"; |
10751 | 230 |
by (induct_tac "n" 1); |
231 |
by (auto_tac (claset() addIs [real_add_le_mono], |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
232 |
simpset() addsimps [real_add_mult_distrib, real_of_nat_Suc])); |
10751 | 233 |
qed_spec_mp "sumr_bound"; |
234 |
||
235 |
Goal "(ALL p. 0 <= p & p < n --> (f(p) <= K)) \ |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10784
diff
changeset
|
236 |
\ --> (sumr 0 n f <= (real n * K))"; |
10751 | 237 |
by (induct_tac "n" 1); |
238 |
by (auto_tac (claset() addIs [real_add_le_mono], |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
239 |
simpset() addsimps [real_add_mult_distrib, real_of_nat_Suc])); |
10751 | 240 |
qed_spec_mp "sumr_bound2"; |
241 |
||
242 |
Goal "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f"; |
|
243 |
by (subgoal_tac "k = 0 | 0 < k" 1); |
|
244 |
by (Auto_tac); |
|
245 |
by (induct_tac "n" 1); |
|
246 |
by (auto_tac (claset(),simpset() addsimps [sumr_split_add,add_commute])); |
|
247 |
qed "sumr_group"; |
|
248 |
Addsimps [sumr_group]; |
|
249 |
||
250 |
(*------------------------------------------------------------------- |
|
251 |
Infinite sums |
|
252 |
Theorems follow from properties of limits and sums |
|
253 |
-------------------------------------------------------------------*) |
|
254 |
(*---------------------- |
|
255 |
suminf is the sum |
|
256 |
---------------------*) |
|
257 |
Goalw [sums_def,summable_def] |
|
258 |
"f sums l ==> summable f"; |
|
259 |
by (Blast_tac 1); |
|
260 |
qed "sums_summable"; |
|
261 |
||
262 |
Goalw [summable_def,suminf_def] |
|
263 |
"summable f ==> f sums (suminf f)"; |
|
264 |
by (blast_tac (claset() addIs [someI2]) 1); |
|
265 |
qed "summable_sums"; |
|
266 |
||
267 |
Goalw [summable_def,suminf_def,sums_def] |
|
268 |
"summable f ==> (%n. sumr 0 n f) ----> (suminf f)"; |
|
269 |
by (blast_tac (claset() addIs [someI2]) 1); |
|
270 |
qed "summable_sumr_LIMSEQ_suminf"; |
|
271 |
||
272 |
(*------------------- |
|
273 |
sum is unique |
|
274 |
------------------*) |
|
275 |
Goal "f sums s ==> (s = suminf f)"; |
|
276 |
by (forward_tac [sums_summable RS summable_sums] 1); |
|
277 |
by (auto_tac (claset() addSIs [LIMSEQ_unique], |
|
278 |
simpset() addsimps [sums_def])); |
|
279 |
qed "sums_unique"; |
|
280 |
||
281 |
(* |
|
282 |
Goalw [sums_def,LIMSEQ_def] |
|
283 |
"(ALL m. n <= Suc m --> f(m) = #0) ==> f sums (sumr 0 n f)"; |
|
284 |
by (Step_tac 1); |
|
285 |
by (res_inst_tac [("x","n")] exI 1); |
|
286 |
by (Step_tac 1 THEN forward_tac [le_imp_less_or_eq] 1); |
|
287 |
by (Step_tac 1); |
|
288 |
by (dres_inst_tac [("f","f")] sumr_split_add_minus 1); |
|
289 |
by (ALLGOALS (Asm_simp_tac)); |
|
290 |
by (dtac (conjI RS sumr_interval_const) 1); |
|
291 |
by (Auto_tac); |
|
292 |
qed "series_zero"; |
|
293 |
next one was called series_zero2 |
|
294 |
**********************) |
|
295 |
||
296 |
Goalw [sums_def,LIMSEQ_def] |
|
297 |
"(ALL m. n <= m --> f(m) = #0) ==> f sums (sumr 0 n f)"; |
|
298 |
by (Step_tac 1); |
|
299 |
by (res_inst_tac [("x","n")] exI 1); |
|
300 |
by (Step_tac 1 THEN forward_tac [le_imp_less_or_eq] 1); |
|
301 |
by (Step_tac 1); |
|
302 |
by (dres_inst_tac [("f","f")] sumr_split_add_minus 1); |
|
303 |
by (ALLGOALS (Asm_simp_tac)); |
|
304 |
by (dtac (conjI RS sumr_interval_const2) 1); |
|
305 |
by (Auto_tac); |
|
306 |
qed "series_zero"; |
|
307 |
||
308 |
Goalw [sums_def] "x sums x0 ==> (%n. c * x(n)) sums (c * x0)"; |
|
309 |
by (auto_tac (claset() addSIs [LIMSEQ_mult] addIs [LIMSEQ_const], |
|
310 |
simpset() addsimps [sumr_mult RS sym])); |
|
311 |
qed "sums_mult"; |
|
312 |
||
313 |
Goal "x sums x' ==> (%n. x(n)/c) sums (x'/c)"; |
|
314 |
by (asm_simp_tac (simpset() addsimps [real_divide_def, sums_mult, |
|
315 |
inst "w" "inverse c" real_mult_commute]) 1); |
|
316 |
qed "sums_divide"; |
|
317 |
||
318 |
Goalw [sums_def] "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)"; |
|
319 |
by (auto_tac (claset() addIs [LIMSEQ_diff], |
|
320 |
simpset() addsimps [sumr_diff RS sym])); |
|
321 |
qed "sums_diff"; |
|
322 |
||
323 |
Goal "summable f ==> suminf f * c = suminf(%n. f n * c)"; |
|
324 |
by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums], |
|
325 |
simpset() addsimps [real_mult_commute])); |
|
326 |
qed "suminf_mult"; |
|
327 |
||
328 |
Goal "summable f ==> c * suminf f = suminf(%n. c * f n)"; |
|
329 |
by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums], |
|
330 |
simpset())); |
|
331 |
qed "suminf_mult2"; |
|
332 |
||
333 |
Goal "[| summable f; summable g |] \ |
|
334 |
\ ==> suminf f - suminf g = suminf(%n. f n - g n)"; |
|
335 |
by (auto_tac (claset() addSIs [sums_diff,sums_unique,summable_sums], simpset())); |
|
336 |
qed "suminf_diff"; |
|
337 |
||
338 |
Goalw [sums_def] |
|
339 |
"x sums x0 ==> (%n. - x n) sums - x0"; |
|
340 |
by (auto_tac (claset() addSIs [LIMSEQ_minus], simpset() addsimps [sumr_minus])); |
|
341 |
qed "sums_minus"; |
|
342 |
||
343 |
Goal "[|summable f; 0 < k |] \ |
|
344 |
\ ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)"; |
|
345 |
by (dtac summable_sums 1); |
|
346 |
by (auto_tac (claset(),simpset() addsimps [sums_def,LIMSEQ_def])); |
|
347 |
by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1); |
|
348 |
by (res_inst_tac [("x","no")] exI 1 THEN Step_tac 1); |
|
349 |
by (dres_inst_tac [("x","n*k")] spec 1); |
|
350 |
by (auto_tac (claset() addSDs [not_leE], simpset())); |
|
351 |
by (dres_inst_tac [("j","no")] less_le_trans 1); |
|
352 |
by (Auto_tac); |
|
353 |
qed "sums_group"; |
|
354 |
||
355 |
Goal "[|summable f; ALL d. #0 < (f(n + (2 * d))) + f(n + ((2 * d) + 1))|] \ |
|
356 |
\ ==> sumr 0 n f < suminf f"; |
|
357 |
by (dtac summable_sums 1); |
|
358 |
by (auto_tac (claset(),simpset() addsimps [sums_def,LIMSEQ_def])); |
|
359 |
by (dres_inst_tac [("x","f(n) + f(n + 1)")] spec 1); |
|
360 |
by (Auto_tac); |
|
361 |
by (rtac ccontr 2 THEN dtac real_leI 2); |
|
362 |
by (subgoal_tac "sumr 0 (n + 2) f <= sumr 0 (2 * (Suc no) + n) f" 2); |
|
363 |
by (induct_tac "no" 3 THEN Simp_tac 3); |
|
364 |
by (res_inst_tac [("y","sumr 0 (2*(Suc na)+n) f")] order_trans 3); |
|
365 |
by (assume_tac 3); |
|
366 |
by (dres_inst_tac [("x","Suc na")] spec 3); |
|
367 |
by (dres_inst_tac [("x","0")] spec 1); |
|
368 |
by (Asm_full_simp_tac 1); |
|
369 |
by (asm_full_simp_tac (simpset() addsimps add_ac) 2); |
|
370 |
by (rotate_tac 1 1 THEN dres_inst_tac [("x","2 * (Suc no) + n")] spec 1); |
|
371 |
by (Step_tac 1 THEN Asm_full_simp_tac 1); |
|
372 |
by (subgoal_tac "suminf f + (f(n) + f(n + 1)) <= \ |
|
373 |
\ sumr 0 (2 * (Suc no) + n) f" 1); |
|
374 |
by (res_inst_tac [("y","sumr 0 (n+2) f")] order_trans 2); |
|
375 |
by (assume_tac 3); |
|
376 |
by (res_inst_tac [("y","sumr 0 n f + (f(n) + f(n + 1))")] order_trans 2); |
|
377 |
by (REPEAT(Asm_simp_tac 2)); |
|
378 |
by (subgoal_tac "suminf f <= sumr 0 (2 * (Suc no) + n) f" 1); |
|
379 |
by (res_inst_tac [("y","suminf f + (f(n) + f(n + 1))")] order_trans 2); |
|
380 |
by (assume_tac 3); |
|
381 |
by (dres_inst_tac [("x","0")] spec 2); |
|
382 |
by (Asm_full_simp_tac 2); |
|
383 |
by (subgoal_tac "#0 <= sumr 0 (2 * Suc no + n) f + - suminf f" 1); |
|
384 |
by (dtac (rename_numerals abs_eqI1) 1 ); |
|
385 |
by (Asm_full_simp_tac 1); |
|
386 |
by (auto_tac (claset(),simpset() addsimps [real_le_def])); |
|
387 |
qed "sumr_pos_lt_pair"; |
|
388 |
||
389 |
(*----------------------------------------------------------------- |
|
390 |
Summable series of positive terms has limit >= any partial sum |
|
391 |
----------------------------------------------------------------*) |
|
392 |
Goal |
|
393 |
"[| summable f; ALL m. n <= m --> #0 <= f(m) |] \ |
|
394 |
\ ==> sumr 0 n f <= suminf f"; |
|
395 |
by (dtac summable_sums 1); |
|
396 |
by (rewtac sums_def); |
|
397 |
by (cut_inst_tac [("k","sumr 0 n f")] LIMSEQ_const 1); |
|
398 |
by (etac LIMSEQ_le 1 THEN Step_tac 1); |
|
399 |
by (res_inst_tac [("x","n")] exI 1 THEN Step_tac 1); |
|
400 |
by (dtac le_imp_less_or_eq 1 THEN Step_tac 1); |
|
401 |
by (auto_tac (claset() addIs [sumr_le], simpset())); |
|
402 |
qed "series_pos_le"; |
|
403 |
||
404 |
Goal "[| summable f; ALL m. n <= m --> #0 < f(m) |] \ |
|
405 |
\ ==> sumr 0 n f < suminf f"; |
|
406 |
by (res_inst_tac [("y","sumr 0 (Suc n) f")] order_less_le_trans 1); |
|
407 |
by (rtac series_pos_le 2); |
|
408 |
by (Auto_tac); |
|
409 |
by (dres_inst_tac [("x","m")] spec 1); |
|
410 |
by (Auto_tac); |
|
411 |
qed "series_pos_less"; |
|
412 |
||
413 |
(*------------------------------------------------------------------- |
|
414 |
sum of geometric progression |
|
415 |
-------------------------------------------------------------------*) |
|
416 |
||
417 |
Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) / (x - #1)"; |
|
418 |
by (induct_tac "n" 1); |
|
419 |
by (Auto_tac); |
|
420 |
by (res_inst_tac [("c1","x - #1")] (real_mult_right_cancel RS iffD1) 1); |
|
421 |
by (auto_tac (claset(), |
|
422 |
simpset() addsimps [real_mult_assoc, real_add_mult_distrib])); |
|
423 |
by (auto_tac (claset(), |
|
424 |
simpset() addsimps [real_add_mult_distrib2, |
|
425 |
real_diff_def, real_mult_commute])); |
|
426 |
qed "sumr_geometric"; |
|
427 |
||
428 |
Goal "abs(x) < #1 ==> (%n. x ^ n) sums (#1/(#1 - x))"; |
|
429 |
by (case_tac "x = #1" 1); |
|
430 |
by (auto_tac (claset() addSDs [LIMSEQ_rabs_realpow_zero2], |
|
431 |
simpset() addsimps [sumr_geometric ,sums_def, |
|
432 |
real_diff_def, real_add_divide_distrib])); |
|
433 |
by (subgoal_tac "#1 / (#1 + - x) = #0/(x-#1) + - #1/(x-#1)" 1); |
|
434 |
by (asm_full_simp_tac (simpset() addsimps [real_divide_eq_cancel1, |
|
435 |
real_divide_minus_eq RS sym, real_diff_def]) 2); |
|
436 |
by (etac ssubst 1); |
|
437 |
by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_divide 1); |
|
438 |
by (auto_tac (claset() addIs [LIMSEQ_const], |
|
439 |
simpset() addsimps [real_diff_def, LIMSEQ_rabs_realpow_zero2])); |
|
440 |
qed "geometric_sums"; |
|
441 |
||
442 |
(*------------------------------------------------------------------- |
|
443 |
Cauchy-type criterion for convergence of series (c.f. Harrison) |
|
444 |
-------------------------------------------------------------------*) |
|
445 |
Goalw [summable_def,sums_def,convergent_def] |
|
446 |
"summable f = convergent (%n. sumr 0 n f)"; |
|
447 |
by (Auto_tac); |
|
448 |
qed "summable_convergent_sumr_iff"; |
|
449 |
||
450 |
Goal "summable f = \ |
|
451 |
\ (ALL e. #0 < e --> (EX N. ALL m n. N <= m --> abs(sumr m n f) < e))"; |
|
452 |
by (auto_tac (claset(),simpset() addsimps [summable_convergent_sumr_iff, |
|
453 |
Cauchy_convergent_iff RS sym,Cauchy_def])); |
|
454 |
by (ALLGOALS(dtac spec) THEN Auto_tac); |
|
455 |
by (res_inst_tac [("x","M")] exI 1); |
|
456 |
by (res_inst_tac [("x","N")] exI 2); |
|
457 |
by (Auto_tac); |
|
458 |
by (ALLGOALS(cut_inst_tac [("m","m"),("n","n")] less_linear)); |
|
459 |
by (Auto_tac); |
|
460 |
by (ftac (le_less_trans RS less_imp_le) 1 THEN assume_tac 1); |
|
461 |
by (dres_inst_tac [("x","n")] spec 1); |
|
462 |
by (dres_inst_tac [("x","m")] spec 1); |
|
463 |
by (auto_tac (claset() addIs [(abs_minus_add_cancel RS subst)], |
|
464 |
simpset() addsimps [sumr_split_add_minus,abs_minus_add_cancel])); |
|
465 |
qed "summable_Cauchy"; |
|
466 |
||
467 |
(*------------------------------------------------------------------- |
|
468 |
Terms of a convergent series tend to zero |
|
469 |
> Goalw [LIMSEQ_def] "summable f ==> f ----> #0"; |
|
470 |
Proved easily in HSeries after proving nonstandard case. |
|
471 |
-------------------------------------------------------------------*) |
|
472 |
(*------------------------------------------------------------------- |
|
473 |
Comparison test |
|
474 |
-------------------------------------------------------------------*) |
|
475 |
Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \ |
|
476 |
\ summable g \ |
|
477 |
\ |] ==> summable f"; |
|
478 |
by (auto_tac (claset(),simpset() addsimps [summable_Cauchy])); |
|
479 |
by (dtac spec 1 THEN Auto_tac); |
|
480 |
by (res_inst_tac [("x","N + Na")] exI 1 THEN Auto_tac); |
|
481 |
by (rotate_tac 2 1); |
|
482 |
by (dres_inst_tac [("x","m")] spec 1); |
|
483 |
by (Auto_tac THEN rotate_tac 2 1 THEN dres_inst_tac [("x","n")] spec 1); |
|
484 |
by (res_inst_tac [("y","sumr m n (%k. abs(f k))")] order_le_less_trans 1); |
|
485 |
by (rtac sumr_rabs 1); |
|
486 |
by (res_inst_tac [("y","sumr m n g")] order_le_less_trans 1); |
|
487 |
by (auto_tac (claset() addIs [sumr_le2], |
|
488 |
simpset() addsimps [abs_interval_iff])); |
|
489 |
qed "summable_comparison_test"; |
|
490 |
||
491 |
Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \ |
|
492 |
\ summable g \ |
|
493 |
\ |] ==> summable (%k. abs (f k))"; |
|
494 |
by (rtac summable_comparison_test 1); |
|
495 |
by (auto_tac (claset(),simpset() addsimps [abs_idempotent])); |
|
496 |
qed "summable_rabs_comparison_test"; |
|
497 |
||
498 |
(*------------------------------------------------------------------*) |
|
499 |
(* Limit comparison property for series (c.f. jrh) *) |
|
500 |
(*------------------------------------------------------------------*) |
|
501 |
Goal "[|ALL n. f n <= g n; summable f; summable g |] \ |
|
502 |
\ ==> suminf f <= suminf g"; |
|
503 |
by (REPEAT(dtac summable_sums 1)); |
|
504 |
by (auto_tac (claset() addSIs [LIMSEQ_le], simpset() addsimps [sums_def])); |
|
505 |
by (rtac exI 1); |
|
506 |
by (auto_tac (claset() addSIs [sumr_le2], simpset())); |
|
507 |
qed "summable_le"; |
|
508 |
||
509 |
Goal "[|ALL n. abs(f n) <= g n; summable g |] \ |
|
510 |
\ ==> summable f & suminf f <= suminf g"; |
|
511 |
by (auto_tac (claset() addIs [summable_comparison_test] |
|
512 |
addSIs [summable_le], simpset())); |
|
513 |
by (auto_tac (claset(),simpset() addsimps [abs_le_interval_iff])); |
|
514 |
qed "summable_le2"; |
|
515 |
||
516 |
(*------------------------------------------------------------------- |
|
517 |
Absolute convergence imples normal convergence |
|
518 |
-------------------------------------------------------------------*) |
|
519 |
Goal "summable (%n. abs (f n)) ==> summable f"; |
|
520 |
by (auto_tac (claset(),simpset() addsimps [sumr_rabs,summable_Cauchy])); |
|
521 |
by (dtac spec 1 THEN Auto_tac); |
|
522 |
by (res_inst_tac [("x","N")] exI 1 THEN Auto_tac); |
|
523 |
by (dtac spec 1 THEN Auto_tac); |
|
524 |
by (res_inst_tac [("y","sumr m n (%n. abs(f n))")] order_le_less_trans 1); |
|
525 |
by (auto_tac (claset() addIs [sumr_rabs], simpset())); |
|
526 |
qed "summable_rabs_cancel"; |
|
527 |
||
528 |
(*------------------------------------------------------------------- |
|
529 |
Absolute convergence of series |
|
530 |
-------------------------------------------------------------------*) |
|
531 |
Goal "summable (%n. abs (f n)) ==> abs(suminf f) <= suminf (%n. abs(f n))"; |
|
532 |
by (auto_tac (claset() addIs [LIMSEQ_le,LIMSEQ_imp_rabs,summable_rabs_cancel, |
|
533 |
summable_sumr_LIMSEQ_suminf,sumr_rabs], |
|
534 |
simpset())); |
|
535 |
qed "summable_rabs"; |
|
536 |
||
537 |
(*------------------------------------------------------------------- |
|
538 |
The ratio test |
|
539 |
-------------------------------------------------------------------*) |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
540 |
|
10751 | 541 |
Goal "[| c <= #0; abs x <= c * abs y |] ==> x = (#0::real)"; |
542 |
by (dtac order_le_imp_less_or_eq 1); |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
543 |
by Auto_tac; |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
544 |
by (subgoal_tac "#0 <= c * abs y" 1); |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
545 |
by (arith_tac 2); |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
546 |
by (asm_full_simp_tac (simpset() addsimps [real_0_le_mult_iff]) 1); |
10751 | 547 |
qed "rabs_ratiotest_lemma"; |
548 |
||
549 |
(* lemmas *) |
|
550 |
||
551 |
Goal "(k::nat) <= l ==> (EX n. l = k + n)"; |
|
552 |
by (dtac le_imp_less_or_eq 1); |
|
553 |
by (auto_tac (claset() addDs [less_imp_Suc_add], simpset())); |
|
554 |
qed "le_Suc_ex"; |
|
555 |
||
556 |
Goal "((k::nat) <= l) = (EX n. l = k + n)"; |
|
557 |
by (auto_tac (claset(),simpset() addsimps [le_Suc_ex])); |
|
558 |
qed "le_Suc_ex_iff"; |
|
559 |
||
560 |
(*All this trouble just to get #0<c *) |
|
561 |
Goal "[| ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \ |
|
562 |
\ ==> #0 < c | summable f"; |
|
563 |
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); |
|
564 |
by (asm_full_simp_tac (simpset() addsimps [summable_Cauchy]) 1); |
|
565 |
by (Step_tac 1 THEN subgoal_tac "ALL n. N <= n --> f (Suc n) = #0" 1); |
|
566 |
by (blast_tac (claset() addIs [rabs_ratiotest_lemma]) 2); |
|
567 |
by (res_inst_tac [("x","Suc N")] exI 1 THEN Step_tac 1); |
|
568 |
by (dtac Suc_le_imp_diff_ge2 1 THEN Auto_tac); |
|
569 |
qed "ratio_test_lemma2"; |
|
570 |
||
571 |
Goal "[| c < #1; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \ |
|
572 |
\ ==> summable f"; |
|
573 |
by (forward_tac [ratio_test_lemma2] 1); |
|
574 |
by Auto_tac; |
|
575 |
by (res_inst_tac [("g","%n. (abs (f N)/(c ^ N))*c ^ n")] |
|
576 |
summable_comparison_test 1); |
|
577 |
by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1); |
|
578 |
by (dtac (le_Suc_ex_iff RS iffD1) 1); |
|
579 |
by (auto_tac (claset(),simpset() addsimps [realpow_add, |
|
580 |
rename_numerals realpow_not_zero])); |
|
581 |
by (induct_tac "na" 1 THEN Auto_tac); |
|
582 |
by (res_inst_tac [("y","c*abs(f(N + n))")] order_trans 1); |
|
10784 | 583 |
by (auto_tac (claset() addIs [real_mult_le_mono1], |
584 |
simpset() addsimps [summable_def])); |
|
10751 | 585 |
by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 1); |
586 |
by (res_inst_tac [("x","abs(f N) * (#1/(#1 - c)) / (c ^ N)")] exI 1); |
|
587 |
by (rtac sums_divide 1); |
|
588 |
by (rtac sums_mult 1); |
|
589 |
by (auto_tac (claset() addSIs [sums_mult,geometric_sums], |
|
590 |
simpset() addsimps [real_abs_def])); |
|
591 |
qed "ratio_test"; |
|
592 |
||
593 |
||
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
594 |
(*--------------------------------------------------------------------------*) |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
595 |
(* Differentiation of finite sum *) |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
596 |
(*--------------------------------------------------------------------------*) |
10751 | 597 |
|
598 |
Goal "(ALL r. m <= r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) \ |
|
599 |
\ --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)"; |
|
600 |
by (induct_tac "n" 1); |
|
601 |
by (auto_tac (claset() addIs [DERIV_add], simpset())); |
|
602 |
qed "DERIV_sumr"; |