src/HOL/Analysis/Complex_Transcendental.thy
 changeset 66252 b73f94b366b7 parent 65719 7c57d79d61b7 child 66447 a1f5c5c26fa6
```     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Jul 02 20:13:38 2017 +0200
1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jul 04 09:36:25 2017 +0100
1.3 @@ -582,6 +582,35 @@
1.4
1.5  declare power_Suc [simp del]
1.6
1.7 +lemma Taylor_exp_field:
1.8 +  fixes z::"'a::{banach,real_normed_field}"
1.9 +  shows "norm (exp z - (\<Sum>i\<le>n. z ^ i / fact i)) \<le> exp (norm z) * (norm z ^ Suc n) / fact n"
1.10 +proof (rule field_taylor[of _ n "\<lambda>k. exp" "exp (norm z)" 0 z, simplified])
1.11 +  show "convex (closed_segment 0 z)"
1.12 +    by (rule convex_closed_segment [of 0 z])
1.13 +next
1.14 +  fix k x
1.15 +  assume "x \<in> closed_segment 0 z" "k \<le> n"
1.16 +  show "(exp has_field_derivative exp x) (at x within closed_segment 0 z)"
1.17 +    using DERIV_exp DERIV_subset by blast
1.18 +next
1.19 +  fix x
1.20 +  assume x: "x \<in> closed_segment 0 z"
1.21 +  have "norm (exp x) \<le> exp (norm x)"
1.22 +    by (rule norm_exp)
1.23 +  also have "norm x \<le> norm z"
1.24 +    using x by (auto simp: closed_segment_def intro!: mult_left_le_one_le)
1.25 +  finally show "norm (exp x) \<le> exp (norm z)"
1.26 +    by simp
1.27 +next
1.28 +  show "0 \<in> closed_segment 0 z"
1.29 +    by (auto simp: closed_segment_def)
1.30 +next
1.31 +  show "z \<in> closed_segment 0 z"
1.32 +    apply (simp add: closed_segment_def scaleR_conv_of_real)
1.33 +    using of_real_1 zero_le_one by blast
1.34 +qed
1.35 +
1.36  lemma Taylor_exp:
1.37    "norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
1.38  proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
```