author paulson Mon Jun 04 21:00:21 2018 +0100 (13 months ago) changeset 68372 8e9da2d09dc6 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.118 +  proof
1.119 +    show "\<And>u. cmod (u - z) = r \<Longrightarrow> r - dist z w \<le> cmod (u - w)"
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)
```