# HG changeset patch
# User eberlm
# 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 \ complex"
+ assumes "convex s" and "open s" and "f holomorphic_on s"
+ shows "\g. \x \ s. (g has_field_derivative f x) (at x within s)"
+proof (rule holomorphic_convex_primitive)
+ fix x assume "x \ 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:
"\continuous_on s f; convex s; finite k;
\x. x \ interior s - k \ 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" "\x. x \ A \ f x \ 0"
+ and z0: "z0 \ A"
+ obtains g where "g holomorphic_on A" and "\x. x \ A \ exp (g x) = f x"
+proof -
+ note f' = holomorphic_derivI [OF f(1) A(2)]
+ from A have "\g. \x\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: "\x. x \ A \ (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 = (\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 "\c. \x\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 A\]
+ 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: "\x. x \ A \ 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 "\x. x \ A \ exp (h x) = f x" by simp
+ from that[OF h_holo this] show ?thesis .
+qed
+
end