src/HOL/Analysis/Cauchy_Integral_Theorem.thy
 changeset 67107 cef76a19125e parent 66884 c2128ab11f61 child 67237 1fe0ec14a90a
equal 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`