src/HOL/Series.thy
changeset 62379 340738057c8c
parent 62377 ace69956d018
child 62381 a6479cb85944
     1.1 --- a/src/HOL/Series.thy	Fri Feb 19 13:40:50 2016 +0100
     1.2 +++ b/src/HOL/Series.thy	Mon Feb 22 14:37:56 2016 +0000
     1.3 @@ -390,6 +390,9 @@
     1.4      by (simp add: ac_simps)
     1.5  qed simp
     1.6  
     1.7 +corollary sums_iff_shift': "(\<lambda>i. f (i + n)) sums (s - (\<Sum>i<n. f i)) \<longleftrightarrow> f sums s"
     1.8 +  by (simp add: sums_iff_shift)
     1.9 +
    1.10  lemma summable_iff_shift: "summable (\<lambda>n. f (n + k)) \<longleftrightarrow> summable f"
    1.11    by (metis diff_add_cancel summable_def sums_iff_shift[abs_def])
    1.12  
    1.13 @@ -535,6 +538,12 @@
    1.14  lemma suminf_divide: "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
    1.15    by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric])
    1.16  
    1.17 +lemma sums_mult_D: "\<lbrakk>(\<lambda>n. c * f n) sums a; c \<noteq> 0\<rbrakk> \<Longrightarrow> f sums (a/c)"
    1.18 +  using sums_mult_iff by fastforce
    1.19 +
    1.20 +lemma summable_mult_D: "\<lbrakk>summable (\<lambda>n. c * f n); c \<noteq> 0\<rbrakk> \<Longrightarrow> summable f"
    1.21 +  by (auto dest: summable_divide)
    1.22 +
    1.23  text\<open>Sum of a geometric progression.\<close>
    1.24  
    1.25  lemma geometric_sums: "norm c < 1 \<Longrightarrow> (\<lambda>n. c^n) sums (1 / (1 - c))"