section ‹The Residue Theorem, the Argument Principle and Rouch\'{e}'s Theorem› theory Residue_Theorem imports Complex_Residues "HOL-Library.Landau_Symbols" begin text ‹Several theorems that could be moved up, IF there were a previous theory importing both Landau Symbols and Elementary Metric Spaces› lemma continuous_bounded_at_infinity_imp_bounded: fixes f :: "real ⇒ 'a :: real_normed_field" assumes "f ∈ O[at_bot](λ_. 1)" assumes "f ∈ O[at_top](λ_. 1)" assumes cf: "continuous_on UNIV f" shows "bounded (range f)" proof - obtain c1 c2 where "eventually (λx. norm (f x) ≤ c1) at_bot" "eventually (λx. norm (f x) ≤ c2) at_top" using assms by (auto elim!: landau_o.bigE) then obtain x1 x2 where x1: "⋀x. x ≤ x1 ⟹ norm (f x) ≤ c1" and x2: "⋀x. x ≥ x2 ⟹ norm (f x) ≤ c2" by (auto simp: eventually_at_bot_linorder eventually_at_top_linorder) have "compact (f ` {x1..x2})" by (intro compact_continuous_image continuous_on_subset[OF cf]) auto hence "bounded (f ` {x1..x2})" by (rule compact_imp_bounded) then obtain c3 where c3: "⋀x. x ∈ {x1..x2} ⟹ norm (f x) ≤ c3" unfolding bounded_iff by fast have "norm (f x) ≤ Max {c1, c2, c3}" for x by (cases "x ≤ x1"; cases "x ≥ x2") (use x1 x2 c3 in ‹auto simp: le_max_iff_disj›) thus ?thesis unfolding bounded_iff by blast qed lemma holomorphic_on_extend: assumes "f holomorphic_on S - {ξ}" "ξ ∈ interior S" "f ∈ O[at ξ](λ_. 1)" shows "(∃g. g holomorphic_on S ∧ (∀z∈S - {ξ}. g z = f z))" by (subst holomorphic_on_extend_bounded) (insert assms, auto elim!: landau_o.bigE) lemma removable_singularities: assumes "finite X" "X ⊆ interior S" "f holomorphic_on (S - X)" assumes "⋀z. z ∈ X ⟹ f ∈ O[at z](λ_. 1)" shows "∃g. g holomorphic_on S ∧ (∀z∈S-X. g z = f z)" using assms proof (induction arbitrary: f rule: finite_induct) case empty thus ?case by auto next case (insert z0 X f) from insert.prems and insert.hyps have z0: "z0 ∈ interior (S - X)" by (auto simp: interior_diff finite_imp_closed) hence "∃g. g holomorphic_on (S - X) ∧ (∀z∈S - X - {z0}. g z = f z)" using insert.prems insert.hyps by (intro holomorphic_on_extend) auto then obtain g where g: "g holomorphic_on (S - X)" "∀z∈S - X - {z0}. g z = f z" by blast have "∃h. h holomorphic_on S ∧ (∀z∈S - X. h z = g z)" proof (rule insert.IH) fix z0' assume z0': "z0' ∈ X" hence "eventually (λz. z ∈ interior S - (X - {z0'}) - {z0}) (nhds z0')" using insert.prems insert.hyps by (intro eventually_nhds_in_open open_Diff finite_imp_closed) auto hence ev: "eventually (λz. z ∈ S - X - {z0}) (at z0')" unfolding eventually_at_filter by eventually_elim (insert z0' insert.hyps interior_subset[of S], auto) have "g ∈ Θ[at z0'](f)" by (intro bigthetaI_cong eventually_mono[OF ev]) (insert g, auto) also have "f ∈ O[at z0'](λ_. 1)" using z0' by (intro insert.prems) auto finally show "g ∈ …" . qed (use insert.prems g in auto) then obtain h where "h holomorphic_on S" "∀z∈S - X. h z = g z" by blast with g have "h holomorphic_on S" "∀z∈S - insert z0 X. h z = f z" by auto thus ?case by blast qed lemma continuous_imp_bigo_1: assumes "continuous (at x within A) f" shows "f ∈ O[at x within A](λ_. 1)" proof (rule bigoI_tendsto) from assms show "((λx. f x / 1) ⤏ f x) (at x within A)" by (auto simp: continuous_within) qed auto lemma taylor_bigo_linear: assumes "f field_differentiable at x0 within A" shows "(λx. f x - f x0) ∈ O[at x0 within A](λx. x - x0)" proof - from assms obtain f' where "(f has_field_derivative f') (at x0 within A)" by (auto simp: field_differentiable_def) hence "((λx. (f x - f x0) / (x - x0)) ⤏ f') (at x0 within A)" by (auto simp: has_field_derivative_iff) thus ?thesis by (intro bigoI_tendsto[where c = f']) (auto simp: eventually_at_filter) qed subsection ‹Cauchy's residue theorem› lemma get_integrable_path: assumes "open S" "connected (S-pts)" "finite pts" "f holomorphic_on (S-pts) " "a∈S-pts" "b∈S-pts" obtains g where "valid_path g" "pathstart g = a" "pathfinish g = b" "path_image g ⊆ S-pts" "f contour_integrable_on g" using assms proof (induct arbitrary:S thesis a rule:finite_induct[OF ‹finite pts›]) case 1 obtain g where "valid_path g" "path_image g ⊆ S" "pathstart g = a" "pathfinish g = b" using connected_open_polynomial_connected[OF ‹open S›,of a b ] ‹connected (S - {})› 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 S› ‹valid_path g› ‹path_image g ⊆ S›,of f] ‹f holomorphic_on S - {}› 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:"∀w∈ball a e. w ∈ S ∧ (w ≠ a ⟶ w ∉ insert p pts)" using finite_ball_avoid[OF ‹open S› ‹finite (insert p pts)›, of a] ‹a ∈ S - insert p pts› by auto define a' where "a' ≡ a+e/2" have "a'∈S-{p} -pts" using e[rule_format,of "a+e/2"] ‹e>0› 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' ⊆ 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 ≡ 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 ⊆ S - insert p pts" unfolding g_def proof (rule subset_path_image_join) have "closed_segment a a' ⊆ ball a e" using ‹e>0› by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute) then show "path_image (linepath a a') ⊆ S - insert p pts" using e idt(9) by auto next show "path_image g' ⊆ S - insert p pts" using g'(4) by blast qed moreover have "f contour_integrable_on g" proof - have "closed_segment a a' ⊆ ball a e" using ‹e>0› by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute) then have "closed_segment a a' ⊆ S - insert p pts" using e idt.prems(6) by auto then have "continuous_on (closed_segment a a') f" using holomorphic_on_imp_continuous_on holomorphic_on_subset idt.prems(5) by presburger then show ?thesis using contour_integrable_continuous_linepath by (simp add: g_def) 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 ⊆ S" "f holomorphic_on S-pts" "valid_path g" "pathfinish g = pathstart g" "path_image g ⊆ S-pts" "∀z. (z ∉ S) ⟶ winding_number g z = 0" "∀p∈S. h p>0 ∧ (∀w∈cball p (h p). w∈S ∧ (w≠p ⟶ w ∉ pts))" shows "contour_integral g f = (∑p∈pts. winding_number g p * contour_integral (circlepath p (h p)) f)" using assms proof (induct arbitrary:S g rule:finite_induct[OF ‹finite pts›]) case 1 then show ?case by (simp add: Cauchy_theorem_global contour_integral_unique) next case (2 p pts) note fin[simp] = ‹finite (insert p pts)› and connected = ‹connected (S - insert p pts)› and valid[simp] = ‹valid_path g› and g_loop[simp] = ‹pathfinish g = pathstart g› and holo[simp]= ‹f holomorphic_on S - insert p pts› and path_img = ‹path_image g ⊆ S - insert p pts› and winding = ‹∀z. z ∉ S ⟶ winding_number g z = 0› and h = ‹∀pa∈S. 0 < h pa ∧ (∀w∈cball pa (h pa). w ∈ S ∧ (w ≠ pa ⟶ w ∉ insert p pts))› have "h p>0" and "p∈S" and h_p: "∀w∈cball p (h p). w ∈ S ∧ (w ≠ p ⟶ w ∉ insert p pts)" using h ‹insert p pts ⊆ S› by auto obtain pg where pg[simp]: "valid_path pg" "pathstart pg = pathstart g" "pathfinish pg=p+h p" "path_image pg ⊆ S-insert p pts" "f contour_integrable_on pg" proof - have "p + h p∈cball p (h p)" using h[rule_format,of p] by (simp add: ‹p ∈ S› dist_norm) then have "p + h p ∈ S - insert p pts" using h[rule_format,of p] ‹insert p pts ⊆ S› by fastforce moreover have "pathstart g ∈ S - insert p pts " using path_img by auto ultimately show ?thesis using get_integrable_path[OF ‹open S› 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 ≡ circlepath p (h p)" define p_circ_pt where "p_circ_pt ≡ linepath (p+h p) (p+h p)" define n_circ where "n_circ ≡ λn. ((+++) p_circ ^^ n) p_circ_pt" define cp where "cp ≡ if n≥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 ∉ path_image (n_circ k)" "⋀p'. p'∉S - pts ⟹ winding_number (n_circ k) p'=0 ∧ p'∉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 ∉ path_image (n_circ 0)" unfolding n_circ_def p_circ_pt_def using ‹h p > 0› by (auto simp add: dist_norm) show "winding_number (n_circ 0) p'=0 ∧ p'∉path_image (n_circ 0)" when "p'∉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 ∉ path_image p_circ" "valid_path p_circ" "pathfinish p_circ = pathstart (n_circ k)" using Suc(3) unfolding p_circ_def using ‹h p > 0› by (auto simp add: p_circ_def) have pcirc_image:"path_image p_circ ⊆ S - insert p pts" proof - have "path_image p_circ ⊆ cball p (h p)" using ‹0 < h p› 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 ‹0 < h p› by auto then show ?thesis unfolding n_Suc using Suc.hyps(5) ‹h p>0› by (auto simp add: path_image_join[OF pcirc(3)] dist_norm) qed then show "p ∉ path_image (n_circ (Suc k))" using ‹h p>0› 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: ‹h p > 0› p_circ_def winding_number_circlepath_centre) moreover have "p ∉ path_image (n_circ k)" using Suc(5) ‹h p>0› 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 ∧ p'∉path_image (n_circ (Suc k))" when "p'∉S-pts" for p' proof - have " p' ∉ path_image p_circ" using ‹p ∈ S› h p_circ_def that using pcirc_image by blast moreover have "p' ∉ 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 ⊆ cball p (h p)" using h unfolding p_circ_def using ‹p ∈ S› by fastforce moreover have "p'∉cball p (h p)" using ‹p ∈ S› h that "2.hyps"(2) by fastforce ultimately show ?thesis unfolding p_circ_def by (intro winding_number_zero_outside) auto qed ultimately show ?thesis unfolding n_Suc using Suc.hyps pcirc by (metis add.right_neutral not_in_path_image_join that valid_path_imp_path winding_number_join) 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" by (simp add: Rings.ring_distribs(2) Suc.hyps n_Suc pcirc pcirc_integrable) qed have cp[simp]:"pathstart cp = p + h p" "pathfinish cp = p + h p" "valid_path cp" "path_image cp ⊆ S - insert p pts" "winding_number cp p = - n" "⋀p'. p'∉S - pts ⟹ winding_number cp p'=0 ∧ p' ∉ 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) ⊆ S - insert p pts" using h[rule_format,of p] ‹insert p pts ⊆ S› by force moreover have "p + complex_of_real (h p) ∈ S - insert p pts" using pg(3) pg(4) by (metis pathfinish_in_path_image subsetCE) ultimately show "path_image cp ⊆ 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 ‹h p>0› by (auto simp: valid_path_imp_path) next show "winding_number cp p'=0 ∧ p' ∉ path_image cp" when "p'∉S - pts" for p' proof - have "winding_number (reversepath (n_circ (nat n))) p' = 0" using n_circ that by (metis add.inverse_neutral valid_path_imp_path winding_number_reversepath) then show ?thesis using cp_def n_circ(7) that by force qed 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' ≡ g +++ pg +++ cp +++ (reversepath pg)" have "contour_integral g' f = (∑p∈pts. winding_number g' p * contour_integral (circlepath p (h p)) f)" proof (rule "2.hyps"(3)[of "S-{p}" "g'",OF _ _ ‹finite pts› ]) show "connected (S - {p} - pts)" using connected by (metis Diff_insert2) show "open (S - {p})" using ‹open S› by auto show " pts ⊆ S - {p}" using ‹insert p pts ⊆ S› ‹ p ∉ pts› by blast show "f holomorphic_on S - {p} - pts" using holo ‹p ∉ pts› 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' ⊆ S - {p} - pts" proof - define s' where "s' ≡ 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) by (simp add: g'_def s'_def subset_path_image_join) qed note path_join_imp[simp] show "∀z. z ∉ S - {p} ⟶ winding_number g' z = 0" proof clarify fix z assume z:"z∉S - {p}" have z_notin_cp: "z ∉ path_image cp" using cp(6) cp_def n_circ(6) z by auto have z_notin_pg: "z ∉ path_image pg" by (metis Diff_iff Diff_insert2 pg(4) subsetD z) 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 ‹valid_path g› by (simp add: valid_path_imp_path) show "z ∉ 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) ⊆ S - insert p pts" using pg(4) cp(4) by (auto simp:subset_path_image_join) then show "z ∉ 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 ∉ path_image pg" using pg(4) z by blast show "z ∉ path_image (cp +++ reversepath pg)" using z by (metis Diff_iff ‹z ∉ path_image pg› 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))" by (simp add: valid_path_imp_path winding_number_join z_notin_cp z_notin_pg) also have "… = winding_number g z + winding_number cp z" by (simp add: valid_path_imp_path winding_number_reversepath z_notin_pg) 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 ‹n=winding_number g p› by auto ultimately show "winding_number g' z = 0" unfolding g'_def by auto qed show "∀pa ∈ S - {p}. 0 < h pa ∧ (∀w∈cball pa (h pa). w ∈ S - {p} ∧ (w ≠ pa ⟶ w ∉ 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 *: "f contour_integrable_on g" "f contour_integrable_on pg" "f contour_integrable_on cp" by (auto simp add: open_Diff[OF ‹open S›,OF finite_imp_closed[OF fin]] intro!: contour_integrable_holomorphic_simple[OF holo _ _ path_img]) have "contour_integral g' f = contour_integral g f + contour_integral pg f + contour_integral cp f + contour_integral (reversepath pg) f" using * by (simp add: g'_def contour_integrable_reversepath_eq) 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 ‹n=winding_number g p› by auto finally show ?thesis . qed moreover have "winding_number g' p' = winding_number g p'" when "p'∈pts" for p' proof - obtain [simp]: "p' ∉ path_image g" "p' ∉ path_image pg" "p'∉path_image cp" using "2.prems"(8) that by (metis Diff_iff Diff_insert2 ‹p' ∈ pts› cp(4) pg(4) subsetD) have "winding_number g' p' = winding_number g p' + winding_number pg p' + winding_number (cp +++ reversepath pg) p'" by (simp add: g'_def not_in_path_image_join valid_path_imp_path winding_number_join) also have "… = winding_number g p'" using that by (simp add: valid_path_imp_path winding_number_join winding_number_reversepath) finally show ?thesis . qed ultimately show ?case unfolding p_circ_def apply (subst (asm) sum.cong[OF refl, of pts _ "λp. winding_number g p * contour_integral (circlepath p (h p)) f"]) by (auto simp: sum.insert[OF ‹finite pts› ‹p∉pts›] 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 ⊆ S-pts" and homo:"∀z. (z ∉ S) ⟶ winding_number g z = 0" and avoid:"∀p∈S. h p>0 ∧ (∀w∈cball p (h p). w∈S ∧ (w≠p ⟶ w ∉ pts))" shows "contour_integral g f = (∑p∈pts. winding_number g p * contour_integral (circlepath p (h p)) f)" (is "?L=?R") proof - define circ where "circ ≡ λp. winding_number g p * contour_integral (circlepath p (h p)) f" define pts1 where "pts1 ≡ pts ∩ S" define pts2 where "pts2 ≡ pts - pts1" have "pts=pts1 ∪ pts2" "pts1 ∩ pts2 = {}" "pts2 ∩ S={}" "pts1⊆S" unfolding pts1_def pts2_def by auto have "contour_integral g f = (∑p∈pts1. circ p)" unfolding circ_def proof (rule Cauchy_theorem_aux[OF ‹open S› _ _ ‹pts1⊆S› _ ‹valid_path g› loop _ homo]) have "finite pts1" unfolding pts1_def using ‹finite pts› by auto then show "connected (S - pts1)" using ‹open S› ‹connected S› connected_open_delete_finite[of S] by auto next show "finite pts1" using ‹pts = pts1 ∪ pts2› assms(3) by auto show "f holomorphic_on S - pts1" by (metis Diff_Int2 Int_absorb holo pts1_def) show "path_image g ⊆ S - pts1" using assms(7) pts1_def by auto show "∀p∈S. 0 < h p ∧ (∀w∈cball p (h p). w ∈ S ∧ (w ≠ p ⟶ w ∉ pts1))" by (simp add: avoid pts1_def) qed moreover have "sum circ pts2 = 0" by (metis ‹pts2 ∩ S = {}› circ_def disjoint_iff_not_equal homo mult_zero_left sum.neutral) moreover have "?R=sum circ pts1 + sum circ pts2" unfolding circ_def using sum.union_disjoint[OF _ _ ‹pts1 ∩ pts2 = {}›] ‹finite pts› ‹pts=pts1 ∪ pts2› by blast ultimately show ?thesis by simp qed theorem Residue_theorem: fixes S pts::"complex set" and f::"complex ⇒ complex" and g::"real ⇒ 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 ⊆ S-pts" and homo:"∀z. (z ∉ S) ⟶ winding_number g z = 0" shows "contour_integral g f = 2 * pi * 𝗂 *(∑p∈pts. winding_number g p * residue f p)" proof - define c where "c ≡ 2 * pi * 𝗂" obtain h where avoid:"∀p∈S. h p>0 ∧ (∀w∈cball p (h p). w∈S ∧ (w≠p ⟶ w ∉ pts))" using finite_cball_avoid[OF ‹open S› ‹finite pts›] by metis have "contour_integral g f = (∑p∈pts. winding_number g p * contour_integral (circlepath p (h p)) f)" using Cauchy_theorem_singularities[OF assms avoid] . also have "… = (∑p∈pts. c * winding_number g p * residue f p)" proof (intro sum.cong) show "pts = pts" by simp next fix x assume "x ∈ pts" show "winding_number g x * contour_integral (circlepath x (h x)) f = c * winding_number g x * residue f x" proof (cases "x∈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 ‹x∈pts› ‹finite pts› 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 S› finite_imp_closed]) then show ?thesis by auto qed qed also have "… = c * (∑p∈pts. winding_number g p * residue f p)" by (simp add: sum_distrib_left algebra_simps) finally show ?thesis unfolding c_def . qed subsection ‹The argument principle› theorem argument_principle: fixes f::"complex ⇒ complex" and poles S:: "complex set" defines "pz ≡ {w∈S. f w = 0 ∨ w ∈ poles}" ― ‹\<^term>‹pz› is the set of poles and zeros› assumes "open S" "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 ⊆ S - pz" and homo:"∀z. (z ∉ S) ⟶ winding_number g z = 0" and finite:"finite pz" and poles:"∀p∈S∩poles. is_pole f p" shows "contour_integral g (λx. deriv f x * h x / f x) = 2 * pi * 𝗂 * (∑p∈pz. winding_number g p * h p * zorder f p)" (is "?L=?R") proof - define c where "c ≡ 2 * complex_of_real pi * 𝗂 " define ff where "ff ≡ (λx. deriv f x * h x / f x)" define cont where "cont ≡ λff p e. (ff has_contour_integral c * zorder f p * h p ) (circlepath p e)" define avoid where "avoid ≡ λp e. ∀w∈cball p e. w ∈ S ∧ (w ≠ p ⟶ w ∉ pz)" have "∃e>0. avoid p e ∧ (p∈pz ⟶ cont ff p e)" when "p∈S" for p proof - obtain e1 where "e1>0" and e1_avoid:"avoid p e1" using finite_cball_avoid[OF ‹open S› finite] ‹p∈S› unfolding avoid_def by auto have "∃e2>0. cball p e2 ⊆ ball p e1 ∧ cont ff p e2" when "p∈pz" proof - define po where "po ≡ zorder f p" define pp where "pp ≡ zor_poly f p" define f' where "f' ≡ λw. pp w * (w - p) powi po" define ff' where "ff' ≡ (λx. deriv f' x * h x / f' x)" obtain r where "pp p≠0" "r>0" and "r<e1" and pp_holo:"pp holomorphic_on cball p r" and pp_po:"(∀w∈cball p r-{p}. f w = pp w * (w - p) powi po ∧ pp w ≠ 0)" proof - have "isolated_singularity_at f p" proof - have "ball p e1 - {p} ⊆ S - poles" using avoid_def e1_avoid pz_def by fastforce then have "f holomorphic_on ball p e1 - {p}" by (intro holomorphic_on_subset[OF f_holo]) then show ?thesis unfolding isolated_singularity_at_def using ‹e1>0› 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∈S-poles" using ‹p∈S› poles unfolding pz_def by auto moreover have "open (S-poles)" proof - have "closed (S ∩ poles)" using finite by (simp add: pz_def finite_imp_closed rev_finite_subset subset_eq) then show ?thesis by (metis Diff_Compl Diff_Diff_Int Diff_eq ‹open S› open_Diff) qed 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 "∃⇩_{F}w in at p. f w ≠ 0 " proof (rule ccontr) assume "¬ (∃⇩_{F}w in at p. f w ≠ 0)" then have "∀⇩_{F}w in at p. f w= 0" unfolding frequently_def by auto then obtain r1 where "r1>0" and r1:"∀w∈ball p r1 - {p}. f w =0" unfolding eventually_at by (auto simp add:dist_commute) obtain r2 where "r2>0" and r2: "ball p r2 ⊆ S" using ‹p∈S› ‹open S› openE by blast define rr where "rr=min r1 r2" from r1 r2 have "ball p rr - {p} ⊆ {w∈ S ∩ ball p rr-{p}. f w=0}" unfolding rr_def by auto moreover have "infinite (ball p rr - {p})" using ‹r1>0› ‹r2>0› finite_imp_not_open unfolding rr_def by fastforce ultimately have "infinite {w∈S ∩ ball p rr-{p}. f w=0}" using infinite_super by blast then have "infinite pz" unfolding pz_def by (smt (verit) infinite_super Collect_mono_iff DiffE Int_iff) then show False using ‹finite pz› by auto qed ultimately obtain r where "pp p ≠ 0" and r:"r>0" "pp holomorphic_on cball p r" "(∀w∈cball p r - {p}. f w = pp w * (w - p) powi po ∧ pp w ≠ 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 ‹e1>0› ‹r>0› by auto moreover have "r1>0" "pp holomorphic_on cball p r1" "(∀w∈cball p r1 - {p}. f w = pp w * (w - p) powi po ∧ pp w ≠ 0)" unfolding r1_def using ‹e1>0› r by auto ultimately show ?thesis using that ‹pp p≠0› by auto qed define e2 where "e2 ≡ r/2" have "e2>0" using ‹r>0› unfolding e2_def by auto define anal where "anal ≡ λw. deriv pp w * h w / pp w" define prin where "prin ≡ λw. po * h w / (w - p)" have "((λ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 ⊆ S" using ‹r<e1› avoid_def ball_subset_cball e1_avoid by (simp add: subset_eq) then have "cball p e2 ⊆ S" using ‹r>0› unfolding e2_def by auto then have "(λ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 "λw. po * h w"] ‹e2>0› 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 ‹ball p r ⊆ S› ‹pp p≠0› by (auto intro!: holomorphic_intros) then show "(anal has_contour_integral 0) (circlepath p e2)" using e2_def ‹r>0› 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 ∈ path_image (circlepath p e2)" then have "w∈ball p r" and "w≠p" unfolding e2_def using ‹r>0› by auto define wp where "wp ≡ w-p" have "wp≠0" and "pp w ≠0" unfolding wp_def using ‹w≠p› ‹w∈ball p r› pp_po by auto moreover have der_f':"deriv f' w = po * pp w * (w-p) powi (po - 1) + deriv pp w * (w-p) powi 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 ‹w≠p› by (meson open_ball ‹w ∈ ball p r› ball_subset_cball holomorphic_derivI holomorphic_on_subset) then show " (f' has_field_derivative of_int po * pp w * (w - p) powi (po - 1) + deriv pp w * (w - p) powi po) (at w)" unfolding f'_def using ‹w≠p› 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 f'_def ff'_def prin_def anal_def apply (simp add: field_simps flip: wp_def) by (metis (no_types, lifting) mult.commute power_int_minus_mult) qed then have "cont ff p e2" unfolding cont_def proof (elim has_contour_integral_eq) fix w assume "w ∈ path_image (circlepath p e2)" then have "w∈ball p r" and "w≠p" unfolding e2_def using ‹r>0› 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} ⊆ S - poles" using ball_subset_cball e1_avoid[unfolded avoid_def] unfolding pz_def by auto then have "ball p r - {p} ⊆ S - poles" using ‹r<e1› by force 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 ∈ ball p r - {p}" using ‹w∈ball p r› ‹w≠p› by auto next fix x assume "x ∈ 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 ‹w ∈ ball p r› ball_subset_cball subset_iff pp_po ‹w≠p› unfolding f'_def by auto ultimately show "ff' w = ff w" unfolding ff'_def ff_def by simp qed moreover have "cball p e2 ⊆ ball p e1" using ‹0 < r› ‹r<e1› e2_def by auto ultimately show ?thesis using ‹e2>0› by auto qed then obtain e2 where e2:"p∈pz ⟶ e2>0 ∧ cball p e2 ⊆ ball p e1 ∧ cont ff p e2" by auto define e4 where "e4 ≡ if p∈pz then e2 else e1" have "e4>0" using e2 ‹e1>0› unfolding e4_def by auto moreover have "avoid p e4" using e2 ‹e1>0› e1_avoid unfolding e4_def avoid_def by auto moreover have "p∈pz ⟶ cont ff p e4" by (auto simp add: e2 e4_def) ultimately show ?thesis by auto qed then obtain get_e where get_e:"∀p∈S. get_e p>0 ∧ avoid p (get_e p) ∧ (p∈pz ⟶ cont ff p (get_e p))" by metis define ci where "ci ≡ λp. contour_integral (circlepath p (get_e p)) ff" define w where "w ≡ λp. winding_number g p" have "contour_integral g ff = (∑p∈pz. w p * ci p)" unfolding ci_def w_def proof (rule Cauchy_theorem_singularities[OF ‹open S› ‹connected S› finite _ ‹valid_path g› loop path_img homo]) have "open (S - pz)" using open_Diff[OF _ finite_imp_closed[OF finite]] ‹open S› 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 "∀p∈S. 0 < get_e p ∧ (∀w∈cball p (get_e p). w ∈ S ∧ (w ≠ p ⟶ w ∉ pz))" using get_e using avoid_def by blast qed also have "… = (∑p∈pz. c * w p * h p * zorder f p)" proof (rule sum.cong[of pz pz,simplified]) fix p assume "p ∈ pz" show "w p * ci p = c * w p * h p * (zorder f p)" proof (cases "p∈S") assume "p ∈ S" have "ci p = c * h p * (zorder f p)" unfolding ci_def using ‹p ∈ S› ‹p ∈ pz› cont_def contour_integral_unique get_e by fastforce thus ?thesis by auto next assume "p∉S" then have "w p=0" using homo unfolding w_def by auto then show ?thesis by auto qed qed also have "… = c*(∑p∈pz. w p * h p * zorder f p)" unfolding sum_distrib_left by (simp add:algebra_simps) finally have "contour_integral g ff = c * (∑p∈pz. w p * h p * of_int (zorder f p))" . then show ?thesis unfolding ff_def c_def w_def by simp qed subsection ‹Coefficient asymptotics for generating functions› text ‹ 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 (‹a⇩_{n}∼ …›). 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). › theorem fixes f :: "complex ⇒ complex" and n :: nat and r :: real defines "g ≡ (λw. f w / w ^ Suc n)" and "γ ≡ circlepath 0 r" assumes "open A" "connected A" "cball 0 r ⊆ A" "r > 0" assumes "f holomorphic_on A - S" "S ⊆ ball 0 r" "finite S" "0 ∉ S" shows fps_coeff_conv_residues: "(deriv ^^ n) f 0 / fact n = contour_integral γ g / (2 * pi * 𝗂) - (∑z∈S. residue g z)" (is ?thesis1) and fps_coeff_residues_bound: "(⋀z. norm z = r ⟹ z ∉ k ⟹ norm (f z) ≤ C) ⟹ C ≥ 0 ⟹ finite k ⟹ norm ((deriv ^^ n) f 0 / fact n + (∑z∈S. residue g z)) ≤ 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 γ g = 2 * pi * 𝗂 * (∑z∈insert 0 S. winding_number γ z * residue g z)" proof (rule Residue_theorem) show "g holomorphic_on A - insert 0 S" by fact from assms show "∀z. z ∉ A ⟶ winding_number γ z = 0" unfolding γ_def by (intro allI impI winding_number_zero_outside[of _ "cball 0 r"]) auto qed (insert assms, auto simp: γ_def) also have "winding_number γ z = 1" if "z ∈ insert 0 S" for z unfolding γ_def using assms that by (intro winding_number_circlepath) auto hence "(∑z∈insert 0 S. winding_number γ z * residue g z) = (∑z∈insert 0 S. residue g z)" by (intro sum.cong) simp_all also have "… = residue g 0 + (∑z∈S. residue g z)" using ‹0 ∉ S› and ‹finite S› by (subst sum.insert) auto also from ‹r > 0› have "0 ∈ cball 0 r" by simp with assms have "0 ∈ 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: "⋀z. norm z = r ⟹ z ∉ k ⟹ norm (f z) ≤ C" "C ≥ 0" and k: "finite k" have "(deriv ^^ n) f 0 / fact n + (∑z∈S. residue g z) = contour_integral γ g / (2 * pi * 𝗂)" using ‹?thesis1› by (simp add: algebra_simps) also have "norm … = norm (contour_integral γ g) / (2 * pi)" by (simp add: norm_divide norm_mult) also have "norm (contour_integral γ g) ≤ C / r ^ Suc n * (2 * pi * r)" proof (rule has_contour_integral_bound_circlepath_strong) from ‹open A› and ‹finite S› have "open (A - insert 0 S)" by (blast intro: finite_imp_closed) with assms show "(g has_contour_integral contour_integral γ g) (circlepath 0 r)" unfolding γ_def by (intro has_contour_integral_integral contour_integrable_holomorphic_simple [OF holo]) auto next fix z assume z: "norm (z - 0) = r" "z ∉ k" hence "norm (g z) = norm (f z) / r ^ Suc n" by (simp add: norm_divide g_def norm_mult norm_power) also have "… ≤ C / r ^ Suc n" using k and ‹r > 0› and z by (intro divide_right_mono C zero_le_power) auto finally show "norm (g z) ≤ C / r ^ Suc n" . qed (insert C(2) k ‹r > 0›, auto) also from ‹r > 0› have "C / r ^ Suc n * (2 * pi * r) / (2 * pi) = C / r ^ n" by simp finally show "norm ((deriv ^^ n) f 0 / fact n + (∑z∈S. residue g z)) ≤ …" by - (simp_all add: divide_right_mono) qed text ‹ 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})$. › corollary fps_coeff_residues_bigo: fixes f :: "complex ⇒ complex" and r :: real assumes "open A" "connected A" "cball 0 r ⊆ A" "r > 0" assumes "f holomorphic_on A - S" "S ⊆ ball 0 r" "finite S" "0 ∉ S" assumes g: "eventually (λn. g n = -(∑z∈S. residue (λz. f z / z ^ Suc n) z)) sequentially" (is "eventually (λn. _ = -?g' n) _") shows "(λn. (deriv ^^ n) f 0 / fact n - g n) ∈ O(λn. 1 / r ^ n)" (is "(λn. ?c n - _) ∈ O(_)") proof - from assms have "compact (f ` sphere 0 r)" by (intro compact_continuous_image holomorphic_on_imp_continuous_on holomorphic_on_subset[OF ‹f holomorphic_on A - S›]) auto hence "bounded (f ` sphere 0 r)" by (rule compact_imp_bounded) then obtain C where C: "⋀z. z ∈ sphere 0 r ⟹ norm (f z) ≤ C" by (auto simp: bounded_iff sphere_def) have "0 ≤ norm (f (of_real r))" by simp also from C[of "of_real r"] and ‹r > 0› have "… ≤ C" by simp finally have C_nonneg: "C ≥ 0" . have "(λn. ?c n + ?g' n) ∈ O(λ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) ≤ C / r ^ n" by (intro fps_coeff_residues_bound[where A = A and k = "{}"]) auto also have "… = C * norm (complex_of_real (1 / r ^ n))" using ‹r > 0› by (simp add: norm_divide norm_power) finally show "norm (?c n + ?g' n) ≤ …" . qed also have "?this ⟷ (λn. ?c n - g n) ∈ O(λ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 ⇒ complex" and r :: real assumes exp: "f has_fps_expansion F" assumes "open A" "connected A" "cball 0 r ⊆ A" "r > 0" assumes "f holomorphic_on A - S" "S ⊆ ball 0 r" "finite S" "0 ∉ S" assumes "eventually (λn. g n = -(∑z∈S. residue (λz. f z / z ^ Suc n) z)) sequentially" (is "eventually (λn. _ = -?g' n) _") shows "(λn. fps_nth F n - g n) ∈ O(λn. 1 / r ^ n)" (is "(λn. ?c n - _) ∈ O(_)") proof - have "fps_nth F = (λ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 ‹Rouche's theorem › theorem Rouche_theorem: fixes f g::"complex ⇒ complex" and s:: "complex set" defines "fg≡(λp. f p + g p)" defines "zeros_fg≡{p∈s. fg p = 0}" and "zeros_f≡{p∈s. 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 γ" and loop:"pathfinish γ = pathstart γ" and path_img:"path_image γ ⊆ s " and path_less:"∀z∈path_image γ. cmod(f z) > cmod(g z)" and homo:"∀z. (z ∉ s) ⟶ winding_number γ z = 0" shows "(∑p∈zeros_fg. winding_number γ p * zorder fg p) = (∑p∈zeros_f. winding_number γ p * zorder f p)" proof - have path_fg:"path_image γ ⊆ s - zeros_fg" proof - have False when "z∈path_image γ" and "f z + g z=0" for z proof - have "cmod (f z) > cmod (g z)" using ‹z∈path_image γ› path_less by auto moreover have "f z = - g z" using ‹f z + g z =0› 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 γ ⊆ s - zeros_f" proof - have False when "z∈path_image γ" and "f z =0" for z proof - have "cmod (g z) < cmod (f z) " using ‹z∈path_image γ› path_less by auto then have "cmod (g z) < 0" using ‹f z=0› 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 ≡ λp. winding_number γ p" define c where "c ≡ 2 * complex_of_real pi * 𝗂" define h where "h ≡ λp. g p / f p + 1" obtain spikes where "finite spikes" and spikes: "∀x∈{0..1} - spikes. γ differentiable at x" using ‹valid_path γ› by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) have h_contour:"((λx. deriv h x / h x) has_contour_integral 0) γ" proof - have outside_img:"0 ∈ outside (path_image (h o γ))" proof - have "h p ∈ ball 1 1" when "p∈path_image γ" for p proof - have "cmod (g p/f p) <1" by (smt (verit) divide_less_eq_1_pos norm_divide norm_ge_zero path_less that) then show ?thesis unfolding h_def by (auto simp add:dist_complex_def) qed then have "path_image (h o γ) ⊆ ball 1 1" by (simp add: image_subset_iff path_image_compose) moreover have " (0::complex) ∉ 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 ∘ γ)" proof (rule valid_path_compose_holomorphic[OF ‹valid_path γ› _ _ 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 ‹finite zeros_f› ‹open s› finite_imp_closed by auto qed have "((λz. 1/z) has_contour_integral 0) (h ∘ γ)" proof - have "0 ∉ path_image (h ∘ γ)" using outside_img by (simp add: outside_def) then have "((λz. 1/z) has_contour_integral c * winding_number (h ∘ γ) 0) (h ∘ γ)" using has_contour_integral_winding_number[of "h o γ" 0,simplified] valid_h unfolding c_def by auto moreover have "winding_number (h o γ) 0 = 0" proof - have "0 ∈ outside (path_image (h ∘ γ))" using outside_img . moreover have "path (h o γ)" using valid_h by (simp add: valid_path_imp_path) moreover have "pathfinish (h o γ) = pathstart (h o γ)" 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 ∘ γ) (at x) = vector_derivative γ (at x) * deriv h (γ x)" when "x∈{0..1} - spikes" for x proof (rule vector_derivative_chain_at_general) show "γ differentiable at x" using that ‹valid_path γ› spikes by auto next define der where "der ≡ λp. (deriv g p * f p - g p * deriv f p)/(f p * f p)" define t where "t ≡ γ x" have "f t≠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∈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 s› by (auto intro!: holomorphic_derivI derivative_eq_intros) then show "h field_differentiable at (γ x)" unfolding t_def field_differentiable_def by blast qed then have " ((/) 1 has_contour_integral 0) (h ∘ γ) = ((λx. deriv h x / h x) has_contour_integral 0) γ" unfolding has_contour_integral by (force intro!: has_integral_spike_eq[OF negligible_finite, OF ‹finite spikes›]) ultimately show ?thesis by auto qed then have "contour_integral γ (λx. deriv h x / h x) = 0" using contour_integral_unique by simp moreover have "contour_integral γ (λx. deriv fg x / fg x) = contour_integral γ (λx. deriv f x / f x) + contour_integral γ (λp. deriv h p / h p)" proof - have "(λp. deriv f p / f p) contour_integrable_on γ" proof (rule contour_integrable_holomorphic_simple[OF _ _ ‹valid_path γ› path_f]) show "open (s - zeros_f)" using finite_imp_closed[OF ‹finite zeros_f›] ‹open s› by auto then show "(λ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 "(λp. deriv h p / h p) contour_integrable_on γ" using h_contour by (simp add: has_contour_integral_integrable) ultimately have "contour_integral γ (λx. deriv f x / f x + deriv h x / h x) = contour_integral γ (λp. deriv f p / f p) + contour_integral γ (λp. deriv h p / h p)" using contour_integral_add[of "(λp. deriv f p / f p)" γ "(λ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∈ path_image γ" for p proof - have "fg p ≠ 0" and "f p ≠ 0" using path_f path_fg that unfolding zeros_f_def zeros_fg_def by auto have "h p ≠ 0" proof (rule ccontr) assume "¬ h p ≠ 0" then have "cmod (g p/f p) = 1" by (simp add: add_eq_0_iff2 h_def) then show False by (smt (verit) divide_eq_1_iff norm_divide path_less that) 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 s›] 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 ≡ λp. (deriv g p * f p - g p * deriv f p)/(f p * f p)" have "p∈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 s› ‹f p≠0› by (auto intro!: derivative_eq_intros holomorphic_derivI) then show ?thesis unfolding der_def using DERIV_imp_deriv by auto qed show ?thesis using ‹h p≠0› ‹f p≠0› ‹fg p≠0› unfolding der_fg der_h apply (simp add: divide_simps h_def fg_def) by (simp add: mult.commute mult.left_commute ring_class.ring_distribs(1)) qed then have "contour_integral γ (λp. deriv fg p / fg p) = contour_integral γ (λ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 γ (λx. deriv fg x / fg x) = c * (∑p∈zeros_fg. w p * zorder fg p)" proof - have "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto moreover have "path_image γ ⊆ s - {p∈s. fg p = 0}" using path_fg unfolding zeros_fg_def . moreover have " finite {p∈s. fg p = 0}" using ‹finite zeros_fg› unfolding zeros_fg_def . ultimately show ?thesis unfolding c_def zeros_fg_def w_def using argument_principle[OF ‹open s› ‹connected s› _ _ ‹valid_path γ› loop _ homo, of _ "{}" "λ_. 1"] by simp qed moreover have "contour_integral γ (λx. deriv f x / f x) = c * (∑p∈zeros_f. w p * zorder f p)" unfolding c_def zeros_f_def w_def proof (rule argument_principle[OF ‹open s› ‹connected s› _ _ ‹valid_path γ› loop _ homo , of _ "{}" "λ_. 1",simplified]) show "f holomorphic_on s" using f_holo g_holo holomorphic_on_add by auto show "path_image γ ⊆ s - {p∈s. f p = 0}" using path_f unfolding zeros_f_def . show " finite {p∈s. f p = 0}" using ‹finite zeros_f› unfolding zeros_f_def . qed ultimately have " c* (∑p∈zeros_fg. w p * (zorder fg p)) = c* (∑p∈zeros_f. w p * (zorder f p))" by auto then show ?thesis unfolding c_def using w_def by auto qed end