src/HOL/Series.thy
 changeset 62087 44841d07ef1d parent 62049 b0f941e207cf child 62217 527488dc8b90
```     1.1 --- a/src/HOL/Series.thy	Wed Jan 06 16:17:50 2016 +0100
1.2 +++ b/src/HOL/Series.thy	Thu Jan 07 17:40:55 2016 +0000
1.3 @@ -30,6 +30,12 @@
1.4  where
1.5    "suminf f = (THE s. f sums s)"
1.6
1.7 +lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s"
1.8 +  apply (simp add: sums_def)
1.9 +  apply (subst LIMSEQ_Suc_iff [symmetric])
1.10 +  apply (simp only: lessThan_Suc_atMost atLeast0AtMost)
1.11 +  done
1.12 +
1.13  subsection \<open>Infinite summability on topological monoids\<close>
1.14
1.15  lemma sums_subst[trans]: "f = g \<Longrightarrow> g sums z \<Longrightarrow> f sums z"
1.16 @@ -674,7 +680,7 @@
1.17
1.18  text\<open>Relations among convergence and absolute convergence for power series.\<close>
1.19
1.20 -lemma abel_lemma:
1.21 +lemma Abel_lemma:
1.22    fixes a :: "nat \<Rightarrow> 'a::real_normed_vector"
1.23    assumes r: "0 \<le> r" and r0: "r < r0" and M: "\<And>n. norm (a n) * r0^n \<le> M"
1.24      shows "summable (\<lambda>n. norm (a n) * r^n)"
1.25 @@ -792,10 +798,10 @@
1.26    by (rule Cauchy_product_sums [THEN sums_unique])
1.27
1.28  lemma summable_Cauchy_product:
1.29 -  assumes "summable (\<lambda>k. norm (a k :: 'a :: {real_normed_algebra,banach}))"
1.30 +  assumes "summable (\<lambda>k. norm (a k :: 'a :: {real_normed_algebra,banach}))"
1.31            "summable (\<lambda>k. norm (b k))"
1.32    shows   "summable (\<lambda>k. \<Sum>i\<le>k. a i * b (k - i))"
1.33 -  using Cauchy_product_sums[OF assms] by (simp add: sums_iff)
1.34 +  using Cauchy_product_sums[OF assms] by (simp add: sums_iff)
1.35
1.36  subsection \<open>Series on @{typ real}s\<close>
1.37
```