src/HOL/Series.thy
changeset 66456 621897f47fab
parent 66447 a1f5c5c26fa6
child 67167 88d1c9d86f48
     1.1 --- a/src/HOL/Series.thy	Fri Aug 18 22:55:54 2017 +0200
     1.2 +++ b/src/HOL/Series.thy	Sun Aug 20 03:35:20 2017 +0200
     1.3 @@ -983,6 +983,20 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +lemma summable_powser_ignore_initial_segment:
     1.8 +  fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra"
     1.9 +  shows "summable (\<lambda>n. f (n + m) * z ^ n) \<longleftrightarrow> summable (\<lambda>n. f n * z ^ n)"
    1.10 +proof (induction m)
    1.11 +  case (Suc m)
    1.12 +  have "summable (\<lambda>n. f (n + Suc m) * z ^ n) = summable (\<lambda>n. f (Suc n + m) * z ^ n)"
    1.13 +    by simp
    1.14 +  also have "\<dots> = summable (\<lambda>n. f (n + m) * z ^ n)"
    1.15 +    by (rule summable_powser_split_head)
    1.16 +  also have "\<dots> = summable (\<lambda>n. f n * z ^ n)"
    1.17 +    by (rule Suc.IH)
    1.18 +  finally show ?case .
    1.19 +qed simp_all
    1.20 +
    1.21  lemma powser_split_head:
    1.22    fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
    1.23    assumes "summable (\<lambda>n. f n * z ^ n)"