src/HOL/Analysis/Cauchy_Integral_Theorem.thy
changeset 67107 cef76a19125e
parent 66884 c2128ab11f61
child 67237 1fe0ec14a90a
equal deleted inserted replaced
67106:66fda545327f 67107:cef76a19125e
  2833 apply (rule contour_integral_convex_primitive [OF _ _ Cauchy_theorem_triangle_cofinite])
  2833 apply (rule contour_integral_convex_primitive [OF _ _ Cauchy_theorem_triangle_cofinite])
  2834 prefer 3
  2834 prefer 3
  2835 apply (erule continuous_on_subset)
  2835 apply (erule continuous_on_subset)
  2836 apply (simp add: subset_hull continuous_on_subset, assumption+)
  2836 apply (simp add: subset_hull continuous_on_subset, assumption+)
  2837 by (metis Diff_iff convex_contains_segment insert_absorb insert_subset interior_mono segment_convex_hull subset_hull)
  2837 by (metis Diff_iff convex_contains_segment insert_absorb insert_subset interior_mono segment_convex_hull subset_hull)
       
  2838 
       
  2839 lemma holomorphic_convex_primitive':
       
  2840   fixes f :: "complex \<Rightarrow> complex"
       
  2841   assumes "convex s" and "open s" and "f holomorphic_on s"
       
  2842   shows   "\<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x within s)"
       
  2843 proof (rule holomorphic_convex_primitive)
       
  2844   fix x assume "x \<in> interior s - {}"
       
  2845   with assms show "f field_differentiable at x"
       
  2846     by (auto intro!: holomorphic_on_imp_differentiable_at simp: interior_open)
       
  2847 qed (insert assms, auto intro: holomorphic_on_imp_continuous_on)
  2838 
  2848 
  2839 lemma Cauchy_theorem_convex:
  2849 lemma Cauchy_theorem_convex:
  2840     "\<lbrakk>continuous_on s f; convex s; finite k;
  2850     "\<lbrakk>continuous_on s f; convex s; finite k;
  2841       \<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x;
  2851       \<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x;
  2842      valid_path g; path_image g \<subseteq> s;
  2852      valid_path g; path_image g \<subseteq> s;
  7546 apply (simp add: simply_connected_eq_contractible_path)
  7556 apply (simp add: simply_connected_eq_contractible_path)
  7547 apply (auto intro!: Cauchy_theorem_null_homotopic [where a = "pathstart g"]
  7557 apply (auto intro!: Cauchy_theorem_null_homotopic [where a = "pathstart g"]
  7548                          homotopic_paths_imp_homotopic_loops)
  7558                          homotopic_paths_imp_homotopic_loops)
  7549 using valid_path_imp_path by blast
  7559 using valid_path_imp_path by blast
  7550 
  7560 
       
  7561 lemma holomorphic_logarithm_exists:
       
  7562   assumes A: "convex A" "open A" 
       
  7563       and f: "f holomorphic_on A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
       
  7564       and z0: "z0 \<in> A"
       
  7565     obtains g where "g holomorphic_on A" and "\<And>x. x \<in> A \<Longrightarrow> exp (g x) = f x"
       
  7566 proof -
       
  7567   note f' = holomorphic_derivI [OF f(1) A(2)]
       
  7568   from A have "\<exists>g. \<forall>x\<in>A. (g has_field_derivative (deriv f x / f x)) (at x within A)"
       
  7569     by (intro holomorphic_convex_primitive' holomorphic_intros f) auto
       
  7570   then obtain g where g: "\<And>x. x \<in> A \<Longrightarrow> (g has_field_derivative deriv f x / f x) (at x)"
       
  7571     using A by (auto simp: at_within_open[of _ A])
       
  7572 
       
  7573   define h where "h = (\<lambda>x. -g z0 + ln (f z0) + g x)"
       
  7574   from g and A have g_holo: "g holomorphic_on A"
       
  7575     by (auto simp: holomorphic_on_def at_within_open[of _ A] field_differentiable_def)
       
  7576   hence h_holo: "h holomorphic_on A"
       
  7577     by (auto simp: h_def intro!: holomorphic_intros)
       
  7578   have "\<exists>c. \<forall>x\<in>A. f x / exp (h x) - 1 = c"
       
  7579   proof (rule DERIV_zero_constant, goal_cases)
       
  7580     case (2 x)
       
  7581     note [simp] = at_within_open[OF _ \<open>open A\<close>]
       
  7582     from 2 and z0 and f show ?case
       
  7583       by (auto simp: h_def exp_diff field_simps intro!: derivative_eq_intros g f')
       
  7584   qed fact+
       
  7585 
       
  7586   then obtain c where c: "\<And>x. x \<in> A \<Longrightarrow> f x / exp (h x) - 1 = c"
       
  7587     by blast
       
  7588   from c[OF z0] and z0 and f have "c = 0"
       
  7589     by (simp add: h_def)
       
  7590   with c have "\<And>x. x \<in> A \<Longrightarrow> exp (h x) = f x" by simp
       
  7591   from that[OF h_holo this] show ?thesis .
       
  7592 qed
       
  7593 
  7551 end
  7594 end