src/HOL/Transcendental.thy
changeset 55719 cdddd073bff8
parent 55417 01fbfb60c33e
child 55734 3f5b2745d659
     1.1 --- a/src/HOL/Transcendental.thy	Mon Feb 24 15:45:55 2014 +0000
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Feb 24 16:56:04 2014 +0000
     1.3 @@ -60,6 +60,23 @@
     1.4    apply (metis atLeastLessThan_iff diff_diff_cancel diff_less_Suc imageI le0 less_Suc_eq_le)
     1.5    done
     1.6  
     1.7 +lemma power_diff_1_eq:
     1.8 +  fixes x :: "'a::{comm_ring,monoid_mult}"
     1.9 +  shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i=0..<n. (x^i))"
    1.10 +using lemma_realpow_diff_sumr2 [of x _ 1] 
    1.11 +  by (cases n) auto
    1.12 +
    1.13 +lemma one_diff_power_eq':
    1.14 +  fixes x :: "'a::{comm_ring,monoid_mult}"
    1.15 +  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i=0..<n. x^(n - Suc i))"
    1.16 +using lemma_realpow_diff_sumr2 [of 1 _ x] 
    1.17 +  by (cases n) auto
    1.18 +
    1.19 +lemma one_diff_power_eq:
    1.20 +  fixes x :: "'a::{comm_ring,monoid_mult}"
    1.21 +  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i=0..<n. x^i)"
    1.22 +by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex)
    1.23 +
    1.24  text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
    1.25    x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
    1.26