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