add lemma tendsto_setsum
authorhuffman
Fri Jun 12 15:46:21 2009 -0700 (2009-06-12)
changeset 315882651f172c38b
parent 31587 a7e187205fc0
child 31589 eeebb2915035
add lemma tendsto_setsum
src/HOL/Limits.thy
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/Limits.thy	Fri Jun 12 12:00:30 2009 -0700
     1.2 +++ b/src/HOL/Limits.thy	Fri Jun 12 15:46:21 2009 -0700
     1.3 @@ -471,6 +471,24 @@
     1.4    shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) net"
     1.5  by (simp add: diff_minus tendsto_add tendsto_minus)
     1.6  
     1.7 +lemma tendsto_setsum [tendsto_intros]:
     1.8 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
     1.9 +  assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) net"
    1.10 +  shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) net"
    1.11 +proof (cases "finite S")
    1.12 +  assume "finite S" thus ?thesis using assms
    1.13 +  proof (induct set: finite)
    1.14 +    case empty show ?case
    1.15 +      by (simp add: tendsto_const)
    1.16 +  next
    1.17 +    case (insert i F) thus ?case
    1.18 +      by (simp add: tendsto_add)
    1.19 +  qed
    1.20 +next
    1.21 +  assume "\<not> finite S" thus ?thesis
    1.22 +    by (simp add: tendsto_const)
    1.23 +qed
    1.24 +
    1.25  lemma (in bounded_linear) tendsto [tendsto_intros]:
    1.26    "(g ---> a) net \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) net"
    1.27  by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
     2.1 --- a/src/HOL/SEQ.thy	Fri Jun 12 12:00:30 2009 -0700
     2.2 +++ b/src/HOL/SEQ.thy	Fri Jun 12 15:46:21 2009 -0700
     2.3 @@ -348,23 +348,7 @@
     2.4    fixes L :: "'a \<Rightarrow> 'b::real_normed_vector"
     2.5    assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
     2.6    shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)"
     2.7 -proof (cases "finite S")
     2.8 -  case True
     2.9 -  thus ?thesis using n
    2.10 -  proof (induct)
    2.11 -    case empty
    2.12 -    show ?case
    2.13 -      by (simp add: LIMSEQ_const)
    2.14 -  next
    2.15 -    case insert
    2.16 -    thus ?case
    2.17 -      by (simp add: LIMSEQ_add)
    2.18 -  qed
    2.19 -next
    2.20 -  case False
    2.21 -  thus ?thesis
    2.22 -    by (simp add: LIMSEQ_const)
    2.23 -qed
    2.24 +using n unfolding LIMSEQ_conv_tendsto by (rule tendsto_setsum)
    2.25  
    2.26  lemma LIMSEQ_setprod:
    2.27    fixes L :: "'a \<Rightarrow> 'b::{real_normed_algebra,comm_ring_1}"