src/HOL/Series.thy
changeset 62381 a6479cb85944
parent 62379 340738057c8c
child 63040 eb4ddd18d635
     1.1 --- a/src/HOL/Series.thy	Mon Feb 22 14:37:56 2016 +0000
     1.2 +++ b/src/HOL/Series.thy	Tue Feb 23 15:47:39 2016 +0000
     1.3 @@ -357,9 +357,12 @@
     1.4    thus "summable (\<lambda>n. f (Suc n))" unfolding summable_def by blast
     1.5  qed (auto simp: sums_Suc_iff summable_def)
     1.6  
     1.7 +lemma sums_Suc_imp: "f 0 = 0 \<Longrightarrow> (\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
     1.8 +  using sums_Suc_iff by simp
     1.9 +
    1.10  end
    1.11  
    1.12 -context
    1.13 +context --\<open>Separate contexts are necessary to allow general use of the results above, here.\<close>
    1.14    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    1.15  begin
    1.16  
    1.17 @@ -393,6 +396,11 @@
    1.18  corollary sums_iff_shift': "(\<lambda>i. f (i + n)) sums (s - (\<Sum>i<n. f i)) \<longleftrightarrow> f sums s"
    1.19    by (simp add: sums_iff_shift)
    1.20  
    1.21 +lemma sums_zero_iff_shift:
    1.22 +  assumes "\<And>i. i < n \<Longrightarrow> f i = 0"
    1.23 +  shows "(\<lambda>i. f (i+n)) sums s \<longleftrightarrow> (\<lambda>i. f i) sums s"
    1.24 +by (simp add: assms sums_iff_shift)
    1.25 +
    1.26  lemma summable_iff_shift: "summable (\<lambda>n. f (n + k)) \<longleftrightarrow> summable f"
    1.27    by (metis diff_add_cancel summable_def sums_iff_shift[abs_def])
    1.28