author | berghofe |
Fri, 01 Jul 2005 13:54:12 +0200 | |
changeset 16633 | 208ebc9311f2 |
parent 15561 | 045a07ac35a7 |
child 16733 | 236dfafbeb63 |
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 |
15561 | 14 |
|
15539 | 15 |
declare atLeastLessThan_iff[iff] |
15561 | 16 |
declare setsum_op_ivl_Suc[simp] |
10751 | 17 |
|
18 |
constdefs |
|
15543 | 19 |
sums :: "(nat => real) => real => bool" (infixr "sums" 80) |
15536 | 20 |
"f sums s == (%n. setsum f {0..<n}) ----> s" |
10751 | 21 |
|
14416 | 22 |
summable :: "(nat=>real) => bool" |
23 |
"summable f == (\<exists>s. f sums s)" |
|
24 |
||
25 |
suminf :: "(nat=>real) => real" |
|
15539 | 26 |
"suminf f == SOME s. f sums s" |
14416 | 27 |
|
15546 | 28 |
syntax |
29 |
"_suminf" :: "idt => real => real" ("\<Sum>_. _" [0, 10] 10) |
|
30 |
translations |
|
31 |
"\<Sum>i. b" == "suminf (%i. b)" |
|
32 |
||
14416 | 33 |
|
15539 | 34 |
lemma sumr_diff_mult_const: |
35 |
"setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}" |
|
15536 | 36 |
by (simp add: diff_minus setsum_addf real_of_nat_def) |
37 |
||
15542 | 38 |
lemma real_setsum_nat_ivl_bounded: |
39 |
"(!!p. p < n \<Longrightarrow> f(p) \<le> K) |
|
40 |
\<Longrightarrow> setsum f {0..<n::nat} \<le> real n * K" |
|
41 |
using setsum_bounded[where A = "{0..<n}"] |
|
42 |
by (auto simp:real_of_nat_def) |
|
14416 | 43 |
|
15539 | 44 |
(* Generalize from real to some algebraic structure? *) |
45 |
lemma sumr_minus_one_realpow_zero [simp]: |
|
15543 | 46 |
"(\<Sum>i=0..<2*n. (-1) ^ Suc i) = (0::real)" |
15251 | 47 |
by (induct "n", auto) |
14416 | 48 |
|
15539 | 49 |
(* FIXME this is an awful lemma! *) |
50 |
lemma sumr_one_lb_realpow_zero [simp]: |
|
51 |
"(\<Sum>n=Suc 0..<n. f(n) * (0::real) ^ n) = 0" |
|
15251 | 52 |
apply (induct "n") |
14416 | 53 |
apply (case_tac [2] "n", auto) |
54 |
done |
|
55 |
||
15543 | 56 |
lemma sumr_group: |
15539 | 57 |
"(\<Sum>m=0..<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {0 ..< n * k}" |
15543 | 58 |
apply (subgoal_tac "k = 0 | 0 < k", auto) |
15251 | 59 |
apply (induct "n") |
15539 | 60 |
apply (simp_all add: setsum_add_nat_ivl add_commute) |
14416 | 61 |
done |
15539 | 62 |
|
14416 | 63 |
|
64 |
subsection{* Infinite Sums, by the Properties of Limits*} |
|
65 |
||
66 |
(*---------------------- |
|
67 |
suminf is the sum |
|
68 |
---------------------*) |
|
69 |
lemma sums_summable: "f sums l ==> summable f" |
|
70 |
by (simp add: sums_def summable_def, blast) |
|
71 |
||
72 |
lemma summable_sums: "summable f ==> f sums (suminf f)" |
|
73 |
apply (simp add: summable_def suminf_def) |
|
74 |
apply (blast intro: someI2) |
|
75 |
done |
|
76 |
||
77 |
lemma summable_sumr_LIMSEQ_suminf: |
|
15539 | 78 |
"summable f ==> (%n. setsum f {0..<n}) ----> (suminf f)" |
14416 | 79 |
apply (simp add: summable_def suminf_def sums_def) |
80 |
apply (blast intro: someI2) |
|
81 |
done |
|
82 |
||
83 |
(*------------------- |
|
84 |
sum is unique |
|
85 |
------------------*) |
|
86 |
lemma sums_unique: "f sums s ==> (s = suminf f)" |
|
87 |
apply (frule sums_summable [THEN summable_sums]) |
|
88 |
apply (auto intro!: LIMSEQ_unique simp add: sums_def) |
|
89 |
done |
|
90 |
||
91 |
lemma series_zero: |
|
15539 | 92 |
"(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})" |
15537 | 93 |
apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe) |
14416 | 94 |
apply (rule_tac x = n in exI) |
15542 | 95 |
apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong) |
14416 | 96 |
done |
97 |
||
15539 | 98 |
|
14416 | 99 |
lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)" |
15536 | 100 |
by (auto simp add: sums_def setsum_mult [symmetric] |
14416 | 101 |
intro!: LIMSEQ_mult intro: LIMSEQ_const) |
102 |
||
103 |
lemma sums_divide: "x sums x' ==> (%n. x(n)/c) sums (x'/c)" |
|
104 |
by (simp add: real_divide_def sums_mult mult_commute [of _ "inverse c"]) |
|
105 |
||
106 |
lemma sums_diff: "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)" |
|
15536 | 107 |
by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff) |
14416 | 108 |
|
15546 | 109 |
lemma suminf_mult: "summable f ==> suminf f * c = (\<Sum>n. f n * c)" |
14416 | 110 |
by (auto intro!: sums_unique sums_mult summable_sums simp add: mult_commute) |
111 |
||
15546 | 112 |
lemma suminf_mult2: "summable f ==> c * suminf f = (\<Sum>n. c * f n)" |
14416 | 113 |
by (auto intro!: sums_unique sums_mult summable_sums) |
114 |
||
115 |
lemma suminf_diff: |
|
116 |
"[| summable f; summable g |] |
|
15546 | 117 |
==> suminf f - suminf g = (\<Sum>n. f n - g n)" |
14416 | 118 |
by (auto intro!: sums_diff sums_unique summable_sums) |
119 |
||
120 |
lemma sums_minus: "x sums x0 ==> (%n. - x n) sums - x0" |
|
15536 | 121 |
by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf) |
14416 | 122 |
|
123 |
lemma sums_group: |
|
15539 | 124 |
"[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)" |
14416 | 125 |
apply (drule summable_sums) |
15543 | 126 |
apply (auto simp add: sums_def LIMSEQ_def sumr_group) |
14416 | 127 |
apply (drule_tac x = r in spec, safe) |
128 |
apply (rule_tac x = no in exI, safe) |
|
129 |
apply (drule_tac x = "n*k" in spec) |
|
130 |
apply (auto dest!: not_leE) |
|
131 |
apply (drule_tac j = no in less_le_trans, auto) |
|
132 |
done |
|
133 |
||
134 |
lemma sumr_pos_lt_pair_lemma: |
|
15539 | 135 |
"[|\<forall>d. - f (n + (d + d)) < (f (Suc (n + (d + d))) :: real) |] |
136 |
==> setsum f {0..<n+Suc(Suc 0)} \<le> setsum f {0..<Suc(Suc 0) * Suc no + n}" |
|
15251 | 137 |
apply (induct "no", auto) |
138 |
apply (drule_tac x = "Suc no" in spec) |
|
15539 | 139 |
apply (simp add: add_ac) |
14416 | 140 |
done |
10751 | 141 |
|
142 |
||
14416 | 143 |
lemma sumr_pos_lt_pair: |
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
144 |
"[|summable f; |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
145 |
\<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|] |
15539 | 146 |
==> setsum f {0..<n} < suminf f" |
14416 | 147 |
apply (drule summable_sums) |
148 |
apply (auto simp add: sums_def LIMSEQ_def) |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
149 |
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
|
150 |
apply (auto iff: real_0_less_add_iff) |
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset
|
151 |
--{*legacy proof: not necessarily better!*} |
14416 | 152 |
apply (rule_tac [2] ccontr, drule_tac [2] linorder_not_less [THEN iffD1]) |
153 |
apply (frule_tac [2] no=no in sumr_pos_lt_pair_lemma) |
|
154 |
apply (drule_tac x = 0 in spec, simp) |
|
155 |
apply (rotate_tac 1, drule_tac x = "Suc (Suc 0) * (Suc no) + n" in spec) |
|
156 |
apply (safe, simp) |
|
15539 | 157 |
apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \<le> |
158 |
setsum f {0 ..< Suc (Suc 0) * (Suc no) + n}") |
|
159 |
apply (rule_tac [2] y = "setsum f {0..<n+ Suc (Suc 0)}" in order_trans) |
|
14416 | 160 |
prefer 3 apply assumption |
15539 | 161 |
apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans) |
14416 | 162 |
apply simp_all |
15539 | 163 |
apply (subgoal_tac "suminf f \<le> setsum f {0..< Suc (Suc 0) * (Suc no) + n}") |
14416 | 164 |
apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans) |
15539 | 165 |
prefer 3 apply simp |
14416 | 166 |
apply (drule_tac [2] x = 0 in spec) |
167 |
prefer 2 apply simp |
|
15539 | 168 |
apply (subgoal_tac "0 \<le> setsum f {0 ..< Suc (Suc 0) * Suc no + n} + - suminf f") |
169 |
apply (simp add: abs_if) |
|
14416 | 170 |
apply (auto simp add: linorder_not_less [symmetric]) |
171 |
done |
|
172 |
||
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset
|
173 |
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
|
174 |
great as any partial sum.*} |
14416 | 175 |
|
176 |
lemma series_pos_le: |
|
15539 | 177 |
"[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> setsum f {0..<n} \<le> suminf f" |
14416 | 178 |
apply (drule summable_sums) |
179 |
apply (simp add: sums_def) |
|
15539 | 180 |
apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const) |
181 |
apply (erule LIMSEQ_le, blast) |
|
182 |
apply (rule_tac x = n in exI, clarify) |
|
183 |
apply (rule setsum_mono2) |
|
184 |
apply auto |
|
14416 | 185 |
done |
186 |
||
187 |
lemma series_pos_less: |
|
15539 | 188 |
"[| summable f; \<forall>m \<ge> n. 0 < f(m) |] ==> setsum f {0..<n} < suminf f" |
189 |
apply (rule_tac y = "setsum f {0..<Suc n}" in order_less_le_trans) |
|
14416 | 190 |
apply (rule_tac [2] series_pos_le, auto) |
191 |
apply (drule_tac x = m in spec, auto) |
|
192 |
done |
|
193 |
||
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset
|
194 |
text{*Sum of a geometric progression.*} |
14416 | 195 |
|
15539 | 196 |
lemma sumr_geometric: |
197 |
"x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = (x ^ n - 1) / (x - 1::real)" |
|
15251 | 198 |
apply (induct "n", auto) |
14416 | 199 |
apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1]) |
15539 | 200 |
apply (auto simp add: mult_assoc left_distrib) |
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
201 |
apply (simp add: right_distrib diff_minus mult_commute) |
14416 | 202 |
done |
203 |
||
204 |
lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))" |
|
205 |
apply (case_tac "x = 1") |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
206 |
apply (auto dest!: LIMSEQ_rabs_realpow_zero2 |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
207 |
simp add: sumr_geometric sums_def diff_minus add_divide_distrib) |
14416 | 208 |
apply (subgoal_tac "1 / (1 + -x) = 0/ (x - 1) + - 1/ (x - 1) ") |
209 |
apply (erule ssubst) |
|
210 |
apply (rule LIMSEQ_add, rule LIMSEQ_divide) |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
211 |
apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2) |
14416 | 212 |
done |
213 |
||
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset
|
214 |
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
|
215 |
|
15539 | 216 |
lemma summable_convergent_sumr_iff: |
217 |
"summable f = convergent (%n. setsum f {0..<n})" |
|
14416 | 218 |
by (simp add: summable_def sums_def convergent_def) |
219 |
||
220 |
lemma summable_Cauchy: |
|
221 |
"summable f = |
|
15539 | 222 |
(\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(setsum f {m..<n}) < e)" |
15537 | 223 |
apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus[symmetric]) |
15539 | 224 |
apply (drule_tac [!] spec, auto) |
14416 | 225 |
apply (rule_tac x = M in exI) |
226 |
apply (rule_tac [2] x = N in exI, auto) |
|
227 |
apply (cut_tac [!] m = m and n = n in less_linear, auto) |
|
228 |
apply (frule le_less_trans [THEN less_imp_le], assumption) |
|
15360 | 229 |
apply (drule_tac x = n in spec, simp) |
14416 | 230 |
apply (drule_tac x = m in spec) |
15539 | 231 |
apply(simp add: setsum_diff[symmetric]) |
15537 | 232 |
apply(subst abs_minus_commute) |
15539 | 233 |
apply(simp add: setsum_diff[symmetric]) |
234 |
apply(simp add: setsum_diff[symmetric]) |
|
14416 | 235 |
done |
236 |
||
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset
|
237 |
text{*Comparison test*} |
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset
|
238 |
|
14416 | 239 |
lemma summable_comparison_test: |
15360 | 240 |
"[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] ==> summable f" |
14416 | 241 |
apply (auto simp add: summable_Cauchy) |
242 |
apply (drule spec, auto) |
|
243 |
apply (rule_tac x = "N + Na" in exI, auto) |
|
244 |
apply (rotate_tac 2) |
|
245 |
apply (drule_tac x = m in spec) |
|
246 |
apply (auto, rotate_tac 2, drule_tac x = n in spec) |
|
15539 | 247 |
apply (rule_tac y = "\<Sum>k=m..<n. abs(f k)" in order_le_less_trans) |
15536 | 248 |
apply (rule setsum_abs) |
15539 | 249 |
apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans) |
250 |
apply (auto intro: setsum_mono simp add: abs_interval_iff) |
|
14416 | 251 |
done |
252 |
||
253 |
lemma summable_rabs_comparison_test: |
|
15360 | 254 |
"[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] |
14416 | 255 |
==> summable (%k. abs (f k))" |
256 |
apply (rule summable_comparison_test) |
|
15543 | 257 |
apply (auto) |
14416 | 258 |
done |
259 |
||
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset
|
260 |
text{*Limit comparison property for series (c.f. jrh)*} |
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset
|
261 |
|
14416 | 262 |
lemma summable_le: |
263 |
"[|\<forall>n. f n \<le> g n; summable f; summable g |] ==> suminf f \<le> suminf g" |
|
264 |
apply (drule summable_sums)+ |
|
265 |
apply (auto intro!: LIMSEQ_le simp add: sums_def) |
|
266 |
apply (rule exI) |
|
15539 | 267 |
apply (auto intro!: setsum_mono) |
14416 | 268 |
done |
269 |
||
270 |
lemma summable_le2: |
|
271 |
"[|\<forall>n. abs(f n) \<le> g n; summable g |] |
|
272 |
==> summable f & suminf f \<le> suminf g" |
|
273 |
apply (auto intro: summable_comparison_test intro!: summable_le) |
|
274 |
apply (simp add: abs_le_interval_iff) |
|
275 |
done |
|
276 |
||
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset
|
277 |
text{*Absolute convergence imples normal convergence*} |
14416 | 278 |
lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f" |
15536 | 279 |
apply (auto simp add: summable_Cauchy) |
14416 | 280 |
apply (drule spec, auto) |
281 |
apply (rule_tac x = N in exI, auto) |
|
282 |
apply (drule spec, auto) |
|
15539 | 283 |
apply (rule_tac y = "\<Sum>n=m..<n. abs(f n)" in order_le_less_trans) |
15536 | 284 |
apply (auto) |
14416 | 285 |
done |
286 |
||
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset
|
287 |
text{*Absolute convergence of series*} |
14416 | 288 |
lemma summable_rabs: |
15546 | 289 |
"summable (%n. abs (f n)) ==> abs(suminf f) \<le> (\<Sum>n. abs(f n))" |
15536 | 290 |
by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf) |
14416 | 291 |
|
292 |
||
293 |
subsection{* The Ratio Test*} |
|
294 |
||
295 |
lemma rabs_ratiotest_lemma: "[| c \<le> 0; abs x \<le> c * abs y |] ==> x = (0::real)" |
|
296 |
apply (drule order_le_imp_less_or_eq, auto) |
|
297 |
apply (subgoal_tac "0 \<le> c * abs y") |
|
298 |
apply (simp add: zero_le_mult_iff, arith) |
|
299 |
done |
|
300 |
||
301 |
lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)" |
|
302 |
apply (drule le_imp_less_or_eq) |
|
303 |
apply (auto dest: less_imp_Suc_add) |
|
304 |
done |
|
305 |
||
306 |
lemma le_Suc_ex_iff: "((k::nat) \<le> l) = (\<exists>n. l = k + n)" |
|
307 |
by (auto simp add: le_Suc_ex) |
|
308 |
||
309 |
(*All this trouble just to get 0<c *) |
|
310 |
lemma ratio_test_lemma2: |
|
15360 | 311 |
"[| \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |] |
14416 | 312 |
==> 0 < c | summable f" |
313 |
apply (simp (no_asm) add: linorder_not_le [symmetric]) |
|
314 |
apply (simp add: summable_Cauchy) |
|
15543 | 315 |
apply (safe, subgoal_tac "\<forall>n. N < n --> f (n) = 0") |
316 |
prefer 2 |
|
317 |
apply clarify |
|
318 |
apply(erule_tac x = "n - 1" in allE) |
|
319 |
apply (simp add:diff_Suc split:nat.splits) |
|
320 |
apply (blast intro: rabs_ratiotest_lemma) |
|
14416 | 321 |
apply (rule_tac x = "Suc N" in exI, clarify) |
15543 | 322 |
apply(simp cong:setsum_ivl_cong) |
14416 | 323 |
done |
324 |
||
325 |
lemma ratio_test: |
|
15360 | 326 |
"[| c < 1; \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |] |
14416 | 327 |
==> summable f" |
328 |
apply (frule ratio_test_lemma2, auto) |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
329 |
apply (rule_tac g = "%n. (abs (f N) / (c ^ N))*c ^ n" |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
330 |
in summable_comparison_test) |
14416 | 331 |
apply (rule_tac x = N in exI, safe) |
332 |
apply (drule le_Suc_ex_iff [THEN iffD1]) |
|
333 |
apply (auto simp add: power_add realpow_not_zero) |
|
15539 | 334 |
apply (induct_tac "na", auto) |
14416 | 335 |
apply (rule_tac y = "c*abs (f (N + n))" in order_trans) |
336 |
apply (auto intro: mult_right_mono simp add: summable_def) |
|
337 |
apply (simp add: mult_ac) |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
338 |
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
|
339 |
apply (rule sums_divide) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
340 |
apply (rule sums_mult) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset
|
341 |
apply (auto intro!: geometric_sums) |
14416 | 342 |
done |
343 |
||
344 |
||
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset
|
345 |
text{*Differentiation of finite sum*} |
14416 | 346 |
|
347 |
lemma DERIV_sumr [rule_format (no_asm)]: |
|
348 |
"(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) |
|
15539 | 349 |
--> DERIV (%x. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)" |
15251 | 350 |
apply (induct "n") |
14416 | 351 |
apply (auto intro: DERIV_add) |
352 |
done |
|
353 |
||
354 |
ML |
|
355 |
{* |
|
356 |
val sums_def = thm"sums_def"; |
|
357 |
val summable_def = thm"summable_def"; |
|
358 |
val suminf_def = thm"suminf_def"; |
|
359 |
||
360 |
val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero"; |
|
361 |
val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero"; |
|
362 |
val sumr_group = thm "sumr_group"; |
|
363 |
val sums_summable = thm "sums_summable"; |
|
364 |
val summable_sums = thm "summable_sums"; |
|
365 |
val summable_sumr_LIMSEQ_suminf = thm "summable_sumr_LIMSEQ_suminf"; |
|
366 |
val sums_unique = thm "sums_unique"; |
|
367 |
val series_zero = thm "series_zero"; |
|
368 |
val sums_mult = thm "sums_mult"; |
|
369 |
val sums_divide = thm "sums_divide"; |
|
370 |
val sums_diff = thm "sums_diff"; |
|
371 |
val suminf_mult = thm "suminf_mult"; |
|
372 |
val suminf_mult2 = thm "suminf_mult2"; |
|
373 |
val suminf_diff = thm "suminf_diff"; |
|
374 |
val sums_minus = thm "sums_minus"; |
|
375 |
val sums_group = thm "sums_group"; |
|
376 |
val sumr_pos_lt_pair_lemma = thm "sumr_pos_lt_pair_lemma"; |
|
377 |
val sumr_pos_lt_pair = thm "sumr_pos_lt_pair"; |
|
378 |
val series_pos_le = thm "series_pos_le"; |
|
379 |
val series_pos_less = thm "series_pos_less"; |
|
380 |
val sumr_geometric = thm "sumr_geometric"; |
|
381 |
val geometric_sums = thm "geometric_sums"; |
|
382 |
val summable_convergent_sumr_iff = thm "summable_convergent_sumr_iff"; |
|
383 |
val summable_Cauchy = thm "summable_Cauchy"; |
|
384 |
val summable_comparison_test = thm "summable_comparison_test"; |
|
385 |
val summable_rabs_comparison_test = thm "summable_rabs_comparison_test"; |
|
386 |
val summable_le = thm "summable_le"; |
|
387 |
val summable_le2 = thm "summable_le2"; |
|
388 |
val summable_rabs_cancel = thm "summable_rabs_cancel"; |
|
389 |
val summable_rabs = thm "summable_rabs"; |
|
390 |
val rabs_ratiotest_lemma = thm "rabs_ratiotest_lemma"; |
|
391 |
val le_Suc_ex = thm "le_Suc_ex"; |
|
392 |
val le_Suc_ex_iff = thm "le_Suc_ex_iff"; |
|
393 |
val ratio_test_lemma2 = thm "ratio_test_lemma2"; |
|
394 |
val ratio_test = thm "ratio_test"; |
|
395 |
val DERIV_sumr = thm "DERIV_sumr"; |
|
396 |
*} |
|
397 |
||
398 |
end |