src/HOL/Hyperreal/Series.thy
changeset 15085 5693a977a767
parent 15053 405be2b48f5b
child 15131 c69542757a4d
equal deleted inserted replaced
15084:07f7b158ef32 15085:5693a977a767
   268      "[|summable f; \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|]  
   268      "[|summable f; \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|]  
   269       ==> sumr 0 n f < suminf f"
   269       ==> sumr 0 n f < suminf f"
   270 apply (drule summable_sums)
   270 apply (drule summable_sums)
   271 apply (auto simp add: sums_def LIMSEQ_def)
   271 apply (auto simp add: sums_def LIMSEQ_def)
   272 apply (drule_tac x = "f (n) + f (n + 1) " in spec)
   272 apply (drule_tac x = "f (n) + f (n + 1) " in spec)
   273 apply auto
   273 apply (auto iff: real_0_less_add_iff)
       
   274    --{*legacy proof: not necessarily better!*}
   274 apply (rule_tac [2] ccontr, drule_tac [2] linorder_not_less [THEN iffD1])
   275 apply (rule_tac [2] ccontr, drule_tac [2] linorder_not_less [THEN iffD1])
   275 apply (frule_tac [2] no=no in sumr_pos_lt_pair_lemma) 
   276 apply (frule_tac [2] no=no in sumr_pos_lt_pair_lemma) 
   276 apply (drule_tac x = 0 in spec, simp)
   277 apply (drule_tac x = 0 in spec, simp)
   277 apply (rotate_tac 1, drule_tac x = "Suc (Suc 0) * (Suc no) + n" in spec)
   278 apply (rotate_tac 1, drule_tac x = "Suc (Suc 0) * (Suc no) + n" in spec)
   278 apply (safe, simp)
   279 apply (safe, simp)
   289 apply (subgoal_tac "0 \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f + - suminf f")
   290 apply (subgoal_tac "0 \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f + - suminf f")
   290 apply (simp add: abs_if) 
   291 apply (simp add: abs_if) 
   291 apply (auto simp add: linorder_not_less [symmetric])
   292 apply (auto simp add: linorder_not_less [symmetric])
   292 done
   293 done
   293 
   294 
   294 
   295 text{*A summable series of positive terms has limit that is at least as
   295 
   296 great as any partial sum.*}
   296 (*-----------------------------------------------------------------
   297 
   297    Summable series of positive terms has limit >= any partial sum 
       
   298  ----------------------------------------------------------------*)
       
   299 lemma series_pos_le: 
   298 lemma series_pos_le: 
   300      "[| summable f; \<forall>m. n \<le> m --> 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f"
   299      "[| summable f; \<forall>m. n \<le> m --> 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f"
   301 apply (drule summable_sums)
   300 apply (drule summable_sums)
   302 apply (simp add: sums_def)
   301 apply (simp add: sums_def)
   303 apply (cut_tac k = "sumr 0 n f" in LIMSEQ_const)
   302 apply (cut_tac k = "sumr 0 n f" in LIMSEQ_const)
   312 apply (rule_tac y = "sumr 0 (Suc n) f" in order_less_le_trans)
   311 apply (rule_tac y = "sumr 0 (Suc n) f" in order_less_le_trans)
   313 apply (rule_tac [2] series_pos_le, auto)
   312 apply (rule_tac [2] series_pos_le, auto)
   314 apply (drule_tac x = m in spec, auto)
   313 apply (drule_tac x = m in spec, auto)
   315 done
   314 done
   316 
   315 
   317 (*-------------------------------------------------------------------
   316 text{*Sum of a geometric progression.*}
   318                     sum of geometric progression                 
       
   319  -------------------------------------------------------------------*)
       
   320 
   317 
   321 lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)"
   318 lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)"
   322 apply (induct_tac "n", auto)
   319 apply (induct_tac "n", auto)
   323 apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1])
   320 apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1])
   324 apply (auto simp add: real_mult_assoc left_distrib)
   321 apply (auto simp add: real_mult_assoc left_distrib)
   332 apply (erule ssubst)
   329 apply (erule ssubst)
   333 apply (rule LIMSEQ_add, rule LIMSEQ_divide)
   330 apply (rule LIMSEQ_add, rule LIMSEQ_divide)
   334 apply (auto intro: LIMSEQ_const simp add: real_diff_def minus_divide_right LIMSEQ_rabs_realpow_zero2)
   331 apply (auto intro: LIMSEQ_const simp add: real_diff_def minus_divide_right LIMSEQ_rabs_realpow_zero2)
   335 done
   332 done
   336 
   333 
   337 (*-------------------------------------------------------------------
   334 text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
   338     Cauchy-type criterion for convergence of series (c.f. Harrison)
   335 
   339  -------------------------------------------------------------------*)
       
   340 lemma summable_convergent_sumr_iff: "summable f = convergent (%n. sumr 0 n f)"
   336 lemma summable_convergent_sumr_iff: "summable f = convergent (%n. sumr 0 n f)"
   341 by (simp add: summable_def sums_def convergent_def)
   337 by (simp add: summable_def sums_def convergent_def)
   342 
   338 
   343 lemma summable_Cauchy:
   339 lemma summable_Cauchy:
   344      "summable f =  
   340      "summable f =  
   353 apply (drule_tac x = m in spec)
   349 apply (drule_tac x = m in spec)
   354 apply (auto intro: abs_minus_add_cancel [THEN subst]
   350 apply (auto intro: abs_minus_add_cancel [THEN subst]
   355             simp add: sumr_split_add_minus abs_minus_add_cancel)
   351             simp add: sumr_split_add_minus abs_minus_add_cancel)
   356 done
   352 done
   357 
   353 
   358 (*-------------------------------------------------------------------
   354 text{*Comparison test*}
   359      Terms of a convergent series tend to zero
   355 
   360      > Goalw [LIMSEQ_def] "summable f ==> f ----> 0"
       
   361      Proved easily in HSeries after proving nonstandard case.
       
   362  -------------------------------------------------------------------*)
       
   363 (*-------------------------------------------------------------------
       
   364                     Comparison test
       
   365  -------------------------------------------------------------------*)
       
   366 lemma summable_comparison_test:
   356 lemma summable_comparison_test:
   367      "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; summable g |] ==> summable f"
   357      "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; summable g |] ==> summable f"
   368 apply (auto simp add: summable_Cauchy)
   358 apply (auto simp add: summable_Cauchy)
   369 apply (drule spec, auto)
   359 apply (drule spec, auto)
   370 apply (rule_tac x = "N + Na" in exI, auto)
   360 apply (rule_tac x = "N + Na" in exI, auto)
   382       ==> summable (%k. abs (f k))"
   372       ==> summable (%k. abs (f k))"
   383 apply (rule summable_comparison_test)
   373 apply (rule summable_comparison_test)
   384 apply (auto simp add: abs_idempotent)
   374 apply (auto simp add: abs_idempotent)
   385 done
   375 done
   386 
   376 
   387 (*------------------------------------------------------------------*)
   377 text{*Limit comparison property for series (c.f. jrh)*}
   388 (*       Limit comparison property for series (c.f. jrh)            *)
   378 
   389 (*------------------------------------------------------------------*)
       
   390 lemma summable_le:
   379 lemma summable_le:
   391      "[|\<forall>n. f n \<le> g n; summable f; summable g |] ==> suminf f \<le> suminf g"
   380      "[|\<forall>n. f n \<le> g n; summable f; summable g |] ==> suminf f \<le> suminf g"
   392 apply (drule summable_sums)+
   381 apply (drule summable_sums)+
   393 apply (auto intro!: LIMSEQ_le simp add: sums_def)
   382 apply (auto intro!: LIMSEQ_le simp add: sums_def)
   394 apply (rule exI)
   383 apply (rule exI)
   400       ==> summable f & suminf f \<le> suminf g"
   389       ==> summable f & suminf f \<le> suminf g"
   401 apply (auto intro: summable_comparison_test intro!: summable_le)
   390 apply (auto intro: summable_comparison_test intro!: summable_le)
   402 apply (simp add: abs_le_interval_iff)
   391 apply (simp add: abs_le_interval_iff)
   403 done
   392 done
   404 
   393 
   405 (*-------------------------------------------------------------------
   394 text{*Absolute convergence imples normal convergence*}
   406          Absolute convergence imples normal convergence
       
   407  -------------------------------------------------------------------*)
       
   408 lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f"
   395 lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f"
   409 apply (auto simp add: sumr_rabs summable_Cauchy)
   396 apply (auto simp add: sumr_rabs summable_Cauchy)
   410 apply (drule spec, auto)
   397 apply (drule spec, auto)
   411 apply (rule_tac x = N in exI, auto)
   398 apply (rule_tac x = N in exI, auto)
   412 apply (drule spec, auto)
   399 apply (drule spec, auto)
   413 apply (rule_tac y = "sumr m n (%n. abs (f n))" in order_le_less_trans)
   400 apply (rule_tac y = "sumr m n (%n. abs (f n))" in order_le_less_trans)
   414 apply (auto intro: sumr_rabs)
   401 apply (auto intro: sumr_rabs)
   415 done
   402 done
   416 
   403 
   417 (*-------------------------------------------------------------------
   404 text{*Absolute convergence of series*}
   418          Absolute convergence of series
       
   419  -------------------------------------------------------------------*)
       
   420 lemma summable_rabs:
   405 lemma summable_rabs:
   421      "summable (%n. abs (f n)) ==> abs(suminf f) \<le> suminf (%n. abs(f n))"
   406      "summable (%n. abs (f n)) ==> abs(suminf f) \<le> suminf (%n. abs(f n))"
   422 by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf sumr_rabs)
   407 by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf sumr_rabs)
   423 
   408 
   424 
   409 
   467 apply (rule sums_mult)
   452 apply (rule sums_mult)
   468 apply (auto intro!: sums_mult geometric_sums simp add: abs_if)
   453 apply (auto intro!: sums_mult geometric_sums simp add: abs_if)
   469 done
   454 done
   470 
   455 
   471 
   456 
   472 (*--------------------------------------------------------------------------*)
   457 text{*Differentiation of finite sum*}
   473 (* Differentiation of finite sum                                            *)
       
   474 (*--------------------------------------------------------------------------*)
       
   475 
   458 
   476 lemma DERIV_sumr [rule_format (no_asm)]:
   459 lemma DERIV_sumr [rule_format (no_asm)]:
   477      "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))  
   460      "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))  
   478       --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)"
   461       --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)"
   479 apply (induct_tac "n")
   462 apply (induct_tac "n")