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])