# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1512057599 -3600
# Node ID cef76a19125ef194bd184854e78e1637f796351d
# Parent  66fda545327f6dec31b50346677b4d223673c8d0
Existence of a holomorphic logarithm

diff -r 66fda545327f -r cef76a19125e src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Nov 29 10:32:42 2017 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Nov 30 16:59:59 2017 +0100
@@ -2836,6 +2836,16 @@
 apply (simp add: subset_hull continuous_on_subset, assumption+)
 by (metis Diff_iff convex_contains_segment insert_absorb insert_subset interior_mono segment_convex_hull subset_hull)
 
+lemma holomorphic_convex_primitive':
+  fixes f :: "complex \<Rightarrow> complex"
+  assumes "convex s" and "open s" and "f holomorphic_on s"
+  shows   "\<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x within s)"
+proof (rule holomorphic_convex_primitive)
+  fix x assume "x \<in> interior s - {}"
+  with assms show "f field_differentiable at x"
+    by (auto intro!: holomorphic_on_imp_differentiable_at simp: interior_open)
+qed (insert assms, auto intro: holomorphic_on_imp_continuous_on)
+
 lemma Cauchy_theorem_convex:
     "\<lbrakk>continuous_on s f; convex s; finite k;
       \<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x;
@@ -7548,4 +7558,37 @@
                          homotopic_paths_imp_homotopic_loops)
 using valid_path_imp_path by blast
 
+lemma holomorphic_logarithm_exists:
+  assumes A: "convex A" "open A" 
+      and f: "f holomorphic_on A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
+      and z0: "z0 \<in> A"
+    obtains g where "g holomorphic_on A" and "\<And>x. x \<in> A \<Longrightarrow> exp (g x) = f x"
+proof -
+  note f' = holomorphic_derivI [OF f(1) A(2)]
+  from A have "\<exists>g. \<forall>x\<in>A. (g has_field_derivative (deriv f x / f x)) (at x within A)"
+    by (intro holomorphic_convex_primitive' holomorphic_intros f) auto
+  then obtain g where g: "\<And>x. x \<in> A \<Longrightarrow> (g has_field_derivative deriv f x / f x) (at x)"
+    using A by (auto simp: at_within_open[of _ A])
+
+  define h where "h = (\<lambda>x. -g z0 + ln (f z0) + g x)"
+  from g and A have g_holo: "g holomorphic_on A"
+    by (auto simp: holomorphic_on_def at_within_open[of _ A] field_differentiable_def)
+  hence h_holo: "h holomorphic_on A"
+    by (auto simp: h_def intro!: holomorphic_intros)
+  have "\<exists>c. \<forall>x\<in>A. f x / exp (h x) - 1 = c"
+  proof (rule DERIV_zero_constant, goal_cases)
+    case (2 x)
+    note [simp] = at_within_open[OF _ \<open>open A\<close>]
+    from 2 and z0 and f show ?case
+      by (auto simp: h_def exp_diff field_simps intro!: derivative_eq_intros g f')
+  qed fact+
+
+  then obtain c where c: "\<And>x. x \<in> A \<Longrightarrow> f x / exp (h x) - 1 = c"
+    by blast
+  from c[OF z0] and z0 and f have "c = 0"
+    by (simp add: h_def)
+  with c have "\<And>x. x \<in> A \<Longrightarrow> exp (h x) = f x" by simp
+  from that[OF h_holo this] show ?thesis .
+qed
+
 end