section ‹Winding numbers› theory Winding_Numbers imports Cauchy_Integral_Theorem begin subsection ‹Definition› definition✐‹tag important› winding_number_prop :: "[real ⇒ complex, complex, real, real ⇒ complex, complex] ⇒ bool" where "winding_number_prop γ z e p n ≡ valid_path p ∧ z ∉ path_image p ∧ pathstart p = pathstart γ ∧ pathfinish p = pathfinish γ ∧ (∀t ∈ {0..1}. norm(γ t - p t) < e) ∧ contour_integral p (λw. 1/(w - z)) = 2 * pi * 𝗂 * n" definition✐‹tag important› winding_number:: "[real ⇒ complex, complex] ⇒ complex" where "winding_number γ z ≡ SOME n. ∀e > 0. ∃p. winding_number_prop γ z e p n" lemma winding_number: assumes "path γ" "z ∉ path_image γ" "0 < e" shows "∃p. winding_number_prop γ z e p (winding_number γ z)" proof - have "path_image γ ⊆ UNIV - {z}" using assms by blast then obtain d where d: "d>0" and pi_eq: "⋀h1 h2. valid_path h1 ∧ valid_path h2 ∧ (∀t∈{0..1}. cmod (h1 t - γ t) < d ∧ cmod (h2 t - γ t) < d) ∧ pathstart h2 = pathstart h1 ∧ pathfinish h2 = pathfinish h1 ⟶ path_image h1 ⊆ UNIV - {z} ∧ path_image h2 ⊆ UNIV - {z} ∧ (∀f. f holomorphic_on UNIV - {z} ⟶ contour_integral h2 f = contour_integral h1 f)" using contour_integral_nearby_ends [of "UNIV - {z}" γ] assms by (auto simp: open_delete) then obtain h where h: "polynomial_function h ∧ pathstart h = pathstart γ ∧ pathfinish h = pathfinish γ ∧ (∀t ∈ {0..1}. norm(h t - γ t) < d/2)" using path_approx_polynomial_function [OF ‹path γ›, of "d/2"] d by (metis half_gt_zero_iff) define nn where "nn = 1/(2* pi*𝗂) * contour_integral h (λw. 1/(w - z))" have "∃n. ∀e > 0. ∃p. winding_number_prop γ z e p n" proof (rule_tac x=nn in exI, clarify) fix e::real assume e: "e>0" obtain p where p: "polynomial_function p ∧ pathstart p = pathstart γ ∧ pathfinish p = pathfinish γ ∧ (∀t∈{0..1}. cmod (p t - γ t) < min e (d/2))" using path_approx_polynomial_function [OF ‹path γ›, of "min e (d/2)"] d ‹0<e› by (metis min_less_iff_conj zero_less_divide_iff zero_less_numeral) have "(λw. 1 / (w - z)) holomorphic_on UNIV - {z}" by (auto simp: intro!: holomorphic_intros) then have "winding_number_prop γ z e p nn" using pi_eq [of h p] h p d by (auto simp: valid_path_polynomial_function norm_minus_commute nn_def winding_number_prop_def) then show "∃p. winding_number_prop γ z e p nn" by metis qed then show ?thesis unfolding winding_number_def by (rule someI2_ex) (blast intro: ‹0<e›) qed lemma winding_number_unique: assumes γ: "path γ" "z ∉ path_image γ" and pi: "⋀e. e>0 ⟹ ∃p. winding_number_prop γ z e p n" shows "winding_number γ z = n" proof - have "path_image γ ⊆ UNIV - {z}" using assms by blast then obtain e where e: "e>0" and pi_eq: "⋀h1 h2 f. ⟦valid_path h1; valid_path h2; (∀t∈{0..1}. cmod (h1 t - γ t) < e ∧ cmod (h2 t - γ t) < e); pathstart h2 = pathstart h1; pathfinish h2 = pathfinish h1; f holomorphic_on UNIV - {z}⟧ ⟹ contour_integral h2 f = contour_integral h1 f" using contour_integral_nearby_ends [of "UNIV - {z}" γ] assms by (auto simp: open_delete) obtain p where p: "winding_number_prop γ z e p n" using pi [OF e] by blast obtain q where q: "winding_number_prop γ z e q (winding_number γ z)" using winding_number [OF γ e] by blast have "2 * complex_of_real pi * 𝗂 * n = contour_integral p (λw. 1 / (w - z))" using p by (auto simp: winding_number_prop_def) also have "… = contour_integral q (λw. 1 / (w - z))" proof (rule pi_eq) show "(λw. 1 / (w - z)) holomorphic_on UNIV - {z}" by (auto intro!: holomorphic_intros) qed (use p q in ‹auto simp: winding_number_prop_def norm_minus_commute›) also have "… = 2 * complex_of_real pi * 𝗂 * winding_number γ z" using q by (auto simp: winding_number_prop_def) finally have "2 * complex_of_real pi * 𝗂 * n = 2 * complex_of_real pi * 𝗂 * winding_number γ z" . then show ?thesis by simp qed lemma winding_number_prop_reversepath: assumes "winding_number_prop γ z e p n" shows "winding_number_prop (reversepath γ) z e (reversepath p) (-n)" proof - have p: "valid_path p" "z ∉ path_image p" "pathstart p = pathstart γ" "pathfinish p = pathfinish γ" "⋀t. t ∈ {0..1} ⟹ norm (γ t - p t) < e" "contour_integral p (λw. 1 / (w - z)) = 2 * complex_of_real pi * 𝗂 * n" using assms by (auto simp: winding_number_prop_def) show ?thesis unfolding winding_number_prop_def proof (intro conjI strip) show "norm (reversepath γ t - reversepath p t) < e" if "t ∈ {0..1}" for t unfolding reversepath_def using p(5)[of "1 - t"] that by auto show "contour_integral (reversepath p) (λw. 1 / (w - z)) = complex_of_real (2 * pi) * 𝗂 * - n" using p by (subst contour_integral_reversepath) auto qed (use p in auto) qed lemma winding_number_prop_reversepath_iff: "winding_number_prop (reversepath γ) z e p n ⟷ winding_number_prop γ z e (reversepath p) (-n)" using winding_number_prop_reversepath[of "reversepath γ" z e p n] winding_number_prop_reversepath[of γ z e "reversepath p" "-n"] by auto (*NB not winding_number_prop here due to the loop in p*) lemma winding_number_unique_loop: assumes γ: "path γ" "z ∉ path_image γ" and loop: "pathfinish γ = pathstart γ" and pi: "⋀e. e>0 ⟹ ∃p. valid_path p ∧ z ∉ path_image p ∧ pathfinish p = pathstart p ∧ (∀t ∈ {0..1}. norm (γ t - p t) < e) ∧ contour_integral p (λw. 1/(w - z)) = 2 * pi * 𝗂 * n" shows "winding_number γ z = n" proof - have "path_image γ ⊆ UNIV - {z}" using assms by blast then obtain e where e: "e>0" and pi_eq: "⋀h1 h2 f. ⟦valid_path h1; valid_path h2; (∀t∈{0..1}. cmod (h1 t - γ t) < e ∧ cmod (h2 t - γ t) < e); pathfinish h1 = pathstart h1; pathfinish h2 = pathstart h2; f holomorphic_on UNIV - {z}⟧ ⟹ contour_integral h2 f = contour_integral h1 f" using contour_integral_nearby_loops [of "UNIV - {z}" γ] assms by (auto simp: open_delete) obtain p where p: "valid_path p ∧ z ∉ path_image p ∧ pathfinish p = pathstart p ∧ (∀t ∈ {0..1}. norm (γ t - p t) < e) ∧ contour_integral p (λw. 1/(w - z)) = 2 * pi * 𝗂 * n" using pi [OF e] by blast obtain q where q: "winding_number_prop γ z e q (winding_number γ z)" using winding_number [OF γ e] by blast have "2 * complex_of_real pi * 𝗂 * n = contour_integral p (λw. 1 / (w - z))" using p by auto also have "… = contour_integral q (λw. 1 / (w - z))" proof (rule pi_eq) show "(λw. 1 / (w - z)) holomorphic_on UNIV - {z}" by (auto intro!: holomorphic_intros) qed (use p q loop in ‹auto simp: winding_number_prop_def norm_minus_commute›) also have "… = 2 * complex_of_real pi * 𝗂 * winding_number γ z" using q by (auto simp: winding_number_prop_def) finally have "2 * complex_of_real pi * 𝗂 * n = 2 * complex_of_real pi * 𝗂 * winding_number γ z" . then show ?thesis by simp qed proposition winding_number_valid_path: assumes "valid_path γ" "z ∉ path_image γ" shows "winding_number γ z = 1/(2*pi*𝗂) * contour_integral γ (λw. 1/(w - z))" by (rule winding_number_unique) (use assms in ‹auto simp: valid_path_imp_path winding_number_prop_def›) proposition has_contour_integral_winding_number: assumes γ: "valid_path γ" "z ∉ path_image γ" shows "((λw. 1/(w - z)) has_contour_integral (2*pi*𝗂*winding_number γ z)) γ" by (simp add: winding_number_valid_path has_contour_integral_integral contour_integrable_inversediff assms) lemma winding_number_trivial [simp]: "z ≠ a ⟹ winding_number(linepath a a) z = 0" by (simp add: winding_number_valid_path) lemma winding_number_subpath_trivial [simp]: "z ≠ g x ⟹ winding_number (subpath x x g) z = 0" by (simp add: path_image_subpath winding_number_valid_path) lemma winding_number_join: assumes γ1: "path γ1" "z ∉ path_image γ1" and γ2: "path γ2" "z ∉ path_image γ2" and "pathfinish γ1 = pathstart γ2" shows "winding_number(γ1 +++ γ2) z = winding_number γ1 z + winding_number γ2 z" proof (rule winding_number_unique) show "∃p. winding_number_prop (γ1 +++ γ2) z e p (winding_number γ1 z + winding_number γ2 z)" if "e > 0" for e proof - obtain p1 where "winding_number_prop γ1 z e p1 (winding_number γ1 z)" using ‹0 < e› γ1 winding_number by blast moreover obtain p2 where "winding_number_prop γ2 z e p2 (winding_number γ2 z)" using ‹0 < e› γ2 winding_number by blast ultimately have "winding_number_prop (γ1+++γ2) z e (p1+++p2) (winding_number γ1 z + winding_number γ2 z)" using assms apply (simp add: winding_number_prop_def not_in_path_image_join contour_integrable_inversediff algebra_simps) apply (auto simp: joinpaths_def) done then show ?thesis by blast qed qed (use assms in ‹auto simp: not_in_path_image_join›) lemma winding_number_reversepath: assumes "path γ" "z ∉ path_image γ" shows "winding_number(reversepath γ) z = - (winding_number γ z)" proof (rule winding_number_unique) show "∃p. winding_number_prop (reversepath γ) z e p (- winding_number γ z)" if "e > 0" for e proof - obtain p where "winding_number_prop γ z e p (winding_number γ z)" using ‹0 < e› assms winding_number by blast then have "winding_number_prop (reversepath γ) z e (reversepath p) (- winding_number γ z)" using assms unfolding winding_number_prop_def apply (simp add: contour_integral_reversepath contour_integrable_inversediff valid_path_imp_reverse) apply (auto simp: reversepath_def) done then show ?thesis by blast qed qed (use assms in auto) lemma winding_number_shiftpath: assumes γ: "path γ" "z ∉ path_image γ" and "pathfinish γ = pathstart γ" "a ∈ {0..1}" shows "winding_number(shiftpath a γ) z = winding_number γ z" proof (rule winding_number_unique_loop) show "∃p. valid_path p ∧ z ∉ path_image p ∧ pathfinish p = pathstart p ∧ (∀t∈{0..1}. cmod (shiftpath a γ t - p t) < e) ∧ contour_integral p (λw. 1 / (w - z)) = 2 * pi * 𝗂 * winding_number γ z" if "e > 0" for e proof - obtain p where "winding_number_prop γ z e p (winding_number γ z)" using ‹0 < e› assms winding_number by blast then show ?thesis apply (rule_tac x="shiftpath a p" in exI) using assms that apply (auto simp: winding_number_prop_def path_image_shiftpath pathfinish_shiftpath pathstart_shiftpath contour_integral_shiftpath) apply (simp add: shiftpath_def) done qed qed (use assms in ‹auto simp: path_shiftpath path_image_shiftpath pathfinish_shiftpath pathstart_shiftpath›) lemma winding_number_split_linepath: assumes "c ∈ closed_segment a b" "z ∉ closed_segment a b" shows "winding_number(linepath a b) z = winding_number(linepath a c) z + winding_number(linepath c b) z" proof - have "z ∉ closed_segment a c" "z ∉ closed_segment c b" using assms by (meson convex_contains_segment convex_segment ends_in_segment subsetCE)+ then show ?thesis using assms by (simp add: winding_number_valid_path contour_integral_split_linepath [symmetric] continuous_on_inversediff field_simps) qed lemma winding_number_cong: "(⋀t. ⟦0 ≤ t; t ≤ 1⟧ ⟹ p t = q t) ⟹ winding_number p z = winding_number q z" by (simp add: winding_number_def winding_number_prop_def pathstart_def pathfinish_def) lemma winding_number_constI: assumes "c≠z" and g: "⋀t. ⟦0≤t; t≤1⟧ ⟹ g t = c" shows "winding_number g z = 0" proof - have "winding_number g z = winding_number (linepath c c) z" using g winding_number_cong by fastforce moreover have "winding_number (linepath c c) z = 0" using ‹c≠z› by auto ultimately show ?thesis by auto qed lemma winding_number_offset: "winding_number p z = winding_number (λw. p w - z) 0" unfolding winding_number_def proof (intro ext arg_cong [where f = Eps] arg_cong [where f = All] imp_cong refl, safe) fix n e g assume "0 < e" and g: "winding_number_prop p z e g n" then show "∃r. winding_number_prop (λw. p w - z) 0 e r n" by (rule_tac x="λt. g t - z" in exI) (force simp: winding_number_prop_def contour_integral_integral valid_path_def path_defs vector_derivative_def has_vector_derivative_diff_const piecewise_C1_differentiable_diff C1_differentiable_imp_piecewise) next fix n e g assume "0 < e" and g: "winding_number_prop (λw. p w - z) 0 e g n" then have "winding_number_prop p z e (λt. g t + z) n" apply (simp add: winding_number_prop_def contour_integral_integral valid_path_def path_defs piecewise_C1_differentiable_add vector_derivative_def has_vector_derivative_add_const C1_differentiable_imp_piecewise) apply (force simp: algebra_simps) done then show "∃r. winding_number_prop p z e r n" by metis qed lemma winding_number_negatepath: assumes γ: "valid_path γ" and 0: "0 ∉ path_image γ" shows "winding_number(uminus ∘ γ) 0 = winding_number γ 0" proof - have "(/) 1 contour_integrable_on γ" using "0" γ contour_integrable_inversediff by fastforce then have "((λz. 1/z) has_contour_integral contour_integral γ ((/) 1)) γ" by (rule has_contour_integral_integral) then have "((λz. 1 / - z) has_contour_integral - contour_integral γ ((/) 1)) γ" using has_contour_integral_neg by auto then have "contour_integral (uminus ∘ γ) ((/) 1) = contour_integral γ ((/) 1)" using γ by (simp add: contour_integral_unique has_contour_integral_negatepath) then show ?thesis using assms by (simp add: winding_number_valid_path valid_path_negatepath image_def path_defs) qed lemma winding_number_cnj: assumes "path γ" "z ∉ path_image γ" shows "winding_number (cnj ∘ γ) (cnj z) = -cnj (winding_number γ z)" proof (rule winding_number_unique) show "∃p. winding_number_prop (cnj ∘ γ) (cnj z) e p (-cnj (winding_number γ z))" if "e > 0" for e proof - from winding_number[OF assms(1,2) ‹e > 0›] obtain p where "winding_number_prop γ z e p (winding_number γ z)" by blast then have p: "valid_path p" "z ∉ path_image p" "pathstart p = pathstart γ" "pathfinish p = pathfinish γ" "⋀t. t ∈ {0..1} ⟹ cmod (γ t - p t) < e" and p_cont:"contour_integral p (λw. 1 / (w - z)) = complex_of_real (2 * pi) * 𝗂 * winding_number γ z" unfolding winding_number_prop_def by auto have "valid_path (cnj ∘ p)" using p(1) by (subst valid_path_cnj) auto moreover have "cnj z ∉ path_image (cnj ∘ p)" using p(2) by (auto simp: path_image_def) moreover have "pathstart (cnj ∘ p) = pathstart (cnj ∘ γ)" using p(3) by (simp add: pathstart_compose) moreover have "pathfinish (cnj ∘ p) = pathfinish (cnj ∘ γ)" using p(4) by (simp add: pathfinish_compose) moreover have "cmod ((cnj ∘ γ) t - (cnj ∘ p) t) < e" if t: "t ∈ {0..1}" for t proof - have "(cnj ∘ γ) t - (cnj ∘ p) t = cnj (γ t - p t)" by simp also have "norm … = norm (γ t - p t)" by (subst complex_mod_cnj) auto also have "… < e" using p(5)[OF t] by simp finally show ?thesis . qed moreover have "contour_integral (cnj ∘ p) (λw. 1 / (w - cnj z)) = cnj (complex_of_real (2 * pi) * 𝗂 * winding_number γ z)" (is "?L=?R") proof - have "?L = contour_integral (cnj ∘ p) (cnj ∘ (λw. 1 / (cnj w - z)))" by (simp add: o_def) also have "… = cnj (contour_integral p (λx. 1 / (x - z)))" using p(1) by (subst contour_integral_cnj) (auto simp: o_def) also have "… = ?R" using p_cont by simp finally show ?thesis . qed ultimately show ?thesis by (intro exI[of _ "cnj ∘ p"]) (auto simp: winding_number_prop_def) qed show "path (cnj ∘ γ)" by (intro path_continuous_image continuous_intros) (use assms in auto) show "cnj z ∉ path_image (cnj ∘ γ)" using ‹z ∉ path_image γ› unfolding path_image_def by auto qed text ‹A combined theorem deducing several things piecewise.› lemma winding_number_join_pos_combined: "⟦valid_path γ1; z ∉ path_image γ1; 0 < Re(winding_number γ1 z); valid_path γ2; z ∉ path_image γ2; 0 < Re(winding_number γ2 z); pathfinish γ1 = pathstart γ2⟧ ⟹ valid_path(γ1 +++ γ2) ∧ z ∉ path_image(γ1 +++ γ2) ∧ 0 < Re(winding_number(γ1 +++ γ2) z)" by (simp add: valid_path_join path_image_join winding_number_join valid_path_imp_path) subsubsection✐‹tag unimportant› ‹Useful sufficient conditions for the winding number to be positive› lemma Re_winding_number: "⟦valid_path γ; z ∉ path_image γ⟧ ⟹ Re(winding_number γ z) = Im(contour_integral γ (λw. 1/(w - z))) / (2*pi)" by (simp add: winding_number_valid_path field_simps Re_divide power2_eq_square) lemma winding_number_pos_le: assumes γ: "valid_path γ" "z ∉ path_image γ" and ge: "⋀x. ⟦0 < x; x < 1⟧ ⟹ 0 ≤ Im (vector_derivative γ (at x) * cnj(γ x - z))" shows "0 ≤ Re(winding_number γ z)" proof - have ge0: "0 ≤ Im (vector_derivative γ (at x) / (γ x - z))" if x: "0 < x" "x < 1" for x using ge by (simp add: Complex.Im_divide algebra_simps x) let ?vd = "λx. 1 / (γ x - z) * vector_derivative γ (at x)" let ?int = "λz. contour_integral γ (λw. 1 / (w - z))" have "0 ≤ Im (?int z)" proof (rule has_integral_component_nonneg [of 𝗂, simplified]) show "⋀x. x ∈ cbox 0 1 ⟹ 0 ≤ Im (if 0 < x ∧ x < 1 then ?vd x else 0)" by (force simp: ge0) have "((λa. 1 / (a - z)) has_contour_integral contour_integral γ (λw. 1 / (w - z))) γ" using γ by (simp flip: add: contour_integrable_inversediff has_contour_integral_integral) then have hi: "(?vd has_integral ?int z) (cbox 0 1)" using has_contour_integral by auto show "((λx. if 0 < x ∧ x < 1 then ?vd x else 0) has_integral ?int z) (cbox 0 1)" by (rule has_integral_spike_interior [OF hi]) simp qed then show ?thesis by (simp add: Re_winding_number [OF γ] field_simps) qed lemma winding_number_pos_lt_lemma: assumes γ: "valid_path γ" "z ∉ path_image γ" and e: "0 < e" and ge: "⋀x. ⟦0 < x; x < 1⟧ ⟹ e ≤ Im (vector_derivative γ (at x) / (γ x - z))" shows "0 < Re(winding_number γ z)" proof - let ?vd = "λx. 1 / (γ x - z) * vector_derivative γ (at x)" let ?int = "λz. contour_integral γ (λw. 1 / (w - z))" have "e ≤ Im (contour_integral γ (λw. 1 / (w - z)))" proof (rule has_integral_component_le [of 𝗂 "λx. 𝗂*e" "𝗂*e" "{0..1}", simplified]) have "((λa. 1 / (a - z)) has_contour_integral contour_integral γ (λw. 1 / (w - z))) γ" thm has_integral_component_le [of 𝗂 "λx. 𝗂*e" "𝗂*e" "{0..1}", simplified] using γ by (simp add: contour_integrable_inversediff has_contour_integral_integral) then have hi: "(?vd has_integral ?int z) (cbox 0 1)" using has_contour_integral by auto show "((λx. if 0 < x ∧ x < 1 then ?vd x else 𝗂 * e) has_integral ?int z) {0..1}" by (rule has_integral_spike_interior [OF hi, simplified box_real]) (use e in simp) show "⋀x. 0 ≤ x ∧ x ≤ 1 ⟹ e ≤ Im (if 0 < x ∧ x < 1 then ?vd x else 𝗂 * e)" by (simp add: ge) qed (use has_integral_const_real [of _ 0 1] in auto) with e show ?thesis by (simp add: Re_winding_number [OF γ] field_simps) qed lemma winding_number_pos_lt: assumes γ: "valid_path γ" "z ∉ path_image γ" and e: "0 < e" and ge: "⋀x. ⟦0 < x; x < 1⟧ ⟹ e ≤ Im (vector_derivative γ (at x) * cnj(γ x - z))" shows "0 < Re (winding_number γ z)" proof - have bm: "bounded ((λw. w - z) ` (path_image γ))" using bounded_translation [of _ "-z"] γ by (simp add: bounded_valid_path_image) then obtain B where B: "B > 0" and Bno: "⋀x. x ∈ (λw. w - z) ` (path_image γ) ⟹ norm x ≤ B" using bounded_pos [THEN iffD1, OF bm] by blast { fix x::real assume x: "0 < x" "x < 1" then have B2: "cmod (γ x - z)^2 ≤ B^2" using Bno [of "γ x - z"] by (simp add: path_image_def power2_eq_square mult_mono') with x have "γ x ≠ z" using γ using path_image_def by fastforce then have "e / B⇧^{2}≤ e / (cmod (γ x - z))⇧^{2}" using B B2 e by (auto simp: divide_left_mono) also have "... ≤ Im (vector_derivative γ (at x) * cnj (γ x - z)) / (cmod (γ x - z))⇧^{2}" using ge [OF x] by (auto simp: divide_right_mono) finally have "e / B⇧^{2}≤ Im (vector_derivative γ (at x) * cnj (γ x - z)) / (cmod (γ x - z))⇧^{2}" . then have "e / B⇧^{2}≤ Im (vector_derivative γ (at x) / (γ x - z))" by (simp add: complex_div_cnj [of _ "γ x - z" for x] del: complex_cnj_diff times_complex.sel) } note * = this show ?thesis using e B by (simp add: * winding_number_pos_lt_lemma [OF γ, of "e/B^2"]) qed subsection‹The winding number is an integer› text‹Proof from the book Complex Analysis by Lars V. Ahlfors, Chapter 4, section 2.1, Also on page 134 of Serge Lang's book with the name title, etc.› lemma exp_fg: fixes z::complex assumes g: "(g has_vector_derivative g') (at x within s)" and f: "(f has_vector_derivative (g' / (g x - z))) (at x within s)" and z: "g x ≠ z" shows "((λx. exp(-f x) * (g x - z)) has_vector_derivative 0) (at x within s)" proof - have *: "(exp ∘ (λx. (- f x)) has_vector_derivative - (g' / (g x - z)) * exp (- f x)) (at x within s)" using assms unfolding has_vector_derivative_def scaleR_conv_of_real by (auto intro!: derivative_eq_intros) show ?thesis using z by (auto intro!: derivative_eq_intros * [unfolded o_def] g) qed lemma winding_number_exp_integral: fixes z::complex assumes γ: "γ piecewise_C1_differentiable_on {a..b}" and ab: "a ≤ b" and z: "z ∉ γ ` {a..b}" shows "(λx. vector_derivative γ (at x) / (γ x - z)) integrable_on {a..b}" (is "?thesis1") "exp (- (integral {a..b} (λx. vector_derivative γ (at x) / (γ x - z)))) * (γ b - z) = γ a - z" (is "?thesis2") proof - let ?Dγ = "λx. vector_derivative γ (at x)" have [simp]: "⋀x. a ≤ x ⟹ x ≤ b ⟹ γ x ≠ z" using z by force have con_g: "continuous_on {a..b} γ" using γ by (simp add: piecewise_C1_differentiable_on_def) obtain k where fink: "finite k" and g_C1_diff: "γ C1_differentiable_on ({a..b} - k)" using γ by (force simp: piecewise_C1_differentiable_on_def) have ∘: "open ({a<..<b} - k)" using ‹finite k› by (simp add: finite_imp_closed open_Diff) moreover have "{a<..<b} - k ⊆ {a..b} - k" by force ultimately have g_diff_at: "⋀x. ⟦x ∉ k; x ∈ {a<..<b}⟧ ⟹ γ differentiable at x" by (metis Diff_iff differentiable_on_subset C1_diff_imp_diff [OF g_C1_diff] differentiable_on_def at_within_open) { fix w assume "w ≠ z" have "continuous_on (ball w (cmod (w - z))) (λw. 1 / (w - z))" by (auto simp: dist_norm intro!: continuous_intros) moreover have "⋀x. cmod (w - x) < cmod (w - z) ⟹ ∃f'. ((λw. 1 / (w - z)) has_field_derivative f') (at x)" by (auto simp: intro!: derivative_eq_intros) ultimately have "∃h. ∀y. norm(y - w) < norm(w - z) ⟶ (h has_field_derivative 1/(y - z)) (at y)" using holomorphic_convex_primitive [of "ball w (norm(w - z))" "{}" "λw. 1/(w - z)"] by (force simp: field_differentiable_def Ball_def dist_norm at_within_open_NO_MATCH norm_minus_commute) } then obtain h where h: "⋀w y. w ≠ z ⟹ norm(y - w) < norm(w - z) ⟹ (h w has_field_derivative 1/(y - z)) (at y)" by meson have exy: "∃y. ((λx. inverse (γ x - z) * ?Dγ x) has_integral y) {a..b}" unfolding integrable_on_def [symmetric] proof (rule contour_integral_local_primitive_any [OF piecewise_C1_imp_differentiable [OF γ]]) show "∃d h. 0 < d ∧ (∀y. cmod (y - w) < d ⟶ (h has_field_derivative inverse (y - z))(at y within - {z}))" if "w ∈ - {z}" for w using that inverse_eq_divide has_field_derivative_at_within h by (metis Compl_insert DiffD2 insertCI right_minus_eq zero_less_norm_iff) qed simp have vg_int: "(λx. ?Dγ x / (γ x - z)) integrable_on {a..b}" unfolding box_real [symmetric] divide_inverse_commute by (auto intro!: exy integrable_subinterval simp add: integrable_on_def ab) with ab show ?thesis1 by (simp add: divide_inverse_commute integral_def integrable_on_def) { fix t assume t: "t ∈ {a..b}" have cball: "continuous_on (ball (γ t) (dist (γ t) z)) (λx. inverse (x - z))" using z by (auto intro!: continuous_intros simp: dist_norm) have icd: "⋀x. cmod (γ t - x) < cmod (γ t - z) ⟹ (λw. inverse (w - z)) field_differentiable at x" unfolding field_differentiable_def by (force simp: intro!: derivative_eq_intros) obtain h where h: "⋀x. cmod (γ t - x) < cmod (γ t - z) ⟹ (h has_field_derivative inverse (x - z)) (at x within {y. cmod (γ t - y) < cmod (γ t - z)})" using holomorphic_convex_primitive [where f = "λw. inverse(w - z)", OF convex_ball finite.emptyI cball icd] by simp (auto simp: ball_def dist_norm that) have "exp (- (integral {a..t} (λx. ?Dγ x / (γ x - z)))) * (γ t - z) =γ a - z" proof (rule has_derivative_zero_unique_strong_interval [of "{a,b} ∪ k" a b]) show "continuous_on {a..b} (λb. exp (- integral {a..b} (λx. ?Dγ x / (γ x - z))) * (γ b - z))" by (auto intro!: continuous_intros con_g indefinite_integral_continuous_1 [OF vg_int]) show "((λb. exp (- integral {a..b} (λx. ?Dγ x / (γ x - z))) * (γ b - z)) has_derivative (λh. 0)) (at x within {a..b})" if "x ∈ {a..b} - ({a, b} ∪ k)" for x proof - have x: "x ∉ k" "a < x" "x < b" using that by auto then have "x ∈ interior ({a..b} - k)" using open_subset_interior [OF ∘] by fastforce then have con: "isCont ?Dγ x" using g_C1_diff x by (auto simp: C1_differentiable_on_eq intro: continuous_on_interior) then have con_vd: "continuous (at x within {a..b}) (λx. ?Dγ x)" by (rule continuous_at_imp_continuous_within) have gdx: "γ differentiable at x" using x by (simp add: g_diff_at) then obtain d where d: "(γ has_derivative (λx. x *⇩_{R}d)) (at x)" by (auto simp add: differentiable_iff_scaleR) show "((λc. exp (- integral {a..c} (λx. ?Dγ x / (γ x - z))) * (γ c - z)) has_derivative (λh. 0)) (at x within {a..b})" proof (rule exp_fg [unfolded has_vector_derivative_def, simplified]) show "(γ has_derivative (λc. c *⇩_{R}d)) (at x within {a..b})" using d by (blast intro: has_derivative_at_withinI) have "((λx. integral {a..x} (λx. ?Dγ x / (γ x - z))) has_vector_derivative d / (γ x - z)) (at x within {a..b})" proof (rule has_vector_derivative_eq_rhs [OF integral_has_vector_derivative_continuous_at [where S = "{}", simplified]]) show "continuous (at x within {a..b}) (λx. vector_derivative γ (at x) / (γ x - z))" using continuous_at_imp_continuous_at_within differentiable_imp_continuous_within gdx x by (intro con_vd continuous_intros) (force+) show "vector_derivative γ (at x) / (γ x - z) = d / (γ x - z)" using d vector_derivative_at by (simp add: vector_derivative_at has_vector_derivative_def) qed (use x vg_int in auto) then show "((λx. integral {a..x} (λx. ?Dγ x / (γ x - z))) has_derivative (λc. c *⇩_{R}(d / (γ x - z)))) (at x within {a..b})" by (auto simp: has_vector_derivative_def) qed (use x in auto) qed qed (use fink t in auto) } with ab show ?thesis2 by (simp add: divide_inverse_commute integral_def) qed lemma winding_number_exp_2pi: "⟦path p; z ∉ path_image p⟧ ⟹ pathfinish p - z = exp (2 * pi * 𝗂 * winding_number p z) * (pathstart p - z)" using winding_number [of p z 1] unfolding valid_path_def path_image_def pathstart_def pathfinish_def winding_number_prop_def by (force dest: winding_number_exp_integral(2) [of _ 0 1 z] simp: field_simps contour_integral_integral exp_minus) lemma integer_winding_number_eq: assumes γ: "path γ" and z: "z ∉ path_image γ" shows "winding_number γ z ∈ ℤ ⟷ pathfinish γ = pathstart γ" proof - obtain p where p: "valid_path p" "z ∉ path_image p" "pathstart p = pathstart γ" "pathfinish p = pathfinish γ" and eq: "contour_integral p (λw. 1 / (w - z)) = complex_of_real (2 * pi) * 𝗂 * winding_number γ z" using winding_number [OF assms, of 1] unfolding winding_number_prop_def by auto then have wneq: "winding_number γ z = winding_number p z" using eq winding_number_valid_path by force have iff: "(winding_number γ z ∈ ℤ) ⟷ (exp (contour_integral p (λw. 1 / (w - z))) = 1)" using eq by (simp add: exp_eq_1 complex_is_Int_iff) have "γ 0 ≠ z" by (metis pathstart_def pathstart_in_path_image z) then have "exp (contour_integral p (λw. 1 / (w - z))) = (γ 1 - z) / (γ 0 - z)" using p winding_number_exp_integral(2) [of p 0 1 z] by (simp add: valid_path_def path_defs contour_integral_integral exp_minus field_split_simps) then have "winding_number p z ∈ ℤ ⟷ pathfinish p = pathstart p" using p wneq iff by (auto simp: path_defs) then show ?thesis using p eq by (auto simp: winding_number_valid_path) qed theorem integer_winding_number: "⟦path γ; pathfinish γ = pathstart γ; z ∉ path_image γ⟧ ⟹ winding_number γ z ∈ ℤ" by (metis integer_winding_number_eq) text‹If the winding number's magnitude is at least one, then the path must contain points in every direction.*) We can thus bound the winding number of a path that doesn't intersect a given ray. › lemma winding_number_pos_meets: fixes z::complex assumes γ: "valid_path γ" and z: "z ∉ path_image γ" and 1: "Re (winding_number γ z) ≥ 1" and w: "w ≠ z" shows "∃a::real. 0 < a ∧ z + of_real a * (w - z) ∈ path_image γ" proof - have [simp]: "⋀x. 0 ≤ x ⟹ x ≤ 1 ⟹ γ x ≠ z" using z by (auto simp: path_image_def) have [simp]: "z ∉ γ ` {0..1}" using path_image_def z by auto have gpd: "γ piecewise_C1_differentiable_on {0..1}" using γ valid_path_def by blast define r where "r = (w - z) / (γ 0 - z)" have [simp]: "r ≠ 0" using w z by (auto simp: r_def) have cont: "continuous_on {0..1} (λx. Im (integral {0..x} (λx. vector_derivative γ (at x) / (γ x - z))))" by (intro continuous_intros indefinite_integral_continuous_1 winding_number_exp_integral [OF gpd]; simp) have "Arg2pi r ≤ 2*pi" by (simp add: Arg2pi less_eq_real_def) also have "… ≤ Im (integral {0..1} (λx. vector_derivative γ (at x) / (γ x - z)))" using 1 by (simp add: winding_number_valid_path [OF γ z] contour_integral_integral Complex.Re_divide field_simps power2_eq_square) finally have "Arg2pi r ≤ Im (integral {0..1} (λx. vector_derivative γ (at x) / (γ x - z)))" . then have "∃t. t ∈ {0..1} ∧ Im(integral {0..t} (λx. vector_derivative γ (at x)/(γ x - z))) = Arg2pi r" by (simp add: Arg2pi_ge_0 cont IVT') then obtain t where t: "t ∈ {0..1}" and eqArg: "Im (integral {0..t} (λx. vector_derivative γ (at x)/(γ x - z))) = Arg2pi r" by blast define i where "i = integral {0..t} (λx. vector_derivative γ (at x) / (γ x - z))" have gpdt: "γ piecewise_C1_differentiable_on {0..t}" by (metis atLeastAtMost_iff atLeastatMost_subset_iff order_refl piecewise_C1_differentiable_on_subset gpd t) have "exp (- i) * (γ t - z) = γ 0 - z" unfolding i_def proof (rule winding_number_exp_integral [OF gpdt]) show "z ∉ γ ` {0..t}" using t z unfolding path_image_def by force qed (use t in auto) then have *: "γ t - z = exp i * (γ 0 - z)" by (simp add: exp_minus field_simps) then have "(w - z) = r * (γ 0 - z)" by (simp add: r_def) moreover have "z + exp (Re i) * (exp (𝗂 * Im i) * (γ 0 - z)) = γ t" using * by (simp add: exp_eq_polar field_simps) moreover have "Arg2pi r = Im i" using eqArg by (simp add: i_def) ultimately have "z + complex_of_real (exp (Re i)) * (w - z) / complex_of_real (cmod r) = γ t" using Complex_Transcendental.Arg2pi_eq [of r] ‹r ≠ 0› by (metis mult.left_commute nonzero_mult_div_cancel_left norm_eq_zero of_real_0 of_real_eq_iff times_divide_eq_left) with t show ?thesis by (rule_tac x="exp(Re i) / norm r" in exI) (auto simp: path_image_def) qed lemma winding_number_big_meets: fixes z::complex assumes γ: "valid_path γ" and z: "z ∉ path_image γ" and "¦Re (winding_number γ z)¦ ≥ 1" and w: "w ≠ z" shows "∃a::real. 0 < a ∧ z + of_real a * (w - z) ∈ path_image γ" proof - { assume "Re (winding_number γ z) ≤ - 1" then have "Re (winding_number (reversepath γ) z) ≥ 1" by (simp add: γ valid_path_imp_path winding_number_reversepath z) moreover have "valid_path (reversepath γ)" using γ valid_path_imp_reverse by auto moreover have "z ∉ path_image (reversepath γ)" by (simp add: z) ultimately have "∃a::real. 0 < a ∧ z + of_real a * (w - z) ∈ path_image (reversepath γ)" using winding_number_pos_meets w by blast then have ?thesis by simp } then show ?thesis using assms by (simp add: abs_if winding_number_pos_meets split: if_split_asm) qed lemma winding_number_less_1: fixes z::complex shows "⟦valid_path γ; z ∉ path_image γ; w ≠ z; ⋀a::real. 0 < a ⟹ z + of_real a * (w - z) ∉ path_image γ⟧ ⟹ Re(winding_number γ z) < 1" by (auto simp: not_less dest: winding_number_big_meets) text‹One way of proving that WN=1 for a loop.› lemma winding_number_eq_1: fixes z::complex assumes γ: "valid_path γ" and z: "z ∉ path_image γ" and loop: "pathfinish γ = pathstart γ" and 0: "0 < Re(winding_number γ z)" and 2: "Re(winding_number γ z) < 2" shows "winding_number γ z = 1" proof - have "winding_number γ z ∈ Ints" by (simp add: γ integer_winding_number loop valid_path_imp_path z) then show ?thesis using 0 2 by (auto simp: Ints_def) qed subsection‹Continuity of winding number and invariance on connected sets› theorem continuous_at_winding_number: fixes z::complex assumes γ: "path γ" and z: "z ∉ path_image γ" shows "continuous (at z) (winding_number γ)" proof - obtain e where "e>0" and cbg: "cball z e ⊆ - path_image γ" using open_contains_cball [of "- path_image γ"] z by (force simp: closed_def [symmetric] closed_path_image [OF γ]) then have ppag: "path_image γ ⊆ - cball z (e/2)" by (force simp: cball_def dist_norm) have oc: "open (- cball z (e/2))" by (simp add: closed_def [symmetric]) obtain d where "d>0" and pi_eq: "⋀h1 h2. ⟦valid_path h1; valid_path h2; (∀t∈{0..1}. cmod (h1 t - γ t) < d ∧ cmod (h2 t - γ t) < d); pathstart h2 = pathstart h1; pathfinish h2 = pathfinish h1⟧ ⟹ path_image h1 ⊆ - cball z (e/2) ∧ path_image h2 ⊆ - cball z (e/2) ∧ (∀f. f holomorphic_on - cball z (e/2) ⟶ contour_integral h2 f = contour_integral h1 f)" using contour_integral_nearby_ends [OF oc γ ppag] by metis obtain p where "valid_path p" "z ∉ path_image p" and p: "pathstart p = pathstart γ" "pathfinish p = pathfinish γ" and pg: "⋀t. t∈{0..1} ⟹ cmod (γ t - p t) < min d e/2" and pi: "contour_integral p (λx. 1 / (x - z)) = complex_of_real (2 * pi) * 𝗂 * winding_number γ z" using winding_number [OF γ z, of "min d e/2"] ‹d>0› ‹e>0› by (auto simp: winding_number_prop_def) { fix w assume d2: "cmod (w - z) < d/2" and e2: "cmod (w - z) < e/2" have wnotp: "w ∉ path_image p" proof (clarsimp simp add: path_image_def) show False if w: "w = p x" and "0 ≤ x" "x ≤ 1" for x proof - have "cmod (γ x - p x) < min d e/2" using pg that by auto then have "cmod (z - γ x) < e" by (metis e2 less_divide_eq_numeral1(1) min_less_iff_conj norm_minus_commute norm_triangle_half_l w) then show ?thesis using cbg that by (auto simp add: path_image_def cball_def dist_norm less_eq_real_def) qed qed have wnotg: "w ∉ path_image γ" using cbg e2 ‹e>0› by (force simp: dist_norm norm_minus_commute) { fix k::real assume k: "k>0" then obtain q where q: "valid_path q" "w ∉ path_image q" "pathstart q = pathstart γ ∧ pathfinish q = pathfinish γ" and qg: "⋀t. t ∈ {0..1} ⟹ cmod (γ t - q t) < min k (min d e) / 2" and qi: "contour_integral q (λu. 1 / (u - w)) = complex_of_real (2 * pi) * 𝗂 * winding_number γ w" using winding_number [OF γ wnotg, of "min k (min d e) / 2"] ‹d>0› ‹e>0› k by (force simp: min_divide_distrib_right winding_number_prop_def) moreover have "⋀t. t ∈ {0..1} ⟹ cmod (q t - γ t) < d ∧ cmod (p t - γ t) < d" using pg qg ‹0 < d› by (fastforce simp add: norm_minus_commute) moreover have "(λu. 1 / (u-w)) holomorphic_on - cball z (e/2)" using e2 by (auto simp: dist_norm norm_minus_commute intro!: holomorphic_intros) ultimately have "contour_integral p (λu. 1 / (u - w)) = contour_integral q (λu. 1 / (u - w))" by (metis p ‹valid_path p› pi_eq) then have "contour_integral p (λx. 1 / (x - w)) = complex_of_real (2 * pi) * 𝗂 * winding_number γ w" by (simp add: pi qi) } note pip = this have "path p" by (simp add: ‹valid_path p› valid_path_imp_path) moreover have "⋀e. e > 0 ⟹ winding_number_prop p w e p (winding_number γ w)" by (simp add: ‹valid_path p› pip winding_number_prop_def wnotp) ultimately have "winding_number p w = winding_number γ w" using winding_number_unique wnotp by blast } note wnwn = this obtain pe where "pe>0" and cbp: "cball z (3 / 4 * pe) ⊆ - path_image p" using ‹valid_path p› ‹z ∉ path_image p› open_contains_cball [of "- path_image p"] by (force simp: closed_def [symmetric] closed_path_image [OF valid_path_imp_path]) obtain L where "L>0" and L: "⋀f B. ⟦f holomorphic_on - cball z (3 / 4 * pe); ∀z ∈ - cball z (3 / 4 * pe). cmod (f z) ≤ B⟧ ⟹ cmod (contour_integral p f) ≤ L * B" using contour_integral_bound_exists [of "- cball z (3/4*pe)" p] cbp ‹valid_path p› by blast { fix e::real and w::complex assume e: "0 < e" and w: "cmod (w - z) < pe/4" "cmod (w - z) < e * pe⇧^{2}/ (8 * L)" then have [simp]: "w ∉ path_image p" using cbp p(2) ‹0 < pe› by (force simp: dist_norm norm_minus_commute path_image_def cball_def) have [simp]: "contour_integral p (λx. 1/(x - w)) - contour_integral p (λx. 1/(x - z)) = contour_integral p (λx. 1/(x - w) - 1/(x - z))" by (simp add: ‹valid_path p› ‹z ∉ path_image p› contour_integrable_inversediff contour_integral_diff) { fix x assume pe: "3/4 * pe < cmod (z - x)" have "cmod (w - x) < pe/4 + cmod (z - x)" by (meson add_less_cancel_right norm_diff_triangle_le order_refl order_trans_rules(21) w(1)) then have wx: "cmod (w - x) < 4/3 * cmod (z - x)" using pe by simp have "cmod (z - x) ≤ cmod (z - w) + cmod (w - x)" using norm_diff_triangle_le by blast also have "… < pe/4 + cmod (w - x)" using w by (simp add: norm_minus_commute) finally have "pe/2 < cmod (w - x)" using pe by auto then have pe_less: "(pe/2)^2 < cmod (w - x) ^ 2" by (simp add: ‹0 < pe› less_eq_real_def power_strict_mono) then have pe2: "pe^2 < 4 * cmod (w - x) ^ 2" by (simp add: power_divide) have "8 * L * cmod (w - z) < e * pe⇧^{2}" using w ‹L>0› by (simp add: field_simps) also have "… < e * 4 * cmod (w - x) * cmod (w - x)" using pe2 ‹e>0› by (simp add: power2_eq_square) also have "… < e * 4 * cmod (w - x) * (4/3 * cmod (z - x))" using ‹0 < pe› pe_less e less_eq_real_def wx by fastforce finally have "L * cmod (w - z) < 2/3 * e * cmod (w - x) * cmod (z - x)" by simp also have "… ≤ e * cmod (w - x) * cmod (z - x)" using e by simp finally have Lwz: "L * cmod (w - z) < e * cmod (w - x) * cmod (z - x)" . have "L * cmod (1 / (x - w) - 1 / (x - z)) ≤ e" proof (cases "x=z ∨ x=w") case True with pe ‹pe>0› w ‹L>0› show ?thesis by (force simp: norm_minus_commute) next case False with wx w(2) ‹L>0› pe pe2 Lwz show ?thesis by (auto simp: divide_simps mult_less_0_iff norm_minus_commute norm_divide norm_mult power2_eq_square) qed } note L_cmod_le = this let ?f = "(λx. 1 / (x - w) - 1 / (x - z))" have "cmod (contour_integral p ?f) ≤ L * (e * pe⇧^{2}/ L / 4 * (inverse (pe / 2))⇧^{2})" proof (rule L) show "?f holomorphic_on - cball z (3 / 4 * pe)" using ‹pe>0› w by (force simp: dist_norm norm_minus_commute intro!: holomorphic_intros) show " ∀u ∈- cball z (3 / 4 * pe). cmod (?f u) ≤ e * pe⇧^{2}/ L / 4 * (inverse (pe / 2))⇧^{2}" using ‹pe>0› w ‹L>0› by (auto simp: cball_def dist_norm field_simps L_cmod_le simp del: less_divide_eq_numeral1 le_divide_eq_numeral1) qed also have "… < 2*e" using ‹L>0› e by (force simp: field_simps) finally have "cmod (winding_number p w - winding_number p z) < e" using pi_ge_two e by (force simp: winding_number_valid_path ‹valid_path p› ‹z ∉ path_image p› field_simps norm_divide norm_mult intro: less_le_trans) } note cmod_wn_diff = this have "isCont (winding_number p) z" proof (clarsimp simp add: continuous_at_eps_delta) fix e::real assume "e>0" show "∃d>0. ∀x'. dist x' z < d ⟶ dist (winding_number p x') (winding_number p z) < e" using ‹pe>0› ‹L>0› ‹e>0› by (rule_tac x="min (pe/4) (e/2*pe^2/L/4)" in exI) (simp add: dist_norm cmod_wn_diff) qed then show ?thesis apply (rule continuous_transform_within [where d = "min d e/2"]) apply (auto simp: ‹d>0› ‹e>0› dist_norm wnwn) done qed corollary continuous_on_winding_number: "path γ ⟹ continuous_on (- path_image γ) (λw. winding_number γ w)" by (simp add: continuous_at_imp_continuous_on continuous_at_winding_number) subsection✐‹tag unimportant› ‹The winding number is constant on a connected region› lemma winding_number_constant: assumes γ: "path γ" and loop: "pathfinish γ = pathstart γ" and cs: "connected S" and sg: "S ∩ path_image γ = {}" shows "winding_number γ constant_on S" proof - have *: "1 ≤ cmod (winding_number γ y - winding_number γ z)" if ne: "winding_number γ y ≠ winding_number γ z" and "y ∈ S" "z ∈ S" for y z proof - have "winding_number γ y ∈ ℤ" "winding_number γ z ∈ ℤ" using that integer_winding_number [OF γ loop] sg ‹y ∈ S› by auto with ne show ?thesis by (auto simp: Ints_def simp flip: of_int_diff) qed have cont: "continuous_on S (λw. winding_number γ w)" using continuous_on_winding_number [OF γ] sg by (meson continuous_on_subset disjoint_eq_subset_Compl) show ?thesis using "*" zero_less_one by (blast intro: continuous_discrete_range_constant [OF cs cont]) qed lemma winding_number_eq: "⟦path γ; pathfinish γ = pathstart γ; w ∈ S; z ∈ S; connected S; S ∩ path_image γ = {}⟧ ⟹ winding_number γ w = winding_number γ z" using winding_number_constant by (metis constant_on_def) lemma open_winding_number_levelsets: assumes γ: "path γ" and loop: "pathfinish γ = pathstart γ" shows "open {z. z ∉ path_image γ ∧ winding_number γ z = k}" proof (clarsimp simp: open_dist) fix z assume z: "z ∉ path_image γ" and k: "k = winding_number γ z" have "open (- path_image γ)" by (simp add: closed_path_image γ open_Compl) then obtain e where "e>0" "ball z e ⊆ - path_image γ" using open_contains_ball [of "- path_image γ"] z by blast then show "∃e>0. ∀y. dist y z < e ⟶ y ∉ path_image γ ∧ winding_number γ y = winding_number γ z" using ‹e>0› by (force simp: norm_minus_commute dist_norm intro: winding_number_eq [OF assms, where S = "ball z e"]) qed subsection‹Winding number is zero "outside" a curve› proposition winding_number_zero_in_outside: assumes γ: "path γ" and loop: "pathfinish γ = pathstart γ" and z: "z ∈ outside (path_image γ)" shows "winding_number γ z = 0" proof - obtain B::real where "0 < B" and B: "path_image γ ⊆ ball 0 B" using bounded_subset_ballD [OF bounded_path_image [OF γ]] by auto obtain w::complex where w: "w ∉ ball 0 (B + 1)" by (metis abs_of_nonneg le_less less_irrefl mem_ball_0 norm_of_real) have "- ball 0 (B + 1) ⊆ outside (path_image γ)" using B subset_ball by (intro outside_subset_convex) auto then have wout: "w ∈ outside (path_image γ)" using w by blast moreover have "winding_number γ constant_on outside (path_image γ)" using winding_number_constant [OF γ loop, of "outside(path_image γ)"] connected_outside by (metis DIM_complex bounded_path_image dual_order.refl γ outside_no_overlap) ultimately have "winding_number γ z = winding_number γ w" by (metis (no_types, opaque_lifting) constant_on_def z) also have "… = 0" proof - have wnot: "w ∉ path_image γ" using wout by (simp add: outside_def) { fix e::real assume "0<e" obtain p where p: "polynomial_function p" "pathstart p = pathstart γ" "pathfinish p = pathfinish γ" and pg1: "(⋀t. ⟦0 ≤ t; t ≤ 1⟧ ⟹ cmod (p t - γ t) < 1)" and pge: "(⋀t. ⟦0 ≤ t; t ≤ 1⟧ ⟹ cmod (p t - γ t) < e)" using path_approx_polynomial_function [OF γ, of "min 1 e"] ‹e>0› by (metis atLeastAtMost_iff min_less_iff_conj zero_less_one) have "∃p. valid_path p ∧ w ∉ path_image p ∧ pathstart p = pathstart γ ∧ pathfinish p = pathfinish γ ∧ (∀t∈{0..1}. cmod (γ t - p t) < e) ∧ contour_integral p (λwa. 1 / (wa - w)) = 0" proof (intro exI conjI) have "⋀x. ⟦0 ≤ x; x ≤ 1⟧ ⟹ cmod (p x) < B + 1" using B unfolding image_subset_iff path_image_def by (meson add_strict_mono atLeastAtMost_iff le_less_trans mem_ball_0 norm_triangle_sub pg1) then have pip: "path_image p ⊆ ball 0 (B + 1)" by (auto simp add: path_image_def dist_norm ball_def) then show "w ∉ path_image p" using w by blast show vap: "valid_path p" by (simp add: p(1) valid_path_polynomial_function) show "∀t∈{0..1}. cmod (γ t - p t) < e" by (metis atLeastAtMost_iff norm_minus_commute pge) show "contour_integral p (λwa. 1 / (wa - w)) = 0" proof (rule contour_integral_unique [OF Cauchy_theorem_convex_simple [OF _ convex_ball [of 0 "B+1"]]]) have "⋀z. cmod z < B + 1 ⟹ z ≠ w" using mem_ball_0 w by blast then show "(λz. 1 / (z - w)) holomorphic_on ball 0 (B + 1)" by (intro holomorphic_intros; simp add: dist_norm) qed (use p vap pip loop in auto) qed (use p in auto) } then show ?thesis by (auto intro: winding_number_unique [OF γ] simp add: winding_number_prop_def wnot) qed finally show ?thesis . qed corollary✐‹tag unimportant› winding_number_zero_const: "a ≠ z ⟹ winding_number (λt. a) z = 0" by (rule winding_number_zero_in_outside) (auto simp: pathfinish_def pathstart_def path_polynomial_function) corollary✐‹tag unimportant› winding_number_zero_outside: "⟦path γ; convex s; pathfinish γ = pathstart γ; z ∉ s; path_image γ ⊆ s⟧ ⟹ winding_number γ z = 0" by (meson convex_in_outside outside_mono subsetCE winding_number_zero_in_outside) lemma winding_number_zero_at_infinity: assumes γ: "path γ" and loop: "pathfinish γ = pathstart γ" shows "∃B. ∀z. B ≤ norm z ⟶ winding_number γ z = 0" proof - obtain B::real where "0 < B" and B: "path_image γ ⊆ ball 0 B" using bounded_subset_ballD [OF bounded_path_image [OF γ]] by auto have "winding_number γ z = 0" if "B + 1 ≤ cmod z" for z proof (rule winding_number_zero_outside [OF γ convex_cball loop]) show "z ∉ cball 0 B" using that by auto show "path_image γ ⊆ cball 0 B" using B order.trans by blast qed then show ?thesis by metis qed lemma bounded_winding_number_nz: assumes "path g" "pathfinish g = pathstart g" shows "bounded {z. winding_number g z ≠ 0}" proof - obtain B where "⋀x. norm x ≥ B ⟹ winding_number g x = 0" using winding_number_zero_at_infinity[OF assms] by auto thus ?thesis unfolding bounded_iff by (intro exI[of _ "B + 1"]) force qed lemma winding_number_zero_point: "⟦path γ; convex S; pathfinish γ = pathstart γ; open S; path_image γ ⊆ S⟧ ⟹ ∃z. z ∈ S ∧ winding_number γ z = 0" using outside_compact_in_open [of "path_image γ" S] path_image_nonempty winding_number_zero_in_outside by (fastforce simp add: compact_path_image) text‹If a path winds round a set, it winds rounds its inside.› lemma winding_number_around_inside: assumes γ: "path γ" and loop: "pathfinish γ = pathstart γ" and cls: "closed S" and cos: "connected S" and S_disj: "S ∩ path_image γ = {}" and z: "z ∈ S" and wn_nz: "winding_number γ z ≠ 0" and w: "w ∈ S ∪ inside S" shows "winding_number γ w = winding_number γ z" proof - have ssb: "S ⊆ inside(path_image γ)" proof fix x :: complex assume "x ∈ S" hence "x ∉ path_image γ" by (meson disjoint_iff_not_equal S_disj) thus "x ∈ inside (path_image γ)" by (metis Compl_iff S_disj UnE γ ‹x ∈ S› cos inside_outside loop winding_number_eq winding_number_zero_in_outside wn_nz z) qed show ?thesis proof (rule winding_number_eq [OF γ loop w]) show "z ∈ S ∪ inside S" using z by blast show "connected (S ∪ inside S)" by (simp add: cls connected_with_inside cos) show "(S ∪ inside S) ∩ path_image γ = {}" unfolding disjoint_iff Un_iff by (metis ComplD UnI1 γ cls compact_path_image connected_path_image inside_Un_outside inside_inside_compact_connected ssb subsetD) qed qed text‹Bounding a WN by 1/2 for a path and point in opposite halfspaces.› lemma winding_number_subpath_continuous: assumes γ: "valid_path γ" and z: "z ∉ path_image γ" shows "continuous_on {0..1} (λx. winding_number(subpath 0 x γ) z)" proof (rule continuous_on_eq) let ?f = "λx. integral {0..x} (λt. vector_derivative γ (at t) / (γ t - z))" show "continuous_on {0..1} (λx. 1 / (2 * pi * 𝗂) * ?f x)" proof (intro indefinite_integral_continuous_1 winding_number_exp_integral continuous_intros) show "γ piecewise_C1_differentiable_on {0..1}" using γ valid_path_def by blast qed (use path_image_def z in auto) show "1 / (2 * pi * 𝗂) * ?f x = winding_number (subpath 0 x γ) z" if x: "x ∈ {0..1}" for x proof - have "1 / (2*pi*𝗂) * ?f x = 1 / (2*pi*𝗂) * contour_integral (subpath 0 x γ) (λw. 1/(w - z))" using assms x by (simp add: contour_integral_subcontour_integral [OF contour_integrable_inversediff]) also have "… = winding_number (subpath 0 x γ) z" proof (subst winding_number_valid_path) show "z ∉ path_image (subpath 0 x γ)" using assms x atLeastAtMost_iff path_image_subpath_subset by force qed (use assms x valid_path_subpath in ‹force+›) finally show ?thesis . qed qed lemma winding_number_ivt_pos: assumes γ: "valid_path γ" and z: "z ∉ path_image γ" and "0 ≤ w" "w ≤ Re(winding_number γ z)" shows "∃t ∈ {0..1}. Re(winding_number(subpath 0 t γ) z) = w" proof - have "continuous_on {0..1} (λx. winding_number (subpath 0 x γ) z)" using γ winding_number_subpath_continuous z by blast moreover have "Re (winding_number (subpath 0 0 γ) z) ≤ w" "w ≤ Re (winding_number (subpath 0 1 γ) z)" using assms by (auto simp: path_image_def image_def) ultimately show ?thesis using ivt_increasing_component_on_1[of 0 1, where ?k = "1"] by force qed lemma winding_number_ivt_neg: assumes γ: "valid_path γ" <