author huffman Fri Jun 12 15:46:21 2009 -0700 (2009-06-12) changeset 31588 2651f172c38b parent 31587 a7e187205fc0 child 31589 eeebb2915035
 src/HOL/Limits.thy file | annotate | diff | revisions src/HOL/SEQ.thy file | annotate | diff | revisions
```     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.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.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