src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
changeset 61426 d53db136e8fd
parent 61070 b72a990adfe2
child 61518 ff12606337e9
     1.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Oct 13 09:21:21 2015 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Oct 13 12:42:08 2015 +0100
     1.3 @@ -522,9 +522,6 @@
     1.4    proof (rule complex_taylor [of "closed_segment 0 z" n 
     1.5                                   "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)" 
     1.6                                   "exp\<bar>Im z\<bar>" 0 z,  simplified])
     1.7 -  show "convex (closed_segment 0 z)"
     1.8 -    by (rule convex_segment [of 0 z])
     1.9 -  next
    1.10      fix k x
    1.11      show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
    1.12              (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
    1.13 @@ -537,13 +534,6 @@
    1.14      assume "x \<in> closed_segment 0 z"
    1.15      then show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>"
    1.16        by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
    1.17 -  next
    1.18 -    show "0 \<in> closed_segment 0 z"
    1.19 -      by (auto simp: closed_segment_def)
    1.20 -  next
    1.21 -    show "z \<in> closed_segment 0 z"
    1.22 -      apply (simp add: closed_segment_def scaleR_conv_of_real)
    1.23 -      using of_real_1 zero_le_one by blast
    1.24    qed
    1.25    have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
    1.26              = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
    1.27 @@ -565,9 +555,6 @@
    1.28             \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
    1.29    proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\<bar>Im z\<bar>" 0 z,
    1.30  simplified])
    1.31 -  show "convex (closed_segment 0 z)"
    1.32 -    by (rule convex_segment [of 0 z])
    1.33 -  next
    1.34      fix k x
    1.35      assume "x \<in> closed_segment 0 z" "k \<le> n"
    1.36      show "((\<lambda>x. (- 1) ^ (Suc k div 2) * (if even k then cos x else sin x)) has_field_derivative
    1.37 @@ -581,13 +568,6 @@
    1.38      assume "x \<in> closed_segment 0 z"
    1.39      then show "cmod ((- 1) ^ Suc (n div 2) * (if odd n then cos x else sin x)) \<le> exp \<bar>Im z\<bar>"
    1.40        by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
    1.41 -  next
    1.42 -    show "0 \<in> closed_segment 0 z"
    1.43 -      by (auto simp: closed_segment_def)
    1.44 -  next
    1.45 -    show "z \<in> closed_segment 0 z"
    1.46 -      apply (simp add: closed_segment_def scaleR_conv_of_real)
    1.47 -      using of_real_1 zero_le_one by blast
    1.48    qed
    1.49    have **: "\<And>k. complex_of_real (cos_coeff k) * z ^ k
    1.50              = (-1)^(Suc k div 2) * (if even k then cos 0 else sin 0) * z^k / of_nat (fact k)"