src/HOL/Hyperreal/Series.thy
 changeset 15085 5693a977a767 parent 15053 405be2b48f5b child 15131 c69542757a4d
```--- a/src/HOL/Hyperreal/Series.thy	Thu Jul 29 16:14:06 2004 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Thu Jul 29 16:14:42 2004 +0200
@@ -270,7 +270,8 @@
apply (drule summable_sums)
apply (auto simp add: sums_def LIMSEQ_def)
apply (drule_tac x = "f (n) + f (n + 1) " in spec)
-apply auto
+apply (auto iff: real_0_less_add_iff)
+   --{*legacy proof: not necessarily better!*}
apply (rule_tac [2] ccontr, drule_tac [2] linorder_not_less [THEN iffD1])
apply (frule_tac [2] no=no in sumr_pos_lt_pair_lemma)
apply (drule_tac x = 0 in spec, simp)
@@ -291,11 +292,9 @@
apply (auto simp add: linorder_not_less [symmetric])
done

-
+text{*A summable series of positive terms has limit that is at least as
+great as any partial sum.*}

-(*-----------------------------------------------------------------
-   Summable series of positive terms has limit >= any partial sum
- ----------------------------------------------------------------*)
lemma series_pos_le:
"[| summable f; \<forall>m. n \<le> m --> 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f"
apply (drule summable_sums)
@@ -314,9 +313,7 @@
apply (drule_tac x = m in spec, auto)
done

-(*-------------------------------------------------------------------
-                    sum of geometric progression
- -------------------------------------------------------------------*)
+text{*Sum of a geometric progression.*}

lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)"
apply (induct_tac "n", auto)
@@ -334,9 +331,8 @@
apply (auto intro: LIMSEQ_const simp add: real_diff_def minus_divide_right LIMSEQ_rabs_realpow_zero2)
done

-(*-------------------------------------------------------------------
-    Cauchy-type criterion for convergence of series (c.f. Harrison)
- -------------------------------------------------------------------*)
+text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
+
lemma summable_convergent_sumr_iff: "summable f = convergent (%n. sumr 0 n f)"
by (simp add: summable_def sums_def convergent_def)

@@ -355,14 +351,8 @@
simp add: sumr_split_add_minus abs_minus_add_cancel)
done

-(*-------------------------------------------------------------------
-     Terms of a convergent series tend to zero
-     > Goalw [LIMSEQ_def] "summable f ==> f ----> 0"
-     Proved easily in HSeries after proving nonstandard case.
- -------------------------------------------------------------------*)
-(*-------------------------------------------------------------------
-                    Comparison test
- -------------------------------------------------------------------*)
+text{*Comparison test*}
+
lemma summable_comparison_test:
"[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; summable g |] ==> summable f"
apply (auto simp add: summable_Cauchy)
@@ -384,9 +374,8 @@
apply (auto simp add: abs_idempotent)
done

-(*------------------------------------------------------------------*)
-(*       Limit comparison property for series (c.f. jrh)            *)
-(*------------------------------------------------------------------*)
+text{*Limit comparison property for series (c.f. jrh)*}
+
lemma summable_le:
"[|\<forall>n. f n \<le> g n; summable f; summable g |] ==> suminf f \<le> suminf g"
apply (drule summable_sums)+
@@ -402,9 +391,7 @@
apply (simp add: abs_le_interval_iff)
done

-(*-------------------------------------------------------------------
-         Absolute convergence imples normal convergence
- -------------------------------------------------------------------*)
+text{*Absolute convergence imples normal convergence*}
lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f"
apply (auto simp add: sumr_rabs summable_Cauchy)
apply (drule spec, auto)
@@ -414,9 +401,7 @@
apply (auto intro: sumr_rabs)
done

-(*-------------------------------------------------------------------
-         Absolute convergence of series
- -------------------------------------------------------------------*)
+text{*Absolute convergence of series*}
lemma summable_rabs:
"summable (%n. abs (f n)) ==> abs(suminf f) \<le> suminf (%n. abs(f n))"
by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf sumr_rabs)
@@ -469,9 +454,7 @@
done

-(*--------------------------------------------------------------------------*)
-(* Differentiation of finite sum                                            *)
-(*--------------------------------------------------------------------------*)
+text{*Differentiation of finite sum*}

lemma DERIV_sumr [rule_format (no_asm)]:
"(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))  ```