src/HOL/Analysis/Cauchy_Integral_Theorem.thy
 changeset 65578 e4997c181cce parent 65037 2cf841ff23be child 65587 16a8991ab398
```     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Apr 25 08:38:23 2017 +0200
1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Apr 25 16:39:54 2017 +0100
1.3 @@ -1727,8 +1727,7 @@
1.4  next
1.5    case False
1.6    then have k: "0 < k" "k < 1" "complex_of_real k \<noteq> 1"
1.7 -    using assms apply auto
1.8 -    using of_real_eq_iff by fastforce
1.9 +    using assms by auto
1.10    have c': "c = k *\<^sub>R (b - a) + a"
1.11      by (metis diff_add_cancel c)
1.12    have bc: "(b - c) = (1 - k) *\<^sub>R (b - a)"
1.13 @@ -3871,7 +3870,7 @@
1.14    shows
1.15    "\<lbrakk>valid_path \<gamma>; z \<notin> path_image \<gamma>; w \<noteq> z;
1.16      \<And>a::real. 0 < a \<Longrightarrow> z + a*(w - z) \<notin> path_image \<gamma>\<rbrakk>
1.17 -   \<Longrightarrow> \<bar>Re(winding_number \<gamma> z)\<bar> < 1"
1.18 +   \<Longrightarrow> Re(winding_number \<gamma> z) < 1"
1.19     by (auto simp: not_less dest: winding_number_big_meets)
1.20
1.21  text\<open>One way of proving that WN=1 for a loop.\<close>
1.22 @@ -6532,6 +6531,21 @@
1.23  apply (force simp add: summable_Re o_def nonneg_Reals_cmod_eq_Re image_subset_iff)
1.24  done
1.25
1.26 +text\<open>Sometimes convenient to compare with a complex series of positive reals. (?)\<close>
1.27 +lemma series_differentiable_comparison_complex:
1.28 +  fixes S :: "complex set"
1.29 +  assumes S: "open S"
1.30 +    and hfd: "\<And>n x. x \<in> S \<Longrightarrow> f n field_differentiable (at x)"
1.31 +    and to_g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>d h. 0 < d \<and> summable h \<and> range h \<subseteq> \<real>\<^sub>\<ge>\<^sub>0 \<and> (\<forall>\<^sub>F n in sequentially. \<forall>y\<in>ball x d \<inter> S. cmod(f n y) \<le> cmod (h n))"
1.32 +  obtains g where "\<forall>x \<in> S. ((\<lambda>n. f n x) sums g x) \<and> g field_differentiable (at x)"
1.33 +proof -
1.34 +  have hfd': "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative deriv (f n) x) (at x)"
1.35 +    using hfd field_differentiable_derivI by blast
1.36 +  have "\<exists>g g'. \<forall>x \<in> S. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. deriv (f n) x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
1.37 +    by (metis series_and_derivative_comparison_complex [OF S hfd' to_g])
1.38 +  then show ?thesis
1.39 +    using field_differentiable_def that by blast
1.40 +qed
1.41
1.42  text\<open>In particular, a power series is analytic inside circle of convergence.\<close>
1.43
1.44 @@ -7441,5 +7455,4 @@
1.45                           homotopic_paths_imp_homotopic_loops)
1.46  using valid_path_imp_path by blast
1.47
1.48 -
1.49  end
```