Theory Residue_Theorem
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}"
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