src/HOL/Analysis/Complex_Transcendental.thy
changeset 63721 492bb53c3420
parent 63627 6ddb43c6b711
child 63918 6bf55e6e0b75
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Wed Aug 24 11:02:23 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Aug 25 15:50:43 2016 +0200
     1.3 @@ -1396,6 +1396,22 @@
     1.4    ultimately show ?thesis by (simp add: sums_iff)
     1.5  qed
     1.6  
     1.7 +lemma Ln_series': "cmod z < 1 \<Longrightarrow> (\<lambda>n. - ((-z)^n) / of_nat n) sums ln (1 + z)"
     1.8 +  by (drule Ln_series) (simp add: power_minus')
     1.9 +
    1.10 +lemma ln_series': 
    1.11 +  assumes "abs (x::real) < 1"
    1.12 +  shows   "(\<lambda>n. - ((-x)^n) / of_nat n) sums ln (1 + x)"
    1.13 +proof -
    1.14 +  from assms have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) sums ln (1 + complex_of_real x)"
    1.15 +    by (intro Ln_series') simp_all
    1.16 +  also have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) = (\<lambda>n. complex_of_real (- ((-x)^n) / of_nat n))"
    1.17 +    by (rule ext) simp
    1.18 +  also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))" 
    1.19 +    by (subst Ln_of_real [symmetric]) simp_all
    1.20 +  finally show ?thesis by (subst (asm) sums_of_real_iff)
    1.21 +qed
    1.22 +
    1.23  lemma Ln_approx_linear:
    1.24    fixes z :: complex
    1.25    assumes "norm z < 1"