src/HOL/Hyperreal/Series.thy
author huffman
Sat Sep 16 02:40:00 2006 +0200 (2006-09-16)
changeset 20552 2c31dd358c21
parent 20432 07ec57376051
child 20688 690d866a165d
permissions -rw-r--r--
generalized types of many constants to work over arbitrary vector spaces;
modified theorems using Rep_star to eliminate existential quantifiers
     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 definition
    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_right_distrib [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 done
   278 
   279 lemma sumr_pos_lt_pair:
   280      "[|summable f; 
   281         \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|]  
   282       ==> setsum f {0..<n} < suminf f"
   283 apply (drule summable_sums)
   284 apply (auto simp add: sums_def LIMSEQ_def)
   285 apply (drule_tac x = "f (n) + f (n + 1)" in spec)
   286 apply (auto iff: real_0_less_add_iff)
   287    --{*legacy proof: not necessarily better!*}
   288 apply (rule_tac [2] ccontr, drule_tac [2] linorder_not_less [THEN iffD1])
   289 apply (frule_tac [2] no=no in sumr_pos_lt_pair_lemma) 
   290 apply (drule_tac x = 0 in spec, simp)
   291 apply (rotate_tac 1, drule_tac x = "Suc (Suc 0) * (Suc no) + n" in spec)
   292 apply (safe, simp)
   293 apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \<le>
   294  setsum f {0 ..< Suc (Suc 0) * (Suc no) + n}")
   295 apply (rule_tac [2] y = "setsum f {0..<n+ Suc (Suc 0)}" in order_trans)
   296 prefer 3 apply assumption
   297 apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans)
   298 apply simp_all
   299 done
   300 
   301 text{*A summable series of positive terms has limit that is at least as
   302 great as any partial sum.*}
   303 
   304 lemma series_pos_le: 
   305      "[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> setsum f {0..<n} \<le> suminf f"
   306 apply (drule summable_sums)
   307 apply (simp add: sums_def)
   308 apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const)
   309 apply (erule LIMSEQ_le, blast)
   310 apply (rule_tac x = n in exI, clarify)
   311 apply (rule setsum_mono2)
   312 apply auto
   313 done
   314 
   315 lemma series_pos_less:
   316      "[| summable f; \<forall>m \<ge> n. 0 < f(m) |] ==> setsum f {0..<n} < suminf f"
   317 apply (rule_tac y = "setsum f {0..<Suc n}" in order_less_le_trans)
   318 apply (rule_tac [2] series_pos_le, auto)
   319 apply (drule_tac x = m in spec, auto)
   320 done
   321 
   322 text{*Sum of a geometric progression.*}
   323 
   324 lemmas sumr_geometric = geometric_sum [where 'a = real]
   325 
   326 lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))"
   327 apply (case_tac "x = 1")
   328 apply (auto dest!: LIMSEQ_rabs_realpow_zero2 
   329         simp add: sumr_geometric sums_def diff_minus add_divide_distrib)
   330 apply (subgoal_tac "1 / (1 + -x) = 0/ (x - 1) + - 1/ (x - 1) ")
   331 apply (erule ssubst)
   332 apply (rule LIMSEQ_add, rule LIMSEQ_divide)
   333 apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2)
   334 done
   335 
   336 text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
   337 
   338 lemma summable_convergent_sumr_iff:
   339  "summable f = convergent (%n. setsum f {0..<n})"
   340 by (simp add: summable_def sums_def convergent_def)
   341 
   342 lemma summable_Cauchy:
   343      "summable f =  
   344       (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(setsum f {m..<n}) < e)"
   345 apply (simp only: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus [symmetric], safe)
   346 apply (drule spec, drule (1) mp)
   347 apply (erule exE, rule_tac x="M" in exI, clarify)
   348 apply (rule_tac x="m" and y="n" in linorder_le_cases)
   349 apply (frule (1) order_trans)
   350 apply (drule_tac x="n" in spec, drule (1) mp)
   351 apply (drule_tac x="m" in spec, drule (1) mp)
   352 apply (simp add: setsum_diff [symmetric])
   353 apply simp
   354 apply (drule spec, drule (1) mp)
   355 apply (erule exE, rule_tac x="N" in exI, clarify)
   356 apply (rule_tac x="m" and y="n" in linorder_le_cases)
   357 apply (subst norm_minus_commute)
   358 apply (simp add: setsum_diff [symmetric])
   359 apply (simp add: setsum_diff [symmetric])
   360 done
   361 
   362 text{*Comparison test*}
   363 
   364 lemma summable_comparison_test:
   365      "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] ==> summable f"
   366 apply (auto simp add: summable_Cauchy)
   367 apply (drule spec, auto)
   368 apply (rule_tac x = "N + Na" in exI, auto)
   369 apply (rotate_tac 2)
   370 apply (drule_tac x = m in spec)
   371 apply (auto, rotate_tac 2, drule_tac x = n in spec)
   372 apply (rule_tac y = "\<Sum>k=m..<n. abs(f k)" in order_le_less_trans)
   373 apply (rule setsum_abs)
   374 apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans)
   375 apply (auto intro: setsum_mono simp add: abs_interval_iff)
   376 done
   377 
   378 lemma summable_rabs_comparison_test:
   379      "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] 
   380       ==> summable (%k. abs (f k))"
   381 apply (rule summable_comparison_test)
   382 apply (auto)
   383 done
   384 
   385 text{*Limit comparison property for series (c.f. jrh)*}
   386 
   387 lemma summable_le:
   388      "[|\<forall>n. f n \<le> g n; summable f; summable g |] ==> suminf f \<le> suminf g"
   389 apply (drule summable_sums)+
   390 apply (auto intro!: LIMSEQ_le simp add: sums_def)
   391 apply (rule exI)
   392 apply (auto intro!: setsum_mono)
   393 done
   394 
   395 lemma summable_le2:
   396      "[|\<forall>n. abs(f n) \<le> g n; summable g |]  
   397       ==> summable f & suminf f \<le> suminf g"
   398 apply (auto intro: summable_comparison_test intro!: summable_le)
   399 apply (simp add: abs_le_interval_iff)
   400 done
   401 
   402 (* specialisation for the common 0 case *)
   403 lemma suminf_0_le:
   404   fixes f::"nat\<Rightarrow>real"
   405   assumes gt0: "\<forall>n. 0 \<le> f n" and sm: "summable f"
   406   shows "0 \<le> suminf f"
   407 proof -
   408   let ?g = "(\<lambda>n. (0::real))"
   409   from gt0 have "\<forall>n. ?g n \<le> f n" by simp
   410   moreover have "summable ?g" by (rule summable_zero)
   411   moreover from sm have "summable f" .
   412   ultimately have "suminf ?g \<le> suminf f" by (rule summable_le)
   413   then show "0 \<le> suminf f" by (simp add: suminf_zero)
   414 qed 
   415 
   416 
   417 text{*Absolute convergence imples normal convergence*}
   418 lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f"
   419 apply (auto simp add: summable_Cauchy)
   420 apply (drule spec, auto)
   421 apply (rule_tac x = N in exI, auto)
   422 apply (drule spec, auto)
   423 apply (rule_tac y = "\<Sum>n=m..<n. abs(f n)" in order_le_less_trans)
   424 apply (auto)
   425 done
   426 
   427 text{*Absolute convergence of series*}
   428 lemma summable_rabs:
   429      "summable (%n. abs (f n)) ==> abs(suminf f) \<le> (\<Sum>n. abs(f n))"
   430 by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf)
   431 
   432 
   433 subsection{* The Ratio Test*}
   434 
   435 lemma rabs_ratiotest_lemma: "[| c \<le> 0; abs x \<le> c * abs y |] ==> x = (0::real)"
   436 apply (drule order_le_imp_less_or_eq, auto)
   437 apply (subgoal_tac "0 \<le> c * abs y")
   438 apply (simp add: zero_le_mult_iff, arith)
   439 done
   440 
   441 lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)"
   442 apply (drule le_imp_less_or_eq)
   443 apply (auto dest: less_imp_Suc_add)
   444 done
   445 
   446 lemma le_Suc_ex_iff: "((k::nat) \<le> l) = (\<exists>n. l = k + n)"
   447 by (auto simp add: le_Suc_ex)
   448 
   449 (*All this trouble just to get 0<c *)
   450 lemma ratio_test_lemma2:
   451      "[| \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |]  
   452       ==> 0 < c | summable f"
   453 apply (simp (no_asm) add: linorder_not_le [symmetric])
   454 apply (simp add: summable_Cauchy)
   455 apply (safe, subgoal_tac "\<forall>n. N < n --> f (n) = 0")
   456  prefer 2
   457  apply clarify
   458  apply(erule_tac x = "n - 1" in allE)
   459  apply (simp add:diff_Suc split:nat.splits)
   460  apply (blast intro: rabs_ratiotest_lemma)
   461 apply (rule_tac x = "Suc N" in exI, clarify)
   462 apply(simp cong:setsum_ivl_cong)
   463 done
   464 
   465 lemma ratio_test:
   466      "[| c < 1; \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |]  
   467       ==> summable f"
   468 apply (frule ratio_test_lemma2, auto)
   469 apply (rule_tac g = "%n. (abs (f N) / (c ^ N))*c ^ n" 
   470        in summable_comparison_test)
   471 apply (rule_tac x = N in exI, safe)
   472 apply (drule le_Suc_ex_iff [THEN iffD1])
   473 apply (auto simp add: power_add realpow_not_zero)
   474 apply (induct_tac "na", auto)
   475 apply (rule_tac y = "c*abs (f (N + n))" in order_trans)
   476 apply (auto intro: mult_right_mono simp add: summable_def)
   477 apply (simp add: mult_ac)
   478 apply (rule_tac x = "abs (f N) * (1/ (1 - c)) / (c ^ N)" in exI)
   479 apply (rule sums_divide) 
   480 apply (rule sums_mult) 
   481 apply (auto intro!: geometric_sums)
   482 done
   483 
   484 
   485 text{*Differentiation of finite sum*}
   486 
   487 lemma DERIV_sumr [rule_format (no_asm)]:
   488      "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))  
   489       --> DERIV (%x. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)"
   490 apply (induct "n")
   491 apply (auto intro: DERIV_add)
   492 done
   493 
   494 end