1435 lemma setsum_shift_lb_Suc0_0_upt: |
1435 lemma setsum_shift_lb_Suc0_0_upt: |
1436 "f(0::nat) = 0 \<Longrightarrow> setsum f {Suc 0..<k} = setsum f {0..<k}" |
1436 "f(0::nat) = 0 \<Longrightarrow> setsum f {Suc 0..<k} = setsum f {0..<k}" |
1437 apply(cases k)apply simp |
1437 apply(cases k)apply simp |
1438 apply(simp add:setsum_head_upt_Suc) |
1438 apply(simp add:setsum_head_upt_Suc) |
1439 done |
1439 done |
|
1440 |
|
1441 lemma setsum_atMost_Suc_shift: |
|
1442 fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add" |
|
1443 shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))" |
|
1444 proof (induct n) |
|
1445 case 0 show ?case by simp |
|
1446 next |
|
1447 case (Suc n) note IH = this |
|
1448 have "(\<Sum>i\<le>Suc (Suc n). f i) = (\<Sum>i\<le>Suc n. f i) + f (Suc (Suc n))" |
|
1449 by (rule setsum_atMost_Suc) |
|
1450 also have "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))" |
|
1451 by (rule IH) |
|
1452 also have "f 0 + (\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) = |
|
1453 f 0 + ((\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)))" |
|
1454 by (rule add_assoc) |
|
1455 also have "(\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) = (\<Sum>i\<le>Suc n. f (Suc i))" |
|
1456 by (rule setsum_atMost_Suc [symmetric]) |
|
1457 finally show ?case . |
|
1458 qed |
|
1459 |
1440 |
1460 |
1441 subsection {* The formula for geometric sums *} |
1461 subsection {* The formula for geometric sums *} |
1442 |
1462 |
1443 lemma geometric_sum: |
1463 lemma geometric_sum: |
1444 assumes "x \<noteq> 1" |
1464 assumes "x \<noteq> 1" |