src/HOL/SEQ.thy
changeset 36625 2ba6525f9905
parent 35748 5f35613d9a65
child 36647 edc381bf7200
child 36657 f376af79f6b7
     1.1 --- a/src/HOL/SEQ.thy	Fri Apr 30 09:54:04 2010 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Fri Apr 30 13:31:32 2010 -0700
     1.3 @@ -532,6 +532,33 @@
     1.4  lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
     1.5  by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
     1.6  
     1.7 +lemma convergent_const: "convergent (\<lambda>n. c)"
     1.8 +by (rule convergentI, rule LIMSEQ_const)
     1.9 +
    1.10 +lemma convergent_add:
    1.11 +  fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
    1.12 +  assumes "convergent (\<lambda>n. X n)"
    1.13 +  assumes "convergent (\<lambda>n. Y n)"
    1.14 +  shows "convergent (\<lambda>n. X n + Y n)"
    1.15 +using assms unfolding convergent_def by (fast intro: LIMSEQ_add)
    1.16 +
    1.17 +lemma convergent_setsum:
    1.18 +  fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
    1.19 +  assumes "finite A" and "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
    1.20 +  shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
    1.21 +using assms
    1.22 +by (induct A set: finite, simp_all add: convergent_const convergent_add)
    1.23 +
    1.24 +lemma (in bounded_linear) convergent:
    1.25 +  assumes "convergent (\<lambda>n. X n)"
    1.26 +  shows "convergent (\<lambda>n. f (X n))"
    1.27 +using assms unfolding convergent_def by (fast intro: LIMSEQ)
    1.28 +
    1.29 +lemma (in bounded_bilinear) convergent:
    1.30 +  assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)"
    1.31 +  shows "convergent (\<lambda>n. X n ** Y n)"
    1.32 +using assms unfolding convergent_def by (fast intro: LIMSEQ)
    1.33 +
    1.34  lemma convergent_minus_iff:
    1.35    fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
    1.36    shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"