src/HOL/Series.thy
changeset 66456 621897f47fab
parent 66447 a1f5c5c26fa6
child 67167 88d1c9d86f48
--- a/src/HOL/Series.thy	Fri Aug 18 22:55:54 2017 +0200
+++ b/src/HOL/Series.thy	Sun Aug 20 03:35:20 2017 +0200
@@ -983,6 +983,20 @@
   finally show ?thesis .
 qed
 
+lemma summable_powser_ignore_initial_segment:
+  fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra"
+  shows "summable (\<lambda>n. f (n + m) * z ^ n) \<longleftrightarrow> summable (\<lambda>n. f n * z ^ n)"
+proof (induction m)
+  case (Suc m)
+  have "summable (\<lambda>n. f (n + Suc m) * z ^ n) = summable (\<lambda>n. f (Suc n + m) * z ^ n)"
+    by simp
+  also have "\<dots> = summable (\<lambda>n. f (n + m) * z ^ n)"
+    by (rule summable_powser_split_head)
+  also have "\<dots> = summable (\<lambda>n. f n * z ^ n)"
+    by (rule Suc.IH)
+  finally show ?case .
+qed simp_all
+
 lemma powser_split_head:
   fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   assumes "summable (\<lambda>n. f n * z ^ n)"