Existence of a holomorphic logarithm
authoreberlm <eberlm@in.tum.de>
Thu Nov 30 16:59:59 2017 +0100 (7 weeks ago)
changeset 67107cef76a19125e
parent 67106 66fda545327f
child 67108 6b350c594ae3
Existence of a holomorphic logarithm
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Nov 29 10:32:42 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Nov 30 16:59:59 2017 +0100
     1.3 @@ -2836,6 +2836,16 @@
     1.4  apply (simp add: subset_hull continuous_on_subset, assumption+)
     1.5  by (metis Diff_iff convex_contains_segment insert_absorb insert_subset interior_mono segment_convex_hull subset_hull)
     1.6  
     1.7 +lemma holomorphic_convex_primitive':
     1.8 +  fixes f :: "complex \<Rightarrow> complex"
     1.9 +  assumes "convex s" and "open s" and "f holomorphic_on s"
    1.10 +  shows   "\<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x within s)"
    1.11 +proof (rule holomorphic_convex_primitive)
    1.12 +  fix x assume "x \<in> interior s - {}"
    1.13 +  with assms show "f field_differentiable at x"
    1.14 +    by (auto intro!: holomorphic_on_imp_differentiable_at simp: interior_open)
    1.15 +qed (insert assms, auto intro: holomorphic_on_imp_continuous_on)
    1.16 +
    1.17  lemma Cauchy_theorem_convex:
    1.18      "\<lbrakk>continuous_on s f; convex s; finite k;
    1.19        \<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x;
    1.20 @@ -7548,4 +7558,37 @@
    1.21                           homotopic_paths_imp_homotopic_loops)
    1.22  using valid_path_imp_path by blast
    1.23  
    1.24 +lemma holomorphic_logarithm_exists:
    1.25 +  assumes A: "convex A" "open A" 
    1.26 +      and f: "f holomorphic_on A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
    1.27 +      and z0: "z0 \<in> A"
    1.28 +    obtains g where "g holomorphic_on A" and "\<And>x. x \<in> A \<Longrightarrow> exp (g x) = f x"
    1.29 +proof -
    1.30 +  note f' = holomorphic_derivI [OF f(1) A(2)]
    1.31 +  from A have "\<exists>g. \<forall>x\<in>A. (g has_field_derivative (deriv f x / f x)) (at x within A)"
    1.32 +    by (intro holomorphic_convex_primitive' holomorphic_intros f) auto
    1.33 +  then obtain g where g: "\<And>x. x \<in> A \<Longrightarrow> (g has_field_derivative deriv f x / f x) (at x)"
    1.34 +    using A by (auto simp: at_within_open[of _ A])
    1.35 +
    1.36 +  define h where "h = (\<lambda>x. -g z0 + ln (f z0) + g x)"
    1.37 +  from g and A have g_holo: "g holomorphic_on A"
    1.38 +    by (auto simp: holomorphic_on_def at_within_open[of _ A] field_differentiable_def)
    1.39 +  hence h_holo: "h holomorphic_on A"
    1.40 +    by (auto simp: h_def intro!: holomorphic_intros)
    1.41 +  have "\<exists>c. \<forall>x\<in>A. f x / exp (h x) - 1 = c"
    1.42 +  proof (rule DERIV_zero_constant, goal_cases)
    1.43 +    case (2 x)
    1.44 +    note [simp] = at_within_open[OF _ \<open>open A\<close>]
    1.45 +    from 2 and z0 and f show ?case
    1.46 +      by (auto simp: h_def exp_diff field_simps intro!: derivative_eq_intros g f')
    1.47 +  qed fact+
    1.48 +
    1.49 +  then obtain c where c: "\<And>x. x \<in> A \<Longrightarrow> f x / exp (h x) - 1 = c"
    1.50 +    by blast
    1.51 +  from c[OF z0] and z0 and f have "c = 0"
    1.52 +    by (simp add: h_def)
    1.53 +  with c have "\<And>x. x \<in> A \<Longrightarrow> exp (h x) = f x" by simp
    1.54 +  from that[OF h_holo this] show ?thesis .
    1.55 +qed
    1.56 +
    1.57  end