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"
```