src/HOL/Series.thy
changeset 57025 e7fd64f82876
parent 56536 aefb4a8da31f
child 57129 7edb7550663e
     1.1 --- a/src/HOL/Series.thy	Tue May 20 16:52:59 2014 +0200
     1.2 +++ b/src/HOL/Series.thy	Tue May 20 19:24:39 2014 +0200
     1.3 @@ -316,6 +316,21 @@
     1.4  
     1.5  end
     1.6  
     1.7 +context
     1.8 +  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_vector" and I :: "'i set"
     1.9 +begin
    1.10 +
    1.11 +lemma sums_setsum: "(\<And>i. i \<in> I \<Longrightarrow> (f i) sums (x i)) \<Longrightarrow> (\<lambda>n. \<Sum>i\<in>I. f i n) sums (\<Sum>i\<in>I. x i)"
    1.12 +  by (induct I rule: infinite_finite_induct) (auto intro!: sums_add)
    1.13 +
    1.14 +lemma suminf_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> (\<Sum>n. \<Sum>i\<in>I. f i n) = (\<Sum>i\<in>I. \<Sum>n. f i n)"
    1.15 +  using sums_unique[OF sums_setsum, OF summable_sums] by simp
    1.16 +
    1.17 +lemma summable_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)"
    1.18 +  using sums_summable[OF sums_setsum[OF summable_sums]] .
    1.19 +
    1.20 +end
    1.21 +
    1.22  lemma (in bounded_linear) sums: "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)"
    1.23    unfolding sums_def by (drule tendsto, simp only: setsum)
    1.24