equal
deleted
inserted
replaced
358 subsection{*Properties of Power Series*} |
358 subsection{*Properties of Power Series*} |
359 |
359 |
360 lemma lemma_realpow_diff_sumr: |
360 lemma lemma_realpow_diff_sumr: |
361 "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) = |
361 "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) = |
362 y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)" |
362 y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)" |
363 apply (auto simp add: setsum_mult simp del: setsum_op_ivl_Suc) |
363 by (auto simp add: setsum_mult lemma_realpow_diff mult_ac |
364 apply (rule setsum_cong[OF refl]) |
364 simp del: setsum_op_ivl_Suc cong: strong_setsum_cong) |
365 apply (subst lemma_realpow_diff) |
|
366 apply (auto simp add: mult_ac) |
|
367 done |
|
368 |
365 |
369 lemma lemma_realpow_diff_sumr2: |
366 lemma lemma_realpow_diff_sumr2: |
370 "x ^ (Suc n) - y ^ (Suc n) = |
367 "x ^ (Suc n) - y ^ (Suc n) = |
371 (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^(n - p))::real)" |
368 (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^(n - p))::real)" |
372 apply (induct "n", simp) |
369 apply (induct "n", simp) |
466 subsection{*Term-by-Term Differentiability of Power Series*} |
463 subsection{*Term-by-Term Differentiability of Power Series*} |
467 |
464 |
468 lemma lemma_termdiff1: |
465 lemma lemma_termdiff1: |
469 "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) = |
466 "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) = |
470 (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p)))::real)" |
467 (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p)))::real)" |
471 apply (rule setsum_cong[OF refl]) |
468 by (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac |
472 apply (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac) |
469 cong: strong_setsum_cong) |
473 done |
|
474 |
470 |
475 lemma less_add_one: "m < n ==> (\<exists>d. n = m + d + Suc 0)" |
471 lemma less_add_one: "m < n ==> (\<exists>d. n = m + d + Suc 0)" |
476 by (simp add: less_iff_Suc_add) |
472 by (simp add: less_iff_Suc_add) |
477 |
473 |
478 lemma sumdiff: "a + b - (c + d) = a - c + b - (d::real)" |
474 lemma sumdiff: "a + b - (c + d) = a - c + b - (d::real)" |