section \<open>The Residue Theorem, the Argument Principle and Rouch\'{e}'s Theorem\<close>
theory Residue_Theorem
imports Complex_Residues "HOL-Library.Landau_Symbols"
begin
subsection \<open>Cauchy's residue theorem\<close>
lemma get_integrable_path:
assumes "open s" "connected (s-pts)" "finite pts" "f holomorphic_on (s-pts) " "a\<in>s-pts" "b\<in>s-pts"
obtains g where "valid_path g" "pathstart g = a" "pathfinish g = b"
"path_image g \<subseteq> s-pts" "f contour_integrable_on g" using assms
proof (induct arbitrary:s thesis a rule:finite_induct[OF \<open>finite pts\<close>])
case 1
obtain g where "valid_path g" "path_image g \<subseteq> s" "pathstart g = a" "pathfinish g = b"
using connected_open_polynomial_connected[OF \<open>open s\<close>,of a b ] \<open>connected (s - {})\<close>
valid_path_polynomial_function "1.prems"(6) "1.prems"(7) by auto
moreover have "f contour_integrable_on g"
using contour_integrable_holomorphic_simple[OF _ \<open>open s\<close> \<open>valid_path g\<close> \<open>path_image g \<subseteq> s\<close>,of f]
\<open>f holomorphic_on s - {}\<close>
by auto
ultimately show ?case using "1"(1)[of g] by auto
next
case idt:(2 p pts)
obtain e where "e>0" and e:"\<forall>w\<in>ball a e. w \<in> s \<and> (w \<noteq> a \<longrightarrow> w \<notin> insert p pts)"
using finite_ball_avoid[OF \<open>open s\<close> \<open>finite (insert p pts)\<close>, of a]
\<open>a \<in> s - insert p pts\<close>
by auto
define a' where "a' \<equiv> a+e/2"
have "a'\<in>s-{p} -pts" using e[rule_format,of "a+e/2"] \<open>e>0\<close>
by (auto simp add:dist_complex_def a'_def)
then obtain g' where g'[simp]:"valid_path g'" "pathstart g' = a'" "pathfinish g' = b"
"path_image g' \<subseteq> s - {p} - pts" "f contour_integrable_on g'"
using idt.hyps(3)[of a' "s-{p}"] idt.prems idt.hyps(1)
by (metis Diff_insert2 open_delete)
define g where "g \<equiv> linepath a a' +++ g'"
have "valid_path g" unfolding g_def by (auto intro: valid_path_join)
moreover have "pathstart g = a" and "pathfinish g = b" unfolding g_def by auto
moreover have "path_image g \<subseteq> s - insert p pts" unfolding g_def
proof (rule subset_path_image_join)
have "closed_segment a a' \<subseteq> ball a e" using \<open>e>0\<close>
by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute)
then show "path_image (linepath a a') \<subseteq> s - insert p pts" using e idt(9)
by auto
next
show "path_image g' \<subseteq> s - insert p pts" using g'(4) by blast
qed
moreover have "f contour_integrable_on g"
proof -
have "closed_segment a a' \<subseteq> ball a e" using \<open>e>0\<close>
by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute)
then have "continuous_on (closed_segment a a') f"
using e idt.prems(6) holomorphic_on_imp_continuous_on[OF idt.prems(5)]
apply (elim continuous_on_subset)
by auto
then have "f contour_integrable_on linepath a a'"
using contour_integrable_continuous_linepath by auto
then show ?thesis unfolding g_def
apply (rule contour_integrable_joinI)
by (auto simp add: \<open>e>0\<close>)
qed
ultimately show ?case using idt.prems(1)[of g] by auto
qed
lemma Cauchy_theorem_aux:
assumes "open s" "connected (s-pts)" "finite pts" "pts \<subseteq> s" "f holomorphic_on s-pts"
"valid_path g" "pathfinish g = pathstart g" "path_image g \<subseteq> s-pts"
"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z = 0"
"\<forall>p\<in>s. h p>0 \<and> (\<forall>w\<in>cball p (h p). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w \<notin> pts))"
shows "contour_integral g f = (\<Sum>p\<in>pts. winding_number g p * contour_integral (circlepath p (h p)) f)"
using assms
proof (induct arbitrary:s g rule:finite_induct[OF \<open>finite pts\<close>])
case 1
then show ?case by (simp add: Cauchy_theorem_global contour_integral_unique)
next
case (2 p pts)
note fin[simp] = \<open>finite (insert p pts)\<close>
and connected = \<open>connected (s - insert p pts)\<close>
and valid[simp] = \<open>valid_path g\<close>
and g_loop[simp] = \<open>pathfinish g = pathstart g\<close>
and holo[simp]= \<open>f holomorphic_on s - insert p pts\<close>
and path_img = \<open>path_image g \<subseteq> s - insert p pts\<close>
and winding = \<open>\<forall>z. z \<notin> s \<longrightarrow> winding_number g z = 0\<close>
and h = \<open>\<forall>pa\<in>s. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s \<and> (w \<noteq> pa \<longrightarrow> w \<notin> insert p pts))\<close>
have "h p>0" and "p\<in>s"
and h_p: "\<forall>w\<in>cball p (h p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> insert p pts)"
using h \<open>insert p pts \<subseteq> s\<close> by auto
obtain pg where pg[simp]: "valid_path pg" "pathstart pg = pathstart g" "pathfinish pg=p+h p"
"path_image pg \<subseteq> s-insert p pts" "f contour_integrable_on pg"
proof -
have "p + h p\<in>cball p (h p)" using h[rule_format,of p]
by (simp add: \<open>p \<in> s\<close> dist_norm)
then have "p + h p \<in> s - insert p pts" using h[rule_format,of p] \<open>insert p pts \<subseteq> s\<close>
by fastforce
moreover have "pathstart g \<in> s - insert p pts " using path_img by auto
ultimately show ?thesis
using get_integrable_path[OF \<open>open s\<close> connected fin holo,of "pathstart g" "p+h p"] that
by blast
qed
obtain n::int where "n=winding_number g p"
using integer_winding_number[OF _ g_loop,of p] valid path_img
by (metis DiffD2 Ints_cases insertI1 subset_eq valid_path_imp_path)
define p_circ where "p_circ \<equiv> circlepath p (h p)"
define p_circ_pt where "p_circ_pt \<equiv> linepath (p+h p) (p+h p)"
define n_circ where "n_circ \<equiv> \<lambda>n. ((+++) p_circ ^^ n) p_circ_pt"
define cp where "cp \<equiv> if n\<ge>0 then reversepath (n_circ (nat n)) else n_circ (nat (- n))"
have n_circ:"valid_path (n_circ k)"
"winding_number (n_circ k) p = k"
"pathstart (n_circ k) = p + h p" "pathfinish (n_circ k) = p + h p"
"path_image (n_circ k) = (if k=0 then {p + h p} else sphere p (h p))"
"p \<notin> path_image (n_circ k)"
"\<And>p'. p'\<notin>s - pts \<Longrightarrow> winding_number (n_circ k) p'=0 \<and> p'\<notin>path_image (n_circ k)"
"f contour_integrable_on (n_circ k)"
"contour_integral (n_circ k) f = k * contour_integral p_circ f"
for k
proof (induct k)
case 0
show "valid_path (n_circ 0)"
and "path_image (n_circ 0) = (if 0=0 then {p + h p} else sphere p (h p))"
and "winding_number (n_circ 0) p = of_nat 0"
and "pathstart (n_circ 0) = p + h p"
and "pathfinish (n_circ 0) = p + h p"
and "p \<notin> path_image (n_circ 0)"
unfolding n_circ_def p_circ_pt_def using \<open>h p > 0\<close>
by (auto simp add: dist_norm)
show "winding_number (n_circ 0) p'=0 \<and> p'\<notin>path_image (n_circ 0)" when "p'\<notin>s- pts" for p'
unfolding n_circ_def p_circ_pt_def
apply (auto intro!:winding_number_trivial)
by (metis Diff_iff pathfinish_in_path_image pg(3) pg(4) subsetCE subset_insertI that)+
show "f contour_integrable_on (n_circ 0)"
unfolding n_circ_def p_circ_pt_def
by (auto intro!:contour_integrable_continuous_linepath simp add:continuous_on_sing)
show "contour_integral (n_circ 0) f = of_nat 0 * contour_integral p_circ f"
unfolding n_circ_def p_circ_pt_def by auto
next
case (Suc k)
have n_Suc:"n_circ (Suc k) = p_circ +++ n_circ k" unfolding n_circ_def by auto
have pcirc:"p \<notin> path_image p_circ" "valid_path p_circ" "pathfinish p_circ = pathstart (n_circ k)"
using Suc(3) unfolding p_circ_def using \<open>h p > 0\<close> by (auto simp add: p_circ_def)
have pcirc_image:"path_image p_circ \<subseteq> s - insert p pts"
proof -
have "path_image p_circ \<subseteq> cball p (h p)" using \<open>0 < h p\<close> p_circ_def by auto
then show ?thesis using h_p pcirc(1) by auto
qed
have pcirc_integrable:"f contour_integrable_on p_circ"
by (auto simp add:p_circ_def intro!: pcirc_image[unfolded p_circ_def]
contour_integrable_continuous_circlepath holomorphic_on_imp_continuous_on
holomorphic_on_subset[OF holo])
show "valid_path (n_circ (Suc k))"
using valid_path_join[OF pcirc(2) Suc(1) pcirc(3)] unfolding n_circ_def by auto
show "path_image (n_circ (Suc k))
= (if Suc k = 0 then {p + complex_of_real (h p)} else sphere p (h p))"
proof -
have "path_image p_circ = sphere p (h p)"
unfolding p_circ_def using \<open>0 < h p\<close> by auto
then show ?thesis unfolding n_Suc using Suc.hyps(5) \<open>h p>0\<close>
by (auto simp add: path_image_join[OF pcirc(3)] dist_norm)
qed
then show "p \<notin> path_image (n_circ (Suc k))" using \<open>h p>0\<close> by auto
show "winding_number (n_circ (Suc k)) p = of_nat (Suc k)"
proof -
have "winding_number p_circ p = 1"
by (simp add: \<open>h p > 0\<close> p_circ_def winding_number_circlepath_centre)
moreover have "p \<notin> path_image (n_circ k)" using Suc(5) \<open>h p>0\<close> by auto
then have "winding_number (p_circ +++ n_circ k) p
= winding_number p_circ p + winding_number (n_circ k) p"
using valid_path_imp_path Suc.hyps(1) Suc.hyps(2) pcirc
apply (intro winding_number_join)
by auto
ultimately show ?thesis using Suc(2) unfolding n_circ_def
by auto
qed
show "pathstart (n_circ (Suc k)) = p + h p"
by (simp add: n_circ_def p_circ_def)
show "pathfinish (n_circ (Suc k)) = p + h p"
using Suc(4) unfolding n_circ_def by auto
show "winding_number (n_circ (Suc k)) p'=0 \<and> p'\<notin>path_image (n_circ (Suc k))" when "p'\<notin>s-pts" for p'
proof -
have " p' \<notin> path_image p_circ" using \<open>p \<in> s\<close> h p_circ_def that using pcirc_image by blast
moreover have "p' \<notin> path_image (n_circ k)"
using Suc.hyps(7) that by blast
moreover have "winding_number p_circ p' = 0"
proof -
have "path_image p_circ \<subseteq> cball p (h p)"
using h unfolding p_circ_def using \<open>p \<in> s\<close> by fastforce
moreover have "p'\<notin>cball p (h p)" using \<open>p \<in> s\<close> h that "2.hyps"(2) by fastforce
ultimately show ?thesis unfolding p_circ_def
apply (intro winding_number_zero_outside)
by auto
qed
ultimately show ?thesis
unfolding n_Suc
apply (subst winding_number_join)
by (auto simp: valid_path_imp_path pcirc Suc that not_in_path_image_join Suc.hyps(7)[OF that])
qed
show "f contour_integrable_on (n_circ (Suc k))"
unfolding n_Suc
by (rule contour_integrable_joinI[OF pcirc_integrable Suc(8) pcirc(2) Suc(1)])
show "contour_integral (n_circ (Suc k)) f = (Suc k) * contour_integral p_circ f"
unfolding n_Suc
by (auto simp add:contour_integral_join[OF pcirc_integrable Suc(8) pcirc(2) Suc(1)]
Suc(9) algebra_simps)
qed
have cp[simp]:"pathstart cp = p + h p" "pathfinish cp = p + h p"
"valid_path cp" "path_image cp \<subseteq> s - insert p pts"
"winding_number cp p = - n"
"\<And>p'. p'\<notin>s - pts \<Longrightarrow> winding_number cp p'=0 \<and> p' \<notin> path_image cp"
"f contour_integrable_on cp"
"contour_integral cp f = - n * contour_integral p_circ f"
proof -
show "pathstart cp = p + h p" and "pathfinish cp = p + h p" and "valid_path cp"
using n_circ unfolding cp_def by auto
next
have "sphere p (h p) \<subseteq> s - insert p pts"
using h[rule_format,of p] \<open>insert p pts \<subseteq> s\<close> by force
moreover have "p + complex_of_real (h p) \<in> s - insert p pts"
using pg(3) pg(4) by (metis pathfinish_in_path_image subsetCE)
ultimately show "path_image cp \<subseteq> s - insert p pts" unfolding cp_def
using n_circ(5) by auto
next
show "winding_number cp p = - n"
unfolding cp_def using winding_number_reversepath n_circ \<open>h p>0\<close>
by (auto simp: valid_path_imp_path)
next
show "winding_number cp p'=0 \<and> p' \<notin> path_image cp" when "p'\<notin>s - pts" for p'
unfolding cp_def
apply (auto)
apply (subst winding_number_reversepath)
by (auto simp add: valid_path_imp_path n_circ(7)[OF that] n_circ(1))
next
show "f contour_integrable_on cp" unfolding cp_def
using contour_integrable_reversepath_eq n_circ(1,8) by auto
next
show "contour_integral cp f = - n * contour_integral p_circ f"
unfolding cp_def using contour_integral_reversepath[OF n_circ(1)] n_circ(9)
by auto
qed
define g' where "g' \<equiv> g +++ pg +++ cp +++ (reversepath pg)"
have "contour_integral g' f = (\<Sum>p\<in>pts. winding_number g' p * contour_integral (circlepath p (h p)) f)"
proof (rule "2.hyps"(3)[of "s-{p}" "g'",OF _ _ \<open>finite pts\<close> ])
show "connected (s - {p} - pts)" using connected by (metis Diff_insert2)
show "open (s - {p})" using \<open>open s\<close> by auto
show " pts \<subseteq> s - {p}" using \<open>insert p pts \<subseteq> s\<close> \<open> p \<notin> pts\<close> by blast
show "f holomorphic_on s - {p} - pts" using holo \<open>p \<notin> pts\<close> by (metis Diff_insert2)
show "valid_path g'"
unfolding g'_def cp_def using n_circ valid pg g_loop
by (auto intro!:valid_path_join )
show "pathfinish g' = pathstart g'"
unfolding g'_def cp_def using pg(2) by simp
show "path_image g' \<subseteq> s - {p} - pts"
proof -
define s' where "s' \<equiv> s - {p} - pts"
have s':"s' = s-insert p pts " unfolding s'_def by auto
then show ?thesis using path_img pg(4) cp(4)
unfolding g'_def
apply (fold s'_def s')
apply (intro subset_path_image_join)
by auto
qed
note path_join_imp[simp]
show "\<forall>z. z \<notin> s - {p} \<longrightarrow> winding_number g' z = 0"
proof clarify
fix z assume z:"z\<notin>s - {p}"
have "winding_number (g +++ pg +++ cp +++ reversepath pg) z = winding_number g z
+ winding_number (pg +++ cp +++ (reversepath pg)) z"
proof (rule winding_number_join)
show "path g" using \<open>valid_path g\<close> by (simp add: valid_path_imp_path)
show "z \<notin> path_image g" using z path_img by auto
show "path (pg +++ cp +++ reversepath pg)" using pg(3) cp
by (simp add: valid_path_imp_path)
next
have "path_image (pg +++ cp +++ reversepath pg) \<subseteq> s - insert p pts"
using pg(4) cp(4) by (auto simp:subset_path_image_join)
then show "z \<notin> path_image (pg +++ cp +++ reversepath pg)" using z by auto
next
show "pathfinish g = pathstart (pg +++ cp +++ reversepath pg)" using g_loop by auto
qed
also have "... = winding_number g z + (winding_number pg z
+ winding_number (cp +++ (reversepath pg)) z)"
proof (subst add_left_cancel,rule winding_number_join)
show "path pg" and "path (cp +++ reversepath pg)"
and "pathfinish pg = pathstart (cp +++ reversepath pg)"
by (auto simp add: valid_path_imp_path)
show "z \<notin> path_image pg" using pg(4) z by blast
show "z \<notin> path_image (cp +++ reversepath pg)" using z
by (metis Diff_iff \<open>z \<notin> path_image pg\<close> contra_subsetD cp(4) insertI1
not_in_path_image_join path_image_reversepath singletonD)
qed
also have "... = winding_number g z + (winding_number pg z
+ (winding_number cp z + winding_number (reversepath pg) z))"
apply (auto intro!:winding_number_join simp: valid_path_imp_path)
apply (metis Diff_iff contra_subsetD cp(4) insertI1 singletonD z)
by (metis Diff_insert2 Diff_subset contra_subsetD pg(4) z)
also have "... = winding_number g z + winding_number cp z"
apply (subst winding_number_reversepath)
apply (auto simp: valid_path_imp_path)
by (metis Diff_iff contra_subsetD insertI1 pg(4) singletonD z)
finally have "winding_number g' z = winding_number g z + winding_number cp z"
unfolding g'_def .
moreover have "winding_number g z + winding_number cp z = 0"
using winding z \<open>n=winding_number g p\<close> by auto
ultimately show "winding_number g' z = 0" unfolding g'_def by auto
qed
show "\<forall>pa\<in>s - {p}. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s - {p} \<and> (w \<noteq> pa \<longrightarrow> w \<notin> pts))"
using h by fastforce
qed
moreover have "contour_integral g' f = contour_integral g f
- winding_number g p * contour_integral p_circ f"
proof -
have "contour_integral g' f = contour_integral g f
+ contour_integral (pg +++ cp +++ reversepath pg) f"
unfolding g'_def
apply (subst contour_integral_join)
by (auto simp add:open_Diff[OF \<open>open s\<close>,OF finite_imp_closed[OF fin]]
intro!: contour_integrable_holomorphic_simple[OF holo _ _ path_img]
contour_integrable_reversepath)
also have "... = contour_integral g f + contour_integral pg f
+ contour_integral (cp +++ reversepath pg) f"
apply (subst contour_integral_join)
by (auto simp add:contour_integrable_reversepath)
also have "... = contour_integral g f + contour_integral pg f
+ contour_integral cp f + contour_integral (reversepath pg) f"
apply (subst contour_integral_join)
by (auto simp add:contour_integrable_reversepath)
also have "... = contour_integral g f + contour_integral cp f"
using contour_integral_reversepath
by (auto simp add:contour_integrable_reversepath)
also have "... = contour_integral g f - winding_number g p * contour_integral p_circ f"
using \<open>n=winding_number g p\<close> by auto
finally show ?thesis .
qed
moreover have "winding_number g' p' = winding_number g p'" when "p'\<in>pts" for p'
proof -
have [simp]: "p' \<notin> path_image g" "p' \<notin> path_image pg" "p'\<notin>path_image cp"
using "2.prems"(8) that
apply blast
apply (metis Diff_iff Diff_insert2 contra_subsetD pg(4) that)
by (meson DiffD2 cp(4) rev_subsetD subset_insertI that)
have "winding_number g' p' = winding_number g p'
+ winding_number (pg +++ cp +++ reversepath pg) p'" unfolding g'_def
apply (subst winding_number_join)
apply (simp_all add: valid_path_imp_path)
apply (intro not_in_path_image_join)
by auto
also have "... = winding_number g p' + winding_number pg p'
+ winding_number (cp +++ reversepath pg) p'"
apply (subst winding_number_join)
apply (simp_all add: valid_path_imp_path)
apply (intro not_in_path_image_join)
by auto
also have "... = winding_number g p' + winding_number pg p'+ winding_number cp p'
+ winding_number (reversepath pg) p'"
apply (subst winding_number_join)
by (simp_all add: valid_path_imp_path)
also have "... = winding_number g p' + winding_number cp p'"
apply (subst winding_number_reversepath)
by (simp_all add: valid_path_imp_path)
also have "... = winding_number g p'" using that by auto
finally show ?thesis .
qed
ultimately show ?case unfolding p_circ_def
apply (subst (asm) sum.cong[OF refl,
of pts _ "\<lambda>p. winding_number g p * contour_integral (circlepath p (h p)) f"])
by (auto simp add:sum.insert[OF \<open>finite pts\<close> \<open>p\<notin>pts\<close>] algebra_simps)
qed
lemma Cauchy_theorem_singularities:
assumes "open s" "connected s" "finite pts" and
holo:"f holomorphic_on s-pts" and
"valid_path g" and
loop:"pathfinish g = pathstart g" and
"path_image g \<subseteq> s-pts" and
homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z = 0" and
avoid:"\<forall>p\<in>s. h p>0 \<and> (\<forall>w\<in>cball p (h p). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w \<notin> pts))"
shows "contour_integral g f = (\<Sum>p\<in>pts. winding_number g p * contour_integral (circlepath p (h p)) f)"
(is "?L=?R")
proof -
define circ where "circ \<equiv> \<lambda>p. winding_number g p * contour_integral (circlepath p (h p)) f"
define pts1 where "pts1 \<equiv> pts \<inter> s"
define pts2 where "pts2 \<equiv> pts - pts1"
have "pts=pts1 \<union> pts2" "pts1 \<inter> pts2 = {}" "pts2 \<inter> s={}" "pts1\<subseteq>s"
unfolding pts1_def pts2_def by auto
have "contour_integral g f = (\<Sum>p\<in>pts1. circ p)" unfolding circ_def
proof (rule Cauchy_theorem_aux[OF \<open>open s\<close> _ _ \<open>pts1\<subseteq>s\<close> _ \<open>valid_path g\<close> loop _ homo])
have "finite pts1" unfolding pts1_def using \<open>finite pts\<close> by auto
then show "connected (s - pts1)"
using \<open>open s\<close> \<open>connected s\<close> connected_open_delete_finite[of s] by auto
next
show "finite pts1" using \<open>pts = pts1 \<union> pts2\<close> assms(3) by auto
show "f holomorphic_on s - pts1" by (metis Diff_Int2 Int_absorb holo pts1_def)
show "path_image g \<subseteq> s - pts1" using assms(7) pts1_def by auto
show "\<forall>p\<in>s. 0 < h p \<and> (\<forall>w\<in>cball p (h p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts1))"
by (simp add: avoid pts1_def)
qed
moreover have "sum circ pts2=0"
proof -
have "winding_number g p=0" when "p\<in>pts2" for p
using \<open>pts2 \<inter> s={}\<close> that homo[rule_format,of p] by auto
thus ?thesis unfolding circ_def
apply (intro sum.neutral)
by auto
qed
moreover have "?R=sum circ pts1 + sum circ pts2"
unfolding circ_def
using sum.union_disjoint[OF _ _ \<open>pts1 \<inter> pts2 = {}\<close>] \<open>finite pts\<close> \<open>pts=pts1 \<union> pts2\<close>
by blast
ultimately show ?thesis
apply (fold circ_def)
by auto
qed
theorem Residue_theorem:
fixes s pts::"complex set" and f::"complex \<Rightarrow> complex"
and g::"real \<Rightarrow> complex"
assumes "open s" "connected s" "finite pts" and
holo:"f holomorphic_on s-pts" and
"valid_path g" and
loop:"pathfinish g = pathstart g" and
"path_image g \<subseteq> s-pts" and
homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z = 0"
shows "contour_integral g f = 2 * pi * \<i> *(\<Sum>p\<in>pts. winding_number g p * residue f p)"
proof -
define c where "c \<equiv> 2 * pi * \<i>"
obtain h where avoid:"\<forall>p\<in>s. h p>0 \<and> (\<forall>w\<in>cball p (h p). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w \<notin> pts))"
using finite_cball_avoid[OF \<open>open s\<close> \<open>finite pts\<close>] by metis
have "contour_integral g f
= (\<Sum>p\<in>pts. winding_number g p * contour_integral (circlepath p (h p)) f)"
using Cauchy_theorem_singularities[OF assms avoid] .
also have "... = (\<Sum>p\<in>pts. c * winding_number g p * residue f p)"
proof (intro sum.cong)
show "pts = pts" by simp
next
fix x assume "x \<in> pts"
show "winding_number g x * contour_integral (circlepath x (h x)) f
= c * winding_number g x * residue f x"
proof (cases "x\<in>s")
case False
then have "winding_number g x=0" using homo by auto
thus ?thesis by auto
next
case True
have "contour_integral (circlepath x (h x)) f = c* residue f x"
using \<open>x\<in>pts\<close> \<open>finite pts\<close> avoid[rule_format,OF True]
apply (intro base_residue[of "s-(pts-{x})",THEN contour_integral_unique,folded c_def])
by (auto intro:holomorphic_on_subset[OF holo] open_Diff[OF \<open>open s\<close> finite_imp_closed])
then show ?thesis by auto
qed
qed
also have "... = c * (\<Sum>p\<in>pts. winding_number g p * residue f p)"
by (simp add: sum_distrib_left algebra_simps)
finally show ?thesis unfolding c_def .
qed
subsection \<open>The argument principle\<close>
theorem argument_principle:
fixes f::"complex \<Rightarrow> complex" and poles s:: "complex set"
defines "pz \<equiv> {w. f w = 0 \<or> w \<in> poles}" \<comment> \<open>\<^term>\<open>pz\<close> is the set of poles and zeros\<close>
assumes "open s" and
"connected s" and
f_holo:"f holomorphic_on s-poles" and
h_holo:"h holomorphic_on s" and
"valid_path g" and
loop:"pathfinish g = pathstart g" and
path_img:"path_image g \<subseteq> s - pz" and
homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z = 0" and
finite:"finite pz" and
poles:"\<forall>p\<in>poles. is_pole f p"
shows "contour_integral g (\<lambda>x. deriv f x * h x / f x) = 2 * pi * \<i> *
(\<Sum>p\<in>pz. winding_number g p * h p * zorder f p)"
(is "?L=?R")
proof -
define c where "c \<equiv> 2 * complex_of_real pi * \<i> "
define ff where "ff \<equiv> (\<lambda>x. deriv f x * h x / f x)"
define cont where "cont \<equiv> \<lambda>ff p e. (ff has_contour_integral c * zorder f p * h p ) (circlepath p e)"
define avoid where "avoid \<equiv> \<lambda>p e. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pz)"
have "\<exists>e>0. avoid p e \<and> (p\<in>pz \<longrightarrow> cont ff p e)" when "p\<in>s" for p
proof -
obtain e1 where "e1>0" and e1_avoid:"avoid p e1"
using finite_cball_avoid[OF \<open>open s\<close> finite] \<open>p\<in>s\<close> unfolding avoid_def by auto
have "\<exists>e2>0. cball p e2 \<subseteq> ball p e1 \<and> cont ff p e2" when "p\<in>pz"
proof -
define po where "po \<equiv> zorder f p"
define pp where "pp \<equiv> zor_poly f p"
define f' where "f' \<equiv> \<lambda>w. pp w * (w - p) powr po"
define ff' where "ff' \<equiv> (\<lambda>x. deriv f' x * h x / f' x)"
obtain r where "pp p\<noteq>0" "r>0" and
"r<e1" and
pp_holo:"pp holomorphic_on cball p r" and
pp_po:"(\<forall>w\<in>cball p r-{p}. f w = pp w * (w - p) powr po \<and> pp w \<noteq> 0)"
proof -
have "isolated_singularity_at f p"
proof -
have "f holomorphic_on ball p e1 - {p}"
apply (intro holomorphic_on_subset[OF f_holo])
using e1_avoid \<open>p\<in>pz\<close> unfolding avoid_def pz_def by force
then show ?thesis unfolding isolated_singularity_at_def
using \<open>e1>0\<close> analytic_on_open open_delete by blast
qed
moreover have "not_essential f p"
proof (cases "is_pole f p")
case True
then show ?thesis unfolding not_essential_def by auto
next
case False
then have "p\<in>s-poles" using \<open>p\<in>s\<close> poles unfolding pz_def by auto
moreover have "open (s-poles)"
using \<open>open s\<close>
apply (elim open_Diff)
apply (rule finite_imp_closed)
using finite unfolding pz_def by simp
ultimately have "isCont f p"
using holomorphic_on_imp_continuous_on[OF f_holo] continuous_on_eq_continuous_at
by auto
then show ?thesis unfolding isCont_def not_essential_def by auto
qed
moreover have "\<exists>\<^sub>F w in at p. f w \<noteq> 0 "
proof (rule ccontr)
assume "\<not> (\<exists>\<^sub>F w in at p. f w \<noteq> 0)"
then have "\<forall>\<^sub>F w in at p. f w= 0" unfolding frequently_def by auto
then obtain rr where "rr>0" "\<forall>w\<in>ball p rr - {p}. f w =0"
unfolding eventually_at by (auto simp add:dist_commute)
then have "ball p rr - {p} \<subseteq> {w\<in>ball p rr-{p}. f w=0}" by blast
moreover have "infinite (ball p rr - {p})" using \<open>rr>0\<close> using finite_imp_not_open by fastforce
ultimately have "infinite {w\<in>ball p rr-{p}. f w=0}" using infinite_super by blast
then have "infinite pz"
unfolding pz_def infinite_super by auto
then show False using \<open>finite pz\<close> by auto
qed
ultimately obtain r where "pp p \<noteq> 0" and r:"r>0" "pp holomorphic_on cball p r"
"(\<forall>w\<in>cball p r - {p}. f w = pp w * (w - p) powr of_int po \<and> pp w \<noteq> 0)"
using zorder_exist[of f p,folded po_def pp_def] by auto
define r1 where "r1=min r e1 / 2"
have "r1<e1" unfolding r1_def using \<open>e1>0\<close> \<open>r>0\<close> by auto
moreover have "r1>0" "pp holomorphic_on cball p r1"
"(\<forall>w\<in>cball p r1 - {p}. f w = pp w * (w - p) powr of_int po \<and> pp w \<noteq> 0)"
unfolding r1_def using \<open>e1>0\<close> r by auto
ultimately show ?thesis using that \<open>pp p\<noteq>0\<close> by auto
qed
define e2 where "e2 \<equiv> r/2"
have "e2>0" using \<open>r>0\<close> unfolding e2_def by auto
define anal where "anal \<equiv> \<lambda>w. deriv pp w * h w / pp w"
define prin where "prin \<equiv> \<lambda>w. po * h w / (w - p)"
have "((\<lambda>w. prin w + anal w) has_contour_integral c * po * h p) (circlepath p e2)"
proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified])
have "ball p r \<subseteq> s"
using \<open>r<e1\<close> avoid_def ball_subset_cball e1_avoid by (simp add: subset_eq)
then have "cball p e2 \<subseteq> s"
using \<open>r>0\<close> unfolding e2_def by auto
then have "(\<lambda>w. po * h w) holomorphic_on cball p e2"
using h_holo by (auto intro!: holomorphic_intros)
then show "(prin has_contour_integral c * po * h p ) (circlepath p e2)"
using Cauchy_integral_circlepath_simple[folded c_def, of "\<lambda>w. po * h w"] \<open>e2>0\<close>
unfolding prin_def by (auto simp add: mult.assoc)
have "anal holomorphic_on ball p r" unfolding anal_def
using pp_holo h_holo pp_po \<open>ball p r \<subseteq> s\<close> \<open>pp p\<noteq>0\<close>
by (auto intro!: holomorphic_intros)
then show "(anal has_contour_integral 0) (circlepath p e2)"
using e2_def \<open>r>0\<close>
by (auto elim!: Cauchy_theorem_disc_simple)
qed
then have "cont ff' p e2" unfolding cont_def po_def
proof (elim has_contour_integral_eq)
fix w assume "w \<in> path_image (circlepath p e2)"
then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto
define wp where "wp \<equiv> w-p"
have "wp\<noteq>0" and "pp w \<noteq>0"
unfolding wp_def using \<open>w\<noteq>p\<close> \<open>w\<in>ball p r\<close> pp_po by auto
moreover have der_f':"deriv f' w = po * pp w * (w-p) powr (po - 1) + deriv pp w * (w-p) powr po"
proof (rule DERIV_imp_deriv)
have "(pp has_field_derivative (deriv pp w)) (at w)"
using DERIV_deriv_iff_has_field_derivative pp_holo \<open>w\<noteq>p\<close>
by (meson open_ball \<open>w \<in> ball p r\<close> ball_subset_cball holomorphic_derivI holomorphic_on_subset)
then show " (f' has_field_derivative of_int po * pp w * (w - p) powr of_int (po - 1)
+ deriv pp w * (w - p) powr of_int po) (at w)"
unfolding f'_def using \<open>w\<noteq>p\<close>
by (auto intro!: derivative_eq_intros DERIV_cong[OF has_field_derivative_powr_of_int])
qed
ultimately show "prin w + anal w = ff' w"
unfolding ff'_def prin_def anal_def
apply simp
apply (unfold f'_def)
apply (fold wp_def)
apply (auto simp add:field_simps)
by (metis (no_types, lifting) diff_add_cancel mult.commute powr_add powr_to_1)
qed
then have "cont ff p e2" unfolding cont_def
proof (elim has_contour_integral_eq)
fix w assume "w \<in> path_image (circlepath p e2)"
then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto
have "deriv f' w = deriv f w"
proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"])
show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo
by (auto intro!: holomorphic_intros)
next
have "ball p e1 - {p} \<subseteq> s - poles"
using ball_subset_cball e1_avoid[unfolded avoid_def] unfolding pz_def
by auto
then have "ball p r - {p} \<subseteq> s - poles"
apply (elim dual_order.trans)
using \<open>r<e1\<close> by auto
then show "f holomorphic_on ball p r - {p}" using f_holo
by auto
next
show "open (ball p r - {p})" by auto
show "w \<in> ball p r - {p}" using \<open>w\<in>ball p r\<close> \<open>w\<noteq>p\<close> by auto
next
fix x assume "x \<in> ball p r - {p}"
then show "f' x = f x"
using pp_po unfolding f'_def by auto
qed
moreover have " f' w = f w "
using \<open>w \<in> ball p r\<close> ball_subset_cball subset_iff pp_po \<open>w\<noteq>p\<close>
unfolding f'_def by auto
ultimately show "ff' w = ff w"
unfolding ff'_def ff_def by simp
qed
moreover have "cball p e2 \<subseteq> ball p e1"
using \<open>0 < r\<close> \<open>r<e1\<close> e2_def by auto
ultimately show ?thesis using \<open>e2>0\<close> by auto
qed
then obtain e2 where e2:"p\<in>pz \<longrightarrow> e2>0 \<and> cball p e2 \<subseteq> ball p e1 \<and> cont ff p e2"
by auto
define e4 where "e4 \<equiv> if p\<in>pz then e2 else e1"
have "e4>0" using e2 \<open>e1>0\<close> unfolding e4_def by auto
moreover have "avoid p e4" using e2 \<open>e1>0\<close> e1_avoid unfolding e4_def avoid_def by auto
moreover have "p\<in>pz \<longrightarrow> cont ff p e4"
by (auto simp add: e2 e4_def)
ultimately show ?thesis by auto
qed
then obtain get_e where get_e:"\<forall>p\<in>s. get_e p>0 \<and> avoid p (get_e p)
\<and> (p\<in>pz \<longrightarrow> cont ff p (get_e p))"
by metis
define ci where "ci \<equiv> \<lambda>p. contour_integral (circlepath p (get_e p)) ff"
define w where "w \<equiv> \<lambda>p. winding_number g p"
have "contour_integral g ff = (\<Sum>p\<in>pz. w p * ci p)" unfolding ci_def w_def
proof (rule Cauchy_theorem_singularities[OF \<open>open s\<close> \<open>connected s\<close> finite _ \<open>valid_path g\<close> loop
path_img homo])
have "open (s - pz)" using open_Diff[OF _ finite_imp_closed[OF finite]] \<open>open s\<close> by auto
then show "ff holomorphic_on s - pz" unfolding ff_def using f_holo h_holo
by (auto intro!: holomorphic_intros simp add:pz_def)
next
show "\<forall>p\<in>s. 0 < get_e p \<and> (\<forall>w\<in>cball p (get_e p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pz))"
using get_e using avoid_def by blast
qed
also have "... = (\<Sum>p\<in>pz. c * w p * h p * zorder f p)"
proof (rule sum.cong[of pz pz,simplified])
fix p assume "p \<in> pz"
show "w p * ci p = c * w p * h p * (zorder f p)"
proof (cases "p\<in>s")
assume "p \<in> s"
have "ci p = c * h p * (zorder f p)" unfolding ci_def
apply (rule contour_integral_unique)
using get_e \<open>p\<in>s\<close> \<open>p\<in>pz\<close> unfolding cont_def by (metis mult.assoc mult.commute)
thus ?thesis by auto
next
assume "p\<notin>s"
then have "w p=0" using homo unfolding w_def by auto
then show ?thesis by auto
qed
qed
also have "... = c*(\<Sum>p\<in>pz. w p * h p * zorder f p)"
unfolding sum_distrib_left by (simp add:algebra_simps)
finally have "contour_integral g ff = c * (\<Sum>p\<in>pz. w p * h p * of_int (zorder f p))" .
then show ?thesis unfolding ff_def c_def w_def by simp
qed
subsection \<open>Coefficient asymptotics for generating functions\<close>
text \<open>
For a formal power series that has a meromorphic continuation on some disc in the
context plane, we can use the Residue Theorem to extract precise asymptotic information
from the residues at the poles. This can be used to derive the asymptotic behaviour
of the coefficients (\<open>a\<^sub>n \<sim> \<dots>\<close>). If the function is meromorphic on the entire
complex plane, one can even derive a full asymptotic expansion.
We will first show the relationship between the coefficients and the sum over the residues
with an explicit remainder term (the contour integral along the circle used in the
Residue theorem).
\<close>
theorem
fixes f :: "complex \<Rightarrow> complex" and n :: nat and r :: real
defines "g \<equiv> (\<lambda>w. f w / w ^ Suc n)" and "\<gamma> \<equiv> circlepath 0 r"
assumes "open A" "connected A" "cball 0 r \<subseteq> A" "r > 0"
assumes "f holomorphic_on A - S" "S \<subseteq> ball 0 r" "finite S" "0 \<notin> S"
shows fps_coeff_conv_residues:
"(deriv ^^ n) f 0 / fact n =
contour_integral \<gamma> g / (2 * pi * \<i>) - (\<Sum>z\<in>S. residue g z)" (is ?thesis1)
and fps_coeff_residues_bound:
"(\<And>z. norm z = r \<Longrightarrow> z \<notin> k \<Longrightarrow> norm (f z) \<le> C) \<Longrightarrow> C \<ge> 0 \<Longrightarrow> finite k \<Longrightarrow>
norm ((deriv ^^ n) f 0 / fact n + (\<Sum>z\<in>S. residue g z)) \<le> C / r ^ n"
proof -
have holo: "g holomorphic_on A - insert 0 S"
unfolding g_def using assms by (auto intro!: holomorphic_intros)
have "contour_integral \<gamma> g = 2 * pi * \<i> * (\<Sum>z\<in>insert 0 S. winding_number \<gamma> z * residue g z)"
proof (rule Residue_theorem)
show "g holomorphic_on A - insert 0 S" by fact
from assms show "\<forall>z. z \<notin> A \<longrightarrow> winding_number \<gamma> z = 0"
unfolding \<gamma>_def by (intro allI impI winding_number_zero_outside[of _ "cball 0 r"]) auto
qed (insert assms, auto simp: \<gamma>_def)
also have "winding_number \<gamma> z = 1" if "z \<in> insert 0 S" for z
unfolding \<gamma>_def using assms that by (intro winding_number_circlepath) auto
hence "(\<Sum>z\<in>insert 0 S. winding_number \<gamma> z * residue g z) = (\<Sum>z\<in>insert 0 S. residue g z)"
by (intro sum.cong) simp_all
also have "\<dots> = residue g 0 + (\<Sum>z\<in>S. residue g z)"
using \<open>0 \<notin> S\<close> and \<open>finite S\<close> by (subst sum.insert) auto
also from \<open>r > 0\<close> have "0 \<in> cball 0 r" by simp
with assms have "0 \<in> A - S" by blast
with assms have "residue g 0 = (deriv ^^ n) f 0 / fact n"
unfolding g_def by (subst residue_holomorphic_over_power'[of "A - S"])
(auto simp: finite_imp_closed)
finally show ?thesis1
by (simp add: field_simps)
assume C: "\<And>z. norm z = r \<Longrightarrow> z \<notin> k \<Longrightarrow> norm (f z) \<le> C" "C \<ge> 0" and k: "finite k"
have "(deriv ^^ n) f 0 / fact n + (\<Sum>z\<in>S. residue g z) = contour_integral \<gamma> g / (2 * pi * \<i>)"
using \<open>?thesis1\<close> by (simp add: algebra_simps)
also have "norm \<dots> = norm (contour_integral \<gamma> g) / (2 * pi)"
by (simp add: norm_divide norm_mult)
also have "norm (contour_integral \<gamma> g) \<le> C / r ^ Suc n * (2 * pi * r)"
proof (rule has_contour_integral_bound_circlepath_strong)
from \<open>open A\<close> and \<open>finite S\<close> have "open (A - insert 0 S)"
by (blast intro: finite_imp_closed)
with assms show "(g has_contour_integral contour_integral \<gamma> g) (circlepath 0 r)"
unfolding \<gamma>_def
by (intro has_contour_integral_integral contour_integrable_holomorphic_simple [OF holo]) auto
next
fix z assume z: "norm (z - 0) = r" "z \<notin> k"
hence "norm (g z) = norm (f z) / r ^ Suc n"
by (simp add: norm_divide g_def norm_mult norm_power)
also have "\<dots> \<le> C / r ^ Suc n"
using k and \<open>r > 0\<close> and z by (intro divide_right_mono C zero_le_power) auto
finally show "norm (g z) \<le> C / r ^ Suc n" .
qed (insert C(2) k \<open>r > 0\<close>, auto)
also from \<open>r > 0\<close> have "C / r ^ Suc n * (2 * pi * r) / (2 * pi) = C / r ^ n"
by simp
finally show "norm ((deriv ^^ n) f 0 / fact n + (\<Sum>z\<in>S. residue g z)) \<le> \<dots>"
by - (simp_all add: divide_right_mono)
qed
text \<open>
Since the circle is fixed, we can get an upper bound on the values of the generating
function on the circle and therefore show that the integral is $O(r^{-n})$.
\<close>
corollary fps_coeff_residues_bigo:
fixes f :: "complex \<Rightarrow> complex" and r :: real
assumes "open A" "connected A" "cball 0 r \<subseteq> A" "r > 0"
assumes "f holomorphic_on A - S" "S \<subseteq> ball 0 r" "finite S" "0 \<notin> S"
assumes g: "eventually (\<lambda>n. g n = -(\<Sum>z\<in>S. residue (\<lambda>z. f z / z ^ Suc n) z)) sequentially"
(is "eventually (\<lambda>n. _ = -?g' n) _")
shows "(\<lambda>n. (deriv ^^ n) f 0 / fact n - g n) \<in> O(\<lambda>n. 1 / r ^ n)" (is "(\<lambda>n. ?c n - _) \<in> O(_)")
proof -
from assms have "compact (f ` sphere 0 r)"
by (intro compact_continuous_image holomorphic_on_imp_continuous_on
holomorphic_on_subset[OF \<open>f holomorphic_on A - S\<close>]) auto
hence "bounded (f ` sphere 0 r)" by (rule compact_imp_bounded)
then obtain C where C: "\<And>z. z \<in> sphere 0 r \<Longrightarrow> norm (f z) \<le> C"
by (auto simp: bounded_iff sphere_def)
have "0 \<le> norm (f (of_real r))" by simp
also from C[of "of_real r"] and \<open>r > 0\<close> have "\<dots> \<le> C" by simp
finally have C_nonneg: "C \<ge> 0" .
have "(\<lambda>n. ?c n + ?g' n) \<in> O(\<lambda>n. of_real (1 / r ^ n))"
proof (intro bigoI[of _ C] always_eventually allI )
fix n :: nat
from assms and C and C_nonneg have "norm (?c n + ?g' n) \<le> C / r ^ n"
by (intro fps_coeff_residues_bound[where A = A and k = "{}"]) auto
also have "\<dots> = C * norm (complex_of_real (1 / r ^ n))"
using \<open>r > 0\<close> by (simp add: norm_divide norm_power)
finally show "norm (?c n + ?g' n) \<le> \<dots>" .
qed
also have "?this \<longleftrightarrow> (\<lambda>n. ?c n - g n) \<in> O(\<lambda>n. of_real (1 / r ^ n))"
by (intro landau_o.big.in_cong eventually_mono[OF g]) simp_all
finally show ?thesis .
qed
corollary fps_coeff_residues_bigo':
fixes f :: "complex \<Rightarrow> complex" and r :: real
assumes exp: "f has_fps_expansion F"
assumes "open A" "connected A" "cball 0 r \<subseteq> A" "r > 0"
assumes "f holomorphic_on A - S" "S \<subseteq> ball 0 r" "finite S" "0 \<notin> S"
assumes "eventually (\<lambda>n. g n = -(\<Sum>z\<in>S. residue (\<lambda>z. f z / z ^ Suc n) z)) sequentially"
(is "eventually (\<lambda>n. _ = -?g' n) _")
shows "(\<lambda>n. fps_nth F n - g n) \<in> O(\<lambda>n. 1 / r ^ n)" (is "(\<lambda>n. ?c n - _) \<in> O(_)")
proof -
have "fps_nth F = (\<lambda>n. (deriv ^^ n) f 0 / fact n)"
using fps_nth_fps_expansion[OF exp] by (intro ext) simp_all
with fps_coeff_residues_bigo[OF assms(2-)] show ?thesis by simp
qed
subsection \<open>Rouche's theorem \<close>
theorem Rouche_theorem:
fixes f g::"complex \<Rightarrow> complex" and s:: "complex set"
defines "fg\<equiv>(\<lambda>p. f p + g p)"
defines "zeros_fg\<equiv>{p. fg p = 0}" and "zeros_f\<equiv>{p. f p = 0}"
assumes
"open s" and "connected s" and
"finite zeros_fg" and
"finite zeros_f" and
f_holo:"f holomorphic_on s" and
g_holo:"g holomorphic_on s" and
"valid_path \<gamma>" and
loop:"pathfinish \<gamma> = pathstart \<gamma>" and
path_img:"path_image \<gamma> \<subseteq> s " and
path_less:"\<forall>z\<in>path_image \<gamma>. cmod(f z) > cmod(g z)" and
homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number \<gamma> z = 0"
shows "(\<Sum>p\<in>zeros_fg. winding_number \<gamma> p * zorder fg p)
= (\<Sum>p\<in>zeros_f. winding_number \<gamma> p * zorder f p)"
proof -
have path_fg:"path_image \<gamma> \<subseteq> s - zeros_fg"
proof -
have False when "z\<in>path_image \<gamma>" and "f z + g z=0" for z
proof -
have "cmod (f z) > cmod (g z)" using \<open>z\<in>path_image \<gamma>\<close> path_less by auto
moreover have "f z = - g z" using \<open>f z + g z =0\<close> by (simp add: eq_neg_iff_add_eq_0)
then have "cmod (f z) = cmod (g z)" by auto
ultimately show False by auto
qed
then show ?thesis unfolding zeros_fg_def fg_def using path_img by auto
qed
have path_f:"path_image \<gamma> \<subseteq> s - zeros_f"
proof -
have False when "z\<in>path_image \<gamma>" and "f z =0" for z
proof -
have "cmod (g z) < cmod (f z) " using \<open>z\<in>path_image \<gamma>\<close> path_less by auto
then have "cmod (g z) < 0" using \<open>f z=0\<close> by auto
then show False by auto
qed
then show ?thesis unfolding zeros_f_def using path_img by auto
qed
define w where "w \<equiv> \<lambda>p. winding_number \<gamma> p"
define c where "c \<equiv> 2 * complex_of_real pi * \<i>"
define h where "h \<equiv> \<lambda>p. g p / f p + 1"
obtain spikes
where "finite spikes" and spikes: "\<forall>x\<in>{0..1} - spikes. \<gamma> differentiable at x"
using \<open>valid_path \<gamma>\<close>
by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
have h_contour:"((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>"
proof -
have outside_img:"0 \<in> outside (path_image (h o \<gamma>))"
proof -
have "h p \<in> ball 1 1" when "p\<in>path_image \<gamma>" for p
proof -
have "cmod (g p/f p) <1" using path_less[rule_format,OF that]
apply (cases "cmod (f p) = 0")
by (auto simp add: norm_divide)
then show ?thesis unfolding h_def by (auto simp add:dist_complex_def)
qed
then have "path_image (h o \<gamma>) \<subseteq> ball 1 1"
by (simp add: image_subset_iff path_image_compose)
moreover have " (0::complex) \<notin> ball 1 1" by (simp add: dist_norm)
ultimately show "?thesis"
using convex_in_outside[of "ball 1 1" 0] outside_mono by blast
qed
have valid_h:"valid_path (h \<circ> \<gamma>)"
proof (rule valid_path_compose_holomorphic[OF \<open>valid_path \<gamma>\<close> _ _ path_f])
show "h holomorphic_on s - zeros_f"
unfolding h_def using f_holo g_holo
by (auto intro!: holomorphic_intros simp add:zeros_f_def)
next
show "open (s - zeros_f)" using \<open>finite zeros_f\<close> \<open>open s\<close> finite_imp_closed
by auto
qed
have "((\<lambda>z. 1/z) has_contour_integral 0) (h \<circ> \<gamma>)"
proof -
have "0 \<notin> path_image (h \<circ> \<gamma>)" using outside_img by (simp add: outside_def)
then have "((\<lambda>z. 1/z) has_contour_integral c * winding_number (h \<circ> \<gamma>) 0) (h \<circ> \<gamma>)"
using has_contour_integral_winding_number[of "h o \<gamma>" 0,simplified] valid_h
unfolding c_def by auto
moreover have "winding_number (h o \<gamma>) 0 = 0"
proof -
have "0 \<in> outside (path_image (h \<circ> \<gamma>))" using outside_img .
moreover have "path (h o \<gamma>)"
using valid_h by (simp add: valid_path_imp_path)
moreover have "pathfinish (h o \<gamma>) = pathstart (h o \<gamma>)"
by (simp add: loop pathfinish_compose pathstart_compose)
ultimately show ?thesis using winding_number_zero_in_outside by auto
qed
ultimately show ?thesis by auto
qed
moreover have "vector_derivative (h \<circ> \<gamma>) (at x) = vector_derivative \<gamma> (at x) * deriv h (\<gamma> x)"
when "x\<in>{0..1} - spikes" for x
proof (rule vector_derivative_chain_at_general)
show "\<gamma> differentiable at x" using that \<open>valid_path \<gamma>\<close> spikes by auto
next
define der where "der \<equiv> \<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)"
define t where "t \<equiv> \<gamma> x"
have "f t\<noteq>0" unfolding zeros_f_def t_def
by (metis DiffD1 image_eqI norm_not_less_zero norm_zero path_defs(4) path_less that)
moreover have "t\<in>s"
using contra_subsetD path_image_def path_fg t_def that by fastforce
ultimately have "(h has_field_derivative der t) (at t)"
unfolding h_def der_def using g_holo f_holo \<open>open s\<close>
by (auto intro!: holomorphic_derivI derivative_eq_intros)
then show "h field_differentiable at (\<gamma> x)"
unfolding t_def field_differentiable_def by blast
qed
then have " ((/) 1 has_contour_integral 0) (h \<circ> \<gamma>)
= ((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>"
unfolding has_contour_integral
apply (intro has_integral_spike_eq[OF negligible_finite, OF \<open>finite spikes\<close>])
by auto
ultimately show ?thesis by auto
qed
then have "contour_integral \<gamma> (\<lambda>x. deriv h x / h x) = 0"
using contour_integral_unique by simp
moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = contour_integral \<gamma> (\<lambda>x. deriv f x / f x)
+ contour_integral \<gamma> (\<lambda>p. deriv h p / h p)"
proof -
have "(\<lambda>p. deriv f p / f p) contour_integrable_on \<gamma>"
proof (rule contour_integrable_holomorphic_simple[OF _ _ \<open>valid_path \<gamma>\<close> path_f])
show "open (s - zeros_f)" using finite_imp_closed[OF \<open>finite zeros_f\<close>] \<open>open s\<close>
by auto
then show "(\<lambda>p. deriv f p / f p) holomorphic_on s - zeros_f"
using f_holo
by (auto intro!: holomorphic_intros simp add:zeros_f_def)
qed
moreover have "(\<lambda>p. deriv h p / h p) contour_integrable_on \<gamma>"
using h_contour
by (simp add: has_contour_integral_integrable)
ultimately have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x + deriv h x / h x) =
contour_integral \<gamma> (\<lambda>p. deriv f p / f p) + contour_integral \<gamma> (\<lambda>p. deriv h p / h p)"
using contour_integral_add[of "(\<lambda>p. deriv f p / f p)" \<gamma> "(\<lambda>p. deriv h p / h p)" ]
by auto
moreover have "deriv fg p / fg p = deriv f p / f p + deriv h p / h p"
when "p\<in> path_image \<gamma>" for p
proof -
have "fg p\<noteq>0" and "f p\<noteq>0" using path_f path_fg that unfolding zeros_f_def zeros_fg_def
by auto
have "h p\<noteq>0"
proof (rule ccontr)
assume "\<not> h p \<noteq> 0"
then have "g p / f p= -1" unfolding h_def by (simp add: add_eq_0_iff2)
then have "cmod (g p/f p) = 1" by auto
moreover have "cmod (g p/f p) <1" using path_less[rule_format,OF that]
apply (cases "cmod (f p) = 0")
by (auto simp add: norm_divide)
ultimately show False by auto
qed
have der_fg:"deriv fg p = deriv f p + deriv g p" unfolding fg_def
using f_holo g_holo holomorphic_on_imp_differentiable_at[OF _ \<open>open s\<close>] path_img that
by auto
have der_h:"deriv h p = (deriv g p * f p - g p * deriv f p)/(f p * f p)"
proof -
define der where "der \<equiv> \<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)"
have "p\<in>s" using path_img that by auto
then have "(h has_field_derivative der p) (at p)"
unfolding h_def der_def using g_holo f_holo \<open>open s\<close> \<open>f p\<noteq>0\<close>
by (auto intro!: derivative_eq_intros holomorphic_derivI)
then show ?thesis unfolding der_def using DERIV_imp_deriv by auto
qed
show ?thesis
apply (simp only:der_fg der_h)
apply (auto simp add:field_simps \<open>h p\<noteq>0\<close> \<open>f p\<noteq>0\<close> \<open>fg p\<noteq>0\<close>)
by (auto simp add:field_simps h_def \<open>f p\<noteq>0\<close> fg_def)
qed
then have "contour_integral \<gamma> (\<lambda>p. deriv fg p / fg p)
= contour_integral \<gamma> (\<lambda>p. deriv f p / f p + deriv h p / h p)"
by (elim contour_integral_eq)
ultimately show ?thesis by auto
qed
moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = c * (\<Sum>p\<in>zeros_fg. w p * zorder fg p)"
unfolding c_def zeros_fg_def w_def
proof (rule argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo
, of _ "{}" "\<lambda>_. 1",simplified])
show "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto
show "path_image \<gamma> \<subseteq> s - {p. fg p = 0}" using path_fg unfolding zeros_fg_def .
show " finite {p. fg p = 0}" using \<open>finite zeros_fg\<close> unfolding zeros_fg_def .
qed
moreover have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x) = c * (\<Sum>p\<in>zeros_f. w p * zorder f p)"
unfolding c_def zeros_f_def w_def
proof (rule argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo
, of _ "{}" "\<lambda>_. 1",simplified])
show "f holomorphic_on s" using f_holo g_holo holomorphic_on_add by auto
show "path_image \<gamma> \<subseteq> s - {p. f p = 0}" using path_f unfolding zeros_f_def .
show " finite {p. f p = 0}" using \<open>finite zeros_f\<close> unfolding zeros_f_def .
qed
ultimately have " c* (\<Sum>p\<in>zeros_fg. w p * (zorder fg p)) = c* (\<Sum>p\<in>zeros_f. w p * (zorder f p))"
by auto
then show ?thesis unfolding c_def using w_def by auto
qed
end