merged
authorpaulson
Mon Jun 04 21:00:21 2018 +0100 (13 months ago)
changeset 683728e9da2d09dc6
parent 68370 bcdc47c9d4af
parent 68371 17c3b22a9575
child 68373 f254e383bfe9
merged
     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jun 04 14:21:16 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jun 04 21:00:21 2018 +0100
     1.3 @@ -6005,7 +6005,7 @@
     1.4      shows "f holomorphic_on S"
     1.5  proof -
     1.6    { fix z
     1.7 -    assume "z \<in> S" and cdf: "\<And>x. x\<in>S - K \<Longrightarrow> f field_differentiable at x"
     1.8 +    assume "z \<in> S" and cdf: "\<And>x. x \<in> S - K \<Longrightarrow> f field_differentiable at x"
     1.9      have "f field_differentiable at z"
    1.10      proof (cases "z \<in> K")
    1.11        case False then show ?thesis by (blast intro: cdf \<open>z \<in> S\<close>)
    1.12 @@ -6018,14 +6018,15 @@
    1.13          using  S \<open>z \<in> S\<close> by (force simp: open_contains_ball)
    1.14        have fde: "continuous_on (ball z (min d e)) f"
    1.15          by (metis Int_iff ball_min_Int continuous_on_subset e f subsetI)
    1.16 +      have cont: "{a,b,c} \<subseteq> ball z (min d e) \<Longrightarrow> continuous_on (convex hull {a, b, c}) f" for a b c
    1.17 +        by (simp add: hull_minimal continuous_on_subset [OF fde])
    1.18 +      have fd: "\<lbrakk>{a,b,c} \<subseteq> ball z (min d e); x \<in> interior (convex hull {a, b, c}) - K\<rbrakk>
    1.19 +            \<Longrightarrow> f field_differentiable at x" for a b c x
    1.20 +        by (metis cdf Diff_iff Int_iff ball_min_Int subsetD convex_ball e interior_mono interior_subset subset_hull)
    1.21        obtain g where "\<And>w. w \<in> ball z (min d e) \<Longrightarrow> (g has_field_derivative f w) (at w within ball z (min d e))"
    1.22 -        apply (rule contour_integral_convex_primitive [OF convex_ball fde])
    1.23 -        apply (rule Cauchy_theorem_triangle_cofinite [OF _ K])
    1.24 -         apply (metis continuous_on_subset [OF fde] closed_segment_subset convex_ball starlike_convex_subset)
    1.25 -        apply (rule cdf)
    1.26 -        apply (metis Diff_iff Int_iff ball_min_Int bot_least contra_subsetD convex_ball e insert_subset
    1.27 -               interior_mono interior_subset subset_hull)
    1.28 -        by auto
    1.29 +        apply (rule contour_integral_convex_primitive 
    1.30 +                     [OF convex_ball fde Cauchy_theorem_triangle_cofinite [OF _ K]])
    1.31 +        using cont fd by auto
    1.32        then have "f holomorphic_on ball z (min d e)"
    1.33          by (metis open_ball at_within_open derivative_is_holomorphic)
    1.34        then show ?thesis
    1.35 @@ -6061,20 +6062,21 @@
    1.36  qed
    1.37  
    1.38  proposition Cauchy_integral_formula_convex:
    1.39 -    assumes S: "convex S" and K: "finite K" and contf: "continuous_on S f"
    1.40 -        and fcd: "(\<And>x. x \<in> interior S - K \<Longrightarrow> f field_differentiable at x)"
    1.41 -        and z: "z \<in> interior S" and vpg: "valid_path \<gamma>"
    1.42 -        and pasz: "path_image \<gamma> \<subseteq> S - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
    1.43 -      shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
    1.44 -  apply (rule Cauchy_integral_formula_weak [OF S finite.emptyI contf])
    1.45 -  apply (simp add: holomorphic_on_open [symmetric] field_differentiable_def)
    1.46 -  using no_isolated_singularity [where S = "interior S"]
    1.47 -  apply (metis K contf fcd holomorphic_on_open field_differentiable_def continuous_on_subset
    1.48 -               has_field_derivative_at_within holomorphic_on_def interior_subset open_interior)
    1.49 -  using assms
    1.50 -  apply auto
    1.51 -  done
    1.52 -
    1.53 +  assumes S: "convex S" and K: "finite K" and contf: "continuous_on S f"
    1.54 +    and fcd: "(\<And>x. x \<in> interior S - K \<Longrightarrow> f field_differentiable at x)"
    1.55 +    and z: "z \<in> interior S" and vpg: "valid_path \<gamma>"
    1.56 +    and pasz: "path_image \<gamma> \<subseteq> S - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
    1.57 +  shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
    1.58 +proof -
    1.59 +  have *: "\<And>x. x \<in> interior S \<Longrightarrow> f field_differentiable at x"
    1.60 +    unfolding holomorphic_on_open [symmetric] field_differentiable_def
    1.61 +    using no_isolated_singularity [where S = "interior S"]
    1.62 +    by (meson K contf continuous_at_imp_continuous_on continuous_on_interior fcd 
    1.63 +          field_differentiable_at_within field_differentiable_def holomorphic_onI
    1.64 +          holomorphic_on_imp_differentiable_at open_interior)
    1.65 +  show ?thesis
    1.66 +    by (rule Cauchy_integral_formula_weak [OF S finite.emptyI contf]) (use * assms in auto)
    1.67 +qed
    1.68  
    1.69  text\<open> Formula for higher derivatives.\<close>
    1.70  
    1.71 @@ -6155,33 +6157,32 @@
    1.72        and w: "w \<in> ball z r"
    1.73      shows "((\<lambda>n. (deriv ^^ n) f z / (fact n) * (w - z)^n) sums f w)"
    1.74  proof -
    1.75 -  have fh': "f holomorphic_on cball z ((r + dist w z) / 2)"
    1.76 -     apply (rule holomorphic_on_subset [OF holf])
    1.77 -     apply (clarsimp simp del: divide_const_simps)
    1.78 -     apply (metis add.commute dist_commute le_less_trans mem_ball real_gt_half_sum w)
    1.79 -     done
    1.80 -  \<comment> \<open>Replacing @{term r} and the original (weak) premises\<close>
    1.81 -  obtain r where "0 < r" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
    1.82 -    apply (rule that [of "(r + dist w z) / 2"])
    1.83 -      apply (simp_all add: fh')
    1.84 -     apply (metis add_0_iff ball_eq_empty dist_nz dist_self empty_iff not_less pos_add_strict w)
    1.85 -    apply (metis add_less_cancel_right dist_commute mem_ball mult_2_right w)
    1.86 -    done
    1.87 -  then have holf: "f holomorphic_on ball z r" and contf: "continuous_on (cball z r) f"
    1.88 -    using ball_subset_cball holomorphic_on_subset apply blast
    1.89 +  \<comment> \<open>Replacing @{term r} and the original (weak) premises with stronger ones\<close>
    1.90 +  obtain r where "r > 0" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
    1.91 +  proof 
    1.92 +    have "cball z ((r + dist w z) / 2) \<subseteq> ball z r"
    1.93 +      using w by (simp add: dist_commute real_sum_of_halves subset_eq)
    1.94 +    then show "f holomorphic_on cball z ((r + dist w z) / 2)"
    1.95 +      by (rule holomorphic_on_subset [OF holf])
    1.96 +    have "r > 0"
    1.97 +      using w by clarsimp (metis dist_norm le_less_trans norm_ge_zero)
    1.98 +    then show "0 < (r + dist w z) / 2"
    1.99 +      by simp (use zero_le_dist [of w z] in linarith)
   1.100 +  qed (use w in \<open>auto simp: dist_commute\<close>)
   1.101 +  then have holf: "f holomorphic_on ball z r" 
   1.102 +    using ball_subset_cball holomorphic_on_subset by blast
   1.103 +  have contf: "continuous_on (cball z r) f"
   1.104      by (simp add: holfc holomorphic_on_imp_continuous_on)
   1.105    have cint: "\<And>k. (\<lambda>u. f u / (u - z) ^ Suc k) contour_integrable_on circlepath z r"
   1.106 -    apply (rule Cauchy_higher_derivative_integral_circlepath [OF contf holf])
   1.107 -    apply (simp add: \<open>0 < r\<close>)
   1.108 -    done
   1.109 +    by (rule Cauchy_higher_derivative_integral_circlepath [OF contf holf]) (simp add: \<open>0 < r\<close>)
   1.110    obtain B where "0 < B" and B: "\<And>u. u \<in> cball z r \<Longrightarrow> norm(f u) \<le> B"
   1.111      by (metis (no_types) bounded_pos compact_cball compact_continuous_image compact_imp_bounded contf image_eqI)
   1.112    obtain k where k: "0 < k" "k \<le> r" and wz_eq: "norm(w - z) = r - k"
   1.113               and kle: "\<And>u. norm(u - z) = r \<Longrightarrow> k \<le> norm(u - w)"
   1.114 -    apply (rule_tac k = "r - dist z w" in that)
   1.115 -    using w
   1.116 -    apply (auto simp: dist_norm norm_minus_commute)
   1.117 -    by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
   1.118 +  proof 
   1.119 +    show "\<And>u. cmod (u - z) = r \<Longrightarrow> r - dist z w \<le> cmod (u - w)"
   1.120 +      by (metis add_diff_eq diff_add_cancel dist_norm norm_diff_ineq)
   1.121 +  qed (use w in \<open>auto simp: dist_norm norm_minus_commute\<close>)
   1.122    have ul: "uniform_limit (sphere z r) (\<lambda>n x. (\<Sum>k<n. (w - z) ^ k * (f x / (x - z) ^ Suc k))) (\<lambda>x. f x / (x - w)) sequentially"
   1.123      unfolding uniform_limit_iff dist_norm 
   1.124    proof clarify
   1.125 @@ -6239,16 +6240,14 @@
   1.126      using contour_integrable_lmul [OF cint, of "(w - z) ^ a" for a] apply (simp add: field_simps)
   1.127      apply (simp only: contour_integral_lmul cint algebra_simps)
   1.128      done
   1.129 +  have cic: "\<And>u. (\<lambda>y. \<Sum>k<u. (w - z) ^ k * (f y / (y - z) ^ Suc k)) contour_integrable_on circlepath z r"
   1.130 +    apply (intro contour_integrable_sum contour_integrable_lmul, simp)
   1.131 +    using \<open>0 < r\<close> by (force intro!: Cauchy_higher_derivative_integral_circlepath [OF contf holf])
   1.132    have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u/(u - z)^(Suc k)) * (w - z)^k)
   1.133          sums contour_integral (circlepath z r) (\<lambda>u. f u/(u - w))"
   1.134      unfolding sums_def
   1.135 -    apply (rule Lim_transform_eventually [OF eq])
   1.136 -    apply (rule contour_integral_uniform_limit_circlepath [OF eventuallyI ul])
   1.137 -    apply (rule contour_integrable_sum, simp)
   1.138 -    apply (rule contour_integrable_lmul)
   1.139 -    apply (rule Cauchy_higher_derivative_integral_circlepath [OF contf holf])
   1.140 -    using \<open>0 < r\<close>
   1.141 -    apply auto
   1.142 +    apply (intro Lim_transform_eventually [OF eq] contour_integral_uniform_limit_circlepath [OF eventuallyI ul] cic)
   1.143 +    using \<open>0 < r\<close> apply auto
   1.144      done
   1.145    then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u/(u - z)^(Suc k)) * (w - z)^k)
   1.146               sums (2 * of_real pi * \<i> * f w)"
   1.147 @@ -6288,16 +6287,12 @@
   1.148      apply (rule Cauchy_integral_circlepath)
   1.149      using \<open>R > 0\<close> apply (auto intro: holomorphic_on_subset [OF holf] holomorphic_on_imp_continuous_on)+
   1.150      done
   1.151 -  have "cmod (x - z) = R \<Longrightarrow> cmod (f x) * 2 \<le> cmod (f z)" for x
   1.152 -    apply (simp add: R_def)
   1.153 -    apply (rule less_imp_le)
   1.154 -    apply (rule B)
   1.155 -    using norm_triangle_ineq4 [of x z]
   1.156 -    apply auto
   1.157 -    done
   1.158 -  with  \<open>R > 0\<close> fz show False
   1.159 +  have "cmod (x - z) = R \<Longrightarrow> cmod (f x) * 2 < cmod (f z)" for x
   1.160 +    unfolding R_def
   1.161 +    by (rule B) (use norm_triangle_ineq4 [of x z] in auto)
   1.162 +  with \<open>R > 0\<close> fz show False
   1.163      using has_contour_integral_bound_circlepath [OF *, of "norm(f z)/2/R"]
   1.164 -    by (auto simp: norm_mult norm_divide divide_simps)
   1.165 +    by (auto simp: less_imp_le norm_mult norm_divide divide_simps)
   1.166  qed
   1.167  
   1.168  proposition Liouville_weak:
   1.169 @@ -6342,7 +6337,7 @@
   1.170    assume i: "i \<in> {1..n}" and nz: "a i \<noteq> 0"
   1.171    have 1: "(\<lambda>z. \<Sum>i\<le>n. a i * z^i) holomorphic_on UNIV"
   1.172      by (rule holomorphic_intros)+
   1.173 -  show ?thesis
   1.174 +  show thesis
   1.175      apply (rule Liouville_weak_inverse [OF 1])
   1.176      apply (rule polyfun_extremal)
   1.177      apply (rule nz)