(* Author: Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com> *) section ‹Evaluate winding numbers by calculating Cauchy indices› theory Winding_Number_Eval imports Cauchy_Index_Theorem "HOL-Eisbach.Eisbach_Tools" begin subsection ‹Misc› lemma not_on_closed_segmentI: fixes z::"'a::euclidean_space" assumes "norm (z - a) *⇩_{R}(b - z) ≠ norm (b - z) *⇩_{R}(z - a)" shows "z ∉ closed_segment a b" using assms by (auto simp add:between_mem_segment[symmetric] between_norm) lemma not_on_closed_segmentI_complex: fixes z::"complex" assumes "(Re b - Re z) * (Im z - Im a) ≠ (Im b - Im z) * (Re z - Re a)" shows "z ∉ closed_segment a b" proof (cases "z≠a ∧ z≠b") case True then have "cmod (z - a)≠0" "cmod (b - z)≠0" by auto then have "(Re b - Re z) * (Im z - Im a) = (Im b - Im z) * (Re z - Re a)" when "cmod (z - a) * (Re b - Re z) = cmod (b - z) * (Re z - Re a)" "cmod (z - a) * (Im b - Im z) = cmod (b - z) * (Im z - Im a)" using that by algebra then show ?thesis using assms apply (intro not_on_closed_segmentI) by (auto simp add:scaleR_complex.ctr simp del:Complex_eq) next case False then have "(Re b - Re z) * (Im z - Im a) = (Im b - Im z) * (Re z - Re a)" by auto then have False using assms by auto then show ?thesis by auto qed subsection ‹finite intersection with the two axes› definition finite_axes_cross::"(real ⇒ complex) ⇒ complex ⇒ bool" where "finite_axes_cross g z = finite {t. (Re (g t-z) = 0 ∨ Im (g t-z) = 0) ∧ 0 ≤ t ∧ t ≤ 1}" lemma finite_cross_intros: "⟦Re a≠Re z ∨ Re b ≠Re z; Im a≠Im z ∨ Im b≠Im z⟧⟹finite_axes_cross (linepath a b) z" "⟦st ≠ tt; r ≠ 0⟧ ⟹ finite_axes_cross (part_circlepath z0 r st tt) z" "⟦finite_axes_cross g1 z;finite_axes_cross g2 z⟧ ⟹ finite_axes_cross (g1+++g2) z" proof - assume asm:"Re a≠Re z ∨ Re b ≠Re z" "Im a≠Im z ∨ Im b≠Im z" let ?S1="{t. Re (linepath a b t-z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" and ?S2="{t. Im (linepath a b t-z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" have "finite ?S1" using linepath_half_finite_inter[of a "Complex 1 0" "Re z" b] asm(1) by (auto simp add:inner_complex_def) moreover have "finite ?S2" using linepath_half_finite_inter[of a "Complex 0 1" "Im z" b] asm(2) by (auto simp add:inner_complex_def) moreover have "{t. (Re (linepath a b t-z) = 0 ∨ Im (linepath a b t-z) = 0) ∧ 0 ≤ t ∧ t ≤ 1} = ?S1 ∪ ?S2" by fast ultimately show "finite_axes_cross (linepath a b) z" unfolding finite_axes_cross_def by force next assume asm: "st ≠tt" "r≠0" let ?S1="{t. Re (part_circlepath z0 r st tt t-z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" and ?S2="{t. Im (part_circlepath z0 r st tt t-z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" have "finite ?S1" using part_circlepath_half_finite_inter[of st tt r "Complex 1 0" z0 "Re z"] asm by (auto simp add:inner_complex_def Complex_eq_0) moreover have "finite ?S2" using part_circlepath_half_finite_inter[of st tt r "Complex 0 1" z0 "Im z"] asm by (auto simp add:inner_complex_def Complex_eq_0) moreover have "{t. (Re (part_circlepath z0 r st tt t-z) = 0 ∨ Im (part_circlepath z0 r st tt t-z) = 0) ∧ 0 ≤ t ∧ t ≤ 1} = ?S1 ∪ ?S2" by fast ultimately show "finite_axes_cross (part_circlepath z0 r st tt) z" unfolding finite_axes_cross_def by auto next assume asm:"finite_axes_cross g1 z" "finite_axes_cross g2 z" let ?g1R="{t. Re (g1 t-z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" and ?g1I="{t. Im (g1 t-z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" and ?g2R="{t. Re (g2 t-z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" and ?g2I="{t. Im (g2 t-z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" have "finite ?g1R" "finite ?g1I" proof - have "{t. (Re (g1 t - z) = 0 ∨ Im (g1 t - z) = 0) ∧ 0 ≤ t ∧ t ≤ 1} = ?g1R ∪ ?g1I" by force then have "finite (?g1R ∪ ?g1I)" using asm(1) unfolding finite_axes_cross_def by auto then show "finite ?g1R" "finite ?g1I" by blast+ qed have "finite ?g2R" "finite ?g2I" proof - have "{t. (Re (g2 t - z) = 0 ∨ Im (g2 t - z) = 0) ∧ 0 ≤ t ∧ t ≤ 1} = ?g2R ∪ ?g2I" by force then have "finite (?g2R ∪ ?g2I)" using asm(2) unfolding finite_axes_cross_def by auto then show "finite ?g2R" "finite ?g2I" by blast+ qed let ?S1 = "{t. Re ((g1 +++ g2) t - z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" and ?S2 = "{t. Im ((g1 +++ g2) t - z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" have "finite ?S1" using finite_half_joinpaths_inter[of g1 "Complex 1 0" "Re z" g2,simplified] ‹finite ?g1R› ‹finite ?g2R› by (auto simp add:inner_complex_def) moreover have "finite ?S2" using finite_half_joinpaths_inter[of g1 "Complex 0 1" "Im z" g2,simplified] ‹finite ?g1I› ‹finite ?g2I› by (auto simp add:inner_complex_def) moreover have "{t. (Re ((g1 +++ g2) t - z) = 0 ∨ Im ((g1 +++ g2) t - z) = 0) ∧ 0 ≤ t ∧ t ≤ 1} = ?S1 ∪ ?S2" by force ultimately show "finite_axes_cross (g1 +++ g2) z" unfolding finite_axes_cross_def by auto qed lemma cindex_path_joinpaths: assumes "finite_axes_cross g1 z" "finite_axes_cross g2 z" and "path g1" "path g2" "pathfinish g1 = pathstart g2" "pathfinish g1≠z" shows "cindex_path (g1+++g2) z = cindex_path g1 z + jumpF_pathstart g2 z - jumpF_pathfinish g1 z + cindex_path g2 z" proof - define h12 where "h12 = (λt. Im ((g1+++g2) t - z) / Re ((g1+++g2) t - z))" let ?h = "λg. λt. Im (g t - z) / Re (g t - z)" have "cindex_path (g1+++g2) z = cindex 0 1 h12" unfolding cindex_path_def h12_def by simp also have "... = cindex 0 (1/2) h12 + jump h12 (1/2) + cindex (1/2) 1 h12" proof (rule cindex_combine) have "finite_axes_cross (g1+++g2) z" using assms by (auto intro:finite_cross_intros) then have "finite {t. Re ((g1+++g2) t - z) = 0 ∧ 0≤t ∧ t≤1}" unfolding finite_axes_cross_def by (auto elim:rev_finite_subset) moreover have " jump h12 t = 0" when "Re ((g1 +++ g2) t - z) ≠ 0" "0 < t" "t < 1" for t apply (rule jump_Im_divide_Re_0[of "λt. (g1+++g2) t- z",folded h12_def,OF _ that]) using assms by (auto intro:path_offset) ultimately show "finite {x. jump h12 x ≠ 0 ∧ 0 < x ∧ x < 1}" apply (elim rev_finite_subset) by auto qed auto also have "... = cindex_path g1 z + jumpF_pathstart g2 z - jumpF_pathfinish g1 z + cindex_path g2 z" proof - have "jump h12 (1/2) = jumpF_pathstart g2 z - jumpF_pathfinish g1 z " proof - have "jump h12 (1 / 2) = jumpF h12 (at_right (1 / 2)) - jumpF h12 (at_left (1 / 2))" proof (cases "Re ((g1+++g2) (1/2) - z) = 0") case False have "jump h12 (1 / 2) = 0" unfolding h12_def apply (rule jump_Im_divide_Re_0) using assms False by (auto intro:path_offset) moreover have "jumpF h12 (at_right (1/2)) = 0" unfolding h12_def apply (intro jumpF_im_divide_Re_0) subgoal using assms by (auto intro:path_offset) subgoal using assms(5-6) False unfolding joinpaths_def pathfinish_def pathstart_def by auto by auto moreover have "jumpF h12 (at_left (1/2)) = 0" unfolding h12_def apply (intro jumpF_im_divide_Re_0) subgoal using assms by (auto intro:path_offset) subgoal using assms(5-6) False unfolding joinpaths_def pathfinish_def pathstart_def by auto by auto ultimately show ?thesis by auto next case True then have "Im ((g1 +++ g2) (1 / 2) - z) ≠ 0" using assms(5,6) by (metis (no_types, hide_lams) Re_divide_numeral complex_Re_numeral complex_eq divide_self_if joinpaths_def minus_complex.simps mult.commute mult.left_neutral numeral_One pathfinish_def pathstart_def right_minus_eq times_divide_eq_left zero_neq_numeral) show ?thesis proof (rule jump_jumpF[of _ h12 "sgnx h12 (at_left (1/2))" "sgnx h12 (at_right (1/2))"]) define g where "g=(λt. (g1 +++ g2) t - z)" have h12_def:"h12 = (λt. Im(g t)/Re(g t))" unfolding h12_def g_def by simp have "path g" using assms unfolding g_def by (auto intro!:path_offset) then have "isCont (λt. Im (g t)) (1 / 2)" "isCont (λt. Re (g t)) (1 / 2)" unfolding path_def by (auto intro!:continuous_intros continuous_on_interior) moreover have "Im (g (1/2)) ≠0" using ‹Im ((g1 +++ g2) (1 / 2) - z) ≠ 0› unfolding g_def . ultimately show "isCont (inverse ∘ h12) (1 / 2)" unfolding h12_def comp_def by (auto intro!: continuous_intros) define l where "l ≡ sgnx h12 (at_left (1/2))" define r where "r ≡ sgnx h12 (at_right (1/2))" have *:"continuous_on ({0<..<1}- {t. h12 t = 0 ∧ 0 < t ∧ t < 1}) h12" using ‹path g›[unfolded path_def] unfolding h12_def apply (auto intro!: continuous_intros) by (auto elim:continuous_on_subset) have **:"finite {t. h12 t = 0 ∧ 0 < t ∧ t < 1}" proof - have "finite_axes_cross (g1 +++ g2) z" using assms(1,2) finite_cross_intros(3)[of g1 z g2] by auto then have "finite {t. (Re (g t) = 0 ∨ Im (g t) = 0) ∧ 0 < t ∧ t < 1}" unfolding finite_axes_cross_def g_def apply (elim rev_finite_subset) by auto then show ?thesis unfolding h12_def by (simp add:disj_commute) qed have "h12 sgnx_able at_left (1/2)" "l ≠ 0" "h12 sgnx_able at_right (1/2)" "r ≠ 0" unfolding l_def r_def using finite_sgnx_at_left_at_right[OF ** * **] by auto then show "(h12 has_sgnx l) (at_left (1/2))" "(h12 has_sgnx r) (at_right (1/2))" "l≠0" "r≠0" unfolding l_def r_def by (auto elim:sgnx_able_sgnx) qed qed moreover have "jumpF h12 (at_right (1/2)) = jumpF_pathstart g2 z" proof - have " jumpF h12 (at_right (1 / 2)) = jumpF (h12 ∘ (λx. x / 2 + 1 / 2)) (at_right 0)" using jumpF_linear_comp[of "1/2" h12 "1/2" 0,simplified] by simp also have "jumpF (h12 ∘ (λx. x / 2 + 1 / 2)) (at_right 0) = jumpF_pathstart g2 z" unfolding h12_def jumpF_pathstart_def proof (rule jumpF_cong) show "∀⇩_{F}x in at_right 0. ((λt. Im ((g1 +++ g2) t - z) / Re ((g1 +++ g2) t - z)) ∘ (λx. x / 2 + 1 / 2)) x = Im (g2 x - z) / Re (g2 x - z)" unfolding eventually_at_right apply (intro exI[where x="1/2"]) unfolding joinpaths_def by auto qed simp finally show ?thesis . qed moreover have "jumpF h12 (at_left (1 / 2)) = jumpF_pathfinish g1 z" proof - have "jumpF h12 (at_left (1 / 2)) = jumpF (h12 ∘ (λx. x / 2)) (at_left 1)" using jumpF_linear_comp[of "1/2" h12 0 1,simplified] by simp also have "jumpF (h12 ∘ (λx. x / 2 )) (at_left 1) = jumpF_pathfinish g1 z" unfolding h12_def jumpF_pathfinish_def proof (rule jumpF_cong) show " ∀⇩_{F}x in at_left 1. ((λt. Im ((g1 +++ g2) t - z) / Re ((g1 +++ g2) t - z)) ∘ (λx. x / 2)) x = Im (g1 x - z) / Re (g1 x - z)" unfolding eventually_at_left apply (intro exI[where x="1/2"]) unfolding joinpaths_def by auto qed simp finally show ?thesis . qed ultimately show ?thesis by auto qed moreover have "cindex 0 (1 / 2) h12 = cindex_path g1 z" proof - have "cindex 0 (1 / 2) h12 = cindex 0 1 (h12 ∘ (λx. x / 2))" using cindex_linear_comp[of "1/2" 0 1 h12 0,simplified,symmetric] . also have "... = cindex_path g1 z" proof - let ?g = " (λt. Im (g1 t - z) / Re (g1 t - z))" have *:"jump (h12 ∘ (λx. x / 2)) x = jump ?g x" when "0<x" "x<1" for x unfolding h12_def proof (rule jump_cong) show "∀⇩_{F}x in at x. ((λt. Im ((g1 +++ g2) t - z) / Re ((g1 +++ g2) t - z)) ∘ (λx. x / 2)) x = Im (g1 x - z) / Re (g1 x - z)" unfolding eventually_at joinpaths_def comp_def using that apply (intro exI[where x="(1-x)/2"]) by (auto simp add: dist_norm) qed simp then have "{x. jump (h12 ∘ (λx. x / 2)) x ≠ 0 ∧ 0 < x ∧ x < 1} = {x. jump ?g x ≠ 0 ∧ 0 < x ∧ x < 1}" by auto then show ?thesis unfolding cindex_def cindex_path_def apply (elim sum.cong) by (auto simp add:*) qed finally show ?thesis . qed moreover have "cindex (1 / 2) 1 h12 = cindex_path g2 z" proof - have "cindex (1 / 2) 1 h12 = cindex 0 1 (h12 ∘ (λx. x / 2 + 1 / 2))" using cindex_linear_comp[of "1/2" 0 1 h12 "1/2",simplified,symmetric] . also have "... = cindex_path g2 z" proof - let ?g = " (λt. Im (g2 t - z) / Re (g2 t - z))" have *:"jump (h12 ∘ (λx. x / 2+1/2)) x = jump ?g x" when "0<x" "x<1" for x unfolding h12_def proof (rule jump_cong) show "∀⇩_{F}x in at x. ((λt. Im ((g1 +++ g2) t - z) / Re ((g1 +++ g2) t - z)) ∘ (λx. x / 2+1/2)) x = Im (g2 x - z) / Re (g2 x - z)" unfolding eventually_at joinpaths_def comp_def using that apply (intro exI[where x="x/2"]) by (auto simp add: dist_norm) qed simp then have "{x. jump (h12 ∘ (λx. x / 2+1/2)) x ≠ 0 ∧ 0 < x ∧ x < 1} = {x. jump ?g x ≠ 0 ∧ 0 < x ∧ x < 1}" by auto then show ?thesis unfolding cindex_def cindex_path_def apply (elim sum.cong) by (auto simp add:*) qed finally show ?thesis . qed ultimately show ?thesis by simp qed finally show ?thesis . qed subsection ‹More lemmas related @{term cindex_pathE} / @{term jumpF_pathstart} / @{term jumpF_pathfinish}› lemma cindex_pathE_linepath: assumes "z∉closed_segment a b" shows "cindex_pathE (linepath a b) z = ( let c1 = Re a - Re z; c2 = Re b - Re z; c3 = Im a * Re b + Re z * Im b + Im z * Re a - Im z * Re b - Im b * Re a - Re z * Im a; d1 = Im a - Im z; d2 = Im b - Im z in if (c1>0 ∧ c2<0) ∨ (c1<0 ∧ c2>0) then (if c3>0 then 1 else -1) else (if (c1=0 ⟷ c2≠0) ∧ (c1=0 ⟶d1≠0) ∧ (c2=0 ⟶ d2≠0) then if (c1=0 ∧ (c2 >0 ⟷ d1>0)) ∨ (c2=0 ∧ (c1 >0 ⟷ d2<0)) then 1/2 else -1/2 else 0))" proof - define c1 c2 where "c1=Re a - Re z" and "c2=Re b - Re z" define d1 d2 where "d1=Im a - Im z" and "d2=Im b - Im z" let ?g = "linepath a b" have ?thesis when "¬ ((c1>0 ∧ c2<0) ∨ (c1<0 ∧ c2>0))" proof - have "Re a= Re z ∧ Re b=Re z" when "0<t" "t<1" and asm:"(1-t)*Re a + t * Re b = Re z" for t unfolding c1_def c2_def using that proof - have ?thesis when "c1≤0" "c1≥0" proof - have "Re a=Re z" using that unfolding c1_def by auto then show ?thesis using ‹0<t› ‹t<1› asm apply (cases "Re b" "Re z" rule:linorder_cases) apply (auto simp add:field_simps) done qed moreover have ?thesis when "c1≤0" "c2≤0" proof - have False when "c1<0" proof - have "(1 - t) * Re a < (1 - t) * Re z" using ‹t<1› ‹c1<0› unfolding c1_def by auto moreover have "t * Re b ≤ t* Re z" using ‹t>0› ‹c2≤0› unfolding c2_def by auto ultimately have "(1 - t) * Re a + t * Re b < (1 - t) * Re z + t * Re z" by auto thus False using asm by (auto simp add:algebra_simps) qed moreover have False when "c2<0" proof - have "(1 - t) * Re a ≤ (1 - t) * Re z" using ‹t<1› ‹c1≤0› unfolding c1_def by auto moreover have "t * Re b < t* Re z" using ‹t>0› ‹c2<0› unfolding c2_def by auto ultimately have "(1 - t) * Re a + t * Re b < (1 - t) * Re z + t * Re z" by auto thus False using asm by (auto simp add:algebra_simps) qed ultimately show ?thesis using that unfolding c1_def c2_def by argo qed moreover have ?thesis when "c2≤0" "c2≥0" proof - have "Re b=Re z" using that unfolding c2_def by auto then have "(1 - t) * Re a = (1-t)*Re z" using asm by (auto simp add:field_simps) then have "Re a= Re z" using ‹t<1› by auto then show ?thesis using ‹Re b=Re z› by auto qed moreover have ?thesis when "c1≥0" "c2≥0" proof - have False when "c1>0" proof - have "(1 - t) * Re a > (1 - t) * Re z" using ‹t<1› ‹c1>0› unfolding c1_def by auto moreover have "t * Re b ≥ t* Re z" using ‹t>0› ‹c2≥0› unfolding c2_def by auto ultimately have "(1 - t) * Re a + t * Re b > (1 - t) * Re z + t * Re z" by auto thus False using asm by (auto simp add:algebra_simps) qed moreover have False when "c2>0" proof - have "(1 - t) * Re a ≥ (1 - t) * Re z" using ‹t<1› ‹c1≥0› unfolding c1_def by auto moreover have "t * Re b > t* Re z" using ‹t>0› ‹c2>0› unfolding c2_def by auto ultimately have "(1 - t) * Re a + t * Re b > (1 - t) * Re z + t * Re z" by auto thus False using asm by (auto simp add:algebra_simps) qed ultimately show ?thesis using that unfolding c1_def c2_def by argo qed moreover have "c1≤0 ∨ c2≥0" "c1≥0 ∨ c2≤0" using ‹¬ ((c1>0 ∧ c2<0) ∨ (c1<0 ∧ c2>0))› by auto ultimately show ?thesis by fast qed then have "(∀t. 0<t ∧ t<1 ⟶ Re(linepath a b t - z) ≠ 0) ∨ (c1=0 ∧ c2=0)" using that unfolding linepath_def c1_def c2_def by auto moreover have ?thesis when asm:"∀t. 0<t ∧ t<1 ⟶ Re(linepath a b t - z) ≠ 0" and "¬ (c1=0 ∧ c2=0)" proof - have cindex_ends:"cindex_pathE ?g z = jumpF_pathstart ?g z - jumpF_pathfinish ?g z" proof - define f where "f=(λt. Im (linepath a b t - z) / Re (linepath a b t - z))" define left where "left = {x. jumpF f (at_left x) ≠ 0 ∧ 0 < x ∧ x ≤ 1}" define right where "right = {x. jumpF f (at_right x) ≠ 0 ∧ 0 ≤ x ∧ x < 1}" have jumpF_nz:"jumpF f (at_left x) = 0" "jumpF f (at_right x) = 0" when "0<x" "x<1" for x proof - have "isCont f x" unfolding f_def using asm[rule_format,of x] that by (auto intro!:continuous_intros isCont_Im isCont_Re) then have "continuous (at_left x) f" "continuous (at_right x) f" using continuous_at_split by blast+ then show "jumpF f (at_left x) = 0" "jumpF f (at_right x) = 0" using jumpF_not_infinity by auto qed have "cindex_pathE ?g z = sum (λx. jumpF f (at_right x)) right - sum (λx. jumpF f (at_left x)) left" unfolding cindex_pathE_def cindexE_def right_def left_def by (fold f_def,simp) moreover have "sum (λx. jumpF f (at_right x)) right = jumpF_pathstart ?g z" proof (cases " jumpF f (at_right 0) = 0") case True hence False if "x ∈ right" for x using that by (cases "x = 0") (auto simp: jumpF_nz right_def) then have "right = {}" by blast then show ?thesis unfolding jumpF_pathstart_def using True apply (fold f_def) by auto next case False hence "x ∈ right ⟷ x = 0" for x using that by (cases "x = 0") (auto simp: jumpF_nz right_def) then have "right = {0}" by blast then show ?thesis unfolding jumpF_pathstart_def using False apply (fold f_def) by auto qed moreover have "sum (λx. jumpF f (at_left x)) left = jumpF_pathfinish ?g z" proof (cases " jumpF f (at_left 1) = 0") case True then have "left = {}" unfolding left_def using jumpF_nz by force then show ?thesis unfolding jumpF_pathfinish_def using True apply (fold f_def) by auto next case False then have "left = {1}" unfolding left_def using jumpF_nz by force then show ?thesis unfolding jumpF_pathfinish_def using False apply (fold f_def) by auto qed ultimately show ?thesis by auto qed moreover have jF_start:"jumpF_pathstart ?g z = (if c1=0 ∧ c2 ≠0 ∧ d1 ≠0 then if c2 >0 ⟷ d1 > 0 then 1/2 else -1/2 else 0)" proof - define f where "f=(λt. (Im b - Im a )* t + d1)" define g where "g=(λt. (Re b - Re a )* t + c1)" have jump_eq:"jumpF_pathstart (linepath a b) z = jumpF (λt. f t/g t) (at_right 0)" unfolding jumpF_pathstart_def f_def linepath_def g_def d1_def c1_def by (auto simp add:algebra_simps) have ?thesis when "¬ (c1 =0 ∧ c2 ≠0 ∧ d1 ≠0)" proof - have "c2=0 ⟶ c1≠0" using ‹¬ (c1=0 ∧ c2=0)› by auto moreover have "d1 =0 ⟶ c1≠0" proof (rule ccontr) assume "¬ (d1 = 0 ⟶ c1 ≠ 0)" then have "a=z" unfolding d1_def c1_def by (simp add: complex_eqI) then have "z∈path_image (linepath a b)" by auto then show False using ‹z∉closed_segment a b› by auto qed moreover have ?thesis when "c1≠0" proof - have "jumpF (λt. f t/g t) (at_right 0) = 0" apply (rule jumpF_not_infinity) apply (unfold f_def g_def) using that by (auto intro!: continuous_intros) then show ?thesis using jump_eq using that by auto qed ultimately show ?thesis using that by blast qed moreover have ?thesis when "c1=0" "c2 ≠0" "d1 ≠0" "c2 >0 ⟷ d1 > 0" proof - have "(LIM x at_right 0. f x / g x :> at_top)" proof - have "(f ⤏ d1) (at_right 0)" unfolding f_def by (auto intro!: tendsto_eq_intros) moreover have "(g ⤏ 0) (at_right 0)" unfolding g_def using ‹c1=0› by (auto intro!: tendsto_eq_intros) moreover have "(g has_sgnx sgn d1) (at_right 0)" proof - have "(g has_sgnx sgn (c2-c1)) (at_right 0)" unfolding g_def apply (rule has_sgnx_derivative_at_right) subgoal unfolding c2_def c1_def d1_def by (auto intro!: derivative_eq_intros) subgoal using ‹c1=0› by auto subgoal using ‹c1=0› ‹c2≠0› by auto done moreover have "sgn (c2-c1) = sgn d1" using that by fastforce ultimately show ?thesis by auto qed ultimately show ?thesis using filterlim_divide_at_bot_at_top_iff[of f d1 "at_right 0" g] ‹d1≠0› by auto qed then have "jumpF (λt. f t/g t) (at_right 0) = 1/2" unfolding jumpF_def by auto then show ?thesis using that jump_eq by auto qed moreover have ?thesis when "c1=0" "c2 ≠0" "d1 ≠0" "¬ c2 >0 ⟷ d1 > 0" proof - have "(LIM x at_right 0. f x / g x :> at_bot)" proof - have "(f ⤏ d1) (at_right 0)" unfolding f_def by (auto intro!: tendsto_eq_intros) moreover have "(g ⤏ 0) (at_right 0)" unfolding g_def using ‹c1=0› by (auto intro!: tendsto_eq_intros) moreover have "(g has_sgnx - sgn d1) (at_right 0)" proof - have "(g has_sgnx sgn (c2-c1)) (at_right 0)" unfolding g_def apply (rule has_sgnx_derivative_at_right) subgoal unfolding c2_def c1_def d1_def by (auto intro!: derivative_eq_intros) subgoal using ‹c1=0› by auto subgoal using ‹c1=0› ‹c2≠0› by auto done moreover have "sgn (c2-c1) = - sgn d1" using that by fastforce ultimately show ?thesis by auto qed ultimately show ?thesis using filterlim_divide_at_bot_at_top_iff[of f d1 "at_right 0" g] ‹d1≠0› by auto qed then have "jumpF (λt. f t/g t) (at_right 0) = - 1/2" unfolding jumpF_def by auto then show ?thesis using that jump_eq by auto qed ultimately show ?thesis by fast qed moreover have jF_finish:"jumpF_pathfinish ?g z = (if c2=0 ∧ c1 ≠0 ∧ d2 ≠0 then if c1 >0 ⟷ d2 > 0 then 1/2 else -1/2 else 0)" proof - define f where "f=(λt. (Im b - Im a )* t + (Im a - Im z))" define g where "g=(λt. (Re b - Re a )* t + (Re a - Re z))" have jump_eq:"jumpF_pathfinish (linepath a b) z = jumpF (λt. f t/g t) (at_left 1)" unfolding jumpF_pathfinish_def f_def linepath_def g_def d1_def c1_def by (auto simp add:algebra_simps) have ?thesis when "¬ (c2 =0 ∧ c1 ≠0 ∧ d2 ≠0)" proof - have "c1=0 ⟶ c2≠0" using ‹¬ (c1=0 ∧ c2=0)› by auto moreover have "d2 =0 ⟶ c2≠0" proof (rule ccontr) assume "¬ (d2 = 0 ⟶ c2 ≠ 0)" then have "b=z" unfolding d2_def c2_def by (simp add: complex_eqI) then have "z∈path_image (linepath a b)" by auto then show False using ‹z∉closed_segment a b› by auto qed moreover have ?thesis when "c2≠0" proof - have "jumpF (λt. f t/g t) (at_left 1) = 0" apply (rule jumpF_not_infinity) apply (unfold f_def g_def) using that unfolding c2_def by (auto intro!: continuous_intros) then show ?thesis using jump_eq using that by auto qed ultimately show ?thesis using that by blast qed moreover have ?thesis when "c2=0" "c1 ≠0" "d2 ≠0" "c1 >0 ⟷ d2 > 0" proof - have "(LIM x at_left 1. f x / g x :> at_top)" proof - have "(f ⤏ d2) (at_left 1)" unfolding f_def d2_def by (auto intro!: tendsto_eq_intros) moreover have "(g ⤏ 0) (at_left 1)" using ‹c2=0› unfolding g_def c2_def by (auto intro!: tendsto_eq_intros) moreover have "(g has_sgnx sgn d2) (at_left 1)" proof - have "(g has_sgnx - sgn (c2-c1)) (at_left 1)" unfolding g_def apply (rule has_sgnx_derivative_at_left) subgoal unfolding c2_def c1_def d1_def by (auto intro!: derivative_eq_intros) subgoal using ‹c2=0› unfolding c2_def by auto subgoal using ‹c2=0› ‹c1≠0› by auto done moreover have "- sgn (c2-c1) = sgn d2" using that by fastforce ultimately show ?thesis by auto qed ultimately show ?thesis using filterlim_divide_at_bot_at_top_iff[of f d2 "at_left 1" g] ‹d2≠0› by auto qed then have "jumpF (λt. f t/g t) (at_left 1) = 1/2" unfolding jumpF_def by auto then show ?thesis using that jump_eq by auto qed moreover have ?thesis when "c2=0" "c1 ≠0" "d2 ≠0" "¬ c1 >0 ⟷ d2 > 0" proof - have "(LIM x at_left 1. f x / g x :> at_bot)" proof - have "(f ⤏ d2) (at_left 1)" unfolding f_def d2_def by (auto intro!: tendsto_eq_intros) moreover have "(g ⤏ 0) (at_left 1)" using ‹c2=0› unfolding g_def c2_def by (auto intro!: tendsto_eq_intros) moreover have "(g has_sgnx - sgn d2) (at_left 1)" proof - have "(g has_sgnx - sgn (c2-c1)) (at_left 1)" unfolding g_def apply (rule has_sgnx_derivative_at_left) subgoal unfolding c2_def c1_def d1_def by (auto intro!: derivative_eq_intros) subgoal using ‹c2=0› unfolding c2_def by auto subgoal using ‹c2=0› ‹c1≠0› by auto done moreover have "sgn (c2-c1) = sgn d2" using that by fastforce ultimately show ?thesis by auto qed ultimately show ?thesis using filterlim_divide_at_bot_at_top_iff[of f d2 "at_left 1" g] ‹d2≠0› by auto qed then have "jumpF (λt. f t/g t) (at_left 1) = - 1/2" unfolding jumpF_def by auto then show ?thesis using that jump_eq by auto qed ultimately show ?thesis by fast qed ultimately show ?thesis using ‹¬ ((c1>0 ∧ c2<0) ∨ (c1<0 ∧ c2>0))› apply (fold c1_def c2_def d1_def d2_def) by auto qed moreover have ?thesis when "c1=0" "c2=0" proof - have "(λt. Re (linepath a b t - z)) = (λ_. 0)" using that unfolding linepath_def c1_def c2_def by (auto simp add:algebra_simps) then have "(λt. Im (linepath a b t - z) / Re (linepath a b t - z)) = (λ_. 0)" by (metis div_by_0) then have "cindex_pathE (linepath a b) z = 0" unfolding cindex_pathE_def by (auto intro: cindexE_constI) thus ?thesis using ‹¬ ((c1>0 ∧ c2<0) ∨ (c1<0 ∧ c2>0))› that apply (fold c1_def c2_def d1_def d2_def) by auto qed ultimately show ?thesis by fast qed moreover have ?thesis when c1c2_diff_sgn:"(c1>0 ∧ c2<0) ∨ (c1<0 ∧ c2>0)" proof - define f where "f=(λt. (Im b - Im a )* t + (Im a - Im z))" define g where "g=(λt. (Re b - Re a )* t + (Re a - Re z))" define h where "h=(λt. f t/ g t)" define c3 where "c3=Im(a)*Re(b)+Re(z)*Im(b)+Im(z)*Re(a) -Im(z)*Re(b) - Im(b)*Re(a) - Re(z)*Im(a)" define u where "u = (Re z - Re a) / (Re b - Re a)" let ?g = "λt. linepath a b t - z" have "0<u" "u<1" "Re b - Re a≠0" using that unfolding u_def c1_def c2_def by (auto simp add:field_simps) have "Re(?g u) = 0" "g u=0" unfolding linepath_def u_def g_def apply (auto simp add:field_simps) using ‹Re b - Re a≠0› by (auto simp add:field_simps) moreover have "u1 = u2" when "Re(?g u1) = 0" "Re(?g u2) = 0" for u1 u2 proof - have " (u1 - u2) * (Re b - Re a) = Re(?g u1) - Re(?g u2)" unfolding linepath_def by (auto simp add:algebra_simps) also have "... = 0" using that by auto finally have "(u1 - u2) * (Re b - Re a) = 0" . thus ?thesis using ‹Re b - Re a≠0› by auto qed ultimately have re_g_iff:"Re(?g t) = 0 ⟷ t=u" for t by blast have "cindex_pathE (linepath a b) z = jumpF h (at_right u) - jumpF h (at_left u)" proof - define left where "left = {x. jumpF h (at_left x) ≠ 0 ∧ 0 < x ∧ x ≤ 1}" define right where "right = {x. jumpF h (at_right x) ≠ 0 ∧ 0 ≤ x ∧ x < 1}" have jumpF_nz:"jumpF h (at_left x) = 0" "jumpF h (at_right x) = 0" when "0≤x" "x≤1" "x≠u" for x proof - have "g x≠0" using re_g_iff ‹x≠u› unfolding g_def linepath_def by (metis ‹Re b - Re a ≠ 0› add_diff_cancel_left' diff_diff_eq2 diff_zero nonzero_mult_div_cancel_left u_def) then have "isCont h x" unfolding h_def f_def g_def by (auto intro!:continuous_intros) then have "continuous (at_left x) h" "continuous (at_right x) h" using continuous_at_split by blast+ then show "jumpF h (at_left x) = 0" "jumpF h(at_right x) = 0" using jumpF_not_infinity by auto qed have "cindex_pathE (linepath a b) z = sum (λx. jumpF h (at_right x)) right - sum (λx. jumpF h (at_left x)) left" proof - have "cindex_pathE (linepath a b) z = cindexE 0 1 (λt. Im (?g t) / Re (?g t))" unfolding cindex_pathE_def by auto also have "... = cindexE 0 1 h" proof - have "(λt. Im (?g t) / Re (?g t)) = h" unfolding h_def f_def g_def linepath_def by (auto simp add:algebra_simps) then show ?thesis by auto qed also have "... = sum (λx. jumpF h (at_right x)) right - sum (λx. jumpF h (at_left x)) left" unfolding cindexE_def left_def right_def by auto finally show ?thesis . qed moreover have "sum (λx. jumpF h (at_right x)) right = jumpF h (at_right u)" proof (cases " jumpF h (at_right u) = 0") case True then have "right = {}" unfolding right_def using jumpF_nz by force then show ?thesis using True by auto next case False then have "right = {u}" unfolding right_def using jumpF_nz ‹0<u› ‹u<1› by fastforce then show ?thesis by auto qed moreover have "sum (λx. jumpF h (at_left x)) left = jumpF h (at_left u)" proof (cases " jumpF h (at_left u) = 0") case True then have "left = {}" unfolding left_def apply safe apply (case_tac "x=u") using jumpF_nz ‹0<u› ‹u<1› by auto then show ?thesis using True by auto next case False then have "left = {u}" unfolding left_def apply safe apply (case_tac "x=u") using jumpF_nz ‹0<u› ‹u<1› by auto then show ?thesis by auto qed ultimately show ?thesis by auto qed moreover have "jump h u = (if c3>0 then 1 else -1)" proof - have "Re b-Re a≠0" using c1c2_diff_sgn unfolding c1_def c2_def by auto have "jump (λt. Im(?g t) / Re(?g t)) u = jump h u" apply (rule arg_cong2[where f=jump]) unfolding linepath_def h_def f_def g_def by (auto simp add:algebra_simps) moreover have "jump (λt. Im(?g t) / Re(?g t)) u = (if sgn (Re b -Re a) = sgn (Im(?g u)) then 1 else - 1)" proof (rule jump_divide_derivative) have "path ?g" using path_offset by auto then have "continuous_on {0..1} (λt. Im(?g t))" using continuous_on_Im path_def by blast then show "isCont (λt. Im (?g t)) u" unfolding path_def apply (elim continuous_on_interior) using ‹0<u› ‹u<1› by auto next show "Re(?g u) = 0" "Re b - Re a ≠ 0" using ‹Re(?g u) = 0› ‹Re b - Re a ≠ 0› by auto show "Im(?g u) ≠ 0" proof (rule ccontr) assume "¬ Im (linepath a b u - z) ≠ 0 " then have "?g u = 0" using ‹Re(?g u) = 0› by (simp add: complex_eq_iff) then have "z ∈ closed_segment a b" using ‹0<u› ‹u<1› by (auto intro:linepath_in_path) thus False using ‹z ∉ closed_segment a b› by simp qed show "((λt. Re (linepath a b t - z)) has_real_derivative Re b - Re a) (at u)" unfolding linepath_def by (auto intro!:derivative_eq_intros) qed moreover have "sgn (Re b - Re a) = sgn (Im(?g u)) ⟷ c3 > 0" proof - have "Im(?g u) = c3/(Re b-Re a)" proof - define ba where "ba = Re b-Re a" have "ba≠0" using ‹Re b - Re a ≠ 0› unfolding ba_def by auto then show ?thesis unfolding linepath_def u_def c3_def apply (fold ba_def) apply (auto simp add:field_simps) by (auto simp add:algebra_simps ba_def) qed then have "sgn (Re b - Re a) = sgn (Im(?g u)) ⟷ sgn (Re b - Re a) = sgn (c3/(Re b-Re a))" by auto also have "... ⟷ c3>0" using ‹Re b-Re a≠0› apply (cases "0::real" c3 rule:linorder_cases) by (auto simp add:sgn_zero_iff) finally show ?thesis . qed ultimately show ?thesis by auto qed moreover have "jump h u = jumpF h (at_right u) - jumpF h (at_left u)" proof (rule jump_jumpF) have "f u≠0" proof (rule ccontr) assume "¬ f u ≠ 0" then have "z∈path_image (linepath a b)" unfolding path_image_def apply (rule_tac rev_image_eqI[of u]) using re_g_iff[of u,simplified] ‹0<u› ‹u<1› unfolding f_def linepath_def by (auto simp add:algebra_simps complex.expand) then show False using ‹z∉closed_segment a b› by simp qed then show "isCont (inverse ∘ h) u" unfolding h_def comp_def f_def g_def by (auto intro!: continuous_intros) define hs where "hs = sgn ((f u) / (c2 -c1))" show "(h has_sgnx -hs) (at_left u)" "(h has_sgnx hs) (at_right u)" proof - have ff:"(f has_sgnx sgn (f u)) (at_left u)" "(f has_sgnx sgn (f u)) (at_right u)" proof - have "(f ⤏ f u) (at u)" unfolding f_def by (auto intro!:tendsto_intros) then have " (f has_sgnx sgn (f u)) (at u)" using tendsto_nonzero_has_sgnx[of f, OF _ ‹f u≠0›] by auto then show "(f has_sgnx sgn (f u)) (at_left u)" "(f has_sgnx sgn (f u)) (at_right u)" using has_sgnx_split by blast+ qed have gg:"(g has_sgnx - sgn (c2 - c1)) (at_left u)" "(g has_sgnx sgn (c2 - c1)) (at_right u)" proof - have "(g has_real_derivative c2 - c1) (at u)" unfolding g_def c1_def c2_def by (auto intro!:derivative_eq_intros) moreover have "c2 - c1 ≠ 0" using that by auto ultimately show "(g has_sgnx sgn (c2 - c1)) (at_right u)" "(g has_sgnx - sgn (c2 - c1)) (at_left u)" using has_sgnx_derivative_at_right[of g "c2-c1" u] has_sgnx_derivative_at_left[of g "c2-c1" u] ‹g u=0› by auto qed show "(h has_sgnx - hs) (at_left u)" using has_sgnx_divide[OF ff(1) gg(1)] unfolding h_def hs_def by auto show "(h has_sgnx hs) (at_right u)" using has_sgnx_divide[OF ff(2) gg(2)] unfolding h_def hs_def by auto qed show "hs≠0" "-hs≠0" unfolding hs_def using ‹f u≠0› that by (auto simp add:sgn_if) qed ultimately show ?thesis using that apply (fold c1_def c2_def c3_def) by auto qed ultimately show ?thesis by fast qed lemma cindex_path_linepath: assumes "z∉path_image (linepath a b)" shows "cindex_path (linepath a b) z = ( let c1=Re(a)-Re(z) ; c2=Re(b)-Re(z) ; c3 = Im(a)*Re(b)+Re(z)*Im(b)+Im(z)*Re(a) -Im(z)*Re(b) - Im(b)*Re(a) - Re(z)*Im(a) in if (c1>0 ∧ c2<0) ∨ (c1<0 ∧ c2>0) then (if c3>0 then 1 else -1) else 0)" proof - define c1 c2 where "c1=Re(a)-Re(z)" and "c2=Re(b)-Re(z)" let ?g = "linepath a b" have ?thesis when "¬ ((c1>0 ∧ c2<0) ∨ (c1<0 ∧ c2>0))" proof - have "Re a= Re z ∧ Re b=Re z" when "0<t" "t<1" and asm:"(1-t)*Re a + t * Re b = Re z" for t unfolding c1_def c2_def using that proof - have ?thesis when "c1≤0" "c1≥0" proof - have "Re a=Re z" using that unfolding c1_def by auto then show ?thesis using ‹0<t› ‹t<1› asm apply (cases "Re b" "Re z" rule:linorder_cases) apply (auto simp add:field_simps) done qed moreover have ?thesis when "c1≤0" "c2≤0" proof - have False when "c1<0" proof - have "(1 - t) * Re a < (1 - t) * Re z" using ‹t<1› ‹c1<0› unfolding c1_def by auto moreover have "t * Re b ≤ t* Re z" using ‹t>0› ‹c2≤0› unfolding c2_def by auto ultimately have "(1 - t) * Re a + t * Re b < (1 - t) * Re z + t * Re z" by auto thus False using asm by (auto simp add:algebra_simps) qed moreover have False when "c2<0" proof - have "(1 - t) * Re a ≤ (1 - t) * Re z" using ‹t<1› ‹c1≤0› unfolding c1_def by auto moreover have "t * Re b < t* Re z" using ‹t>0› ‹c2<0› unfolding c2_def by auto ultimately have "(1 - t) * Re a + t * Re b < (1 - t) * Re z + t * Re z" by auto thus False using asm by (auto simp add:algebra_simps) qed ultimately show ?thesis using that unfolding c1_def c2_def by argo qed moreover have ?thesis when "c2≤0" "c2≥0" proof - have "Re b=Re z" using that unfolding c2_def by auto then have "(1 - t) * Re a = (1-t)*Re z" using asm by (auto simp add:field_simps) then have "Re a= Re z" using ‹t<1› by auto then show ?thesis using ‹Re b=Re z› by auto qed moreover have ?thesis when "c1≥0" "c2≥0" proof - have False when "c1>0" proof - have "(1 - t) * Re a > (1 - t) * Re z" using ‹t<1› ‹c1>0› unfolding c1_def by auto moreover have "t * Re b ≥ t* Re z" using ‹t>0› ‹c2≥0› unfolding c2_def by auto ultimately have "(1 - t) * Re a + t * Re b > (1 - t) * Re z + t * Re z" by auto thus False using asm by (auto simp add:algebra_simps) qed moreover have False when "c2>0" proof - have "(1 - t) * Re a ≥ (1 - t) * Re z" using ‹t<1› ‹c1≥0› unfolding c1_def by auto moreover have "t * Re b > t* Re z" using ‹t>0› ‹c2>0› unfolding c2_def by auto ultimately have "(1 - t) * Re a + t * Re b > (1 - t) * Re z + t * Re z" by auto thus False using asm by (auto simp add:algebra_simps) qed ultimately show ?thesis using that unfolding c1_def c2_def by argo qed moreover have "c1≤0 ∨ c2≥0" "c1≥0 ∨ c2≤0" using ‹¬ ((c1>0 ∧ c2<0) ∨ (c1<0 ∧ c2>0))› by auto ultimately show ?thesis by fast qed then have "(∀t. 0<t ∧ t<1 ⟶ Re(linepath a b t - z) ≠ 0) ∨ (Re a= Re z ∧ Re b=Re z)" using that unfolding linepath_def by auto moreover have ?thesis when asm:"∀t. 0<t ∧ t<1 ⟶ Re(linepath a b t - z) ≠ 0" proof - have "jump (λt. Im (linepath a b t - z) / Re (linepath a b t - z)) t = 0" when "0<t" "t<1" for t apply (rule jump_Im_divide_Re_0[of "λt. linepath a b t - z", OF _ asm[rule_format]]) by (auto simp add:path_offset that) then have "cindex_path (linepath a b) z = 0" unfolding cindex_path_def cindex_def by auto thus ?thesis using ‹¬ ((c1>0 ∧ c2<0) ∨ (c1<0 ∧ c2>0))› apply (fold c1_def c2_def) by auto qed moreover have ?thesis when "Re a= Re z" "Re b=Re z" proof - have "(λt. Re (linepath a b t - z)) = (λ_. 0)" unfolding linepath_def using ‹Re a= Re z› ‹Re b=Re z› by (auto simp add:algebra_simps) then have "(λt. Im (linepath a b t - z) / Re (linepath a b t - z)) = (λ_. 0)" by (metis div_by_0) then have "jump (λt. Im (linepath a b t - z) / Re (linepath a b t - z)) t = 0" for t using jump_const by auto then have "cindex_path (linepath a b) z = 0" unfolding cindex_path_def cindex_def by auto thus ?thesis using ‹¬ ((c1>0 ∧ c2<0) ∨ (c1<0 ∧ c2>0))› apply (fold c1_def c2_def) by auto qed ultimately show ?thesis by auto qed moreover have ?thesis when c1c2_diff_sgn:"(c1>0 ∧ c2<0) ∨ (c1<0 ∧ c2>0)" proof - define c3 where "c3=Im(a)*Re(b)+Re(z)*Im(b)+Im(z)*Re(a) -Im(z)*Re(b) - Im(b)*Re(a) - Re(z)*Im(a)" define u where "u = (Re z - Re a) / (Re b - Re a)" let ?g = "λt. linepath a b t - z" have "0<u" "u<1" "Re b - Re a≠0" using that unfolding u_def c1_def c2_def by (auto simp add:field_simps) have "Re(?g u) = 0" unfolding linepath_def u_def apply (auto simp add:field_simps) using ‹Re b - Re a≠0› by (auto simp add:field_simps) moreover have "u1 = u2" when "Re(?g u1) = 0" "Re(?g u2) = 0" for u1 u2 proof - have " (u1 - u2) * (Re b - Re a) = Re(?g u1) - Re(?g u2)" unfolding linepath_def by (auto simp add:algebra_simps) also have "... = 0" using that by auto finally have "(u1 - u2) * (Re b - Re a) = 0" . thus ?thesis using ‹Re b - Re a≠0› by auto qed ultimately have re_g_iff:"Re(?g t) = 0 ⟷ t=u" for t by blast have "cindex_path (linepath a b) z = jump (λt. Im (?g t)/Re(?g t)) u" proof - define f where "f=(λt. Im (linepath a b t - z) / Re (linepath a b t - z))" have "jump f t =0" when "t≠u" "0<t" "t<1" for t unfolding f_def apply (rule jump_Im_divide_Re_0) using that re_g_iff by (auto simp add: path_offset) then have "{x. jump f x ≠ 0 ∧ 0 < x ∧ x < 1} = (if jump f u=0 then {} else {u})" using ‹0<u› ‹u<1› apply auto by fastforce then show ?thesis unfolding cindex_path_def cindex_def apply (fold f_def) by auto qed moreover have "jump (λt. Im (?g t)/Re(?g t)) u = (if c3>0 then 1 else -1)" proof - have "Re b-Re a≠0" using c1c2_diff_sgn unfolding c1_def c2_def by auto have "jump (λt. Im(?g t) / Re(?g t)) u = (if sgn (Re b -Re a) = sgn (Im(?g u)) then 1 else - 1)" proof (rule jump_divide_derivative) have "path ?g" using path_offset by auto then have "continuous_on {0..1} (λt. Im(?g t))" using continuous_on_Im path_def by blast then show "isCont (λt. Im (?g t)) u" unfolding path_def apply (elim continuous_on_interior) using ‹0<u› ‹u<1› by auto next show "Re(?g u) = 0" "Re b - Re a ≠ 0" using ‹Re(?g u) = 0› ‹Re b - Re a ≠ 0› by auto show "Im(?g u) ≠ 0" proof (rule ccontr) assume "¬ Im (linepath a b u - z) ≠ 0 " then have "?g u = 0" using ‹Re(?g u) = 0› by (simp add: complex_eq_iff) thus False using assms ‹0<u› ‹u<1› unfolding path_image_def by fastforce qed show "((λt. Re (linepath a b t - z)) has_real_derivative Re b - Re a) (at u)" unfolding linepath_def by (auto intro!:derivative_eq_intros) qed moreover have "sgn (Re b - Re a) = sgn (Im(?g u)) ⟷ c3 > 0" proof - have "Im(?g u) = c3/(Re b-Re a)" proof - define ba where "ba = Re b-Re a" have "ba≠0" using ‹Re b - Re a ≠ 0› unfolding ba_def by auto then show ?thesis unfolding linepath_def u_def c3_def apply (fold ba_def) apply (auto simp add:field_simps) by (auto simp add:algebra_simps ba_def) qed then have "sgn (Re b - Re a) = sgn (Im(?g u)) ⟷ sgn (Re b - Re a) = sgn (c3/(Re b-Re a))" by auto also have "... ⟷ c3>0" using ‹Re b-Re a≠0› apply (cases "0::real" c3 rule:linorder_cases) by (auto simp add:sgn_zero_iff) finally show ?thesis . qed ultimately show ?thesis by auto qed ultimately show ?thesis using c1c2_diff_sgn apply (fold c1_def c2_def c3_def) by auto qed ultimately show ?thesis by blast qed lemma cindex_pathE_part_circlepath: assumes "cmod (z-z0) ≠r" and "r>0" "0≤st" "st<tt" "tt≤2*pi" shows "cindex_pathE (part_circlepath z r st tt) z0 = ( if ¦Re z - Re z0¦ < r then (let θ = arccos ((Re z0 - Re z)/r); β = 2*pi - θ in jumpF_pathstart (part_circlepath z r st tt) z0 + (if st<θ ∧ θ<tt then if r * sin θ + Im z > Im z0 then -1 else 1 else 0) + (if st<β ∧ β < tt then if r * sin β + Im z > Im z0 then 1 else -1 else 0) - jumpF_pathfinish (part_circlepath z r st tt) z0 ) else if ¦Re z - Re z0¦ = r then jumpF_pathstart (part_circlepath z r st tt) z0 - jumpF_pathfinish (part_circlepath z r st tt) z0 else 0 )" proof - define f where "f=(λi. r * sin i + Im z - Im z0)" define g where "g=(λi. r * cos i + Re z - Re z0)" define h where "h=(λt. f t / g t)" have index_eq:"cindex_pathE (part_circlepath z r st tt) z0 = cindexE st tt h" proof - have "cindex_pathE (part_circlepath z r st tt) z0 = cindexE 0 1 ((λi. f i/g i) o (linepath st tt))" unfolding cindex_pathE_def part_circlepath_def exp_Euler f_def g_def comp_def by (simp add:cos_of_real sin_of_real algebra_simps) also have "... = cindexE st tt (λi. f i/g i)" unfolding linepath_def using cindexE_linear_comp[of "tt-st" 0 1 _ st] ‹st<tt› by (simp add:algebra_simps) also have "... = cindexE st tt h" unfolding h_def by simp finally show ?thesis . qed have jstart_eq:"jumpF_pathstart (part_circlepath z r st tt) z0 = jumpF h (at_right st)" proof - have "jumpF_pathstart (part_circlepath z r st tt) z0 = jumpF ((λi. f i/g i) o (linepath st tt)) (at_right 0) " unfolding jumpF_pathstart_def part_circlepath_def exp_Euler f_def g_def comp_def by (simp add:cos_of_real sin_of_real algebra_simps) also have "... = jumpF (λi. f i/g i) (at_right st)" unfolding linepath_def using jumpF_linear_comp(2)[of "tt-st" _ st 0] ‹st<tt› by (simp add:algebra_simps) also have "... = jumpF h (at_right st)" unfolding h_def by simp finally show ?thesis . qed have jfinish_eq:"jumpF_pathfinish (part_circlepath z r st tt) z0 = jumpF h (at_left tt)" proof - have "jumpF_pathfinish (part_circlepath z r st tt) z0 = jumpF ((λi. f i/g i) o (linepath st tt)) (at_left 1) " unfolding jumpF_pathfinish_def part_circlepath_def exp_Euler f_def g_def comp_def by (simp add:cos_of_real sin_of_real algebra_simps) also have "... = jumpF (λi. f i/g i) (at_left tt)" unfolding linepath_def using jumpF_linear_comp(1)[of "tt-st" _ st 1] ‹st<tt› by (simp add:algebra_simps) also have "... = jumpF h (at_left tt)" unfolding h_def by simp finally show ?thesis . qed have finite_jFs:"finite_jumpFs h st tt" proof - note finite_ReZ_segments_imp_jumpFs[OF finite_ReZ_segments_part_circlepath ,of z r st tt z0,simplified] then have "finite_jumpFs ((λi. f i/g i) o (linepath st tt)) 0 1" unfolding h_def f_def g_def part_circlepath_def exp_Euler comp_def by (simp add:cos_of_real sin_of_real algebra_simps) then have "finite_jumpFs (λi. f i/g i) st tt" unfolding linepath_def using finite_jumpFs_linear_pos[of "tt-st" _ st 0 1] ‹st<tt› by (simp add:algebra_simps) then show ?thesis unfolding h_def by auto qed have g_imp_f:"g i = 0 ⟹ f i≠0" for i proof (rule ccontr) assume "g i = 0" "¬ f i ≠ 0 " then have "r * sin i = Im (z0 - z)" "r * cos i = Re (z0 - z)" unfolding f_def g_def by auto then have "(r * sin i) ^2 + (r * cos i)^2 = Im (z0 - z) ^ 2 + Re (z0 - z) ^2" by auto then have "r^2 * (sin i ^2 + cos i^2) = Im (z0 - z) ^ 2 + Re (z0 - z) ^2" by (auto simp only:algebra_simps power_mult_distrib) then have "r^2 = cmod (z0-z) ^ 2" unfolding cmod_def by auto then have "r = cmod (z0-z)" using ‹r>0› power2_eq_imp_eq by fastforce then show False using ‹cmod (z-z0) ≠r› using norm_minus_commute by blast qed have ?thesis when "¦Re z - Re z0¦ > r" proof - have "jumpF h (at_right x) = 0" "jumpF h (at_left x) = 0" for x proof - have "g x ≠0" proof (rule ccontr) assume "¬ g x ≠ 0" then have "cos x = (Re z0 - Re z) / r" unfolding g_def using ‹r>0› by (auto simp add:field_simps) then have "¦(Re z0 - Re z)/r¦ ≤ 1" by (metis abs_cos_le_one) then have "¦Re z0 - Re z¦ ≤ r" using ‹r>0› by (auto simp add:field_simps) then show False using that by auto qed then have "isCont h x" unfolding h_def f_def g_def by (auto intro:continuous_intros) then show "jumpF h (at_right x) = 0" "jumpF h (at_left x) = 0" using jumpF_not_infinity unfolding continuous_at_split by auto qed then have "cindexE st tt h = 0" unfolding cindexE_def by auto then show ?thesis using index_eq that by auto qed moreover have ?thesis when "¦Re z - Re z0¦ = r" proof - define R where "R=(λS.{x. jumpF h (at_right x) ≠ 0 ∧ x∈S})" define L where "L=(λS.{x. jumpF h (at_left x) ≠ 0 ∧ x∈S})" define right where "right = (λS. (∑x∈R S. jumpF h (at_right x)))" define left where "left = (λS. (∑x∈L S. jumpF h (at_left x)))" have "cindex_pathE (part_circlepath z r st tt) z0 = cindexE st tt h" using index_eq by simp also have "... = right {st..<tt} - left {st<..tt}" unfolding cindexE_def right_def left_def R_def L_def by auto also have "... = jumpF h (at_right st) + right {st<..<tt} - left {st<..<tt} - jumpF h (at_left tt)" proof - have "right {st..<tt} = jumpF h (at_right st) + right {st<..<tt}" proof (cases "jumpF h (at_right st) =0") case True then have "R {st..<tt} = R {st<..<tt}" unfolding R_def using less_eq_real_def by auto then have "right {st..<tt} = right {st<..<tt}" unfolding right_def by auto then show ?thesis using True by auto next case False have "finite (R {st..<tt})" using finite_jFs unfolding R_def finite_jumpFs_def by (auto elim:rev_finite_subset) moreover have "st ∈ R {st..<tt}" using False ‹st<tt› unfolding R_def by auto moreover have "R {st..<tt} - {st} = R {st<..<tt}" unfolding R_def by auto ultimately show "right {st..<tt}= jumpF h (at_right st) + right {st<..<tt}" using sum.remove[of "R {st..<tt}" st "λx. jumpF h (at_right x)"] unfolding right_def by simp qed moreover have "left {st<..tt} = jumpF h (at_left tt) + left {st<..<tt}" proof (cases "jumpF h (at_left tt) =0") case True then have "L {st<..tt} = L {st<..<tt}" unfolding L_def using less_eq_real_def by auto then have "left {st<..tt} = left {st<..<tt}" unfolding left_def by auto then show ?thesis using True by auto next case False have "finite (L {st<..tt})" using finite_jFs unfolding L_def finite_jumpFs_def by (auto elim:rev_finite_subset) moreover have "tt ∈ L {st<..tt}" using False ‹st<tt› unfolding L_def by auto moreover have "L {st<..tt} - {tt} = L {st<..<tt}" unfolding L_def by auto ultimately show "left {st<..tt}= jumpF h (at_left tt) + left {st<..<tt}" using sum.remove[of "L {st<..tt}" tt "λx. jumpF h (at_left x)"] unfolding left_def by simp qed ultimately show ?thesis by simp qed also have "... = jumpF h (at_right st) - jumpF h (at_left tt)" proof - define S where "S={x. (jumpF h (at_left x) ≠ 0 ∨ jumpF h (at_right x) ≠ 0) ∧ st < x ∧ x < tt}" have "right {st<..<tt} = sum (λx. jumpF h (at_right x)) S" unfolding right_def S_def R_def apply (rule sum.mono_neutral_left) subgoal using finite_jFs unfolding finite_jumpFs_def by (auto elim:rev_finite_subset) subgoal by auto subgoal by auto done moreover have "left {st<..<tt} = sum (λx. jumpF h (at_left x)) S" unfolding left_def S_def L_def apply (rule sum.mono_neutral_left) subgoal using finite_jFs unfolding finite_jumpFs_def by (auto elim:rev_finite_subset) subgoal by auto subgoal by auto done ultimately have "right {st<..<tt} - left {st<..<tt} = sum (λx. jumpF h (at_right x) - jumpF h (at_left x)) S" by (simp add: sum_subtractf) also have "... = 0" proof - have "jumpF h (at_right i) - jumpF h (at_left i) = 0" when "g i=0" for i proof - have "(LIM x at i. f x / g x :> at_bot) ∨ (LIM x at i. f x / g x :> at_top)" proof - have *: "f ─i→ f i" "g ─i→ 0" "f i ≠ 0" using g_imp_f[OF ‹g i=0›] ‹g i=0› unfolding f_def g_def by (auto intro!:tendsto_eq_intros) have ?thesis when "Re z > Re z0" proof - have g_alt:"g = (λt. r * cos t + r)" unfolding g_def using ‹¦Re z - Re z0¦ = r› that by auto have "(g has_sgnx 1) (at i)" proof - have "sgn (g t) = 1" when "t ≠ i " "dist t i < pi" for t proof - have "cos i = - 1" using ‹g i =0› ‹r>0› unfolding g_alt by (metis add.inverse_inverse less_numeral_extra(3) mult_cancel_left mult_minus1_right real_add_minus_iff) then obtain k::int where k_def:"i = (2 * k + 1) * pi" using cos_eq_minus1[of i] by auto show ?thesis proof (rule ccontr) assume "sgn (g t) ≠ 1" then have "cos t + 1≤0" using ‹r>0› unfolding g_alt by (metis (no_types, hide_lams) add_le_same_cancel1 add_minus_cancel mult_le_cancel_left1 mult_le_cancel_right1 mult_minus_right mult_zero_left sgn_pos zero_le_one) then have "cos t = -1" by (metis add.commute cos_ge_minus_one le_less not_less real_add_le_0_iff) then obtain k'::int where k'_def:"t = (2 * k' + 1) * pi" using cos_eq_minus1[of t] by auto then have "t - i = 2 * pi*(k' - k)" using k_def by (auto simp add:algebra_simps) then have "2 * pi * ¦ (k' - k)¦ < pi" using ‹dist t i < pi› by (simp add:dist_norm abs_mult) from divide_strict_right_mono[OF this, of "2*pi",simplified] have "¦k' - k ¦ < 1/2" by auto then have "k=k'" by linarith then have "t=i" using k_def k'_def by auto then show False using ‹t≠i› by auto qed qed then show ?thesis unfolding has_sgnx_def eventually_at apply(intro exI[where x="pi"]) by auto qed then show ?thesis using * filterlim_divide_at_bot_at_top_iff[of f "f i" "at i" g] by (simp add: sgn_if) qed moreover have ?thesis when "Re z < Re z0" proof - have g_alt:"g = (λt. r * cos t - r)" unfolding g_def using ‹¦Re z - Re z0¦ = r› that by auto have "(g has_sgnx - 1) (at i)" proof - have "sgn (g t) = - 1" when "t ≠ i " "dist t i < pi" for t proof - have "cos i = 1" using ‹g i =0› ‹r>0› unfolding g_alt by simp then obtain k::int where k_def:"i = (2 * k * pi)" using cos_one_2pi_int[of i] by auto show ?thesis proof (rule ccontr) assume "sgn (g t) ≠ - 1" then have "cos t - 1≥0" using ‹r>0› unfolding g_alt using mult_le_cancel_left1 by fastforce then have "cos t = 1" by (meson cos_le_one diff_ge_0_iff_ge le_less not_less) then obtain k'::int where k'_def:"t = 2 * k'* pi" using cos_one_2pi_int[of t] by auto then have "t - i = 2 * pi*(k' - k)" using k_def by (auto simp add:algebra_simps) then have "2 * pi * ¦ (k' - k)¦ < pi" using ‹dist t i < pi› by (simp add:dist_norm abs_mult) from divide_strict_right_mono[OF this, of "2*pi",simplified] have "¦k' - k ¦ < 1/2" by auto then have "k=k'" by linarith then have "t=i" using k_def k'_def by auto then show False using ‹t≠i› by auto qed qed then show ?thesis unfolding has_sgnx_def eventually_at apply(intro exI[where x="pi"]) by auto qed then show ?thesis using * filterlim_divide_at_bot_at_top_iff[of f "f i" "at i" g] by (simp add: sgn_if) qed moreover have "Re z≠ Re z0" using ‹¦Re z - Re z0¦ = r› ‹r>0› by fastforce ultimately show ?thesis by fastforce qed moreover have ?thesis when "(LIM x at i. f x / g x :> at_bot)" proof - have "jumpF h (at_right i) = - 1/2" "jumpF h (at_left i) = -1/2" using that unfolding jumpF_def h_def filterlim_at_split by auto then show ?thesis by auto qed moreover have ?thesis when "(LIM x at i. f x / g x :> at_top)" proof - have "jumpF h (at_right i) = 1/2" "jumpF h (at_left i) = 1/2" using that unfolding jumpF_def h_def filterlim_at_split by auto then show ?thesis by auto qed ultimately show ?thesis by auto qed moreover have "jumpF h (at_right i) - jumpF h (at_left i) = 0" when "g i≠0" for i proof - have "isCont h i" using that unfolding h_def f_def g_def by (auto intro!:continuous_intros) then have "jumpF h (at_right i) = 0" "jumpF h (at_left i) = 0" using jumpF_not_infinity unfolding continuous_at_split by auto then show ?thesis by auto qed ultimately show ?thesis by (intro sum.neutral,auto) qed finally show ?thesis by simp qed also have "... = jumpF_pathstart (part_circlepath z r st tt) z0 - jumpF_pathfinish (part_circlepath z r st tt) z0" using jstart_eq jfinish_eq by auto finally have "cindex_pathE (part_circlepath z r st tt) z0 = jumpF_pathstart (part_circlepath z r st tt) z0 - jumpF_pathfinish (part_circlepath z r st tt) z0" . then show ?thesis using that by auto qed moreover have ?thesis when "¦Re z - Re z0¦ < r" proof - define zr where "zr= (Re z0 - Re z)/r" define θ where "θ = arccos zr" define β where "β = 2*pi - θ" have "0<θ" "θ<pi" proof - have "- 1 < zr" "zr < 1" using that ‹r>0› unfolding zr_def by (auto simp add:field_simps) from arccos_lt_bounded[OF this] show "0<θ" "θ<pi" unfolding θ_def by auto qed have "g θ = 0" "g β = 0" proof - have "¦zr¦≤1" using that unfolding zr_def by auto then have "cos θ = zr" "cos β = cos θ" unfolding θ_def[folded zr_def] β_def by auto then show "g θ = 0" "g β = 0" unfolding zr_def g_def using ‹r>0› by auto qed have g_sgnx_θ:"(g has_sgnx 1) (at_left θ)" "(g has_sgnx -1) (at_right θ)" proof - have "(g has_real_derivative - r * sin θ) (at θ)" unfolding g_def by (auto intro!:derivative_eq_intros) moreover have "- r * sin θ <0" using sin_gt_zero[OF ‹0<θ› ‹θ<pi›] ‹r>0› by auto ultimately show "(g has_sgnx 1) (at_left θ)" "(g has_sgnx -1) (at_right θ)" using has_sgnx_derivative_at_left[of g "- r * sin θ", OF _ ‹g θ=0›] has_sgnx_derivative_at_right[of g "- r * sin θ", OF _ ‹g θ=0›] by force+ qed have g_sgnx_β:"(g has_sgnx -1) (at_left β)" "(g has_sgnx 1) (at_right β)" proof - have "(g has_real_derivative - r * sin β) (at β)" unfolding g_def by (auto intro!:derivative_eq_intros) moreover have "pi<β" "β<2*pi" unfolding β_def using ‹0<θ› ‹θ<pi› by auto from sin_lt_zero[OF this] ‹r>0› have "- r * sin β >0" by (simp add: mult_pos_neg) ultimately show "(g has_sgnx -1) (at_left β)" "(g has_sgnx 1) (at_right β)" using has_sgnx_derivative_at_left[of g "- r * sin β", OF _ ‹g β=0›] has_sgnx_derivative_at_right[of g "- r * sin β", OF _ ‹g β=0›] by force+ qed have f_tendsto: "(f ⤏ f i) (at_left i)" "(f ⤏ f i) (at_right i)" and g_tendsto: "(g ⤏ g i) (at_left i)" "(g ⤏ g i) (at_right i)" for i proof - have "(f ⤏ f i) (at i)" unfolding f_def by (auto intro!:tendsto_eq_intros) then show "(f ⤏ f i) (at_left i)" "(f ⤏ f i) (at_right i)" by (auto simp add: filterlim_at_split) next have "(g ⤏ g i) (at i)" unfolding g_def by (auto intro!:tendsto_eq_intros) then show "(g ⤏ g i) (at_left i)" "(g ⤏ g i) (at_right i)" by (auto simp add: filterlim_at_split) qed define θ_if::real where "θ_if = (if r * sin θ + Im z > Im z0 then -1 else 1)" define β_if::real where "β_if = (if r * sin β + Im z > Im z0 then 1 else -1)" have "jump (λi. f i/g i) θ = θ_if" proof - have ?thesis when "r * sin θ + Im z > Im z0" proof - have "f θ > 0" using that unfolding f_def by auto have "(LIM x (at_left θ). f x / g x :> at_top)" apply (subst filterlim_divide_at_bot_at_top_iff[of f "f θ" _ g]) using ‹f θ > 0› ‹g θ =0› f_tendsto g_tendsto[of θ] g_sgnx_θ by auto moreover then have "¬ (LIM x (at_left θ). f x / g x :> at_bot)" by auto moreover have "(LIM x (at_right θ). f x / g x :> at_bot)" apply (subst filterlim_divide_at_bot_at_top_iff[of f "f θ" _ g]) using ‹f θ > 0› ‹g θ =0› f_tendsto g_tendsto[of θ] g_sgnx_θ by auto ultimately show ?thesis using that unfolding jump_def θ_if_def by auto qed moreover have ?thesis when "r * sin θ + Im z < Im z0" proof - have "f θ < 0" using that unfolding f_def by auto have "(LIM x (at_left θ). f x / g x :> at_bot)" apply (subst filterlim_divide_at_bot_at_top_iff[of f "f θ" _ g]) using ‹f θ < 0› ‹g θ =0› f_tendsto g_tendsto[of θ] g_sgnx_θ by auto moreover have "(LIM x (at_right θ). f x / g x :> at_top)" apply (subst filterlim_divide_at_bot_at_top_iff[of f "f θ" _ g]) using ‹f θ < 0› ‹g θ =0› f_tendsto g_tendsto[of θ] g_sgnx_θ by auto ultimately show ?thesis using that unfolding jump_def θ_if_def by auto qed moreover have "r * sin θ + Im z ≠ Im z0" using g_imp_f[OF ‹g θ=0›] unfolding f_def by auto ultimately show ?thesis by fastforce qed moreover have "jump (λi. f i/g i) β = β_if" proof - have ?thesis when "r * sin β + Im z > Im z0" proof - have "f β > 0" using that unfolding f_def by auto have "(LIM x (at_left β). f x / g x :> at_bot)" apply (subst filterlim_divide_at_bot_at_top_iff[of f "f β" _ g]) using ‹f β > 0› ‹g β =0› f_tendsto g_tendsto[of β] g_sgnx_β by auto moreover have "(LIM x (at_right β). f x / g x :> at_top)" apply (subst filterlim_divide_at_bot_at_top_iff[of f "f β" _ g]) using ‹f β > 0› ‹g β =0› f_tendsto g_tendsto[of β] g_sgnx_β by auto ultimately show ?thesis using that unfolding jump_def β_if_def by auto qed moreover have ?thesis when "r * sin β + Im z < Im z0" proof - have "f β < 0" using that unfolding f_def by auto have "(LIM x (at_left β). f x / g x :> at_top)" apply (subst filterlim_divide_at_bot_at_top_iff[of f "f β" _ g]) using ‹f β < 0› ‹g β =0› f_tendsto g_tendsto[of β] g_sgnx_β by auto moreover have "(LIM x (at_right β). f x / g x :> at_bot)" apply (subst filterlim_divide_at_bot_at_top_iff[of f "f β" _ g]) using ‹f β < 0› ‹g β =0› f_tendsto g_tendsto[of β] g_sgnx_β by auto ultimately show ?thesis using that unfolding jump_def β_if_def by auto qed moreover have "r * sin β + Im z ≠ Im z0" using g_imp_f[OF ‹g β=0›] unfolding f_def by auto ultimately show ?thesis by fastforce qed moreover have "jump (λi. f i / g i) x ≠ 0 ⟷ x=θ ∨ x=β" when "st<x" "x<tt" for x proof assume "x = θ ∨ x = β" then show "jump (λi. f i / g i) x ≠ 0" using ‹jump (λi. f i/g i) θ = θ_if› ‹jump (λi. f i/g i) β = β_if› unfolding θ_if_def β_if_def by (metis add.inverse_inverse add.inverse_neutral of_int_0 one_neq_zero) next assume asm:"jump (λi. f i / g i) x ≠ 0" let ?thesis = "x = θ ∨ x = β" have "g x=0" proof (rule ccontr) assume "g x ≠ 0" then have "isCont (λi. f i / g i) x" unfolding f_def g_def by (auto intro:continuous_intros) then have "jump (λi. f i / g i) x = 0" using jump_not_infinity by simp then show False using asm by auto qed then have "cos x = zr" unfolding g_def zr_def using ‹r>0› by (auto simp add:field_simps) have ?thesis when "x≤pi" proof- have "x≥0" using ‹st<x› ‹st≥0› by auto then have "arccos (cos x) = x" using arccos_cos[of x] that by auto then have "x=θ" unfolding θ_def ‹cos x=zr› by auto then show ?thesis by auto qed moreover have ?thesis when "¬ x≤pi" proof - have "x-2*pi≤0" "-pi≤x-2*pi" using that ‹x<tt› ‹tt≤2*pi› by auto from arccos_cos2[OF this] have "arccos (cos (x - 2 * pi)) = 2*pi-x" by auto then have "arccos (cos x) = 2*pi-x" by (metis arccos cos_2pi_minus cos_ge_minus_one cos_le_one) then have "x=β" unfolding β_def θ_def using ‹cos x =zr› by auto then show ?thesis by auto qed ultimately show ?thesis by auto qed then have "{x. jump (λi. f i / g i) x ≠ 0 ∧ st < x ∧ x < tt} = {θ,β} ∩ {st<..<tt}" by force moreover have "θ≠β" using β_def ‹θ < pi› by auto ultimately have "cindex st tt h = (if st<θ ∧ θ<tt then θ_if else 0) + (if st<β ∧ β < tt then β_if else 0)" unfolding cindex_def h_def by fastforce moreover have "cindexE st tt h = jumpF h (at_right st) + cindex st tt h - jumpF h (at_left tt)" proof (rule cindex_eq_cindexE_divide[of st tt f g,folded h_def]) show "st < tt" using ‹st < tt› . show "∀x∈{st..tt}. g x = 0 ⟶ f x ≠ 0" using g_imp_f by auto show "continuous_on {st..tt} f" "continuous_on {st..tt} g" unfolding f_def g_def by (auto intro!:continuous_intros) next let ?S1="{t. Re (part_circlepath z r st tt t-z0) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" let ?S2="{t. Im (part_circlepath z r st tt t-z0) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" define G where "G={t. g (linepath st tt t) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" define F where "F={t. f (linepath st tt t) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" define vl where "vl=(λx. (x-st)/(tt-st))" have "finite G" "finite F" proof - have "finite {t. Re (part_circlepath z r st tt t-z0) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" "finite {t. Im (part_circlepath z r st tt t-z0) = 0 ∧ 0 ≤ t ∧ t ≤ 1}" using part_circlepath_half_finite_inter[of st tt r "Complex 1 0" z "Re z0"] part_circlepath_half_finite_inter[of st tt r "Complex 0 1" z "Im z0"] ‹st<tt› ‹r>0› by (auto simp add:inner_complex_def Complex_eq_0) moreover have "Re (part_circlepath z r st tt t-z0) = 0 ⟷ g (linepath st tt t) = 0" "Im (part_circlepath z r st tt t-z0) = 0 ⟷ f (linepath st tt t) = 0" for t unfolding cindex_pathE_def part_circlepath_def exp_Euler f_def g_def comp_def by (auto simp add:cos_of_real sin_of_real algebra_simps) ultimately show "finite G" "finite F" unfolding G_def F_def by auto qed then have "finite (linepath st tt ` F)" "finite (linepath st tt ` G)" by auto moreover have "{x. f x = 0 ∧ st ≤ x ∧ x ≤ tt} ⊆ linepath st tt ` F" "{x. g x = 0 ∧ st ≤ x ∧ x ≤ tt} ⊆ linepath st tt ` G" proof - have *: "linepath st tt (vl t) = t" "vl t≥0 ⟷ t≥st" "vl t≤1 ⟷t≤tt" for t unfolding linepath_def vl_def using ‹tt>st› apply (auto simp add:divide_simps) by (simp add:algebra_simps) then show "{x. f x = 0 ∧ st ≤ x ∧ x ≤ tt} ⊆ linepath st tt `F" "{x. g x = 0 ∧ st ≤ x ∧ x ≤ tt} ⊆ linepath st tt `G" unfolding F_def G_def by (clarify|rule_tac x="vl x" in rev_image_eqI,auto)+ qed ultimately have "finite {x. f x = 0 ∧ st ≤ x ∧ x ≤ tt}" "finite {x. g x = 0 ∧ st ≤ x ∧ x ≤ tt}" by (auto elim:rev_finite_subset) from finite_UnI[OF this] show "finite {x. (f x = 0 ∨ g x = 0) ∧ st ≤ x ∧ x ≤ tt}" by (elim rev_finite_subset,auto) qed ultimately show ?thesis unfolding Let_def apply (fold zr_def θ_def β_def θ_if_def β_if_def)+ using jstart_eq jfinish_eq index_eq that by auto qed ultimately show ?thesis by fastforce qed lemma jumpF_pathstart_part_circlepath: assumes "st<tt" "r>0" "cmod (z-z0) ≠r" shows "jumpF_pathstart (part_circlepath z r st tt) z0 = ( if r * cos st + Re z - Re z0 = 0 then (let Δ = r* sin st + Im z - Im z0 in if (sin st > 0 ∨ cos st=1 ) ∧ Δ < 0 ∨ (sin st < 0 ∨ cos st=-1 ) ∧ Δ > 0 then 1/2 else - 1/2) else 0)" proof - define f where "f=(λi. r * sin i + Im z - Im z0)" define g where "g=(λi. r * cos i + Re z - Re z0)" have jumpF_eq:"jumpF_pathstart (part_circlepath z r st tt) z0 = jumpF (λi. f i/g i) (at_right st)" proof - have "jumpF_pathstart (part_circlepath z r st tt) z0 = jumpF ((λi. f i/g i) o linepath st tt) (at_right 0)" unfolding jumpF_pathstart_def part_circlepath_def exp_Euler f_def g_def comp_def by (simp add:cos_of_real sin_of_real algebra_simps) also have "... = jumpF (λi. f i/g i) (at_right st)" using jumpF_linear_comp(2)[of "tt-st" "(λi. f i/g i)" st 0,symmetric] ‹st<tt› unfolding linepath_def by (auto simp add:algebra_simps) finally show ?thesis . qed have g_has_sgnx1:"(g has_sgnx 1) (at_right st)" when "g st=0" "sin st < 0 ∨ cos st=-1" proof - have ?thesis when "sin st<0" proof - have "(g has_sgnx sgn (- r * sin st)) (at_right st)" apply (rule has_sgnx_derivative_at_right[of g "- r * sin st" st]) subgoal unfolding g_def by (auto intro!:derivative_eq_intros) subgoal using ‹g st=0› . subgoal using ‹r>0› ‹sin st<0› by (simp add: mult_pos_neg) done then show ?thesis using ‹r>0› that by (simp add: sgn_mult) qed moreover have ?thesis when "cos st = -1" proof - have "g i > 0" when "st<i" "i<st+pi" for i proof - obtain k where k_def:"st = 2 * of_int k * pi+ pi" using ‹cos st = -1› by (metis cos_eq_minus1 distrib_left mult.commute mult.right_neutral) have "cos (i-st) < 1" using cos_monotone_0_pi[of 0 "i-st" ] that by auto moreover have "cos (i-st) = - cos i" apply (rule cos_eq_neg_periodic_intro[of _ _ "-k-1"]) unfolding k_def by (auto simp add:algebra_simps) ultimately have "cos i>-1" by auto then have "cos st<cos i" using ‹cos st=-1› by auto have "0 = r * cos st + Re z - Re z0" using ‹g st = 0› unfolding g_def by auto also have "... < r * cos i + Re z - Re z0" using ‹cos st < cos i› ‹r>0› by auto finally show ?thesis unfolding g_def by auto qed then show ?thesis unfolding has_sgnx_def eventually_at_right apply (intro exI[where x="st+pi"]) by auto qed ultimately show ?thesis using that(2) by auto qed have g_has_sgnx2:"(g has_sgnx -1) (at_right st)" when "g st=0" "sin st > 0 ∨ cos st=1" proof - have ?thesis when "sin st>0" proof - have "(g has_sgnx sgn (- r * sin st)) (at_right st)" apply (rule has_sgnx_derivative_at_right[of _ "- r * sin st"]) subgoal unfolding g_def by (auto intro!:derivative_eq_intros) subgoal using ‹g st=0› . subgoal using ‹r>0› ‹sin st>0› by (simp add: mult_pos_neg) done then show ?thesis using ‹r>0› that by (simp add: sgn_mult) qed moreover have ?thesis when "cos st=1" proof - have "g i < 0" when "st<i" "i<st+pi" for i proof - obtain k where k_def:"st = 2 * of_int k * pi" using ‹cos st=1› cos_one_2pi_int by auto have "cos (i-st) < 1" using cos_monotone_0_pi[of 0 "i-st" ] that by auto moreover have "cos (i-st) = cos i" apply (rule cos_eq_periodic_intro[of _ _ "-k"]) unfolding k_def by (auto simp add:algebra_simps) ultimately have "cos i<1" by auto then have "cos st>cos i" using ‹cos st=1› by auto have "0 = r * cos st + Re z - Re z0" using ‹g st = 0› unfolding g_def by auto also have "... > r * cos i + Re z - Re z0" using ‹cos st > cos i› ‹r>0› by auto finally show ?thesis unfolding g_def by auto qed then show ?thesis unfolding has_sgnx_def eventually_at_right apply (intro exI[where x="st+pi"]) by auto qed ultimately show ?thesis using that(2) by auto qed have ?thesis when "r * cos st + Re z - Re z0 ≠ 0" proof - have "g st ≠0" using that unfolding g_def by auto then have "continuous (at_right st) (λi. f i / g i)" unfolding f_def g_def by (auto intro!:continuous_intros) then have "jumpF (λi. f i/g i) (at_right st) = 0" using jumpF_not_infinity[of "at_right st" "(λi. f i/g i)"] by auto then show ?thesis using jumpF_eq that by auto qed moreover have ?thesis when "r * cos st + Re z - Re z0 = 0" "(sin st > 0 ∨ (cos st=1) ) ∧ f st < 0 ∨ (sin st < 0 ∨ (cos st=-1) ) ∧ f st > 0" proof - have "g st = 0" "f st≠0" and g_cont: "continuous (at_right st) g" and f_cont:"continuous (at_right st) f" using that unfolding g_def f_def by (auto intro!:continuous_intros) have "(g has_sgnx sgn (f st)) (at_right st)" using g_has_sgnx1[OF ‹g st=0›] g_has_sgnx2[OF ‹g st=0›] that(2) by auto then have "LIM x at_right st. f x / g x :> at_top" apply (subst filterlim_divide_at_bot_at_top_iff[of f "f st" "at_right st" g]) using ‹f st≠0› ‹g st = 0› g_cont f_cont by (auto simp add: continuous_within) then have "jumpF (λi. f i/g i) (at_right st) = 1/2" unfolding jumpF_def by auto then show ?thesis using jumpF_eq that unfolding f_def by auto qed moreover have ?thesis when "r * cos st + Re z - Re z0 = 0" "¬ ((sin st > 0 ∨ cos st=1 ) ∧ f st < 0 ∨ (sin st < 0 ∨ cos st=-1 ) ∧ f st > 0)" proof - define neq1 where "neq1 = (∀k::int. st ≠ 2*k*pi)" define neq2 where "neq2 = (∀k::int. st ≠ 2*k*pi+pi)" have "g st = 0" and g_cont: "continuous (at_right st) g" and f_cont:"continuous (at_right st) f" using that unfolding g_def f_def by (auto intro!:continuous_intros) have "f st≠0" proof (rule ccontr) assume "¬ f st ≠ 0" then have "f st = 0" by auto then have "Im (z0 - z) =r * sin st " "Re (z0 - z) = r * cos st" using ‹g st=0› unfolding f_def g_def by (auto simp add:algebra_simps) then have "cmod (z0 - z) = sqrt((r * sin st)^2 + (r * cos st)^2)" unfolding cmod_def by auto also have "... = sqrt (r^2 * ((sin st)^2 + (cos st)^2))" by (auto simp only:algebra_simps power_mult_distrib) also have "... = r" using ‹r>0› by simp finally have "cmod (z0 - z) = r" . then show False using ‹cmod (z-z0) ≠r› by (simp add: norm_minus_commute) qed have "(sin st > 0 ∨ (cos st=1) ) ∧ f st > 0 ∨ (sin st < 0 ∨ (cos st=-1) ) ∧ f st < 0" proof - have "sin st = 0 ⟷ cos st=-1 ∨ cos st=1" by (metis (no_types, hide_lams) add.right_neutral cancel_comm_monoid_add_class.diff_cancel cos_diff cos_zero mult_eq_0_iff power2_eq_1_iff power2_eq_square sin_squared_eq) moreover have "((sin st ≤ 0 ∧ cos st ≠1 ) ∨ f st > 0) ∧ ((sin st ≥ 0 ∧ cos st≠-1) ∨ f st < 0)" using that(2) ‹f st≠0› by argo ultimately show ?thesis by (meson linorder_neqE_linordered_idom not_le) qed then have "(g has_sgnx - sgn (f st)) (at_right st)" using g_has_sgnx1[OF ‹g st=0›] g_has_sgnx2[OF ‹g st=0›] by auto then have "LIM x at_right st. f x / g x :> at_bot" apply (subst filterlim_divide_at_bot_at_top_iff[of f "f st" "at_right st" g]) using ‹f st≠0› ‹g st = 0› g_cont f_cont by (auto simp add: continuous_within) then have "jumpF (λi. f i/g i) (at_right st) = -1/2" unfolding jumpF_def by auto then show ?thesis using jumpF_eq that unfolding f_def by auto qed ultimately show ?thesis by fast qed lemma jumpF_pathfinish_part_circlepath: assumes "st<tt" "r>0" "cmod (z-z0) ≠r" shows "jumpF_pathfinish (part_circlepath z r st tt) z0 = ( if r * cos tt + Re z - Re z0 = 0 then (let Δ = r* sin tt + Im z - Im z0 in if (sin tt > 0 ∨ cos tt=-1 ) ∧ Δ < 0 ∨ (sin tt < 0 ∨ cos tt=1 ) ∧ Δ > 0 then - 1/2 else 1/2) else 0)" proof - define f where "f=(λi. r * sin i + Im z - Im z0)" define g where "g=(λi. r * cos i + Re z - Re z0)" have jumpF_eq:"jumpF_pathfinish (part_circlepath z r st tt) z0 = jumpF (λi. f i/g i) (at_left tt)" proof - have "jumpF_pathfinish (part_circlepath z r st tt) z0 = jumpF ((λi. f i/g i) o linepath st tt) (at_left 1)" unfolding jumpF_pathfinish_def part_circlepath_def exp_Euler f_def g_def comp_def by (simp add:cos_of_real sin_of_real algebra_simps) also have "... = jumpF (λi. f i/g i) (at_left tt)" using jumpF_linear_comp(1)[of "tt-st" "(λi. f i/g i)" st 1,symmetric] ‹st<tt› unfolding linepath_def by (auto simp add:algebra_simps) finally show ?thesis . qed have g_has_sgnx1:"(g has_sgnx -1) (at_left tt)" when "g tt=0" "sin tt < 0 ∨ cos tt=1" proof - have ?thesis when "sin tt<0" proof - have "(g has_sgnx - sgn (- r * sin tt)) (at_left tt)" apply (rule has_sgnx_derivative_at_left[of _ "- r * sin tt"]) subgoal unfolding g_def by (auto intro!:derivative_eq_intros) subgoal using ‹g tt=0› . subgoal using ‹r>0› ‹sin tt<0› by (simp add: mult_pos_neg) done then show ?thesis using ‹r>0› that by (simp add: sgn_mult) qed moreover have ?thesis when "cos tt=1" proof - have "g i < 0" when "tt-pi<i" "i<tt" for i proof - obtain k where k_def:"tt = 2 * of_int k * pi" using ‹cos tt=1› cos_one_2pi_int by auto have "cos (i-tt) < 1" using cos_monotone_0_pi[of 0 "tt-i" ] that cos_minus[of "tt-i",simplified] by auto moreover have "cos (i-tt) = cos i" apply (rule cos_eq_periodic_intro[of _ _ "-k"]) unfolding k_def by (auto simp add:algebra_simps) ultimately have "cos i<1" by auto then have "cos tt>cos i" using ‹cos tt=1› by auto have "0 = r * cos tt + Re z - Re z0" using ‹g tt = 0› unfolding g_def by auto also have "... > r * cos i + Re z - Re z0" using ‹cos tt > cos i› ‹r>0› by auto finally show ?thesis unfolding g_def by auto qed then show ?thesis unfolding has_sgnx_def eventually_at_left apply (intro exI[where x="tt-pi"]) by auto qed ultimately show ?thesis using that(2) by auto qed have g_has_sgnx2:"(g has_sgnx 1) (at_left tt)" when "g tt=0" "sin tt > 0 ∨ cos tt=-1" proof - have ?thesis when "sin tt>0" proof - have "(g has_sgnx - sgn (- r * sin tt)) (at_left tt)" apply (rule has_sgnx_derivative_at_left[of _ "- r * sin tt"]) subgoal unfolding g_def by (auto intro!:derivative_eq_intros) subgoal using ‹g tt=0› . subgoal using ‹r>0› ‹sin tt>0› by (simp add: mult_pos_neg) done then show ?thesis using ‹r>0› that by (simp add: sgn_mult) qed moreover have ?thesis when "cos tt = -1" proof - have "g i > 0" when "tt-pi<i" "i<tt" for i proof - obtain k where k_def:"tt = 2 * of_int k * pi+ pi" using ‹cos tt = -1› by (metis cos_eq_minus1 distrib_left mult.commute mult.right_neutral) have "cos (i-tt) < 1" using cos_monotone_0_pi[of 0 "tt-i" ] that cos_minus[of "tt-i",simplified] by auto moreover have "cos (i-tt) = - cos i" apply (rule cos_eq_neg_periodic_intro[of _ _ "-k-1"]) unfolding k_def by (auto simp add:algebra_simps) ultimately have "cos i>-1" by auto then have "cos tt<cos i" using ‹cos tt=-1› by auto have "0 = r * cos tt + Re z - Re z0" using ‹g tt = 0› unfolding g_def by auto also have "... < r * cos i + Re z - Re z0" using ‹cos tt < cos i› ‹r>0› by auto finally show ?thesis unfolding g_def by auto qed then show ?thesis unfolding has_sgnx_def eventually_at_left apply (intro exI[where x="tt-pi"]) by auto qed ultimately show ?thesis using that(2) by auto qed have ?thesis when "r * cos tt + Re z - Re z0 ≠ 0" proof - have "g tt ≠0" using that unfolding g_def by auto then have "continuous (at_left tt) (λi. f i / g i)" unfolding f_def g_def by (auto intro!:continuous_intros) then have "jumpF (λi. f i/g i) (at_left tt) = 0" using jumpF_not_infinity[of "at_left tt" "(λi. f i/g i)"] by auto then show ?thesis using jumpF_eq that by auto qed moreover have ?thesis when "r * cos tt + Re z - Re z0 = 0" "(sin tt > 0 ∨ cos tt=-1 ) ∧ f tt < 0 ∨ (sin tt < 0 ∨ cos tt=1 ) ∧ f tt > 0" proof - have "g tt = 0" "f tt≠0" and g_cont: "continuous (at_left tt) g" and f_cont:"continuous (at_left tt) f" using that unfolding g_def f_def by (auto intro!:continuous_intros) have "(g has_sgnx - sgn (f tt)) (at_left tt)" using g_has_sgnx1[OF ‹g tt=0›] g_has_sgnx2[OF ‹g tt=0›] that(2) by auto then have "LIM x at_left tt. f x / g x :> at_bot" apply (subst filterlim_divide_at_bot_at_top_iff[of f "f tt" "at_left tt" g]) using ‹f tt≠0› ‹g tt = 0› g_cont f_cont by (auto simp add: continuous_within) then have "jumpF (λi. f i/g i) (at_left tt) = - 1/2" unfolding jumpF_def by auto then show ?thesis using jumpF_eq that unfolding f_def by auto qed moreover have ?thesis when "r * cos tt + Re z - Re z0 = 0" "¬ ((sin tt > 0 ∨ cos tt=-1 ) ∧ f tt < 0 ∨ (sin tt < 0 ∨ cos tt=1 ) ∧ f tt > 0)" proof - have "g tt = 0" and g_cont: "continuous (at_left tt) g" and f_cont:"continuous (at_left tt) f" using that unfolding g_def f_def by (auto intro!:continuous_intros) have "f tt≠0" proof (rule ccontr) assume "¬ f tt ≠ 0" then have "f tt = 0" by auto then have "Im (z0 - z) =r * sin tt " "Re (z0 - z) = r * cos tt" using ‹g tt=0› unfolding f_def g_def by (auto simp add:algebra_simps) then have "cmod (z0 - z) = sqrt((r * sin tt)^2 + (r * cos tt)^2)" unfolding cmod_def by auto also have "... = sqrt (r^2 * ((sin tt)^2 + (cos tt)^2))" by (auto simp only:algebra_simps power_mult_distrib) also have "... = r" using ‹r>0› by simp finally have "cmod (z0 - z) = r" . then show False using ‹cmod (z-z0) ≠r› by (simp add: norm_minus_commute) qed have "(sin tt > 0 ∨ cos tt=-1 ) ∧ f tt > 0 ∨ (sin tt < 0 ∨ cos tt=1 ) ∧ f tt < 0" proof - have "sin tt = 0 ⟷ cos tt=-1 ∨ cos tt=1" by (metis (no_types, hide_lams) add.right_neutral cancel_comm_monoid_add_class.diff_cancel cos_diff cos_zero mult_eq_0_iff power2_eq_1_iff power2_eq_square sin_squared_eq) moreover have "((sin tt ≤ 0 ∧ cos tt ≠-1 ) ∨ f tt > 0) ∧ ((sin tt ≥ 0 ∧ cos tt≠1) ∨ f tt < 0)" using that(2) ‹f tt≠0› by argo ultimately show ?thesis by (meson linorder_neqE_linordered_idom not_le) qed then have "(g has_sgnx sgn (f tt)) (at_left tt)" using g_has_sgnx1[OF ‹g tt=0›] g_has_sgnx2[OF ‹g tt=0›] by auto then have "LIM x at_left tt. f x / g x :> at_top" apply (subst filterlim_divide_at_bot_at_top_iff[of f "f tt" "at_left tt" g]) using ‹f tt≠0› ‹g tt = 0› g_cont f_cont by (auto simp add: continuous_within) then have "jumpF (λi. f i/g i) (at_left tt) = 1/2" unfolding jumpF_def by auto then show ?thesis using jumpF_eq that unfolding f_def by auto qed ultimately show ?thesis by fast qed lemma fixes z0 z::complex and r::real defines "upper ≡ cindex_pathE (part_circlepath z r 0 pi) z0" and "lower ≡ cindex_pathE (part_circlepath z r pi (2*pi)) z0" shows cindex_pathE_circlepath_upper: "⟦cmod (z0-z) < r⟧ ⟹ upper = -1" "⟦Im (z0-z) > r; ¦Re (z0 - z)¦ < r⟧ ⟹ upper = 1" "⟦Im (z0-z) < -r; ¦Re (z0 - z)¦ < r⟧ ⟹ upper = -1" "⟦¦Re (z0 - z)¦ > r; r>0⟧ ⟹ upper = 0" and cindex_pathE_circlepath_lower: "⟦cmod (z0-z) < r⟧ ⟹ lower = -1" "⟦Im (z0-z) > r; ¦Re (z0 - z)¦ < r⟧ ⟹ lower = -1" "⟦Im (z0-z) < -r; ¦Re (z0 - z)¦ < r⟧ ⟹ lower = 1" "⟦¦Re (z0 - z)¦ > r; r>0⟧ ⟹ lower = 0" proof - assume assms:"cmod (z0-z) < r" have zz_facts:"-r<Re z - Re z0" "Re z - Re z0<r" "r>0" subgoal using assms complex_Re_le_cmod le_less_trans by fastforce subgoal by (metis assms complex_Re_le_cmod le_less_trans minus_complex.simps(1) norm_minus_commute) subgoal using assms le_less_trans norm_ge_zero by blast done define θ where "θ = arccos ((Re z0 - Re z) / r)" have θ_bound:"0 < θ ∧ θ < pi" unfolding θ_def apply (rule arccos_lt_bounded) using zz_facts by (auto simp add:field_simps) have Im_sin:"abs (Im z0 - Im z) < r * sin θ" proof - define zz where "zz=z0-z" have "sqrt ((Re zz)⇧^{2}+ (Im zz)⇧^{2}) < r" using assms unfolding zz_def cmod_def . then have "(Re zz)⇧^{2}+ (Im zz)⇧^{2}< r^2" by (metis cmod_power2 dvd_refl linorder_not_le norm_complex_def power2_le_imp_le real_sqrt_power zero_le_power_eq_numeral) then have "(Im zz)⇧^{2}< r^2 - (Re zz)^2" by auto then have "abs (Im zz) < sqrt (r^2 - (Re zz)^2)" by (simp add: real_less_rsqrt) then show ?thesis unfolding θ_def zz_def apply (subst sin_arccos_abs) subgoal using zz_facts by auto subgoal using ‹r>0› by (auto simp add:field_simps divide_simps real_sqrt_divide) done qed show "upper = - 1" proof - have "jumpF_pathstart (part_circlepath z r 0 pi) z0 = 0" apply (subst jumpF_pathstart_part_circlepath) using zz_facts assms by (auto simp add: norm_minus_commute) moreover have "jumpF_pathfinish (part_circlepath z r 0 pi) z0 = 0" apply (subst jumpF_pathfinish_part_circlepath) using zz_facts assms by (auto simp add: norm_minus_commute) ultimately show ?thesis using assms zz_facts θ_bound Im_sin unfolding upper_def apply (subst cindex_pathE_part_circlepath) by (fold θ_def,auto simp add: norm_minus_commute) qed show "lower = - 1" proof - have "jumpF_pathstart (part_circlepath z r pi (2*pi)) z0 = 0" apply (subst jumpF_pathstart_part_circlepath) using zz_facts assms by (auto simp add: norm_minus_commute) moreover have "jumpF_pathfinish (part_circlepath z r pi (2*pi)) z0 = 0" apply (subst jumpF_pathfinish_part_circlepath) using zz_facts assms by (auto simp add: norm_minus_commute) ultimately show ?thesis using assms zz_facts θ_bound Im_sin unfolding lower_def apply (subst cindex_pathE_part_circlepath) by (fold θ_def,auto simp add: norm_minus_commute) qed next assume assms:"¦Re (z0 - z)¦ > r" "r>0" show "upper = 0" using assms unfolding upper_def apply (subst cindex_pathE_part_circlepath) apply auto by (metis abs_Re_le_cmod abs_minus_commute eucl_less_le_not_le minus_complex.simps(1)) show "lower = 0" using assms unfolding lower_def apply (subst cindex_pathE_part_circlepath) apply auto by (metis abs_Re_le_cmod abs_minus_commute eucl_less_le_not_le minus_complex.simps(1)) next assume assms:"¦Re (z0 - z)¦ < r" then have "r>0" by auto define θ where "θ = arccos ((Re z0 - Re z) / r)" have θ_bound:"0 < θ ∧ θ < pi" unfolding θ_def apply (rule arccos_lt_bounded) using assms by (auto simp add:field_simps) note norm_minus_commute[simp] have jumpFs: "jumpF_pathstart (part_circlepath z r 0 pi) z0 = 0" "jumpF_pathfinish (part_circlepath z r 0 pi) z0 = 0" "jumpF_pathstart (part_circlepath z r pi (2*pi)) z0 = 0" "jumpF_pathfinish (part_circlepath z r pi (2*pi)) z0 = 0" when "cmod (z0 - z) ≠ r" subgoal by (subst jumpF_pathstart_part_circlepath,use assms that in auto) subgoal by (subst jumpF_pathfinish_part_circlepath,use assms that in auto) subgoal by (subst jumpF_pathstart_part_circlepath,use assms that in auto) subgoal by (subst jumpF_pathfinish_part_circlepath,use assms that in auto) done show "upper = 1" "lower = -1" when "Im (z0-z) > r" proof - have "cmod (z0 - z) ≠ r" using that assms abs_Im_le_cmod abs_le_D1 not_le by blast moreover have "Im z0 - Im z > r * sin θ" proof - have "r * sin θ ≤ r" using ‹r>0› by auto also have "... < Im z0 - Im z" using that by auto finally show ?thesis . qed ultimately show "upper = 1" using assms jumpFs θ_bound that unfolding upper_def apply (subst cindex_pathE_part_circlepath) by (fold θ_def,auto) have "Im z - Im z0 < r * sin θ" proof - have "Im z - Im z0 <0" using that ‹r>0› by auto moreover have "r * sin θ>0" using ‹r>0› θ_bound by (simp add: sin_gt_zero) ultimately show ?thesis by auto qed then show "lower = -1" using ‹cmod (z0 - z) ≠ r› ‹Im z0 - Im z > r * sin θ› assms jumpFs θ_bound that unfolding lower_def apply (subst cindex_pathE_part_circlepath) by (fold θ_def,auto) qed show "upper = - 1" "lower = 1" when "Im (z0-z) < -r" proof - have "cmod (z0 - z) ≠ r" using that assms by (metis abs_Im_le_cmod abs_le_D1 minus_complex.simps(2) minus_diff_eq neg_less_iff_less norm_minus_cancel not_le) moreover have "Im z - Im z0 > r * sin θ" proof - have "r * sin θ ≤ r" using ‹r>0› by auto also have "... < Im z - Im z0" using that by auto finally show ?thesis . qed moreover have "Im z0 - Im z < r * sin θ" proof - have "Im z0 - Im z<0" using that ‹r>0› by auto moreover have "r * sin θ>0" using ‹r>0› θ_bound by (simp add: sin_gt_zero) ultimately show ?thesis by auto qed ultimately show "upper = - 1" using assms jumpFs θ_bound that unfolding upper_def apply (subst cindex_pathE_part_circlepath) by (fold θ_def,auto) show "lower = 1" using ‹Im z0 - Im z < r * sin θ› ‹Im z - Im z0 > r * sin θ› ‹cmod (z0 - z) ≠ r› assms jumpFs θ_bound that unfolding lower_def apply (subst cindex_pathE_part_circlepath) by (fold θ_def,auto) qed qed lemma jumpF_pathstart_linepath: "jumpF_pathstart (linepath a b) z = (if Re a = Re z ∧ Im a≠Im z ∧ Re b ≠ Re a then if (Im a>Im z ∧ Re b > Re a) ∨ (Im a<Im z ∧ Re b < Re a) then 1/2 else -1/2 else 0)" proof - define f where "f=(λt. (Im b - Im a )* t + (Im a - Im z))" define g where "g=(λt. (Re b - Re a )* t + (Re a - Re z))" have jump_eq:"jumpF_pathstart (linepath a b) z = jumpF (λt. f t/g t) (at_right 0)" unfolding jumpF_pathstart_def f_def linepath_def g_def by (auto simp add:algebra_simps) have ?thesis when "Re a≠Re z" proof - have "jumpF_pathstart (linepath a b) z = 0" unfolding jumpF_pathstart_def apply (rule jumpF_im_divide_Re_0) apply auto by (auto simp add:linepath_def that) then show ?thesis using that by auto qed moreover have ?thesis when "Re a=Re z" "Im a = Im z" proof - define c where "c=(Im b - Im a) / (Re b - Re a)" have "jumpF (λt. f t/g t) (at_right 0) = jumpF (λ_. c) (at_right 0)" proof (rule jumpF_cong) show "∀⇩_{F}x in at_right 0. f x / g x = c" unfolding eventually_at_right f_def g_def c_def using that apply (intro exI[where x=1]) by auto qed simp then show ?thesis using jump_eq that by auto qed moreover have ?thesis when "Re a=Re z" "Re b = Re a" proof - have "(λt. f t/g t) = (λ_. 0)" unfolding f_def g_def using that by auto then have "jumpF (λt. f t/g t) (at_right 0) = jumpF (λ_. 0) (at_right 0)" by auto then show ?thesis using jump_eq that by auto qed moreover have ?thesis when "Re a = Re z" "(Im a>Im z ∧ Re b > Re a) ∨ (Im a<Im z ∧ Re b < Re a)" proof - have "LIM x at_right 0. f x / g x :> at_top" apply (subst filterlim_divide_at_bot_at_top_iff[of _ "Im a - Im z"]) unfolding f_def g_def using that by (auto intro!:tendsto_eq_intros sgnx_eq_intros) then have "jumpF (λt. f t/g t) (at_right 0) = 1/2" unfolding jumpF_def by simp then show ?thesis using jump_eq that by auto qed moreover have ?thesis when "Re a = Re z" "Im a≠Im z" "Re b ≠ Re a" "¬ ((Im a>Im z ∧ Re b > Re a) ∨ (Im a<Im z ∧ Re b < Re a))" proof - have "(Im a>Im z ∧ Re b < Re a) ∨ (Im a<Im z ∧ Re b > Re a)" using that by argo then have "LIM x at_right 0. f x / g x :> at_bot" apply (subst filterlim_divide_at_bot_at_top_iff[of _ "Im a - Im z"]) unfolding f_def g_def using that by (auto intro!:tendsto_eq_intros sgnx_eq_intros) moreover then have "¬ (LIM x at_right 0. f x / g x :> at_top)" using filterlim_at_top_at_bot by fastforce ultimately have "jumpF (λt. f t/g t) (at_right 0) = - 1/2" unfolding jumpF_def by simp then show ?thesis using jump_eq that by auto qed ultimately show ?thesis by fast qed lemma jumpF_pathfinish_linepath: "jumpF_pathfinish (linepath a b) z = (if Re b = Re z ∧ Im b ≠Im z ∧ Re b ≠ Re a then if (Im b>Im z ∧ Re a > Re b) ∨ (Im b<Im z ∧ Re a < Re b) then 1/2 else -1/2 else 0)" proof - define f where "f=(λt. (Im b - Im a )* t + (Im a - Im z))" define g where "g=(λt. (Re b - Re a )* t + (Re a - Re z))" have jump_eq:"jumpF_pathfinish (linepath a b) z = jumpF (λt. f t/g t) (at_left 1)" unfolding jumpF_pathfinish_def f_def linepath_def g_def by (auto simp add:algebra_simps) have ?thesis when "Re b≠Re z" proof - have "jumpF_pathfinish (linepath a b) z = 0" unfolding jumpF_pathfinish_def apply (rule jumpF_im_divide_Re_0) apply auto by (auto simp add:linepath_def that) then show ?thesis using that by auto qed moreover have ?thesis when "Re z=Re b" "Im z = Im b" proof - define c where "c=(Im a - Im b) / (Re a - Re b)" have "jumpF (λt. f t/g t) (at_left 1) = jumpF (λ_. c) (at_left 1)" proof (rule jumpF_cong) have "f x / g x = c" when "x<1" for x proof - have "f x / g x = ((Im a - Im b)*(1-x))/((Re a - Re b)*(1-x))" unfolding f_def g_def by (auto simp add:algebra_simps ‹Re z=Re b› ‹Im z = Im b›) also have "... = c" using that unfolding c_def by auto finally show ?thesis . qed then show "∀⇩_{F}x in at_left 1. f x / g x = c" unfolding eventually_at_left using that apply (intro exI[where x=0]) by auto qed simp then show ?thesis using jump_eq that by auto qed moreover have ?thesis when "Re a=Re z" "Re b = Re a" proof - have "(λt. f t/g t) = (λ_. 0)" unfolding f_def g_def using that by auto then have "jumpF (λt. f t/g t) (at_left 1) = jumpF (λ_. 0) (at_left 1)" by auto then show ?thesis using jump_eq that by auto qed moreover have ?thesis when "Re b = Re z" "(Im b>Im z ∧ Re a > Re b) ∨ (Im b<Im z ∧ Re a < Re b)" proof - have "LIM x at_left 1. f x / g x :> at_top" proof - have "(g has_real_derivative Re b - Re a) (at 1)" unfolding g_def by (auto intro!:derivative_eq_intros) from has_sgnx_derivative_at_left[OF this] have "(g has_sgnx sgn (Im b - Im z)) (at_left 1)" using that unfolding g_def by auto then show ?thesis apply (subst filterlim_divide_at_bot_at_top_iff[of _ "Im b - Im z"]) unfolding f_def g_def using that by (auto intro!:tendsto_eq_intros) qed then have "jumpF (λt. f t/g t) (at_left 1) = 1/2" unfolding jumpF_def by simp then show ?thesis using jump_eq that by auto qed moreover have ?thesis when "Re b = Re z" "Im b≠Im z" "Re b ≠ Re a" "¬ ((Im b>Im z ∧ Re a > Re b) ∨ (Im b<Im z ∧ Re a < Re b))" proof - have "(Im b>Im z ∧ Re a < Re b) ∨ (Im b<Im z ∧ Re a > Re b)" using that by argo have "LIM x at_left 1. f x / g x :> at_bot" proof - have "(g has_real_derivative Re b - Re a) (at 1)" unfolding g_def by (auto intro!:derivative_eq_intros) from has_sgnx_derivative_at_left[OF this] have "(g has_sgnx - sgn (Im b - Im z)) (at_left 1)" using that unfolding g_def by auto then show ?thesis apply (subst filterlim_divide_at_bot_at_top_iff[of _ "Im b - Im z"]) unfolding f_def g_def using that by (auto intro!:tendsto_eq_intros ) qed moreover then have "¬ (LIM x at_left 1. f x / g x :> at_top)" using filterlim_at_top_at_bot by fastforce ultimately have "jumpF (λt. f t/g t) (at_left 1) = - 1/2" unfolding jumpF_def by simp then show ?thesis using jump_eq that by auto qed ultimately show ?thesis by argo qed subsection ‹Setting up the method for evaluating winding numbers› lemma pathfinish_pathstart_partcirclepath_simps: "pathstart (part_circlepath z0 r (3*pi/2) tt) = z0 - Complex 0 r" "pathstart (part_circlepath z0 r (2*pi) tt) = z0 + r" "pathfinish (part_circlepath z0 r st (3*pi/2)) = z0 - Complex 0 r" "pathfinish (part_circlepath z0 r st (2*pi)) = z0 + r" "pathstart (part_circlepath z0 r 0 tt) = z0 + r" "pathstart (part_circlepath z0 r (pi/2) tt) = z0 + Complex 0 r" "pathstart (part_circlepath z0 r (pi) tt) = z0 - r" "pathfinish (part_circlepath z0 r st 0) = z0+r" "pathfinish (part_circlepath z0 r st (pi/2)) = z0 + Complex 0 r" "pathfinish (part_circlepath z0 r st (pi)) = z0 - r" unfolding part_circlepath_def linepath_def pathstart_def pathfinish_def exp_Euler subgoal apply(simp, subst sin.minus_1[symmetric],subst cos.minus_1[symmetric]) by (simp add: complex_of_real_i) subgoal by (simp, subst sin.minus_1[symmetric],subst cos.minus_1[symmetric],auto) subgoal apply (simp, subst sin.minus_1[symmetric],subst cos.minus_1[symmetric]) by (simp add: complex_of_real_i) subgoal by (simp, subst sin.minus_1[symmetric],subst cos.minus_1[symmetric],auto) by (simp_all add: complex_of_real_i) lemma winding_eq_intro: "finite_ReZ_segments g z ⟹ valid_path g ⟹ z ∉ path_image g ⟹ pathfinish g = pathstart g ⟹ - of_real(cindex_pathE g z) =2*n ⟹ winding_number g z = (n::complex)" apply (subst winding_number_cindex_pathE[of g z]) by (auto simp add:field_simps) named_theorems winding_intros and winding_simps lemmas [winding_intros] = finite_ReZ_segments_joinpaths valid_path_join path_join_imp not_in_path_image_join lemmas [winding_simps] = finite_ReZ_segments_linepath finite_ReZ_segments_part_circlepath jumpF_pathfinish_joinpaths jumpF_pathstart_joinpaths pathfinish_linepath pathstart_linepath pathfinish_join pathstart_join valid_path_linepath valid_path_part_circlepath path_part_circlepath Re_complex_of_real Im_complex_of_real of_real_linepath pathfinish_pathstart_partcirclepath_simps method rep_subst = (subst cindex_pathE_joinpaths; rep_subst)? text ‹ The method "eval\_winding" @{term 1} will try to simplify of the form @{term "winding_number g z = n"} where @{term n} is an integer and @{term g} is a closed path comprised of @{term linepath}, @{term part_circlepath} and @{term joinpaths}. Suppose @{term "g=l1+++l2"}, usually, the key behind the success of this framework is whether we can prove @{term "z ∉ path_image l1"}, @{term "z ∉ path_image l2"} and calculate @{term "cindex_pathE l1 z"} and @{term "cindex_pathE l2 z"}. › method eval_winding = ((rule_tac winding_eq_intro; rep_subst ) , auto simp only:winding_simps del:notI intro!:winding_intros , tactic ‹distinct_subgoals_tac›) end