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