src/HOL/Series.thy
changeset 62049 b0f941e207cf
parent 61969 e01015e49041
child 62087 44841d07ef1d
     1.1 --- a/src/HOL/Series.thy	Sun Jan 03 21:45:34 2016 +0100
     1.2 +++ b/src/HOL/Series.thy	Mon Jan 04 17:45:36 2016 +0100
     1.3 @@ -791,6 +791,12 @@
     1.4    using a b
     1.5    by (rule Cauchy_product_sums [THEN sums_unique])
     1.6  
     1.7 +lemma summable_Cauchy_product:
     1.8 +  assumes "summable (\<lambda>k. norm (a k :: 'a :: {real_normed_algebra,banach}))" 
     1.9 +          "summable (\<lambda>k. norm (b k))"
    1.10 +  shows   "summable (\<lambda>k. \<Sum>i\<le>k. a i * b (k - i))"
    1.11 +  using Cauchy_product_sums[OF assms] by (simp add: sums_iff)  
    1.12 +
    1.13  subsection \<open>Series on @{typ real}s\<close>
    1.14  
    1.15  lemma summable_norm_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. norm (f n))"