Theory Argument_Principle_Sparse
section ‹A more convenient Argument Principle›
theory Argument_Principle_Sparse
imports "HOL-Complex_Analysis.Complex_Analysis" "Detour_Calculus.Detour_Calculus"
begin
text ‹TODO: replace the @{thm isolated_zeros} in the library;
optimise the proof of @{thm non_zero_neighbour_alt}›
proposition isolated_zeros:
assumes holf: "f holomorphic_on S"
and "open S" "connected S" "ξ ∈ S" "β ∈ S" "f β ≠ 0"
obtains r where "0 < r" and "ball ξ r ⊆ S" and
"⋀z. z ∈ ball ξ r - {ξ} ⟹ f z ≠ 0"
proof (cases "f ξ = 0")
case True
obtain r where "0 < r" and r: "ball ξ r ⊆ S"
using ‹open S› ‹ξ ∈ S› open_contains_ball_eq by blast
have powf: "((λn. (deriv ^^ n) f ξ / (fact n) * (z - ξ)^n) sums f z)" if "z ∈ ball ξ r" for z
by (intro holomorphic_power_series [OF _ that] holomorphic_on_subset [OF holf r])
obtain m where m: "(deriv ^^ m) f ξ / (fact m) ≠ 0"
using holomorphic_fun_eq_0_on_connected [OF holf ‹open S› ‹connected S› _ ‹ξ ∈ S› ‹β ∈ S›] ‹f β ≠ 0›
by auto
then have "m ≠ 0" using True funpow_0 by fastforce
obtain s where "0 < s" and s: "⋀z. z ∈ cball ξ s - {ξ} ⟹ f z ≠ 0"
using powser_0_nonzero [OF ‹0 < r› powf ‹f ξ = 0› m]
by (metis ‹m ≠ 0› dist_norm mem_ball norm_minus_commute not_gr_zero)
have "0 < min r s" by (simp add: ‹0 < r› ‹0 < s›)
then show thesis
apply (rule that)
using r s by auto
next
case False
moreover have "isCont f ξ"
using assms(2) assms(4) field_differentiable_imp_continuous_at holf
holomorphic_on_imp_differentiable_at
by blast
ultimately obtain e1 where "e1>0" "∀y. dist ξ y < e1 ⟶ f y ≠ 0"
using continuous_at_avoid by blast
obtain e2 where "e2>0" "ball ξ e2 ⊆ S"
using assms(2) assms(4) openE by auto
define e where "e = min e1 e2"
have "e>0" by (simp add: ‹0 < e1› ‹0 < e2› e_def)
moreover have "∀y. dist ξ y < e ⟶ f y ≠ 0"
by (simp add: ‹∀y. dist ξ y < e1 ⟶ f y ≠ 0› e_def)
moreover have "ball ξ e ⊆ S"
using ‹ball ξ e2 ⊆ S› e_def by fastforce
ultimately show thesis
using that by auto
qed
lemma holomorphic_compact_finite_zeros':
assumes S: "f holomorphic_on S" "open S" "connected S"
and "compact K" "K ⊆ S"
and "β ∈ S" "f β ≠0"
shows "finite {z∈K. f z = 0}"
proof (rule ccontr)
assume "infinite {z∈K. f z = 0}"
then obtain z where "z ∈ K" and z: "z islimpt {z∈K. f z = 0}"
using ‹compact K› by (auto simp: compact_eq_Bolzano_Weierstrass)
moreover have "{z∈K. f z = 0} ⊆ S"
using ‹K ⊆ S› by blast
ultimately show False
using assms analytic_continuation [OF S] by blast
qed
lemma holomorphic_imp_sparse_zeros:
assumes f_holo: "f holomorphic_on D" and "open D" and "connected D"
and f_nconst: "β ∈ D" "f β ≠ 0"
shows "{x. f x = 0} sparse_in D"
unfolding sparse_in_open[OF ‹open D›]
proof
fix y assume "y ∈ D"
from isolated_zeros[OF f_holo ‹open D› ‹connected D› ‹y ∈ D› ‹β ∈ D› ‹f β≠0›]
obtain r where "0 < r" "ball y r ⊆ D"
"(⋀z. z ∈ ball y r - {y} ⟹ f z ≠ 0)"
by auto
then show "¬ y islimpt {x. f x = 0}"
by (smt (verit) Elementary_Metric_Spaces.open_ball centre_in_ball
insert_Diff insert_iff islimpt_def mem_Collect_eq)
qed
lemma sparse_in_imp_isolated_singularity:
assumes "pts sparse_in D" and f_ana: "f analytic_on D - pts"
and "z ∈ D" and "open D"
shows "isolated_singularity_at f z"
proof -
have "open (D - (pts-{z}))"
by (meson Diff_subset assms(1) assms(4)
open_diff_sparse_pts sparse_in_subset2)
then obtain e1 where "e1>0" "ball z e1 ⊆ D - (pts-{z})"
by (metis Diff_iff assms(3) insertCI openE)
then have "f analytic_on ball z e1 - {z}"
using ‹f analytic_on D - pts›
by (smt (verit, ccfv_threshold) Diff_eq_empty_iff Diff_iff
analytic_on_analytic_at insert_absorb insert_not_empty)
with ‹e1>0›
show ?thesis unfolding isolated_singularity_at_def by auto
qed
lemma nconst_sparse_imp_nzero_neighbour:
assumes f_holo: "f holomorphic_on D - pts"
and "open D" and "connected D" and "pts sparse_in D"
and f_nconst: "¬(∀w∈D-pts. f w=0)"
and "z∈D"and "not_essential f z"
shows "(∀⇩F w in at z. f w ≠ 0 ∧ w ∈ D - pts)"
proof -
obtain β where β: "β ∈ D - pts" "f β≠0"
using f_nconst by auto
have ?thesis if "z∉pts"
proof -
have "∀⇩F w in at z. f w ≠ 0 ∧ w ∈ D - pts"
apply (rule non_zero_neighbour_alt[of f "D-pts" z β])
subgoal by fact
subgoal by (simp add: assms(2) assms(4) open_diff_sparse_pts)
subgoal using sparse_imp_connected
by (metis DIM_complex assms(2) assms(3) assms(4) dual_order.refl)
subgoal by (simp add: assms(6) that)
using β by auto
then show ?thesis by (auto elim:eventually_mono)
qed
moreover have ?thesis if "z∈pts" "¬ f ─z→ 0"
proof -
have "∀⇩F w in at z. w ∈ D - pts"
by (smt (verit, del_insts) Diff_iff assms(2) assms(4) assms(6)
at_within_open eventually_at_topological sparse_in_not_in)
moreover have "∀⇩F w in at z. f w ≠ 0"
proof (cases "is_pole f z")
case True
then show ?thesis using non_zero_neighbour_pole by auto
next
case False
moreover have "not_essential f z" by fact
ultimately obtain c where "c≠0" "f ─z→ c"
by (metis ‹¬ f ─z→ 0› not_essential_def)
then show ?thesis
using tendsto_imp_eventually_ne by auto
qed
ultimately show ?thesis by eventually_elim auto
qed
moreover have ?thesis if "z∈pts" "f ─z→ 0"
proof -
define ff where "ff=(λx. if x=z then 0 else f x)"
define A where "A=D - (pts - {z})"
have "f holomorphic_on A - {z}"
using A_def f_holo by fastforce
moreover have "open A"
by (smt (verit, del_insts) A_def DiffE assms(2) assms(4)
islimpt_def open_diff_sparse_pts sparse_in_def)
ultimately have "ff holomorphic_on A"
using ‹f ─z→ 0› unfolding ff_def
by (rule removable_singularity)
moreover have "connected A"
proof -
have "connected (D - pts)"
by (simp add: assms(2) assms(3) assms(4) sparse_imp_connected)
moreover have "D - pts ⊆ A"
unfolding A_def by auto
moreover have "A ⊆ closure (D - pts)" unfolding A_def
by (metis A_def Diff_empty Diff_insert Diff_insert0
‹open A› at_within_open closure_subset insert_Diff
insert_subset not_trivial_limit_within trivial_limit_at)
ultimately show ?thesis using connected_intermediate_closure
by auto
qed
moreover have "z ∈ A" using A_def assms(6) by blast
moreover have "ff z = 0" unfolding ff_def by auto
moreover have "β ∈ A " using A_def β(1) by blast
moreover have "ff β ≠ 0" using β(1) β(2) ff_def that(1) by auto
ultimately obtain r where "0 < r"
"ball z r ⊆ A" "⋀x. x ∈ ball z r - {z} ⟹ ff x ≠ 0"
using ‹open A› isolated_zeros[of ff A z β] by auto
then show ?thesis unfolding eventually_at ff_def
by (intro exI[of _ r]) (auto simp: A_def dist_commute ball_def)
qed
ultimately show ?thesis by auto
qed
subsection ‹Argument principle›
lemma get_analytic_cover_path:
fixes f :: "complex ⇒ complex" and A pts :: "complex set"
assumes f_analytic: "f analytic_on (path_image γ)" and
γ: "path γ"
obtains e where "e > 0" "f analytic_on (⋃x∈path_image γ. ball x e)"
proof -
obtain get_e where get_e: "get_e x>0" "f holomorphic_on ball x (get_e x)"
if "x∈path_image γ" for x
using f_analytic by (metis analytic_at_ball analytic_on_analytic_at)
obtain e where "e>0"
and "(⋃x∈path_image γ. ball x e)
⊆ (⋃x∈path_image γ. ball x (get_e x))"
proof -
have "compact (path_image γ)"
using ‹path γ› by blast
moreover have "open (⋃x∈path_image γ. ball x (get_e x))"
by blast
moreover have "path_image γ ⊆ (⋃x∈path_image γ. ball x (get_e x))"
using get_e(1) by auto
ultimately show ?thesis
using compact_subset_open_imp_ball_epsilon_subset that by blast
qed
then have "f analytic_on (⋃x∈path_image γ. ball x e)"
using get_e(2)
by (smt (verit) open_ball analytic_on_UN analytic_on_open
analytic_on_subset)
then show ?thesis using that ‹e>0› by auto
qed
lemma get_sparse_cover_path:
assumes sparse: "pts sparse_in (path_image γ)" and "path γ"
obtains e where "e > 0" "∀z∈ (⋃x∈path_image γ. ball x e). ¬z islimpt pts"
proof -
obtain get_e where get_e: "get_e x>0"
"(∀y∈(ball x (get_e x)). ¬ y islimpt pts)"
if "x∈path_image γ" for x
using sparse unfolding sparse_in_ball_def by metis
obtain e where "e>0"
and "(⋃x∈path_image γ. ball x e)
⊆ (⋃x∈path_image γ. ball x (get_e x))"
proof -
have "compact (path_image γ)"
using ‹path γ› by blast
moreover have "open (⋃x∈path_image γ. ball x (get_e x))"
by blast
moreover have "path_image γ ⊆ (⋃x∈path_image γ. ball x (get_e x))"
using get_e(1) by auto
ultimately show ?thesis
using compact_subset_open_imp_ball_epsilon_subset that by blast
qed
then have "∀z∈ (⋃x∈path_image γ. ball x e). ¬ z islimpt pts"
using get_e(2) by blast
then show ?thesis using that ‹e>0› by auto
qed
theorem argument_principle_sparse:
fixes f:: "complex ⇒ complex"
assumes f_analytic: "f analytic_on A - pts" and
γ: "valid_path γ" "pathfinish γ = pathstart γ" "path_image γ ⊆ A - pts" and
inside_subset: "inside (path_image γ) ⊆ A" and
not_essential: "∀p∈pts. not_essential f p" and
sparse: "pts sparse_in A" and
f_nz: "⋀z. z ∈ A - pts ⟹ f z ≠ 0"
shows "contour_integral γ (λx. deriv f x / f x) = 2 * pi * 𝗂 *
(∑⇩∞ z∈pts. winding_number γ z * zorder f z)"
proof -
note [simp del] = div_mult_self3 div_mult_self4 div_mult_self2 div_mult_self1
define B1 where "B1 = path_image γ ∪ inside (path_image γ)"
have "compact B1"
proof -
have "closed B1" unfolding B1_def
apply (rule closed_path_image_Un_inside)
by (simp add: γ(1) valid_path_imp_path)
moreover have "bounded B1" unfolding B1_def
by (simp add: γ(1) bounded_inside bounded_path_image valid_path_imp_path)
ultimately show ?thesis using compact_eq_bounded_closed by auto
qed
have "connected B1"
proof -
have "closed (path_image γ)"
by (simp add: assms(2) closed_valid_path_image)
moreover have "connected (path_image γ)"
by (simp add: assms(2) connected_valid_path_image)
ultimately show ?thesis
unfolding B1_def using connected_with_inside by auto
qed
have "finite (B1 ∩ pts)"
proof (rule sparse_in_compact_finite)
have "B1 ⊆ A" using B1_def assms(4) local.inside_subset by auto
then show "pts sparse_in B1"
using sparse_in_subset sparse by auto
qed fact
obtain get_e where get_e: "get_e x>0" "f holomorphic_on ball x (get_e x)"
if "x∈A - pts" for x
using f_analytic by (metis analytic_at_ball analytic_on_analytic_at)
obtain get_b where get_b: "get_b x>0"
"(∀y∈(ball x (get_b x)). ¬ y islimpt pts)" if "x∈A" for x
using sparse unfolding sparse_in_ball_def by metis
define g_eb where "g_eb = (λx. ball x (min (get_e x) (get_b x)))"
have open_g_eb: "open (⋃x∈path_image γ. g_eb x)"
unfolding g_eb_def using assms(4) get_b(2) by auto
have g_eb_path_image: "path_image γ ⊆ ⋃ (g_eb ` path_image γ)"
unfolding g_eb_def
using assms(4) get_b(1) get_e(1) by force
define B2 where "B2 = (⋃x∈path_image γ. g_eb x) ∪ inside (path_image γ)"
have not_islimpt_B2: "¬ z islimpt pts" if "z∈B2" for z
proof -
have ?thesis if "z∈(⋃x∈path_image γ. g_eb x)"
proof -
from that
obtain x where "x∈path_image γ" "z∈g_eb x"
using get_b(2) unfolding B2_def by auto
from ‹x∈path_image γ› have "x∈A"
using assms(4) by auto
moreover have "z∈ball x (get_b x)"
using ‹z∈g_eb x› unfolding g_eb_def by auto
ultimately show ?thesis using get_b(2) by auto
qed
moreover have ?thesis if "z∈inside (path_image γ)"
using get_b(1) get_b(2) local.inside_subset that by auto
ultimately show ?thesis using that unfolding B2_def by auto
qed
have f_B2_holo: "f holomorphic_on B2 - (B1∩ pts)"
proof -
have "f holomorphic_on (⋃x∈path_image γ. g_eb x) - B1 ∩ pts"
proof -
have "(⋃x∈path_image γ. g_eb x) - B1 ∩ pts
⊆ (⋃x∈path_image γ. ball x (get_e x))"
unfolding g_eb_def by auto
moreover have "f holomorphic_on (⋃x∈path_image γ. ball x (get_e x))"
using assms(4) get_e(2)
by (meson Elementary_Metric_Spaces.open_ball holomorphic_on_UN_open subsetD)
ultimately show ?thesis by auto
qed
moreover have "f holomorphic_on (inside (path_image γ) - B1 ∩ pts)"
by (smt (verit, best) B1_def Diff_Int2 Diff_eq Un_Int_eq(4)
analytic_imp_holomorphic f_analytic holomorphic_on_subset inf_commute
inf_sup_distrib2 local.inside_subset sup.absorb_iff2)
moreover have "open (⋃ (g_eb ` path_image γ) - B1 ∩ pts)"
apply (rule open_Diff)
using open_g_eb ‹finite (B1 ∩ pts)›[THEN finite_imp_closed] by auto
moreover have "open (inside (path_image γ) - B1 ∩ pts)"
by (simp add: γ(1) ‹finite (B1 ∩ pts)› closed_valid_path_image
finite_imp_closed open_Diff open_inside)
ultimately show ?thesis
unfolding B2_def Un_Diff by (rule holomorphic_on_Un)
qed
have "open B2"
proof -
have "open (inside (path_image γ))"
by (simp add: γ(1) closed_valid_path_image open_inside)
with open_g_eb show ?thesis unfolding B2_def by auto
qed
moreover have "B1 ⊆ B2"
using g_eb_path_image unfolding B1_def B2_def by auto
ultimately obtain e0 where e0: "e0 > 0" "(⋃x∈B1. cball x e0) ⊆ B2"
using compact_subset_open_imp_cball_epsilon_subset[OF ‹compact B1›] that
by auto
define e where "e = e0 / 2"
have "e>0" unfolding e_def using ‹e0>0› by auto
have B1_e_open: "open (⋃x∈B1. ball x e)" by blast
have connected_B1_ball: "connected (⋃x∈B1. ball x e)" if "e>0" for e
proof -
have "connected (B1 ∪ (⋃x∈B1. ball x e))"
apply (rule connected_Un_UN)
subgoal by fact
subgoal by blast
subgoal using ‹0 < e› imageE by auto
done
moreover have "B1 ∪ (⋃x∈B1. ball x e) = (⋃x∈B1. ball x e)"
using ‹0 < e› by auto
ultimately show "connected (⋃x∈B1. ball x e)" by simp
qed
have "compact (⋃x∈B1. cball x e)"
apply (rule compact_minkowski_sum_cball)
by fact
obtain β where "β ∈ path_image γ" by auto
then have "β ∈ B1" "β ∉ pts" "f β ≠ 0"
unfolding B1_def using assms(4) f_nz by auto
define B3 where "B3 = (⋃x∈B1. ball x e)"
define pz where "pz = B3 ∩ (pts ∪ {x. f x =0})"
have "open B3" using B3_def by blast
have "finite pz"
proof -
have "pz = (B3 ∩ pts) ∪ ((B3-B1) ∩ -pts ∩ {x. f x =0})
∪ (B1 ∩ -pts ∩ {x. f x =0})"
proof -
have "B1 ⊆ B3" unfolding B1_def B3_def using ‹e>0› by auto
then show ?thesis unfolding pz_def by fast
qed
moreover have "(B1 ∩ -pts ∩ {x. f x =0}) = {}"
proof -
have "B1 ⊆ A" unfolding B1_def
using assms(4) local.inside_subset by auto
with f_nz show ?thesis by blast
qed
moreover have "finite ((B3-B1) ∩ -pts ∩ {x. f x =0})"
proof -
have "finite {z ∈ (⋃x∈B1. cball x e) - inside (path_image γ). f z = 0}"
proof (rule holomorphic_compact_finite_zeros')
from f_B2_holo
show "f holomorphic_on (⋃x∈B1. ball x e0) - B1 ∩ pts"
apply (elim holomorphic_on_subset)
using e0(2) by force
show "open ((⋃x∈B1. ball x e0) - B1 ∩ pts)"
by (simp add: ‹finite (B1 ∩ pts)›
finite_imp_sparse open_UN open_diff_sparse_pts)
show "connected ((⋃x∈B1. ball x e0) - B1 ∩ pts)"
proof (rule connected_open_delete_finite)
show "connected (⋃x∈B1. ball x e0)"
using connected_B1_ball[OF ‹e0>0›] .
qed (use ‹finite (B1 ∩ pts)› in auto)
show "compact ((⋃x∈B1. cball x e) - inside (path_image γ))"
using ‹compact (⋃x∈B1. cball x e)› assms(2)
closed_valid_path_image compact_diff open_inside
by blast
have "(⋃x∈B1. cball x e) ⊆ (⋃x∈B1. ball x e0)"
unfolding e_def using ‹e0>0› by force
moreover have " B1 ∩ pts ⊆ inside (path_image γ)"
unfolding B1_def using DiffE UnE assms(4) by auto
ultimately show "(⋃x∈B1. cball x e) - inside (path_image γ)
⊆ (⋃x∈B1. ball x e0) - B1 ∩ pts"
by auto
show "β ∈ (⋃x∈B1. ball x e0) - B1 ∩ pts"
by (metis Diff_iff IntD2 UN_iff ‹β ∈ B1› ‹β ∉ pts› centre_in_ball e0(1))
show "f β ≠ 0" by fact
qed
moreover have "((B3-B1) ∩ -pts ∩ {x. f x =0})
⊆ {z ∈ (⋃x∈B1. cball x e) - inside (path_image γ). f z = 0}"
unfolding B3_def B1_def using ‹e>0› by force
ultimately show ?thesis by (elim rev_finite_subset)
qed
moreover have "finite (B3 ∩ pts)"
proof -
have "finite ((⋃x∈B1. cball x e) ∩ pts)"
proof (rule finite_not_islimpt_in_compact)
show "¬ z islimpt pts" if "z ∈ (⋃x∈B1. cball x e)" for z
proof -
have "z∈B2" using e0(2) that ‹e0>0› unfolding e_def by force
then show ?thesis by (simp add: not_islimpt_B2)
qed
qed fact
moreover have "(B3 ∩ pts) ⊆ ((⋃x∈B1. cball x e) ∩ pts)"
unfolding pz_def B3_def by auto
ultimately show ?thesis by (elim finite_subset)
qed
ultimately show ?thesis by auto
qed
have f_holo: "f holomorphic_on B3 - (B1 ∩ pts)"
proof -
have "B3 - (B1 ∩ pts) ⊆ B2 - (B1∩ pts)"
using e0 unfolding B3_def e_def by force
then show ?thesis using f_B2_holo by fast
qed
have "connected B3"
by (simp add: B3_def ‹0 < e› connected_B1_ball)
define c where "c ≡ 2 * complex_of_real pi * 𝗂 "
define ff where "ff ≡ (λx. deriv f x / f x)"
define cont where "cont ≡ λff p e. (ff has_contour_integral c * zorder f p) (circlepath p e)"
define avoid where "avoid ≡ λp e. ∀w∈cball p e. w ∈ B3 ∧ (w ≠ p ⟶ w ∉ pz)"
have "∃e>0. avoid p e ∧ (p∈pz ⟶ cont ff p e)" when "p∈B3" for p
proof -
obtain e1 where "e1>0" and e1_avoid: "avoid p e1"
using finite_cball_avoid[OF ‹open B3› ‹finite pz›] ‹p∈B3› 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 / 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 "f holomorphic_on ball p e1 - {p}"
apply (intro holomorphic_on_subset[OF f_holo])
using e1_avoid ‹p∈pz› unfolding avoid_def pz_def by force
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"
using ‹p ∈ pz› not_essential pz_def
by (meson DiffI IntD2 ‹finite (B1 ∩ pts)› ‹open B3› ‹p ∈ B3›
f_holo finite_imp_closed not_essential_holomorphic open_Diff)
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
have "∀⇩F w in at p. f w ≠ 0 ∧ w ∈ B3 - B1 ∩ pts"
proof (rule nconst_sparse_imp_nzero_neighbour)
have "β ∈ B3 - B1 ∩ pts"
by (metis B3_def Diff_iff IntE SUP_upper
‹0 < e› ‹β ∈ B1› ‹β ∉ pts› ‹open B3› open_contains_ball_eq)
then show " ¬ (∀w∈B3 - B1 ∩ pts. f w = 0)"
using ‹f β≠0› by blast
show "B1 ∩ pts sparse_in B3"
by (simp add: ‹finite (B1 ∩ pts)› finite_imp_sparse)
qed fact+
then have "∀⇩F w in at p. False" using ‹∀⇩F w in at p. f w= 0›
by eventually_elim simp
then show False by simp
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/ pp w"
define prin where "prin ≡ λw. po/ (w - p)"
have "((λw. prin w + anal w) has_contour_integral c * po) (circlepath p e2)"
proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified])
have "ball p r ⊆ B3"
using ‹r<e1› avoid_def ball_subset_cball e1_avoid by (simp add: subset_eq)
then have "cball p e2 ⊆ B3"
using ‹r>0› unfolding e2_def by auto
then show "(prin has_contour_integral c * po) (circlepath p e2)"
unfolding prin_def
apply (intro Cauchy_integral_circlepath_simple[folded c_def])
using ‹e2>0› by auto
have "anal holomorphic_on ball p r" unfolding anal_def
using pp_holo pp_po ‹ball p r ⊆ B3› ‹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 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) 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} ⊆ B3 - pts"
using ball_subset_cball e1_avoid[unfolded avoid_def] unfolding pz_def
by auto
then have "ball p r - {p} ⊆ B3 - pts"
apply (elim dual_order.trans)
using ‹r<e1› 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 ∈ 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∈B3. 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 γ p"
have "contour_integral γ ff = (∑p∈pz. w p * ci p)" unfolding ci_def w_def
proof (rule Cauchy_theorem_singularities)
have "open (B3 - pz)" using open_Diff[OF _ finite_imp_closed[OF ‹finite pz›]] ‹open B3›
by auto
then show "ff holomorphic_on B3 - pz" unfolding ff_def using f_holo
by (auto intro!: holomorphic_intros simp add:pz_def)
show "∀p∈B3. 0 < get_e p ∧ (∀w∈cball p (get_e p). w ∈ B3 ∧ (w ≠ p ⟶ w ∉ pz))"
using get_e using avoid_def by blast
show "open B3" "connected B3" "finite pz" "valid_path γ" "pathfinish γ = pathstart γ"
by fact+
show "path_image γ ⊆ B3 - pz"
proof -
have "path_image γ ⊆ B3"
unfolding B3_def B1_def using ‹e>0› by auto
moreover have "path_image γ ⊆ - pts"
using ComplI assms(4) by auto
moreover have "path_image γ ⊆ - {x. f x = 0}"
using assms(4) f_nz by auto
ultimately show ?thesis unfolding pz_def by auto
qed
have "winding_number γ z = 0" if "z ∉ B3" for z
proof (rule winding_number_zero_in_outside)
show "z ∈ outside (path_image γ)"
by (metis B1_def B3_def ComplI SUP_upper ‹0 < e› ‹open B3›
open_contains_ball_eq that union_with_inside)
show "path γ" by (simp add: assms(2) valid_path_imp_path)
qed fact
then show " ∀z. z ∉ B3 ⟶ winding_number γ z = 0" by simp
qed
also have "... = (∑p∈pz. c * w 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 * (zorder f p)"
proof (cases "p∈B3")
assume "p ∈ B3"
have "ci p = c * (zorder f p)" unfolding ci_def
apply (rule contour_integral_unique)
using get_e ‹p∈B3› ‹p∈pz› unfolding cont_def by metis
thus ?thesis by auto
next
assume "p∉B3"
then have "w p=0" unfolding w_def
using ‹p ∈ pz› pz_def by auto
then show ?thesis by auto
qed
qed
also have "... = c*(∑p∈pz. w p * zorder f p)"
unfolding sum_distrib_left by (simp add:algebra_simps)
also have "... = c*(∑p∈(pz∩B1). w p * zorder f p)"
proof -
have "(∑p∈pz. w p * zorder f p)
= (∑p∈(pz∩B1). w p * zorder f p)"
proof (rule sum.mono_neutral_right)
show "∀x∈pz - pz ∩ B1. w x * complex_of_int (zorder f x) = 0"
proof
fix x assume "x ∈ pz - pz ∩ B1"
then have "x ∈ outside (path_image γ)" unfolding B1_def
by (auto simp add: union_with_inside)
then have "w x = 0"
unfolding w_def using winding_number_zero_in_outside
by (simp add: assms(2) assms(3) valid_path_imp_path)
then show "w x * complex_of_int (zorder f x) = 0" by simp
qed
show "finite pz" by fact
show "pz ∩ B1 ⊆ pz" by simp
qed
then show ?thesis by simp
qed
also have "... = c*(∑p∈(B1 ∩ pts). w p * zorder f p)"
proof -
have "B1 ⊆ B3" unfolding B3_def using ‹e>0› by auto
moreover have "{x. f x = 0}∩B1 ⊆ pts ∩ B1 "
using f_nz unfolding B1_def
by (smt (verit, del_insts) Diff_iff Int_iff UnE assms(4)
local.inside_subset mem_Collect_eq subset_eq)
ultimately have "pz∩B1 = (B1 ∩ pts)" unfolding pz_def by auto
then show ?thesis by auto
qed
also have "... = c*(∑⇩∞p∈(B1 ∩ pts). w p * zorder f p)"
using ‹finite (B1 ∩ pts)› by auto
also have "... = c*(∑⇩∞p∈pts. w p * zorder f p)"
proof -
have "(∑⇩∞p∈(B1 ∩ pts). w p * zorder f p)
= (∑⇩∞p∈pts. w p * zorder f p)"
proof (rule infsum_cong_neutral)
fix x assume "x ∈ pts - B1 ∩ pts"
then have "x ∈ outside (path_image γ)" unfolding B1_def
by (auto simp add: union_with_inside)
then have "w x = 0"
unfolding w_def using winding_number_zero_in_outside
by (simp add: assms(2) assms(3) valid_path_imp_path)
then show "w x * complex_of_int (zorder f x) = 0" by simp
qed auto
then show ?thesis by simp
qed
finally show ?thesis unfolding ff_def c_def w_def by simp
qed
corollary argument_principle_finite:
fixes f:: "complex ⇒ complex"
assumes f_analytic: "f analytic_on A - pts" and
γ: "valid_path γ" "pathfinish γ = pathstart γ" "path_image γ ⊆ A - pts" and
inside_subset: "inside (path_image γ) ⊆ A" and
not_essential: "∀p∈pts. not_essential f p" and
sparse: "finite pts" and
f_nz: "⋀z. z ∈ A - pts ⟹ f z ≠ 0"
shows "contour_integral γ (λx. deriv f x / f x) = 2 * pi * 𝗂 *
(∑z∈pts. winding_number γ z * zorder f z)"
proof -
have "contour_integral γ (λx. deriv f x / f x) = 2 * pi * 𝗂 *
(∑⇩∞ z∈pts. winding_number γ z * zorder f z)"
proof (rule argument_principle_sparse)
show " pts sparse_in A"
by (simp add: finite_imp_sparse ‹finite pts›)
qed fact+
moreover have "(∑⇩∞ z∈pts. winding_number γ z * zorder f z)
= (∑z∈pts. winding_number γ z * zorder f z)"
by (rule infsum_finite) fact
ultimately show ?thesis by simp
qed
corollary argument_principle_ccw_analytic:
fixes f:: "complex ⇒ complex"
assumes f_analytic: "f analytic_on A - pts" and
γ: "valid_path γ" "simple_loop_ccw γ" "path_image γ ⊆ A - pts" and
inside_subset: "inside (path_image γ) ⊆ A" and
not_essential: "∀p∈pts. not_essential f p" and
sparse: "pts sparse_in A" and
f_nz: "⋀z. z ∈ A - pts ⟹ f z ≠ 0"
shows "contour_integral γ (λx. deriv f x / f x) = 2 * pi * 𝗂 *
(∑z∈pts∩inside (path_image γ). zorder f z)"
proof -
have "contour_integral γ (λx. deriv f x / f x) =
2 * pi * 𝗂 * (∑⇩∞z∈pts. winding_number γ z * (zorder f z))"
proof (rule argument_principle_sparse)
show "pathfinish γ = pathstart γ"
by (metis γ(2) simple_loop_ccw_def simple_loop_def)
qed fact+
moreover have "(∑⇩∞z∈pts. winding_number γ z * (zorder f z))
= (∑z∈pts∩inside (path_image γ). complex_of_int (zorder f z))" (is "?L=?R")
proof -
have "?L = (∑⇩∞z∈pts ∩ inside (path_image γ).
winding_number γ z * (zorder f z))"
proof (rule infsum_cong_neutral)
fix x assume "x ∈ pts - pts ∩ inside (path_image γ)"
then have "x ∈ outside (path_image γ)"
using γ(2) γ(3)
by (metis DiffE Int_iff Set.basic_monos(7)
inside_simple_loop_iff outside_simple_loop_iff simple_loop_ccw_def)
then have "winding_number γ x =0"
using γ(2) outside_simple_loop_iff simple_loop_ccw_def by blast
then show "winding_number γ x * complex_of_int (zorder f x) = 0"
by simp
qed auto
also have "... = (∑z∈pts ∩ inside (path_image γ).
winding_number γ z * (zorder f z))"
proof (rule infsum_finite)
define B1 where "B1 = path_image γ ∪ inside (path_image γ)"
have "compact B1"
proof -
have "closed B1" unfolding B1_def
apply (rule closed_path_image_Un_inside)
by (simp add: γ(1) valid_path_imp_path)
moreover have "bounded B1" unfolding B1_def
by (simp add: γ(1) bounded_inside bounded_path_image valid_path_imp_path)
ultimately show ?thesis using compact_eq_bounded_closed by auto
qed
moreover have "pts sparse_in B1"
unfolding B1_def using assms(4) assms(5) assms(7)
by (meson Diff_subset dual_order.trans sparse_in_subset sup_least)
ultimately have "finite (B1 ∩ pts)"
using sparse_in_compact_finite by auto
then show "finite (pts ∩ inside (path_image γ))"
apply (elim rev_finite_subset)
unfolding B1_def by auto
qed
also have "... = ?R"
proof (rule sum.cong)
fix x assume "x ∈ pts ∩ inside (path_image γ)"
then have "winding_number γ x = 1"
by (metis IntD2 γ(2) inside_simple_loop_iff
simple_closed_path_winding_number_inside
simple_loop_ccw_def simple_loop_cw_def simple_loop_def
simple_path_not_cw_and_ccw)
then show "winding_number γ x * zorder f x = zorder f x" by simp
qed simp
finally show ?thesis .
qed
ultimately show ?thesis by simp
qed
end