src/HOL/Hyperreal/Series.thy
author kleing
Sun Feb 19 13:21:32 2006 +0100 (2006-02-19)
changeset 19106 6e6b5b1fdc06
parent 17149 e2b19c92ef51
child 19279 48b527d0331b
permissions -rw-r--r--
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
* added Complex/ex/ASeries_Complex (instantiation of the above for reals)
* added Complex/ex/HarmonicSeries (should really be in something like Complex/Library)

(these are contributions by Benjamin Porter, numbers 68 and 34 of
http://www.cs.ru.nl/~freek/100/)
     1 (*  Title       : Series.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4 
     5 Converted to Isar and polished by lcp
     6 Converted to setsum and polished yet more by TNN
     7 Additional contributions by Jeremy Avigad
     8 *) 
     9 
    10 header{*Finite Summation and Infinite Series*}
    11 
    12 theory Series
    13 imports SEQ Lim
    14 begin
    15 
    16 declare atLeastLessThan_iff[iff]
    17 declare setsum_op_ivl_Suc[simp]
    18 
    19 constdefs
    20    sums  :: "(nat => real) => real => bool"     (infixr "sums" 80)
    21    "f sums s  == (%n. setsum f {0..<n}) ----> s"
    22 
    23    summable :: "(nat=>real) => bool"
    24    "summable f == (\<exists>s. f sums s)"
    25 
    26    suminf   :: "(nat=>real) => real"
    27    "suminf f == SOME s. f sums s"
    28 
    29 syntax
    30   "_suminf" :: "idt => real => real"    ("\<Sum>_. _" [0, 10] 10)
    31 translations
    32   "\<Sum>i. b" == "suminf (%i. b)"
    33 
    34 
    35 lemma sumr_diff_mult_const:
    36  "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
    37 by (simp add: diff_minus setsum_addf real_of_nat_def)
    38 
    39 lemma real_setsum_nat_ivl_bounded:
    40      "(!!p. p < n \<Longrightarrow> f(p) \<le> K)
    41       \<Longrightarrow> setsum f {0..<n::nat} \<le> real n * K"
    42 using setsum_bounded[where A = "{0..<n}"]
    43 by (auto simp:real_of_nat_def)
    44 
    45 (* Generalize from real to some algebraic structure? *)
    46 lemma sumr_minus_one_realpow_zero [simp]:
    47   "(\<Sum>i=0..<2*n. (-1) ^ Suc i) = (0::real)"
    48 by (induct "n", auto)
    49 
    50 (* FIXME this is an awful lemma! *)
    51 lemma sumr_one_lb_realpow_zero [simp]:
    52   "(\<Sum>n=Suc 0..<n. f(n) * (0::real) ^ n) = 0"
    53 apply (induct "n")
    54 apply (case_tac [2] "n", auto)
    55 done
    56 
    57 lemma sumr_group:
    58      "(\<Sum>m=0..<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {0 ..< n * k}"
    59 apply (subgoal_tac "k = 0 | 0 < k", auto)
    60 apply (induct "n")
    61 apply (simp_all add: setsum_add_nat_ivl add_commute)
    62 done
    63 
    64 (* FIXME generalize? *)
    65 lemma sumr_offset:
    66  "(\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
    67 by (induct "n", auto)
    68 
    69 lemma sumr_offset2:
    70  "\<forall>f. (\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
    71 by (induct "n", auto)
    72 
    73 lemma sumr_offset3:
    74   "setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
    75 by (simp  add: sumr_offset)
    76 
    77 lemma sumr_offset4:
    78  "\<forall>n f. setsum f {0::nat..<n+k} =
    79         (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
    80 by (simp add: sumr_offset)
    81 
    82 (*
    83 lemma sumr_from_1_from_0: "0 < n ==>
    84       (\<Sum>n=Suc 0 ..< Suc n. if even(n) then 0 else
    85              ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n =
    86       (\<Sum>n=0..<Suc n. if even(n) then 0 else
    87              ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n"
    88 by (rule_tac n1 = 1 in sumr_split_add [THEN subst], auto)
    89 *)
    90 
    91 subsection{* Infinite Sums, by the Properties of Limits*}
    92 
    93 (*----------------------
    94    suminf is the sum   
    95  ---------------------*)
    96 lemma sums_summable: "f sums l ==> summable f"
    97 by (simp add: sums_def summable_def, blast)
    98 
    99 lemma summable_sums: "summable f ==> f sums (suminf f)"
   100 apply (simp add: summable_def suminf_def)
   101 apply (blast intro: someI2)
   102 done
   103 
   104 lemma summable_sumr_LIMSEQ_suminf: 
   105      "summable f ==> (%n. setsum f {0..<n}) ----> (suminf f)"
   106 apply (simp add: summable_def suminf_def sums_def)
   107 apply (blast intro: someI2)
   108 done
   109 
   110 (*-------------------
   111     sum is unique                    
   112  ------------------*)
   113 lemma sums_unique: "f sums s ==> (s = suminf f)"
   114 apply (frule sums_summable [THEN summable_sums])
   115 apply (auto intro!: LIMSEQ_unique simp add: sums_def)
   116 done
   117 
   118 lemma sums_split_initial_segment: "f sums s ==> 
   119   (%n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
   120   apply (unfold sums_def);
   121   apply (simp add: sumr_offset); 
   122   apply (rule LIMSEQ_diff_const)
   123   apply (rule LIMSEQ_ignore_initial_segment)
   124   apply assumption
   125 done
   126 
   127 lemma summable_ignore_initial_segment: "summable f ==> 
   128     summable (%n. f(n + k))"
   129   apply (unfold summable_def)
   130   apply (auto intro: sums_split_initial_segment)
   131 done
   132 
   133 lemma suminf_minus_initial_segment: "summable f ==>
   134     suminf f = s ==> suminf (%n. f(n + k)) = s - (SUM i = 0..< k. f i)"
   135   apply (frule summable_ignore_initial_segment)
   136   apply (rule sums_unique [THEN sym])
   137   apply (frule summable_sums)
   138   apply (rule sums_split_initial_segment)
   139   apply auto
   140 done
   141 
   142 lemma suminf_split_initial_segment: "summable f ==> 
   143     suminf f = (SUM i = 0..< k. f i) + suminf (%n. f(n + k))"
   144 by (auto simp add: suminf_minus_initial_segment)
   145 
   146 lemma series_zero: 
   147      "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})"
   148 apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)
   149 apply (rule_tac x = n in exI)
   150 apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong)
   151 done
   152 
   153 lemma sums_zero: "(%n. 0) sums 0";
   154   apply (unfold sums_def);
   155   apply simp;
   156   apply (rule LIMSEQ_const);
   157 done;
   158 
   159 lemma summable_zero: "summable (%n. 0)";
   160   apply (rule sums_summable);
   161   apply (rule sums_zero);
   162 done;
   163 
   164 lemma suminf_zero: "suminf (%n. 0) = 0";
   165   apply (rule sym);
   166   apply (rule sums_unique);
   167   apply (rule sums_zero);
   168 done;
   169   
   170 lemma sums_mult: "f sums a ==> (%n. c * f n) sums (c * a)"
   171 by (auto simp add: sums_def setsum_mult [symmetric]
   172          intro!: LIMSEQ_mult intro: LIMSEQ_const)
   173 
   174 lemma summable_mult: "summable f ==> summable (%n. c * f n)";
   175   apply (unfold summable_def);
   176   apply (auto intro: sums_mult);
   177 done;
   178 
   179 lemma suminf_mult: "summable f ==> suminf (%n. c * f n) = c * suminf f";
   180   apply (rule sym);
   181   apply (rule sums_unique);
   182   apply (rule sums_mult);
   183   apply (erule summable_sums);
   184 done;
   185 
   186 lemma sums_mult2: "f sums a ==> (%n. f n * c) sums (a * c)"
   187 apply (subst mult_commute)
   188 apply (subst mult_commute);back;
   189 apply (erule sums_mult)
   190 done
   191 
   192 lemma summable_mult2: "summable f ==> summable (%n. f n * c)"
   193   apply (unfold summable_def)
   194   apply (auto intro: sums_mult2)
   195 done
   196 
   197 lemma suminf_mult2: "summable f ==> suminf f * c = (\<Sum>n. f n * c)"
   198 by (auto intro!: sums_unique sums_mult summable_sums simp add: mult_commute)
   199 
   200 lemma sums_divide: "f sums a ==> (%n. (f n)/c) sums (a/c)"
   201 by (simp add: real_divide_def sums_mult mult_commute [of _ "inverse c"])
   202 
   203 lemma summable_divide: "summable f ==> summable (%n. (f n) / c)";
   204   apply (unfold summable_def);
   205   apply (auto intro: sums_divide);
   206 done;
   207 
   208 lemma suminf_divide: "summable f ==> suminf (%n. (f n) / c) = (suminf f) / c";
   209   apply (rule sym);
   210   apply (rule sums_unique);
   211   apply (rule sums_divide);
   212   apply (erule summable_sums);
   213 done;
   214 
   215 lemma sums_add: "[| x sums x0; y sums y0 |] ==> (%n. x n + y n) sums (x0+y0)"
   216 by (auto simp add: sums_def setsum_addf intro: LIMSEQ_add)
   217 
   218 lemma summable_add: "summable f ==> summable g ==> summable (%x. f x + g x)";
   219   apply (unfold summable_def);
   220   apply clarify;
   221   apply (rule exI);
   222   apply (erule sums_add);
   223   apply assumption;
   224 done;
   225 
   226 lemma suminf_add:
   227      "[| summable f; summable g |]   
   228       ==> suminf f + suminf g  = (\<Sum>n. f n + g n)"
   229 by (auto intro!: sums_add sums_unique summable_sums)
   230 
   231 lemma sums_diff: "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)"
   232 by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff)
   233 
   234 lemma summable_diff: "summable f ==> summable g ==> summable (%x. f x - g x)";
   235   apply (unfold summable_def);
   236   apply clarify;
   237   apply (rule exI);
   238   apply (erule sums_diff);
   239   apply assumption;
   240 done;
   241 
   242 lemma suminf_diff:
   243      "[| summable f; summable g |]   
   244       ==> suminf f - suminf g  = (\<Sum>n. f n - g n)"
   245 by (auto intro!: sums_diff sums_unique summable_sums)
   246 
   247 lemma sums_minus: "f sums s ==> (%x. - f x) sums (- s)";
   248   by (simp add: sums_def setsum_negf LIMSEQ_minus);
   249 
   250 lemma summable_minus: "summable f ==> summable (%x. - f x)";
   251   by (auto simp add: summable_def intro: sums_minus);
   252 
   253 lemma suminf_minus: "summable f ==> suminf (%x. - f x) = - (suminf f)";
   254   apply (rule sym);
   255   apply (rule sums_unique);
   256   apply (rule sums_minus);
   257   apply (erule summable_sums);
   258 done;
   259 
   260 lemma sums_group:
   261      "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
   262 apply (drule summable_sums)
   263 apply (auto simp add: sums_def LIMSEQ_def sumr_group)
   264 apply (drule_tac x = r in spec, safe)
   265 apply (rule_tac x = no in exI, safe)
   266 apply (drule_tac x = "n*k" in spec)
   267 apply (auto dest!: not_leE)
   268 apply (drule_tac j = no in less_le_trans, auto)
   269 done
   270 
   271 lemma sumr_pos_lt_pair_lemma:
   272   "[|\<forall>d. - f (n + (d + d)) < (f (Suc (n + (d + d))) :: real) |]
   273    ==> setsum f {0..<n+Suc(Suc 0)} \<le> setsum f {0..<Suc(Suc 0) * Suc no + n}"
   274 apply (induct "no", auto)
   275 apply (drule_tac x = "Suc no" in spec)
   276 apply (simp add: add_ac)
   277 (* FIXME why does simp require a separate step to prove the (pure arithmetic)
   278    left-over? With del cong: strong_setsum_cong it works!
   279 *)
   280 apply simp
   281 done
   282 
   283 lemma sumr_pos_lt_pair:
   284      "[|summable f; 
   285         \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|]  
   286       ==> setsum f {0..<n} < suminf f"
   287 apply (drule summable_sums)
   288 apply (auto simp add: sums_def LIMSEQ_def)
   289 apply (drule_tac x = "f (n) + f (n + 1)" in spec)
   290 apply (auto iff: real_0_less_add_iff)
   291    --{*legacy proof: not necessarily better!*}
   292 apply (rule_tac [2] ccontr, drule_tac [2] linorder_not_less [THEN iffD1])
   293 apply (frule_tac [2] no=no in sumr_pos_lt_pair_lemma) 
   294 apply (drule_tac x = 0 in spec, simp)
   295 apply (rotate_tac 1, drule_tac x = "Suc (Suc 0) * (Suc no) + n" in spec)
   296 apply (safe, simp)
   297 apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \<le>
   298  setsum f {0 ..< Suc (Suc 0) * (Suc no) + n}")
   299 apply (rule_tac [2] y = "setsum f {0..<n+ Suc (Suc 0)}" in order_trans)
   300 prefer 3 apply assumption
   301 apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans)
   302 apply simp_all 
   303 apply (subgoal_tac "suminf f \<le> setsum f {0..< Suc (Suc 0) * (Suc no) + n}")
   304 apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans)
   305 prefer 3 apply simp
   306 apply (drule_tac [2] x = 0 in spec)
   307  prefer 2 apply simp 
   308 apply (subgoal_tac "0 \<le> setsum f {0 ..< Suc (Suc 0) * Suc no + n} + - suminf f")
   309 apply (simp add: abs_if)
   310 apply (auto simp add: linorder_not_less [symmetric])
   311 done
   312 
   313 text{*A summable series of positive terms has limit that is at least as
   314 great as any partial sum.*}
   315 
   316 lemma series_pos_le: 
   317      "[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> setsum f {0..<n} \<le> suminf f"
   318 apply (drule summable_sums)
   319 apply (simp add: sums_def)
   320 apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const)
   321 apply (erule LIMSEQ_le, blast)
   322 apply (rule_tac x = n in exI, clarify)
   323 apply (rule setsum_mono2)
   324 apply auto
   325 done
   326 
   327 lemma series_pos_less:
   328      "[| summable f; \<forall>m \<ge> n. 0 < f(m) |] ==> setsum f {0..<n} < suminf f"
   329 apply (rule_tac y = "setsum f {0..<Suc n}" in order_less_le_trans)
   330 apply (rule_tac [2] series_pos_le, auto)
   331 apply (drule_tac x = m in spec, auto)
   332 done
   333 
   334 text{*Sum of a geometric progression.*}
   335 
   336 lemmas sumr_geometric = geometric_sum [where 'a = real]
   337 
   338 lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))"
   339 apply (case_tac "x = 1")
   340 apply (auto dest!: LIMSEQ_rabs_realpow_zero2 
   341         simp add: sumr_geometric sums_def diff_minus add_divide_distrib)
   342 apply (subgoal_tac "1 / (1 + -x) = 0/ (x - 1) + - 1/ (x - 1) ")
   343 apply (erule ssubst)
   344 apply (rule LIMSEQ_add, rule LIMSEQ_divide)
   345 apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2)
   346 done
   347 
   348 text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
   349 
   350 lemma summable_convergent_sumr_iff:
   351  "summable f = convergent (%n. setsum f {0..<n})"
   352 by (simp add: summable_def sums_def convergent_def)
   353 
   354 lemma summable_Cauchy:
   355      "summable f =  
   356       (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(setsum f {m..<n}) < e)"
   357 apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus[symmetric])
   358 apply (drule_tac [!] spec, auto)
   359 apply (rule_tac x = M in exI)
   360 apply (rule_tac [2] x = N in exI, auto)
   361 apply (cut_tac [!] m = m and n = n in less_linear, auto)
   362 apply (frule le_less_trans [THEN less_imp_le], assumption)
   363 apply (drule_tac x = n in spec, simp)
   364 apply (drule_tac x = m in spec)
   365 apply(simp add: setsum_diff[symmetric])
   366 apply(subst abs_minus_commute)
   367 apply(simp add: setsum_diff[symmetric])
   368 apply(simp add: setsum_diff[symmetric])
   369 done
   370 
   371 text{*Comparison test*}
   372 
   373 lemma summable_comparison_test:
   374      "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] ==> summable f"
   375 apply (auto simp add: summable_Cauchy)
   376 apply (drule spec, auto)
   377 apply (rule_tac x = "N + Na" in exI, auto)
   378 apply (rotate_tac 2)
   379 apply (drule_tac x = m in spec)
   380 apply (auto, rotate_tac 2, drule_tac x = n in spec)
   381 apply (rule_tac y = "\<Sum>k=m..<n. abs(f k)" in order_le_less_trans)
   382 apply (rule setsum_abs)
   383 apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans)
   384 apply (auto intro: setsum_mono simp add: abs_interval_iff)
   385 done
   386 
   387 lemma summable_rabs_comparison_test:
   388      "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] 
   389       ==> summable (%k. abs (f k))"
   390 apply (rule summable_comparison_test)
   391 apply (auto)
   392 done
   393 
   394 text{*Limit comparison property for series (c.f. jrh)*}
   395 
   396 lemma summable_le:
   397      "[|\<forall>n. f n \<le> g n; summable f; summable g |] ==> suminf f \<le> suminf g"
   398 apply (drule summable_sums)+
   399 apply (auto intro!: LIMSEQ_le simp add: sums_def)
   400 apply (rule exI)
   401 apply (auto intro!: setsum_mono)
   402 done
   403 
   404 lemma summable_le2:
   405      "[|\<forall>n. abs(f n) \<le> g n; summable g |]  
   406       ==> summable f & suminf f \<le> suminf g"
   407 apply (auto intro: summable_comparison_test intro!: summable_le)
   408 apply (simp add: abs_le_interval_iff)
   409 done
   410 
   411 (* specialisation for the common 0 case *)
   412 lemma suminf_0_le:
   413   fixes f::"nat\<Rightarrow>real"
   414   assumes gt0: "\<forall>n. 0 \<le> f n" and sm: "summable f"
   415   shows "0 \<le> suminf f"
   416 proof -
   417   let ?g = "(\<lambda>n. (0::real))"
   418   from gt0 have "\<forall>n. ?g n \<le> f n" by simp
   419   moreover have "summable ?g" by (rule summable_zero)
   420   moreover from sm have "summable f" .
   421   ultimately have "suminf ?g \<le> suminf f" by (rule summable_le)
   422   then show "0 \<le> suminf f" by (simp add: suminf_zero)
   423 qed 
   424 
   425 
   426 text{*Absolute convergence imples normal convergence*}
   427 lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f"
   428 apply (auto simp add: summable_Cauchy)
   429 apply (drule spec, auto)
   430 apply (rule_tac x = N in exI, auto)
   431 apply (drule spec, auto)
   432 apply (rule_tac y = "\<Sum>n=m..<n. abs(f n)" in order_le_less_trans)
   433 apply (auto)
   434 done
   435 
   436 text{*Absolute convergence of series*}
   437 lemma summable_rabs:
   438      "summable (%n. abs (f n)) ==> abs(suminf f) \<le> (\<Sum>n. abs(f n))"
   439 by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf)
   440 
   441 
   442 subsection{* The Ratio Test*}
   443 
   444 lemma rabs_ratiotest_lemma: "[| c \<le> 0; abs x \<le> c * abs y |] ==> x = (0::real)"
   445 apply (drule order_le_imp_less_or_eq, auto)
   446 apply (subgoal_tac "0 \<le> c * abs y")
   447 apply (simp add: zero_le_mult_iff, arith)
   448 done
   449 
   450 lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)"
   451 apply (drule le_imp_less_or_eq)
   452 apply (auto dest: less_imp_Suc_add)
   453 done
   454 
   455 lemma le_Suc_ex_iff: "((k::nat) \<le> l) = (\<exists>n. l = k + n)"
   456 by (auto simp add: le_Suc_ex)
   457 
   458 (*All this trouble just to get 0<c *)
   459 lemma ratio_test_lemma2:
   460      "[| \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |]  
   461       ==> 0 < c | summable f"
   462 apply (simp (no_asm) add: linorder_not_le [symmetric])
   463 apply (simp add: summable_Cauchy)
   464 apply (safe, subgoal_tac "\<forall>n. N < n --> f (n) = 0")
   465  prefer 2
   466  apply clarify
   467  apply(erule_tac x = "n - 1" in allE)
   468  apply (simp add:diff_Suc split:nat.splits)
   469  apply (blast intro: rabs_ratiotest_lemma)
   470 apply (rule_tac x = "Suc N" in exI, clarify)
   471 apply(simp cong:setsum_ivl_cong)
   472 done
   473 
   474 lemma ratio_test:
   475      "[| c < 1; \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |]  
   476       ==> summable f"
   477 apply (frule ratio_test_lemma2, auto)
   478 apply (rule_tac g = "%n. (abs (f N) / (c ^ N))*c ^ n" 
   479        in summable_comparison_test)
   480 apply (rule_tac x = N in exI, safe)
   481 apply (drule le_Suc_ex_iff [THEN iffD1])
   482 apply (auto simp add: power_add realpow_not_zero)
   483 apply (induct_tac "na", auto)
   484 apply (rule_tac y = "c*abs (f (N + n))" in order_trans)
   485 apply (auto intro: mult_right_mono simp add: summable_def)
   486 apply (simp add: mult_ac)
   487 apply (rule_tac x = "abs (f N) * (1/ (1 - c)) / (c ^ N)" in exI)
   488 apply (rule sums_divide) 
   489 apply (rule sums_mult) 
   490 apply (auto intro!: geometric_sums)
   491 done
   492 
   493 
   494 text{*Differentiation of finite sum*}
   495 
   496 lemma DERIV_sumr [rule_format (no_asm)]:
   497      "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))  
   498       --> DERIV (%x. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)"
   499 apply (induct "n")
   500 apply (auto intro: DERIV_add)
   501 done
   502 
   503 ML
   504 {*
   505 val sums_def = thm"sums_def";
   506 val summable_def = thm"summable_def";
   507 val suminf_def = thm"suminf_def";
   508 
   509 val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
   510 val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero";
   511 val sumr_group = thm "sumr_group";
   512 val sums_summable = thm "sums_summable";
   513 val summable_sums = thm "summable_sums";
   514 val summable_sumr_LIMSEQ_suminf = thm "summable_sumr_LIMSEQ_suminf";
   515 val sums_unique = thm "sums_unique";
   516 val series_zero = thm "series_zero";
   517 val sums_mult = thm "sums_mult";
   518 val sums_divide = thm "sums_divide";
   519 val sums_diff = thm "sums_diff";
   520 val suminf_mult = thm "suminf_mult";
   521 val suminf_mult2 = thm "suminf_mult2";
   522 val suminf_diff = thm "suminf_diff";
   523 val sums_minus = thm "sums_minus";
   524 val sums_group = thm "sums_group";
   525 val sumr_pos_lt_pair_lemma = thm "sumr_pos_lt_pair_lemma";
   526 val sumr_pos_lt_pair = thm "sumr_pos_lt_pair";
   527 val series_pos_le = thm "series_pos_le";
   528 val series_pos_less = thm "series_pos_less";
   529 val sumr_geometric = thm "sumr_geometric";
   530 val geometric_sums = thm "geometric_sums";
   531 val summable_convergent_sumr_iff = thm "summable_convergent_sumr_iff";
   532 val summable_Cauchy = thm "summable_Cauchy";
   533 val summable_comparison_test = thm "summable_comparison_test";
   534 val summable_rabs_comparison_test = thm "summable_rabs_comparison_test";
   535 val summable_le = thm "summable_le";
   536 val summable_le2 = thm "summable_le2";
   537 val summable_rabs_cancel = thm "summable_rabs_cancel";
   538 val summable_rabs = thm "summable_rabs";
   539 val rabs_ratiotest_lemma = thm "rabs_ratiotest_lemma";
   540 val le_Suc_ex = thm "le_Suc_ex";
   541 val le_Suc_ex_iff = thm "le_Suc_ex_iff";
   542 val ratio_test_lemma2 = thm "ratio_test_lemma2";
   543 val ratio_test = thm "ratio_test";
   544 val DERIV_sumr = thm "DERIV_sumr";
   545 *}
   546 
   547 end