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