src/HOL/Hyperreal/Series.thy
author huffman
Sun Sep 24 03:38:36 2006 +0200 (2006-09-24)
changeset 20688 690d866a165d
parent 20552 2c31dd358c21
child 20689 4950e45442b8
permissions -rw-r--r--
change definitions from SOME to THE
     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 = (THE 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 sums_def)
   101 apply (blast intro: theI LIMSEQ_unique)
   102 done
   103 
   104 lemma summable_sumr_LIMSEQ_suminf: 
   105      "summable f ==> (%n. setsum f {0..<n}) ----> (suminf f)"
   106 by (rule summable_sums [unfolded sums_def])
   107 
   108 (*-------------------
   109     sum is unique                    
   110  ------------------*)
   111 lemma sums_unique: "f sums s ==> (s = suminf f)"
   112 apply (frule sums_summable [THEN summable_sums])
   113 apply (auto intro!: LIMSEQ_unique simp add: sums_def)
   114 done
   115 
   116 lemma sums_split_initial_segment: "f sums s ==> 
   117   (%n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
   118   apply (unfold sums_def);
   119   apply (simp add: sumr_offset); 
   120   apply (rule LIMSEQ_diff_const)
   121   apply (rule LIMSEQ_ignore_initial_segment)
   122   apply assumption
   123 done
   124 
   125 lemma summable_ignore_initial_segment: "summable f ==> 
   126     summable (%n. f(n + k))"
   127   apply (unfold summable_def)
   128   apply (auto intro: sums_split_initial_segment)
   129 done
   130 
   131 lemma suminf_minus_initial_segment: "summable f ==>
   132     suminf f = s ==> suminf (%n. f(n + k)) = s - (SUM i = 0..< k. f i)"
   133   apply (frule summable_ignore_initial_segment)
   134   apply (rule sums_unique [THEN sym])
   135   apply (frule summable_sums)
   136   apply (rule sums_split_initial_segment)
   137   apply auto
   138 done
   139 
   140 lemma suminf_split_initial_segment: "summable f ==> 
   141     suminf f = (SUM i = 0..< k. f i) + suminf (%n. f(n + k))"
   142 by (auto simp add: suminf_minus_initial_segment)
   143 
   144 lemma series_zero: 
   145      "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})"
   146 apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)
   147 apply (rule_tac x = n in exI)
   148 apply (clarsimp simp add:setsum_diff[symmetric] cong:setsum_ivl_cong)
   149 done
   150 
   151 lemma sums_zero: "(%n. 0) sums 0";
   152   apply (unfold sums_def);
   153   apply simp;
   154   apply (rule LIMSEQ_const);
   155 done;
   156 
   157 lemma summable_zero: "summable (%n. 0)";
   158   apply (rule sums_summable);
   159   apply (rule sums_zero);
   160 done;
   161 
   162 lemma suminf_zero: "suminf (%n. 0) = 0";
   163   apply (rule sym);
   164   apply (rule sums_unique);
   165   apply (rule sums_zero);
   166 done;
   167   
   168 lemma sums_mult: "f sums a ==> (%n. c * f n) sums (c * a)"
   169 by (auto simp add: sums_def setsum_right_distrib [symmetric]
   170          intro!: LIMSEQ_mult intro: LIMSEQ_const)
   171 
   172 lemma summable_mult: "summable f ==> summable (%n. c * f n)";
   173   apply (unfold summable_def);
   174   apply (auto intro: sums_mult);
   175 done;
   176 
   177 lemma suminf_mult: "summable f ==> suminf (%n. c * f n) = c * suminf f";
   178   apply (rule sym);
   179   apply (rule sums_unique);
   180   apply (rule sums_mult);
   181   apply (erule summable_sums);
   182 done;
   183 
   184 lemma sums_mult2: "f sums a ==> (%n. f n * c) sums (a * c)"
   185 apply (subst mult_commute)
   186 apply (subst mult_commute);back;
   187 apply (erule sums_mult)
   188 done
   189 
   190 lemma summable_mult2: "summable f ==> summable (%n. f n * c)"
   191   apply (unfold summable_def)
   192   apply (auto intro: sums_mult2)
   193 done
   194 
   195 lemma suminf_mult2: "summable f ==> suminf f * c = (\<Sum>n. f n * c)"
   196 by (auto intro!: sums_unique sums_mult summable_sums simp add: mult_commute)
   197 
   198 lemma sums_divide: "f sums a ==> (%n. (f n)/c) sums (a/c)"
   199 by (simp add: real_divide_def sums_mult mult_commute [of _ "inverse c"])
   200 
   201 lemma summable_divide: "summable f ==> summable (%n. (f n) / c)";
   202   apply (unfold summable_def);
   203   apply (auto intro: sums_divide);
   204 done;
   205 
   206 lemma suminf_divide: "summable f ==> suminf (%n. (f n) / c) = (suminf f) / c";
   207   apply (rule sym);
   208   apply (rule sums_unique);
   209   apply (rule sums_divide);
   210   apply (erule summable_sums);
   211 done;
   212 
   213 lemma sums_add: "[| x sums x0; y sums y0 |] ==> (%n. x n + y n) sums (x0+y0)"
   214 by (auto simp add: sums_def setsum_addf intro: LIMSEQ_add)
   215 
   216 lemma summable_add: "summable f ==> summable g ==> summable (%x. f x + g x)";
   217   apply (unfold summable_def);
   218   apply clarify;
   219   apply (rule exI);
   220   apply (erule sums_add);
   221   apply assumption;
   222 done;
   223 
   224 lemma suminf_add:
   225      "[| summable f; summable g |]   
   226       ==> suminf f + suminf g  = (\<Sum>n. f n + g n)"
   227 by (auto intro!: sums_add sums_unique summable_sums)
   228 
   229 lemma sums_diff: "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)"
   230 by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff)
   231 
   232 lemma summable_diff: "summable f ==> summable g ==> summable (%x. f x - g x)";
   233   apply (unfold summable_def);
   234   apply clarify;
   235   apply (rule exI);
   236   apply (erule sums_diff);
   237   apply assumption;
   238 done;
   239 
   240 lemma suminf_diff:
   241      "[| summable f; summable g |]   
   242       ==> suminf f - suminf g  = (\<Sum>n. f n - g n)"
   243 by (auto intro!: sums_diff sums_unique summable_sums)
   244 
   245 lemma sums_minus: "f sums s ==> (%x. - f x) sums (- s)";
   246   by (simp add: sums_def setsum_negf LIMSEQ_minus);
   247 
   248 lemma summable_minus: "summable f ==> summable (%x. - f x)";
   249   by (auto simp add: summable_def intro: sums_minus);
   250 
   251 lemma suminf_minus: "summable f ==> suminf (%x. - f x) = - (suminf f)";
   252   apply (rule sym);
   253   apply (rule sums_unique);
   254   apply (rule sums_minus);
   255   apply (erule summable_sums);
   256 done;
   257 
   258 lemma sums_group:
   259      "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
   260 apply (drule summable_sums)
   261 apply (auto simp add: sums_def LIMSEQ_def sumr_group)
   262 apply (drule_tac x = r in spec, safe)
   263 apply (rule_tac x = no in exI, safe)
   264 apply (drule_tac x = "n*k" in spec)
   265 apply (auto dest!: not_leE)
   266 apply (drule_tac j = no in less_le_trans, auto)
   267 done
   268 
   269 lemma sumr_pos_lt_pair_lemma:
   270   "[|\<forall>d. - f (n + (d + d)) < (f (Suc (n + (d + d))) :: real) |]
   271    ==> setsum f {0..<n+Suc(Suc 0)} \<le> setsum f {0..<Suc(Suc 0) * Suc no + n}"
   272 apply (induct "no", auto)
   273 apply (drule_tac x = "Suc no" in spec)
   274 apply (simp add: add_ac)
   275 done
   276 
   277 lemma sumr_pos_lt_pair:
   278      "[|summable f; 
   279         \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|]  
   280       ==> setsum f {0..<n} < suminf f"
   281 apply (drule summable_sums)
   282 apply (auto simp add: sums_def LIMSEQ_def)
   283 apply (drule_tac x = "f (n) + f (n + 1)" in spec)
   284 apply (auto iff: real_0_less_add_iff)
   285    --{*legacy proof: not necessarily better!*}
   286 apply (rule_tac [2] ccontr, drule_tac [2] linorder_not_less [THEN iffD1])
   287 apply (frule_tac [2] no=no in sumr_pos_lt_pair_lemma) 
   288 apply (drule_tac x = 0 in spec, simp)
   289 apply (rotate_tac 1, drule_tac x = "Suc (Suc 0) * (Suc no) + n" in spec)
   290 apply (safe, simp)
   291 apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \<le>
   292  setsum f {0 ..< Suc (Suc 0) * (Suc no) + n}")
   293 apply (rule_tac [2] y = "setsum f {0..<n+ Suc (Suc 0)}" in order_trans)
   294 prefer 3 apply assumption
   295 apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans)
   296 apply simp_all
   297 done
   298 
   299 text{*A summable series of positive terms has limit that is at least as
   300 great as any partial sum.*}
   301 
   302 lemma series_pos_le: 
   303      "[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> setsum f {0..<n} \<le> suminf f"
   304 apply (drule summable_sums)
   305 apply (simp add: sums_def)
   306 apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const)
   307 apply (erule LIMSEQ_le, blast)
   308 apply (rule_tac x = n in exI, clarify)
   309 apply (rule setsum_mono2)
   310 apply auto
   311 done
   312 
   313 lemma series_pos_less:
   314      "[| summable f; \<forall>m \<ge> n. 0 < f(m) |] ==> setsum f {0..<n} < suminf f"
   315 apply (rule_tac y = "setsum f {0..<Suc n}" in order_less_le_trans)
   316 apply (rule_tac [2] series_pos_le, auto)
   317 apply (drule_tac x = m in spec, auto)
   318 done
   319 
   320 text{*Sum of a geometric progression.*}
   321 
   322 lemmas sumr_geometric = geometric_sum [where 'a = real]
   323 
   324 lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))"
   325 apply (case_tac "x = 1")
   326 apply (auto dest!: LIMSEQ_rabs_realpow_zero2 
   327         simp add: sumr_geometric sums_def diff_minus add_divide_distrib)
   328 apply (subgoal_tac "1 / (1 + -x) = 0/ (x - 1) + - 1/ (x - 1) ")
   329 apply (erule ssubst)
   330 apply (rule LIMSEQ_add, rule LIMSEQ_divide)
   331 apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2)
   332 done
   333 
   334 text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
   335 
   336 lemma summable_convergent_sumr_iff:
   337  "summable f = convergent (%n. setsum f {0..<n})"
   338 by (simp add: summable_def sums_def convergent_def)
   339 
   340 lemma summable_Cauchy:
   341      "summable f =  
   342       (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(setsum f {m..<n}) < e)"
   343 apply (simp only: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus [symmetric], safe)
   344 apply (drule spec, drule (1) mp)
   345 apply (erule exE, rule_tac x="M" in exI, clarify)
   346 apply (rule_tac x="m" and y="n" in linorder_le_cases)
   347 apply (frule (1) order_trans)
   348 apply (drule_tac x="n" in spec, drule (1) mp)
   349 apply (drule_tac x="m" in spec, drule (1) mp)
   350 apply (simp add: setsum_diff [symmetric])
   351 apply simp
   352 apply (drule spec, drule (1) mp)
   353 apply (erule exE, rule_tac x="N" in exI, clarify)
   354 apply (rule_tac x="m" and y="n" in linorder_le_cases)
   355 apply (subst norm_minus_commute)
   356 apply (simp add: setsum_diff [symmetric])
   357 apply (simp add: setsum_diff [symmetric])
   358 done
   359 
   360 text{*Comparison test*}
   361 
   362 lemma summable_comparison_test:
   363      "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] ==> summable f"
   364 apply (auto simp add: summable_Cauchy)
   365 apply (drule spec, auto)
   366 apply (rule_tac x = "N + Na" in exI, auto)
   367 apply (rotate_tac 2)
   368 apply (drule_tac x = m in spec)
   369 apply (auto, rotate_tac 2, drule_tac x = n in spec)
   370 apply (rule_tac y = "\<Sum>k=m..<n. abs(f k)" in order_le_less_trans)
   371 apply (rule setsum_abs)
   372 apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans)
   373 apply (auto intro: setsum_mono simp add: abs_interval_iff)
   374 done
   375 
   376 lemma summable_rabs_comparison_test:
   377      "[| \<exists>N. \<forall>n \<ge> N. abs(f n) \<le> g n; summable g |] 
   378       ==> summable (%k. abs (f k))"
   379 apply (rule summable_comparison_test)
   380 apply (auto)
   381 done
   382 
   383 text{*Limit comparison property for series (c.f. jrh)*}
   384 
   385 lemma summable_le:
   386      "[|\<forall>n. f n \<le> g n; summable f; summable g |] ==> suminf f \<le> suminf g"
   387 apply (drule summable_sums)+
   388 apply (auto intro!: LIMSEQ_le simp add: sums_def)
   389 apply (rule exI)
   390 apply (auto intro!: setsum_mono)
   391 done
   392 
   393 lemma summable_le2:
   394      "[|\<forall>n. abs(f n) \<le> g n; summable g |]  
   395       ==> summable f & suminf f \<le> suminf g"
   396 apply (auto intro: summable_comparison_test intro!: summable_le)
   397 apply (simp add: abs_le_interval_iff)
   398 done
   399 
   400 (* specialisation for the common 0 case *)
   401 lemma suminf_0_le:
   402   fixes f::"nat\<Rightarrow>real"
   403   assumes gt0: "\<forall>n. 0 \<le> f n" and sm: "summable f"
   404   shows "0 \<le> suminf f"
   405 proof -
   406   let ?g = "(\<lambda>n. (0::real))"
   407   from gt0 have "\<forall>n. ?g n \<le> f n" by simp
   408   moreover have "summable ?g" by (rule summable_zero)
   409   moreover from sm have "summable f" .
   410   ultimately have "suminf ?g \<le> suminf f" by (rule summable_le)
   411   then show "0 \<le> suminf f" by (simp add: suminf_zero)
   412 qed 
   413 
   414 
   415 text{*Absolute convergence imples normal convergence*}
   416 lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f"
   417 apply (auto simp add: summable_Cauchy)
   418 apply (drule spec, auto)
   419 apply (rule_tac x = N in exI, auto)
   420 apply (drule spec, auto)
   421 apply (rule_tac y = "\<Sum>n=m..<n. abs(f n)" in order_le_less_trans)
   422 apply (auto)
   423 done
   424 
   425 text{*Absolute convergence of series*}
   426 lemma summable_rabs:
   427      "summable (%n. abs (f n)) ==> abs(suminf f) \<le> (\<Sum>n. abs(f n))"
   428 by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf)
   429 
   430 
   431 subsection{* The Ratio Test*}
   432 
   433 lemma rabs_ratiotest_lemma: "[| c \<le> 0; abs x \<le> c * abs y |] ==> x = (0::real)"
   434 apply (drule order_le_imp_less_or_eq, auto)
   435 apply (subgoal_tac "0 \<le> c * abs y")
   436 apply (simp add: zero_le_mult_iff, arith)
   437 done
   438 
   439 lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)"
   440 apply (drule le_imp_less_or_eq)
   441 apply (auto dest: less_imp_Suc_add)
   442 done
   443 
   444 lemma le_Suc_ex_iff: "((k::nat) \<le> l) = (\<exists>n. l = k + n)"
   445 by (auto simp add: le_Suc_ex)
   446 
   447 (*All this trouble just to get 0<c *)
   448 lemma ratio_test_lemma2:
   449      "[| \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |]  
   450       ==> 0 < c | summable f"
   451 apply (simp (no_asm) add: linorder_not_le [symmetric])
   452 apply (simp add: summable_Cauchy)
   453 apply (safe, subgoal_tac "\<forall>n. N < n --> f (n) = 0")
   454  prefer 2
   455  apply clarify
   456  apply(erule_tac x = "n - 1" in allE)
   457  apply (simp add:diff_Suc split:nat.splits)
   458  apply (blast intro: rabs_ratiotest_lemma)
   459 apply (rule_tac x = "Suc N" in exI, clarify)
   460 apply(simp cong:setsum_ivl_cong)
   461 done
   462 
   463 lemma ratio_test:
   464      "[| c < 1; \<forall>n \<ge> N. abs(f(Suc n)) \<le> c*abs(f n) |]  
   465       ==> summable f"
   466 apply (frule ratio_test_lemma2, auto)
   467 apply (rule_tac g = "%n. (abs (f N) / (c ^ N))*c ^ n" 
   468        in summable_comparison_test)
   469 apply (rule_tac x = N in exI, safe)
   470 apply (drule le_Suc_ex_iff [THEN iffD1])
   471 apply (auto simp add: power_add realpow_not_zero)
   472 apply (induct_tac "na", auto)
   473 apply (rule_tac y = "c*abs (f (N + n))" in order_trans)
   474 apply (auto intro: mult_right_mono simp add: summable_def)
   475 apply (simp add: mult_ac)
   476 apply (rule_tac x = "abs (f N) * (1/ (1 - c)) / (c ^ N)" in exI)
   477 apply (rule sums_divide) 
   478 apply (rule sums_mult) 
   479 apply (auto intro!: geometric_sums)
   480 done
   481 
   482 
   483 text{*Differentiation of finite sum*}
   484 
   485 lemma DERIV_sumr [rule_format (no_asm)]:
   486      "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))  
   487       --> DERIV (%x. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)"
   488 apply (induct "n")
   489 apply (auto intro: DERIV_add)
   490 done
   491 
   492 end