Quelle  Winding_Numbers.thy

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 * i * 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*i) * 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🚫›
        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🚫›)
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 * i * 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 * i * winding_number γ z"
    using q by (auto simp: winding_number_prop_def)
  finally have "2 * complex_of_real pi * i * n = 2 * complex_of_real pi * i * 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 * i * 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) * i * - 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 * i * 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 * i * 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 * i * 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 * i * winding_number γ z"
    using q by (auto simp: winding_number_prop_def)
  finally have "2 * complex_of_real pi * i * n = 2 * complex_of_real pi * i * 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*i) * 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*i*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 🚫› γ1 winding_number by blast
    moreover
    obtain p2 where "winding_number_prop γ2 z e p2 (winding_number γ2 z)"
      using ‹0 🚫› γ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 🚫› 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 * i * winding_number γ z"
    if "e > 0" for e
  proof -
    obtain p where "winding_number_prop γ z e p (winding_number γ z)"
      using ‹0 🚫› 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_offset_NO_MATCH: 
  "NO_MATCH 0 z ==> winding_number p z = winding_number (λw. p w - z) 0"
  using winding_number_offset by metis

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) * i * 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) * i * 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 i, 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 i "λx. i*e" "i*e" "{0..1}", simplified])
    have "((λa. 1 / (a - z)) has_contour_integral contour_integral γ (λw. 1 / (w - z))) γ"
      thm has_integral_component_le [of i "λx. i*e" "i*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 i * 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 i * 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<..
    using ‹finite k› by (simp add: finite_imp_closed open_Diff)
  moreover have "{a<..⊆ {a..b} - k"
    by force
  ultimately have g_diff_at: "∧x. [x ∉ k; x ∈ {a<..] ==> γ 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 * i * 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) * i * 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 (i * 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) * i * 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) * i * 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 🚫› 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) * i * 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 🚫›
      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 🚫› 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_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 δ = "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
      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 * i) * ?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 * i) * ?f x = winding_number (subpath 0 x γ) z"
    if x: "x ∈ {0..1}" for x
  proof -
    have "1 / (2*pi*i) * ?f x = 1 / (2*pi*i) * 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 γ" and z: "z ∉ path_image γ" and "Re(winding_number γ z) ≤ w" "w ≤ 0"
      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_decreasing_component_on_1[of 0 1, where ?k = "1"] by force
qed

lemma winding_number_ivt_abs:
    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"
  using assms winding_number_ivt_pos [of γ z w] winding_number_ivt_neg [of γ z "-w"]
  by force

lemma winding_number_lt_half_lemma:
  assumes γ: "valid_path γ" and z: "z ∉ path_image γ" and az: "a ∙ z ≤ b" and pag: "path_image γ ⊆ {w. a ∙ w > b}"
    shows "Re(winding_number γ z) < 1/2"
proof -
  { assume "Re(winding_number γ z) ≥ 1/2"
    then obtain t::real where t: "0 ≤ t" "t ≤ 1" and sub12: "Re (winding_number (subpath 0 t γ) z) = 1/2"
      using winding_number_ivt_pos [OF γ z, of "1/2"] by auto
    have gt: "γ t - z = - (of_real (exp (- (2 * pi * Im (winding_number (subpath 0 t γ) z)))) * (γ 0 - z))"
      using winding_number_exp_2pi [of "subpath 0 t γ" z]
      apply (simp add: t γ valid_path_imp_path)
      using closed_segment_eq_real_ivl path_image_def t z by (fastforce simp: path_image_subpath Euler sub12)
    have "b < a ∙ γ 0"
    proof -
      have "γ 0 ∈ {c. b < a ∙ c}"
        by (metis (no_types) pag atLeastAtMost_iff image_subset_iff order_refl path_image_def zero_le_one)
      thus ?thesis
        by blast
    qed
    moreover have "b < a ∙ γ t"
      by (metis atLeastAtMost_iff image_eqI mem_Collect_eq pag path_image_def subset_iff t)
    ultimately have "0 < a ∙ (γ 0 - z)" "0 < a ∙ (γ t - z)" using az
      by (simp add: inner_diff_right)+
    then have False
      by (simp add: gt inner_mult_right mult_less_0_iff)
  }
  then show ?thesis by force
qed

lemma winding_number_lt_half:
  assumes "valid_path γ" "a ∙ z ≤ b" "path_image γ ⊆ {w. a ∙ w > b}"
    shows "∣Re (winding_number γ z)∣ < 1/2"
proof -
  have "z ∉ path_image γ" using assms by auto
  with assms have "Re (winding_number γ z) < 0 ==> - Re (winding_number γ z) < 1/2"
    by (metis complex_inner_1_right winding_number_lt_half_lemma [OF valid_path_imp_reverse, of γ z a b]
        winding_number_reversepath valid_path_imp_path inner_minus_left path_image_reversepath)
  with assms show ?thesis
    using ‹z ∉ path_image γ› winding_number_lt_half_lemma by fastforce
qed

lemma winding_number_le_half:
  assumes γ: "valid_path γ" and z: "z ∉ path_image γ"
      and anz: "a ≠ 0" and azb: "a ∙ z ≤ b" and pag: "path_image γ ⊆ {w. a ∙ w ≥ b}"
    shows "∣Re (winding_number γ z)∣ ≤ 1/2"
proof -
  { assume wnz_12: "∣Re (winding_number γ z)∣ > 1/2"
    have "isCont (winding_number γ) z"
      by (metis continuous_at_winding_number valid_path_imp_path γ z)
    then obtain d where "d>0" and d: "∧x'. dist x' z < d ==> dist (winding_number γ x') (winding_number γ z) < ∣Re(winding_number γ z)∣ - 1/2"
      using continuous_at_eps_delta wnz_12 diff_gt_0_iff_gt by blast
    define z' where "z' = z - (d / (2 * cmod a)) *🪙R a"
    have "a ∙ z * 6 ≤ d * cmod a + b * 6"
      by (metis ‹0 🚫› add_increasing azb less_eq_real_def mult_nonneg_nonneg mult_right_mono norm_ge_zero norm_numeral)
    with anz have *: "a ∙ z' ≤ b - d / 3 * cmod a"
      unfolding z'_def inner_mult_right' divide_inverse
      by (simp add: field_split_simps algebra_simps dot_square_norm power2_eq_square)
    have "cmod (winding_number γ z' - winding_number γ z) < ∣Re (winding_number γ z)∣ - 1/2"
      using d [of z'] anz ‹d>0› by (simp add: dist_norm z'_def)
    then have "1/2 < ∣Re (winding_number γ z)∣ - cmod (winding_number γ z' - winding_number γ z)"
      by simp
    then have "1/2 < ∣Re (winding_number γ z)∣ - ∣Re (winding_number γ z') - Re (winding_number γ z)∣"
      using abs_Re_le_cmod [of "winding_number γ z' - winding_number γ z"] by simp
    then have wnz_12': "∣Re (winding_number γ z')∣ > 1/2"
      by linarith
    moreover have "∣Re (winding_number γ z')∣ < 1/2"
    proof (rule winding_number_lt_half [OF γ *])
      show "path_image γ ⊆ {w. b - d / 3 * cmod a < a ∙ w}"
        using azb ‹d>0› pag by (auto simp: add_strict_increasing anz field_split_simps dest!: subsetD)
    qed
    ultimately have False
      by simp
  }
  then show ?thesis by force
qed

lemma winding_number_lt_half_linepath:
  assumes "z ∉ closed_segment a b" shows "∣Re (winding_number (linepath a b) z)∣ < 1/2"
proof -
  obtain u v where "u ∙ z ≤ v" and uv: "∧x. x ∈ closed_segment a b ==> inner u x > v"
    using separating_hyperplane_closed_point assms closed_segment convex_closed_segment less_eq_real_def by metis
  moreover have "path_image (linepath a b) ⊆ {w. v < u ∙ w}"
    using in_segment(1) uv by auto
  ultimately show ?thesis
    using winding_number_lt_half by auto
qed

text‹ Positivity of WN for a linepath.›
lemma winding_number_linepath_pos_lt:
    assumes "0 < Im ((b - a) * cnj (b - z))"
      shows "0 < Re(winding_number(linepath a b) z)"
proof -
  have z: "z ∉ path_image (linepath a b)"
    using assms
    by (simp add: closed_segment_def) (force simp: algebra_simps)
  show ?thesis
    by (intro winding_number_pos_lt [OF valid_path_linepath z assms]) (simp add: linepath_def algebra_simps)
qed

lemma winding_number_linepath_neg_lt:
    assumes "0 < Im ((a - b) * cnj (a - z))"
      shows "Re(winding_number(linepath a b) z) < 0"
proof -
  have z: "z ∉ path_image (linepath a b)"
    using assms
    by (simp add: closed_segment_def) (force simp: algebra_simps)
  have "Re(winding_number(linepath a b) z) =
          -Re(winding_number(reversepath (linepath a b)) z)"
    by (subst winding_number_reversepath) (use z in auto)
  also have "… = - Re(winding_number(linepath b a) z)"
    by simp
  finally have "Re (winding_number (linepath a b) z)
      = - Re (winding_number (linepath b a) z)" .
  moreover have "0 < Re (winding_number (linepath b a) z)"
    using winding_number_linepath_pos_lt[OF assms] .
  ultimately show ?thesis by auto
qed


subsection🍋‹tag unimportant› ‹More winding number properties›

text‹including the fact that it's +-1 inside a simple closed curve.›

lemma winding_number_homotopic_paths:
    assumes "homotopic_paths (-{z}) g h"
      shows "winding_number g z = winding_number h z"
proof -
  have "path g" "path h" using homotopic_paths_imp_path [OF assms] by auto
  moreover have pag: "z ∉ path_image g" and pah: "z ∉ path_image h"
    using homotopic_paths_imp_subset [OF assms] by auto
  ultimately obtain d e where "d > 0" "e > 0"
      and d: "∧p. [path p; pathstart p = pathstart g; pathfinish p = pathfinish g; ∀t∈{0..1}. norm (p t - g t) < d]
            ==> homotopic_paths (-{z}) g p"
      and e: "∧q. [path q; pathstart q = pathstart h; pathfinish q = pathfinish h; ∀t∈{0..1}. norm (q t - h t) < e]
            ==> homotopic_paths (-{z}) h q"
    using homotopic_nearby_paths [of g "-{z}"] homotopic_nearby_paths [of h "-{z}"] by force
  obtain p where p:
       "valid_path p" "z ∉ path_image p"
       "pathstart p = pathstart g" "pathfinish p = pathfinish g"
       and gp_less:"∀t∈{0..1}. cmod (g t - p t) < d"
       and pap: "contour_integral p (λw. 1 / (w - z)) = complex_of_real (2 * pi) * i * winding_number g z"
    using winding_number [OF ‹path g› pag ‹0 🚫›] unfolding winding_number_prop_def by blast
  obtain q where q:
       "valid_path q" "z ∉ path_image q"
       "pathstart q = pathstart h" "pathfinish q = pathfinish h"
       and hq_less: "∀t∈{0..1}. cmod (h t - q t) < e"
       and paq:  "contour_integral q (λw. 1 / (w - z)) = complex_of_real (2 * pi) * i * winding_number h z"
    using winding_number [OF ‹path h› pah ‹0 🚫›] unfolding winding_number_prop_def by blast
  have "homotopic_paths (- {z}) g p"
    by (simp add: d p valid_path_imp_path norm_minus_commute gp_less)
  moreover have "homotopic_paths (- {z}) h q"
    by (simp add: e q valid_path_imp_path norm_minus_commute hq_less)
  ultimately have "homotopic_paths (- {z}) p q"
    by (blast intro: homotopic_paths_trans homotopic_paths_sym assms)
  then have "contour_integral p (λw. 1/(w - z)) = contour_integral q (λw. 1/(w - z))"
    by (rule Cauchy_theorem_homotopic_paths) (auto intro!: holomorphic_intros simp: p q)
  then show ?thesis
    by (simp add: pap paq)
qed

lemma winding_number_homotopic_loops:
    assumes "homotopic_loops (-{z}) g h"
      shows "winding_number g z = winding_number h z"
proof -
  have "path g" "path h" using homotopic_loops_imp_path [OF assms] by auto
  moreover have pag: "z ∉ path_image g" and pah: "z ∉ path_image h"
    using homotopic_loops_imp_subset [OF assms] by auto
  moreover have gloop: "pathfinish g = pathstart g" and hloop: "pathfinish h = pathstart h"
    using homotopic_loops_imp_loop [OF assms] by auto
  ultimately obtain d e where "d > 0" "e > 0"
      and d: "∧p. [path p; pathfinish p = pathstart p; ∀t∈{0..1}. norm (p t - g t) < d]
            ==> homotopic_loops (-{z}) g p"
      and e: "∧q. [path q; pathfinish q = pathstart q; ∀t∈{0..1}. norm (q t - h t) < e]
            ==> homotopic_loops (-{z}) h q"
    using homotopic_nearby_loops [of g "-{z}"] homotopic_nearby_loops [of h "-{z}"] by force
  obtain p where p:
       "valid_path p" "z ∉ path_image p"
       "pathstart p = pathstart g" "pathfinish p = pathfinish g"
       and gp_less:"∀t∈{0..1}. cmod (g t - p t) < d"
       and pap: "contour_integral p (λw. 1 / (w - z)) = complex_of_real (2 * pi) * i * winding_number g z"
    using winding_number [OF ‹path g› pag ‹0 🚫›] unfolding winding_number_prop_def by blast
  obtain q where q:
       "valid_path q" "z ∉ path_image q"
       "pathstart q = pathstart h" "pathfinish q = pathfinish h"
       and hq_less: "∀t∈{0..1}. cmod (h t - q t) < e"
       and paq:  "contour_integral q (λw. 1 / (w - z)) = complex_of_real (2 * pi) * i * winding_number h z"
    using winding_number [OF ‹path h› pah ‹0 🚫›] unfolding winding_number_prop_def by blast
  have gp: "homotopic_loops (- {z}) g p"
    by (simp add: gloop d gp_less norm_minus_commute p valid_path_imp_path)
  have hq: "homotopic_loops (- {z}) h q"
    by (simp add: e hloop hq_less norm_minus_commute q valid_path_imp_path)
  have "contour_integral p (λw. 1/(w - z)) = contour_integral q (λw. 1/(w - z))"
  proof (rule Cauchy_theorem_homotopic_loops)
    show "homotopic_loops (- {z}) p q"
      by (blast intro: homotopic_loops_trans homotopic_loops_sym gp hq assms)
  qed (auto intro!: holomorphic_intros simp: p q)
  then show ?thesis
    by (simp add: pap paq)
qed

lemma winding_number_paths_linear_eq:
  "[path g; path h; pathstart h = pathstart g; pathfinish h = pathfinish g;
    ∧t. t ∈ {0..1} ==> z ∉ closed_segment (g t) (h t)]
        ==> winding_number h z = winding_number g z"
  by (blast intro: sym homotopic_paths_linear winding_number_homotopic_paths)

lemma winding_number_loops_linear_eq:
  "[path g; path h; pathfinish g = pathstart g; pathfinish h = pathstart h;
    ∧t. t ∈ {0..1} ==> z ∉ closed_segment (g t) (h t)]
        ==> winding_number h z = winding_number g z"
  by (blast intro: sym homotopic_loops_linear winding_number_homotopic_loops)

lemma winding_number_nearby_paths_eq:
     "[path g; path h; pathstart h = pathstart g; pathfinish h = pathfinish g;
      ∧t. t ∈ {0..1} ==> norm(h t - g t) < norm(g t - z)]
      ==> winding_number h z = winding_number g z"
  by (metis segment_bound(2) norm_minus_commute not_le winding_number_paths_linear_eq)

lemma winding_number_nearby_loops_eq:
     "[path g; path h; pathfinish g = pathstart g; pathfinish h = pathstart h;
      ∧t. t ∈ {0..1} ==> norm(h t - g t) < norm(g t - z)]
      ==> winding_number h z = winding_number g z"
  by (metis segment_bound(2) norm_minus_commute not_le winding_number_loops_linear_eq)


lemma winding_number_subpath_combine:
  assumes "path g" and notin: "z ∉ path_image g" and "u ∈ {0..1}" "v ∈ {0..1}" "w ∈ {0..1}"
  shows "winding_number (subpath u v g) z + winding_number (subpath v w g) z =
         winding_number (subpath u w g) z" (is "?lhs = ?rhs")
proof -
  have "?lhs = winding_number (subpath u v g +++ subpath v w g) z"
    using assms
    by (metis (no_types, lifting) path_image_subpath_subset path_subpath pathfinish_subpath pathstart_subpath subsetD winding_number_join)
  also have "... = ?rhs"
    by (meson assms homotopic_join_subpaths subset_Compl_singleton winding_number_homotopic_paths)
  finally show ?thesis .
qed

text ‹Winding numbers of circular contours›

proposition winding_number_part_circlepath_pos_less:
  assumes "s < t" and no: "norm(w - z) < r"
    shows "0 < Re (winding_number(part_circlepath z r s t) w)"
proof -
  have "0 < r" by (meson no norm_not_less_zero not_le order.strict_trans2)
  note valid_path_part_circlepath
  moreover have " w ∉ path_image (part_circlepath z r s t)"
    using assms by (auto simp: path_image_def image_def part_circlepath_def norm_mult linepath_def)
  moreover have "0 < r * (t - s) * (r - cmod (w - z))"
    using assms by (metis ‹0 🚫› diff_gt_0_iff_gt mult_pos_pos)
  ultimately show ?thesis
    apply (rule winding_number_pos_lt [where e = "r*(t - s)*(r - norm(w - z))"])
    apply (simp add: vector_derivative_part_circlepath right_diff_distrib [symmetric] mult_ac mult_le_cancel_left_pos assms ‹0🚫›)
    using Re_Im_le_cmod [of "w-z" "linepath s t x" for x]
    by (simp add: exp_Euler cos_of_real sin_of_real part_circlepath_def algebra_simps cos_squared_eq [unfolded power2_eq_square])
qed

lemma winding_number_circlepath_centre: "0 < r ==> winding_number (circlepath z r) z = 1"
  apply (rule winding_number_unique_loop)
  apply (simp_all add: sphere_def valid_path_imp_path)
  apply (rule_tac x="circlepath z r" in exI)
  apply (simp add: sphere_def contour_integral_circlepath)
  done

proposition winding_number_circlepath:
  assumes "norm(w - z) < r" shows "winding_number(circlepath z r) w = 1"
proof (cases "w = z")
  case True then show ?thesis
    using assms winding_number_circlepath_centre by auto
next
  case False
  have [simp]: "r > 0"
    using assms le_less_trans norm_ge_zero by blast
  define r' where "r' = norm(w - z)"
  have "r' < r"
    by (simp add: assms r'_def)
  have disjo: "cball z r' ∩ sphere z r = {}"
    using ‹r' 🚫› by (force simp: cball_def sphere_def)
  have "winding_number(circlepath z r) w = winding_number(circlepath z r) z"
  proof (rule winding_number_around_inside [where S = "cball z r'"])
    show "winding_number (circlepath z r) z ≠ 0"
      by (simp add: winding_number_circlepath_centre)
    show "cball z r' ∩ path_image (circlepath z r) = {}"
      by (simp add: disjo less_eq_real_def)
  qed (auto simp: r'_def dist_norm norm_minus_commute)
  also have "… = 1"
    by (simp add: winding_number_circlepath_centre)
  finally show ?thesis .
qed

lemma no_bounded_connected_component_imp_winding_number_zero:
  assumes g: "path g" "path_image g ⊆ S" "pathfinish g = pathstart g" "z ∉ S"
      and nb: "∧z. bounded (connected_component_set (- S) z) ==> z ∈ S"
    shows "winding_number g z = 0"
proof -
  have "z ∈ outside (path_image g)"
    by (metis nb [of z] ‹path_image g ⊆ S› ‹z ∉ S› subsetD mem_Collect_eq outside outside_mono)
  then show ?thesis
    by (simp add: g winding_number_zero_in_outside)
qed

lemma no_bounded_path_component_imp_winding_number_zero:
  assumes g: "path g" "path_image g ⊆ S" "pathfinish g = pathstart g" "z ∉ S"
      and nb: "∧z. bounded (path_component_set (- S) z) ==> z ∈ S"
  shows "winding_number g z = 0"
  by (simp add: bounded_subset nb path_component_subset_connected_component 
                no_bounded_connected_component_imp_winding_number_zero [OF g])

subsection‹Winding number for a triangle›

lemma wn_triangle1:
  assumes "0 ∈ interior(convex hull {a,b,c})"
    shows "¬ (Im(a/b) ≤ 0 ∧ 0 ≤ Im(b/c))"
proof -
  { assume 0: "Im(a/b) ≤ 0" "0 ≤ Im(b/c)"
    have "0 ∉ interior (convex hull {a,b,c})"
    proof (cases "a=0 ∨ b=0 ∨ c=0")
      case True then show ?thesis
        by (auto simp: not_in_interior_convex_hull_3)
    next
      case False
      then have "b ≠ 0" by blast
      { fix x y::complex and u::real
        assume eq_f': "Im x * Re b ≤ Im b * Re x" "Im y * Re b ≤ Im b * Re y" "0 ≤ u" "u ≤ 1"
        then have "((1 - u) * Im x) * Re b ≤ Im b * ((1 - u) * Re x)"
          by (simp add: mult_left_mono mult.assoc mult.left_commute [of "Im b"])
        then have "((1 - u) * Im x + u * Im y) * Re b ≤ Im b * ((1 - u) * Re x + u * Re y)"
          using eq_f' ordered_comm_semiring_class.comm_mult_left_mono
          by (fastforce simp add: algebra_simps)
      }
      then have "convex {z. Im z * Re b ≤ Im b * Re z}"
        by (auto simp: algebra_simps convex_alt)
      with False 0 have "convex hull {a,b,c} ≤ {z. Im z * Re b ≤ Im b * Re z}"
        by (simp add: subset_hull mult.commute Complex.Im_divide divide_simps complex_neq_0 [symmetric])
      moreover have "0 ∉ interior({z. Im z * Re b ≤ Im b * Re z})"
      proof
        assume "0 ∈ interior {z. Im z * Re b ≤ Im b * Re z}"
        then obtain e where "e>0" and e: "ball 0 e ⊆ {z. Im z * Re b ≤ Im b * Re z}"
          by (meson mem_interior)
        define z where "z ≡ - sgn (Im b) * (e/3) + sgn (Re b) * (e/3) * i"
        have "cmod z = cmod (e/3) * cmod (- sgn (Im b) + sgn (Re b) * i)"
          unfolding z_def norm_mult [symmetric] by (simp add: algebra_simps)
        also have "... < e"
          using ‹e>0› by (auto simp: norm_mult intro: le_less_trans [OF norm_triangle_ineq4])
        finally have "z ∈ ball 0 e"
          using ‹e>0› by simp
        then have "Im z * Re b ≤ Im b * Re z"
          using e by blast
        then have b: "0 < Re b" "0 < Im b" and disj: "e * Re b < - (Im b * e) ∨ e * Re b = - (Im b * e)"
          using ‹e>0› ‹b ≠ 0›
          by (auto simp add: z_def dist_norm sgn_if less_eq_real_def mult_less_0_iff complex.expand split: if_split_asm)
        show False 🍋‹or just one smt line›
          using disj
        proof
          assume "e * Re b < - (Im b * e)"
          with b ‹0 🚫› less_trans [of _ 0] show False
            by (metis (no_types) mult_pos_pos neg_less_0_iff_less not_less_iff_gr_or_eq)
        next
          assume "e * Re b = - (Im b * e)"
          with b ‹0 🚫› show False
            by (metis mult_pos_pos neg_less_0_iff_less not_less_iff_gr_or_eq) 
        qed
      qed
      ultimately show ?thesis
        using interior_mono by blast
    qed
  } with assms show ?thesis by blast
qed

lemma wn_triangle2_0:
  assumes "0 ∈ interior(convex hull {a,b,c})"
  shows
       "0 < Im((b - a) * cnj (b)) ∧
        0 < Im((c - b) * cnj (c)) ∧
        0 < Im((a - c) * cnj (a))
        ∨
        Im((b - a) * cnj (b)) < 0 ∧
        0 < Im((b - c) * cnj (b)) ∧
        0 < Im((a - b) * cnj (a)) ∧
        0 < Im((c - a) * cnj (c))"
proof -
  have [simp]: "{b,c,a} = {a,b,c}" "{c,a,b} = {a,b,c}" by auto
  show ?thesis
    using wn_triangle1 [OF assms] wn_triangle1 [of b c a] wn_triangle1 [of c a b] assms
    by (auto simp: algebra_simps Im_complex_div_gt_0 Im_complex_div_lt_0 not_le not_less)
qed

lemma wn_triangle2:
  assumes "z ∈ interior(convex hull {a,b,c})"
   shows "0 < Im((b - a) * cnj (b - z)) ∧
          0 < Im((c - b) * cnj (c - z)) ∧
          0 < Im((a - c) * cnj (a - z))
          ∨
          Im((b - a) * cnj (b - z)) < 0 ∧
          0 < Im((b - c) * cnj (b - z)) ∧
          0 < Im((a - b) * cnj (a - z)) ∧
          0 < Im((c - a) * cnj (c - z))"
proof -
  have 0: "0 ∈ interior(convex hull {a-z, b-z, c-z})"
    using assms convex_hull_translation [of "-z" "{a,b,c}"]
                interior_translation [of "-z"]
    by (simp cong: image_cong_simp)
  show ?thesis using wn_triangle2_0 [OF 0]
    by simp
qed

lemma wn_triangle3:
  assumes z: "z ∈ interior(convex hull {a,b,c})"
      and "0 < Im((b-a) * cnj (b-z))"
          "0 < Im((c-b) * cnj (c-z))"
          "0 < Im((a-c) * cnj (a-z))"
    shows "winding_number (linepath a b +++ linepath b c +++ linepath c a) z = 1"
proof -
  have znot[simp]: "z ∉ closed_segment a b" "z ∉ closed_segment b c" "z ∉ closed_segment c a"
    using z interior_of_triangle [of a b c]
    by (auto simp: closed_segment_def)
  have gt0: "0 < Re (winding_number (linepath a b +++ linepath b c +++ linepath c a) z)"
    using assms
    by (simp add: winding_number_linepath_pos_lt path_image_join winding_number_join_pos_combined)
  have lt2: "Re (winding_number (linepath a b +++ linepath b c +++ linepath c a) z) < 2"
    using winding_number_lt_half_linepath [of _ a b]
    using winding_number_lt_half_linepath [of _ b c]
    using winding_number_lt_half_linepath [of _ c a] znot
    by (fastforce simp add: winding_number_join path_image_join)
  show ?thesis
    by (rule winding_number_eq_1) (simp_all add: path_image_join gt0 lt2)
qed

proposition winding_number_triangle:
  assumes z: "z ∈ interior(convex hull {a,b,c})"
    shows "winding_number(linepath a b +++ linepath b c +++ linepath c a) z =
           (if 0 < Im((b - a) * cnj (b - z)) then 1 else -1)"
proof -
  have [simp]: "{a,c,b} = {a,b,c}"  by auto
  have znot[simp]: "z ∉ closed_segment a b" "z ∉ closed_segment b c" "z ∉ closed_segment c a"
    using z interior_of_triangle [of a b c]
    by (auto simp: closed_segment_def)
  then have [simp]: "z ∉ closed_segment b a" "z ∉ closed_segment c b" "z ∉ closed_segment a c"
    using closed_segment_commute by blast+
  have *: "winding_number (linepath a b +++ linepath b c +++ linepath c a) z =
            winding_number (reversepath (linepath a c +++ linepath c b +++ linepath b a)) z"
    by (simp add: reversepath_joinpaths winding_number_join not_in_path_image_join)
  show ?thesis
    apply (rule disjE [OF wn_triangle2 [OF z]])
    subgoal
      by (simp add: wn_triangle3 z)
    subgoal
      by (simp add: path_image_join winding_number_reversepath * wn_triangle3 z)
    done
qed

subsection‹Winding numbers for simple closed paths›

lemma winding_number_from_innerpath:
  assumes "simple_path c1" and c1: "pathstart c1 = a" "pathfinish c1 = b"
      and "simple_path c2" and c2: "pathstart c2 = a" "pathfinish c2 = b"
      and "simple_path c" and c: "pathstart c = a" "pathfinish c = b"
      and c1c2: "path_image c1 ∩ path_image c2 = {a,b}"
      and c1c:  "path_image c1 ∩ path_image c = {a,b}"
      and c2c:  "path_image c2 ∩ path_image c = {a,b}"
      and ne_12: "path_image c ∩ inside(path_image c1 ∪ path_image c2) ≠ {}"
      and z: "z ∈ inside(path_image c1 ∪ path_image c)"
      and wn_d: "winding_number (c1 +++ reversepath c) z = d"
      and "a ≠ b" "d ≠ 0"
  obtains "z ∈ inside(path_image c1 ∪ path_image c2)" "winding_number (c1 +++ reversepath c2) z = d"
proof -
  obtain 0: "inside(path_image c1 ∪ path_image c) ∩ inside(path_image c2 ∪ path_image c) = {}"
     and 1: "inside(path_image c1 ∪ path_image c) ∪ inside(path_image c2 ∪ path_image c) ∪
             (path_image c - {a,b}) = inside(path_image c1 ∪ path_image c2)"
    by (rule split_inside_simple_closed_curve
              [OF ‹simple_path c1› c1 ‹simple_path c2› c2 ‹simple_path c› c ‹a ≠ b› c1c2 c1c c2c ne_12])
  have znot: "z ∉ path_image c"  "z ∉ path_image c1" "z ∉ path_image c2"
    using union_with_outside z 1 by auto
  then have zout: "z ∈ outside (path_image c ∪ path_image c2)"
    by (metis "0" ComplI UnE disjoint_iff_not_equal sup.commute union_with_inside z)
  have wn_cc2: "winding_number (c +++ reversepath c2) z = 0"
    by (rule winding_number_zero_in_outside; simp add: zout ‹simple_path c2› c c2 ‹simple_path c› simple_path_imp_path path_image_join)
  show ?thesis
  proof
    show "z ∈ inside (path_image c1 ∪ path_image c2)"
      using "1" z by blast
    have "winding_number c1 z - winding_number c z = d "
      using assms znot
      by (metis wn_d winding_number_join simple_path_imp_path winding_number_reversepath add.commute path_image_reversepath path_reversepath pathstart_reversepath uminus_add_conv_diff)
    then show "winding_number (c1 +++ reversepath c2) z = d"
      using wn_cc2 by (simp add: winding_number_join simple_path_imp_path assms znot winding_number_reversepath)
  qed
qed

lemma simple_closed_path_wn1:
  fixes a::complex and e::real
  assumes "0 < e"
    and sp_pl: "simple_path(p +++ linepath (a - e) (a + e))" (is "simple_path ?pae")
    and psp:   "pathstart p = a + e"
    and pfp:   "pathfinish p = a - e"
    and disj:  "ball a e ∩ path_image p = {}"
obtains z where "z ∈ inside (path_image ?pae)" "cmod (winding_number ?pae z) = 1"
proof -
  have "arc p" and arc_lp: "arc (linepath (a - e) (a + e))"
    and pap: "path_image p ∩ path_image (linepath (a - e) (a + e)) ⊆ {pathstart p, a-e}"
    using simple_path_join_loop_eq [of "linepath (a - e) (a + e)" p] assms by auto
  have mid_eq_a: "midpoint (a - e) (a + e) = a"
    by (simp add: midpoint_def)
  with assms have "a ∈ path_image ?pae"
    by (simp add: assms path_image_join) (metis midpoint_in_closed_segment)
  then have "a ∈ frontier(inside (path_image ?pae))"
    using assms by (simp add: Jordan_inside_outside )
  with ‹0 🚫› obtain c where c: "c ∈ inside (path_image ?pae)"
                  and dac: "dist a c < e"
    by (auto simp: frontier_straddle)
  then have "c ∉ path_image ?pae"
    using inside_no_overlap by blast
  then have "c ∉ path_image p" "c ∉ closed_segment (a - e) (a + e)"
    by (simp_all add: assms path_image_join)
  with ‹0 🚫› dac have "c ∉ affine hull {a - e, a + e}"
    by (simp add: segment_as_ball not_le)
  with ‹0 🚫› have *: "¬ collinear {a - e, c,a + e}"
    using collinear_3_affine_hull [of "a-e" "a+e"] by (auto simp: insert_commute)
  have 13: "1/3 + 1/3 + 1/3 = (1::real)" by simp
  have "(1/3) *🪙R (a - of_real e) + (1/3) *🪙R c + (1/3) *🪙R (a + of_real e) ∈ interior(convex hull {a - e, c, a + e})"
    using interior_convex_hull_3_minimal [OF * DIM_complex]
    by clarsimp (metis 13 zero_less_divide_1_iff zero_less_numeral)
  then obtain z where z: "z ∈ interior(convex hull {a - e, c, a + e})" by force
  have [simp]: "z ∉ closed_segment (a - e) c"
    by (metis DIM_complex Diff_iff IntD2 inf_sup_absorb interior_of_triangle z)
  have [simp]: "z ∉ closed_segment (a + e) (a - e)"
    by (metis DIM_complex DiffD2 Un_iff interior_of_triangle z)
  have [simp]: "z ∉ closed_segment c (a + e)"
    by (metis (no_types, lifting) DIM_complex DiffD2 Un_insert_right inf_sup_aci(5) insertCI interior_of_triangle mk_disjoint_insert z)
  show thesis
  proof
    have "norm (winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z) = 1"
      using winding_number_triangle [OF z] by simp
    have zin: "z ∈ inside (path_image (linepath (a + e) (a - e)) ∪ path_image p)"
      and zeq: "winding_number (linepath (a + e) (a - e) +++ reversepath p) z =
                winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z"
    proof (rule winding_number_from_innerpath
        [of "linepath (a + e) (a - e)" "a+e" "a-e" p
          "linepath (a + e) c +++ linepath c (a - e)" z
          "winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z"])
      show sp_aec: "simple_path (linepath (a + e) c +++ linepath c (a - e))"
      proof (rule arc_imp_simple_path [OF arc_join])
        show "arc (linepath (a + e) c)"
          by (metis ‹c ∉ path_image p› arc_linepath pathstart_in_path_image psp)
        show "arc (linepath c (a - e))"
          by (metis ‹c ∉ path_image p› arc_linepath pathfinish_in_path_image pfp)
        show "path_image (linepath (a + e) c) ∩ path_image (linepath c (a - e)) ⊆ {pathstart (linepath c (a - e))}"
          by clarsimp (metis "*" IntI Int_closed_segment closed_segment_commute singleton_iff)
      qed auto
      show "simple_path p"
        using ‹arc p› arc_simple_path by blast
      show sp_ae2: "simple_path (linepath (a + e) (a - e))"
        using ‹arc p› arc_distinct_ends pfp psp by fastforce
      show pa: "pathfinish (linepath (a + e) (a - e)) = a - e"
           "pathstart (linepath (a + e) c +++ linepath c (a - e)) = a + e"
           "pathfinish (linepath (a + e) c +++ linepath c (a - e)) = a - e"
           "pathstart p = a + e" "pathfinish p = a - e"
           "pathstart (linepath (a + e) (a - e)) = a + e"
        by (simp_all add: assms)
      show 1: "path_image (linepath (a + e) (a - e)) ∩ path_image p = {a + e, a - e}"
      proof
        show "path_image (linepath (a + e) (a - e)) ∩ path_image p ⊆ {a + e, a - e}"
          using pap closed_segment_commute psp segment_convex_hull by fastforce
        show "{a + e, a - e} ⊆ path_image (linepath (a + e) (a - e)) ∩ path_image p"
          using pap pathfinish_in_path_image pathstart_in_path_image pfp psp by fastforce
      qed
      show 2: "path_image (linepath (a + e) (a - e)) ∩ path_image (linepath (a + e) c +++ linepath c (a - e)) =
               {a + e, a - e}"  (is "?lhs = ?rhs")
      proof
        have "¬ collinear {c, a + e, a - e}"
          using * by (simp add: insert_commute)
        then have "convex hull {a + e, a - e} ∩ convex hull {a + e, c} = {a + e}"
                  "convex hull {a + e, a - e} ∩ convex hull {c, a - e} = {a - e}"
          by (metis (full_types) Int_closed_segment insert_commute segment_convex_hull)+
        then show "?lhs ⊆ ?rhs"
          by (metis Int_Un_distrib equalityD1 insert_is_Un path_image_join path_image_linepath path_join_eq path_linepath segment_convex_hull simple_path_def sp_aec)
        show "?rhs ⊆ ?lhs"
          using segment_convex_hull by (simp add: path_image_join)
      qed
      have "path_image p ∩ path_image (linepath (a + e) c) ⊆ {a + e}"
      proof (clarsimp simp: path_image_join)
        fix x
        assume "x ∈ path_image p" and x_ac: "x ∈ closed_segment (a + e) c"
        then have "dist x a ≥ e"
          by (metis IntI all_not_in_conv disj dist_commute mem_ball not_less)
        with x_ac dac ‹e > 0› show "x = a + e"
          by (auto simp: norm_minus_commute dist_norm closed_segment_eq_open dest: open_segment_furthest_le [where y=a])
      qed
      moreover
      have "path_image p ∩ path_image (linepath c (a - e)) ⊆ {a - e}"
      proof (clarsimp simp: path_image_join)
        fix x
        assume "x ∈ path_image p" and x_ac: "x ∈ closed_segment c (a - e)"
        then have "dist x a ≥ e"
          by (metis IntI all_not_in_conv disj dist_commute mem_ball not_less)
        with x_ac dac ‹e > 0› show "x = a - e"
          by (auto simp: norm_minus_commute dist_norm closed_segment_eq_open dest: open_segment_furthest_le [where y=a])
      qed
      ultimately
      have "path_image p ∩ path_image (linepath (a + e) c +++ linepath c (a - e)) ⊆ {a + e, a - e}"
        by (force simp: path_image_join)
      then show 3: "path_image p ∩ path_image (linepath (a + e) c +++ linepath c (a - e)) = {a + e, a - e}"
        using "1" "2" by blast
      show 4: "path_image (linepath (a + e) c +++ linepath c (a - e)) ∩
               inside (path_image (linepath (a + e) (a - e)) ∪ path_image p) ≠ {}"
        apply (clarsimp simp: path_image_join segment_convex_hull disjoint_iff_not_equal)
        by (metis (no_types, opaque_lifting) UnI1 Un_commute c closed_segment_commute ends_in_segment(1) path_image_join
                  path_image_linepath pathstart_linepath pfp segment_convex_hull)
      show zin_inside: "z ∈ inside (path_image (linepath (a + e) (a - e)) ∪
                                    path_image (linepath (a + e) c +++ linepath c (a - e)))"
      proof (simp add: path_image_join)
        show "z ∈ inside (closed_segment (a + e) (a - e) ∪ (closed_segment (a + e) c ∪ closed_segment c (a - e)))"
          by (metis z inside_of_triangle DIM_complex Un_commute closed_segment_commute)
      qed
      show 5: "winding_number
             (linepath (a + e) (a - e) +++ reversepath (linepath (a + e) c +++ linepath c (a - e))) z =
            winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z"
        by (simp add: reversepath_joinpaths path_image_join winding_number_join)
      show 6: "winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z ≠ 0"
        by (simp add: winding_number_triangle z)
      show "winding_number (linepath (a + e) (a - e) +++ reversepath p) z =
            winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z"
        by (metis 1 2 3 4 5 6 pa sp_aec sp_ae2 ‹arc p› ‹simple_path p› arc_distinct_ends winding_number_from_innerpath zin_inside)
    qed (use assms ‹e > 0› in auto)
    show z_inside: "z ∈ inside (path_image ?pae)"
      using zin by (simp add: assms path_image_join Un_commute closed_segment_commute)
    have "cmod (winding_number ?pae z) = cmod ((winding_number(reversepath ?pae) z))"
    proof (subst winding_number_reversepath)
      show "path ?pae"
        using simple_path_imp_path sp_pl by blast
      show "z ∉ path_image ?pae"
        by (metis IntI emptyE inside_no_overlap z_inside)
    qed (simp add: inside_def)
    also have "... = cmod (winding_number(linepath (a + e) (a - e) +++ reversepath p) z)"
      by (simp add: pfp reversepath_joinpaths)
    also have "... = cmod (winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z)"
      by (simp add: zeq)
    also have "... = 1"
      using z by (simp add: interior_of_triangle winding_number_triangle)
    finally show "cmod (winding_number ?pae z) = 1" .
  qed
qed

lemma simple_closed_path_wn2:
  fixes a::complex and d e::real
  assumes "0 < d" "0 < e"
    and sp_pl: "simple_path(p +++ linepath (a - d) (a + e))"
    and psp:   "pathstart p = a + e"
    and pfp:   "pathfinish p = a - d"
obtains z where "z ∈ inside (path_image (p +++ linepath (a - d) (a + e)))"
                "cmod (winding_number (p +++ linepath (a - d) (a + e)) z) = 1"
proof -
  have [simp]: "a + of_real x ∈ closed_segment (a - α) (a - β) ⟷ x ∈ closed_segment (-α) (-β)" for x α β::real
    using closed_segment_translation_eq [of a]
    by (metis (no_types, opaque_lifting) add_uminus_conv_diff of_real_minus of_real_closed_segment)
  have [simp]: "a - of_real x ∈ closed_segment (a + α) (a + β) ⟷ -x ∈ closed_segment α β" for x α β::real
    by (metis closed_segment_translation_eq diff_conv_add_uminus of_real_closed_segment of_real_minus)
  have "arc p" and arc_lp: "arc (linepath (a - d) (a + e))" and "path p"
    and pap: "path_image p ∩ closed_segment (a - d) (a + e) ⊆ {a+e, a-d}"
    using simple_path_join_loop_eq [of "linepath (a - d) (a + e)" p] assms arc_imp_path  by auto
  have "0 ∈ closed_segment (-d) e"
    using ‹0 🚫› ‹0 🚫› closed_segment_eq_real_ivl by auto
  then have "a ∈ path_image (linepath (a - d) (a + e))"
    using of_real_closed_segment [THEN iffD2]
    by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment)
  then have "a ∉ path_image p"
    using ‹0 🚫› ‹0 🚫› pap by auto
  then obtain k where "0 < k" and k: "ball a k ∩ (path_image p) = {}"
    using ‹0 🚫› ‹path p› not_on_path_ball by blast
  define kde where "kde ≡ (min k (min d e)) / 2"
  have "0 < kde" "kde < k" "kde < d" "kde < e"
    using ‹0 🚫› ‹0 🚫› ‹0 🚫› by (auto simp: kde_def)
  let ?q = "linepath (a + kde) (a + e) +++ p +++ linepath (a - d) (a - kde)"
  have "- kde ∈ closed_segment (-d) e"
    using ‹0 🚫› ‹kde 🚫› ‹kde 🚫› closed_segment_eq_real_ivl by auto
  then have a_diff_kde: "a - kde ∈ closed_segment (a - d) (a + e)"
    using of_real_closed_segment [THEN iffD2]
    by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment)
  then have clsub2: "closed_segment (a - d) (a - kde) ⊆ closed_segment (a - d) (a + e)"
    by (simp add: subset_closed_segment)
  then have "path_image p ∩ closed_segment (a - d) (a - kde) ⊆ {a + e, a - d}"
    using pap by force
  moreover
  have "a + e ∉ path_image p ∩ closed_segment (a - d) (a - kde)"
    using ‹0 🚫› ‹kde 🚫› ‹0 🚫› by (auto simp: closed_segment_eq_real_ivl)
  ultimately have sub_a_diff_d: "path_image p ∩ closed_segment (a - d) (a - kde) ⊆ {a - d}"
    by blast
  have "kde ∈ closed_segment (-d) e"
    using ‹0 🚫› ‹kde 🚫› ‹kde 🚫› closed_segment_eq_real_ivl by auto
  then have a_diff_kde: "a + kde ∈ closed_segment (a - d) (a + e)"
    using of_real_closed_segment [THEN iffD2]
    by (force dest: closed_segment_translation_eq [of "a", THEN iffD2] simp del: of_real_closed_segment)
  then have clsub1: "closed_segment (a + kde) (a + e) ⊆ closed_segment (a - d) (a + e)"
    by (simp add: subset_closed_segment)
  then have "closed_segment (a + kde) (a + e) ∩ path_image p ⊆ {a + e, a - d}"
    using pap by force
  moreover
  have "closed_segment (a + kde) (a + e) ∩ closed_segment (a - d) (a - kde) = {}"
  proof (clarsimp intro!: equals0I)
    fix y
    assume y1: "y ∈ closed_segment (a + kde) (a + e)"
       and y2: "y ∈ closed_segment (a - d) (a - kde)"
    obtain u::real where u: "y = a + u" and "0 < u"
    proof -
      obtain ξ where ξ: "y = (1 - ξ) *🪙R (a + kde) + ξ *🪙R (a + e)" and "0 ≤ ξ" "ξ ≤ 1"
        using y1 by (auto simp: in_segment)
      show thesis
      proof
        show "y = a + ((1 - ξ)*kde + ξ*e)"
          using ξ by (auto simp: scaleR_conv_of_real algebra_simps)
        have "(1 - ξ)*kde + ξ*e ≥ 0"
          using ‹0 🚫› ‹0 ≤ ξ› ‹ξ ≤ 1› ‹0 🚫› by auto
        moreover have "(1 - ξ)*kde + ξ*e ≠ 0"
          using ‹0 🚫› ‹0 ≤ ξ› ‹ξ ≤ 1› ‹0 🚫› by (auto simp: add_nonneg_eq_0_iff)
        ultimately show "(1 - ξ)*kde + ξ*e > 0" by simp
      qed
    qed
    moreover
    obtain v::real where v: "y = a + v" and "v ≤ 0"
    proof -
      obtain ξ where ξ: "y = (1 - ξ) *🪙R (a - d) + ξ *🪙R (a - kde)" and "0 ≤ ξ" "ξ ≤ 1"
        using y2 by (auto simp: in_segment)
      show thesis
      proof
        show "y = a + (- ((1 - ξ)*d + ξ*kde))"
          using ξ by (force simp: scaleR_conv_of_real algebra_simps)
        show "- ((1 - ξ)*d + ξ*kde) ≤ 0"
          using ‹0 🚫› ‹0 ≤ ξ› ‹ξ ≤ 1› ‹0 🚫›
          by (metis add.left_neutral add_nonneg_nonneg le_diff_eq less_eq_real_def neg_le_0_iff_le split_mult_pos_le)

      qed
    qed
    ultimately show False
      by auto
  qed
  moreover have "a - d ∉ closed_segment (a + kde) (a + e)"
    using ‹0 🚫› ‹kde 🚫› ‹0 🚫› by (auto simp: closed_segment_eq_real_ivl)
  ultimately have sub_a_plus_e:
    "closed_segment (a + kde) (a + e) ∩ (path_image p ∪ closed_segment (a - d) (a - kde)) ⊆ {a + e}"
    by auto
  have "kde ∈ closed_segment (-kde) e"
    using ‹0 🚫› ‹kde 🚫› ‹kde 🚫› closed_segment_eq_real_ivl by auto
  then have a_add_kde: "a + kde ∈ closed_segment (a - kde) (a + e)"
    using of_real_closed_segment [THEN iffD2]
    by (force dest: closed_segment_translation_eq [of "a", THEN iffD2] simp del: of_real_closed_segment)
  have "closed_segment (a - kde) (a + kde) ∩ closed_segment (a + kde) (a + e) = {a + kde}"
    by (metis a_add_kde Int_closed_segment)
  moreover
  have "path_image p ∩ closed_segment (a - kde) (a + kde) = {}"
  proof (rule equals0I, clarify)
    fix y  assume "y ∈ path_image p" "y ∈ closed_segment (a - kde) (a + kde)"
    with equals0D [OF k, of y] ‹0 🚫› ‹kde 🚫› show False
      by (auto simp: dist_norm dest: dist_decreases_closed_segment [where c=a])
  qed
  moreover
  have "- kde ∈ closed_segment (-d) kde"
    using ‹0 🚫› ‹kde 🚫› ‹kde 🚫› closed_segment_eq_real_ivl by auto
  then have a_diff_kde': "a - kde ∈ closed_segment (a - d) (a + kde)"
    using of_real_closed_segment [THEN iffD2]
    by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment)
  then have "closed_segment (a - d) (a - kde) ∩ closed_segment (a - kde) (a + kde) = {a - kde}"
    by (metis Int_closed_segment)
  ultimately
  have pa_subset_pm_kde: "path_image ?q ∩ closed_segment (a - kde) (a + kde) ⊆ {a - kde, a + kde}"
    by (auto simp: path_image_join assms)
  have ge_kde1: "∃y. x = a + of_real y ∧ y ≥ kde" if x: "x ∈ closed_segment (a + kde) (a + e)" for x
  proof -
    obtain u where "0 ≤ u" "u ≤ 1" and u: "x = (1 - u) *🪙R (a + kde) + u *🪙R (a + e)"
      using x by (auto simp: in_segment)
    then have "kde ≤ (1 - u) * kde + u * e"
      using ‹kde 🚫› segment_bound_lemma by auto
    moreover have "x = a + ((1 - u) * kde + u * e)"
      by (fastforce simp: u algebra_simps scaleR_conv_of_real)
    ultimately
    show ?thesis by blast
  qed
  have ge_kde2: "∃y. x = a + of_real y ∧ y ≤ -kde" if x: "x ∈ closed_segment (a - d) (a - kde)" for x
  proof -
    obtain u where "0 ≤ u" "u ≤ 1" and u: "x = (1 - u) *🪙R (a - d) + u *🪙R (a - kde)"
      using x by (auto simp: in_segment)
    then have "kde ≤ ((1-u)*d + u*kde)"
      using ‹kde 🚫› segment_bound_lemma by auto
    moreover have "x = a - ((1-u)*d + u*kde)"
      by (fastforce simp: u algebra_simps scaleR_conv_of_real)
    ultimately show ?thesis
      by (metis add_uminus_conv_diff neg_le_iff_le of_real_minus)
  qed
  have notin_paq: "x ∉ path_image ?q" if "dist a x < kde" for x
  proof -
    have "x ∉ path_image p"
      using k ‹kde 🚫› that by force
    then show ?thesis
      using that assms by (auto simp: path_image_join dist_norm dest!: ge_kde1 ge_kde2)
  qed
  obtain z where zin: "z ∈ inside (path_image (?q +++ linepath (a - kde) (a + kde)))"
           and z1: "cmod (winding_number (?q +++ linepath (a - kde) (a + kde)) z) = 1"
  proof (rule simple_closed_path_wn1 [of kde ?q a])
    show "simple_path (?q +++ linepath (a - kde) (a + kde))"
    proof (intro simple_path_join_loop conjI)
      show "arc ?q"
      proof (rule arc_join)
        show "arc (linepath (a + kde) (a + e))"
          using ‹kde 🚫› ‹arc p› by (force simp: pfp)
        show "arc (p +++ linepath (a - d) (a - kde))"
          using ‹kde 🚫› ‹kde 🚫› ‹arc p› sub_a_diff_d by (force simp: pfp intro: arc_join)
      qed (auto simp: psp pfp path_image_join sub_a_plus_e)
      show "arc (linepath (a - kde) (a + kde))"
        using ‹0 🚫› by auto
    qed (use pa_subset_pm_kde in auto)
  qed (use ‹0 🚫› notin_paq in auto)
  have eq: "path_image (?q +++ linepath (a - kde) (a + kde)) = path_image (p +++ linepath (a - d) (a + e))"
            (is "?lhs = ?rhs")
  proof
    show "?lhs ⊆ ?rhs"
      using clsub1 clsub2 apply (auto simp: path_image_join assms)
      by (meson subsetCE subset_closed_segment)
    show "?rhs ⊆ ?lhs"
      apply (simp add: path_image_join assms Un_ac)
        by (metis Un_closed_segment Un_assoc a_diff_kde a_diff_kde' le_supI2 subset_refl)
    qed
  show thesis
  proof
    show zzin: "z ∈ inside (path_image (p +++ linepath (a - d) (a + e)))"
      by (metis eq zin)
    then have znotin: "z ∉ path_image p"
      by (metis ComplD Un_iff inside_Un_outside path_image_join pathfinish_linepath pathstart_reversepath pfp reversepath_linepath)
    have znotin_d_kde: "z ∉ closed_segment (a - d) (a + kde)"
      by (metis ComplD Un_iff Un_closed_segment a_diff_kde inside_Un_outside path_image_join path_image_linepath pathstart_linepath pfp zzin)
    have znotin_d_e: "z ∉ closed_segment (a - d) (a + e)"
      by (metis IntI UnCI emptyE inside_no_overlap path_image_join path_image_linepath pathstart_linepath pfp zzin)
    have znotin_kde_e: "z ∉ closed_segment (a + kde) (a + e)" and znotin_d_kde': "z ∉ closed_segment (a - d) (a - kde)"
      using clsub1 clsub2 zzin 
      by (metis (no_types, opaque_lifting) IntI Un_iff emptyE inside_no_overlap path_image_join path_image_linepath pathstart_linepath pfp subsetD)+
    have "winding_number (linepath (a - d) (a + e)) z =
          winding_number (linepath (a - d) (a + kde)) z + winding_number (linepath (a + kde) (a + e)) z"
    proof (rule winding_number_split_linepath)
      show "a + complex_of_real kde ∈ closed_segment (a - d) (a + e)"
        by (simp add: a_diff_kde)
      show "z ∉ closed_segment (a - d) (a + e)"
        by (metis ComplD Un_iff inside_Un_outside path_image_join path_image_linepath pathstart_linepath pfp zzin)
    qed
    also have "... = winding_number (linepath (a + kde) (a + e)) z +
                     (winding_number (linepath (a - d) (a - kde)) z + winding_number (linepath (a - kde) (a + kde)) z)"
      by (simp add: winding_number_split_linepath [of "a-kde", symmetric] znotin_d_kde a_diff_kde')
    finally have "winding_number (p +++ linepath (a - d) (a + e)) z =
                    winding_number p z + winding_number (linepath (a + kde) (a + e)) z +
                   (winding_number (linepath (a - d) (a - kde)) z +
                    winding_number (linepath (a - kde) (a + kde)) z)"
      by (metis (no_types, lifting) ComplD Un_iff ‹arc p› add.assoc arc_imp_path eq path_image_join path_join_path_ends path_linepath simple_path_imp_path sp_pl union_with_outside winding_number_join zin)
    also have "... = winding_number (linepath (a + kde) (a + e)) z
                   + winding_number (p +++ linepath (a - d) (a - kde)) z
                   + winding_number (linepath (a - kde) (a + kde)) z"
      using ‹path p› znotin assms 
      by simp (metis Un_iff Un_closed_segment a_diff_kde' path_image_linepath path_linepath pathstart_linepath winding_number_join znotin_d_kde)
    also have "... = winding_number ?q z + winding_number (linepath (a - kde) (a + kde)) z"
      using ‹path p› znotin assms by (simp add: path_image_join winding_number_join znotin_kde_e znotin_d_kde')
    also have "... = winding_number (?q +++ linepath (a - kde) (a + kde)) z"
      by (metis (mono_tags, lifting) ComplD UnCI ‹path p› eq inside_outside path_image_join path_join_eq path_linepath pathfinish_join pathfinish_linepath pathstart_join pathstart_linepath pfp psp winding_number_join zzin)
    finally have "winding_number (p +++ linepath (a - d) (a + e)) z =
                  winding_number (?q +++ linepath (a - kde) (a + kde)) z" .
    then show "cmod (winding_number (p +++ linepath (a - d) (a + e)) z) = 1"
      by (simp add: z1)
  qed
qed

lemma simple_closed_path_wn3:
  fixes p :: "real ==> complex"
  assumes "simple_path p" and loop: "pathfinish p = pathstart p"
  obtains z where "z ∈ inside (path_image p)" "cmod (winding_number p z) = 1"
proof -
  have ins: "inside(path_image p) ≠ {}" "open(inside(path_image p))"
            "connected(inside(path_image p))"
   and out: "outside(path_image p) ≠ {}" "open(outside(path_image p))"
            "connected(outside(path_image p))"
   and bo:  "bounded(inside(path_image p))" "¬ bounded(outside(path_image p))"
   and ins_out: "inside(path_image p) ∩ outside(path_image p) = {}"
                "inside(path_image p) ∪ outside(path_image p) = - path_image p"
   and fro: "frontier(inside(path_image p)) = path_image p"
            "frontier(outside(path_image p)) = path_image p"
    using Jordan_inside_outside [OF assms] by auto
  obtain a where a: "a ∈ inside(path_image p)"
    using ‹inside (path_image p) ≠ {}› by blast
  obtain d::real where "0 < d" and d_fro: "a - d ∈ frontier (inside (path_image p))"
                 and d_int: "∧ε. [0 ≤ ε; ε < d] ==> (a - ε) ∈ inside (path_image p)"
    using ray_to_frontier [of "inside (path_image p)" a "-1"] bo ins a interior_eq
    by (metis ab_group_add_class.ab_diff_conv_add_uminus of_real_def scale_minus_right zero_neq_neg_one)
  obtain e::real where "0 < e" and e_fro: "a + e ∈ frontier (inside (path_image p))"
    and e_int: "∧ε. [0 ≤ ε; ε < e] ==> (a + ε) ∈ inside (path_image p)"
    using ray_to_frontier [of "inside (path_image p)" a 1] bo ins a interior_eq
    by (metis of_real_def zero_neq_one)
  obtain t0 where "0 ≤ t0" "t0 ≤ 1" and pt: "p t0 = a - d"
    using a d_fro fro by (auto simp: path_image_def)
  obtain q where "simple_path q" and q_ends: "pathstart q = a - d" "pathfinish q = a - d"
    and q_eq_p: "path_image q = path_image p"
    and wn_q_eq_wn_p: "∧z. z ∈ inside(path_image p) ==> winding_number q z = winding_number p z"
  proof
    show "simple_path (shiftpath t0 p)"
      by (simp add: pathstart_shiftpath pathfinish_shiftpath
          simple_path_shiftpath path_image_shiftpath ‹0 ≤ t0› ‹t0 ≤ 1› assms)
    show "pathstart (shiftpath t0 p) = a - d"
      using pt by (simp add: ‹t0 ≤ 1› pathstart_shiftpath)
    show "pathfinish (shiftpath t0 p) = a - d"
      by (simp add: ‹0 ≤ t0› loop pathfinish_shiftpath pt)
    show "path_image (shiftpath t0 p) = path_image p"
      by (simp add: ‹0 ≤ t0› ‹t0 ≤ 1› loop path_image_shiftpath)
    show "winding_number (shiftpath t0 p) z = winding_number p z"
      if "z ∈ inside (path_image p)" for z
      by (metis ComplD Un_iff ‹0 ≤ t0› ‹t0 ≤ 1› ‹simple_path p› atLeastAtMost_iff inside_Un_outside
          loop simple_path_imp_path that winding_number_shiftpath)
  qed
  have ad_not_ae: "a - d ≠ a + e"
    by (metis ‹0 🚫› ‹0 🚫› add.left_inverse add_left_cancel add_uminus_conv_diff
        le_add_same_cancel2 less_eq_real_def not_less of_real_add of_real_def of_real_eq_0_iff pt)
  have ad_ae_q: "{a - d, a + e} ⊆ path_image q"
    using ‹path_image q = path_image p› d_fro e_fro fro(1) by auto
  have ada: "open_segment (a - d) a ⊆ inside (path_image p)"
  proof (clarsimp simp: in_segment)
    fix u::real assume "0 < u" "u < 1"
    with d_int have "a - (1 - u) * d ∈ inside (path_image p)"
      by (metis ‹0 🚫› add.commute diff_add_cancel left_diff_distrib' less_add_same_cancel2 less_eq_real_def mult.left_neutral zero_less_mult_iff)
    then show "(1 - u) *🪙R (a - d) + u *🪙R a ∈ inside (path_image p)"
      by (simp add: diff_add_eq of_real_def real_vector.scale_right_diff_distrib)
  qed
  have aae: "open_segment a (a + e) ⊆ inside (path_image p)"
  proof (clarsimp simp: in_segment)
    fix u::real assume "0 < u" "u < 1"
    with e_int have "a + u * e ∈ inside (path_image p)"
      by (meson ‹0 🚫› less_eq_real_def mult_less_cancel_right2 not_less zero_less_mult_iff)
    then show "(1 - u) *🪙R a + u *🪙R (a + e) ∈ inside (path_image p)"
      by (metis (mono_tags, lifting) add.assoc of_real_mult pth_6 scaleR_collapse scaleR_conv_of_real)
  qed
  have "complex_of_real (d * d + (e * e + d * (e + e))) ≠ 0"
    using ad_not_ae
    by (metis ‹0 🚫› ‹0 🚫› add_strict_left_mono less_add_same_cancel1 not_sum_squares_lt_zero
        of_real_eq_0_iff zero_less_double_add_iff_zero_less_single_add zero_less_mult_iff)
  moreover have "∃u>0. u < 1 ∧ d = u * d + u * e"
    using ‹0 🚫› ‹0 🚫›
    by (rule_tac x="d / (d+e)" in exI) (simp add: divide_simps scaleR_conv_of_real flip: distrib_left)
  ultimately have a_in_de: "a ∈ open_segment (a - d) (a + e)"
    using ad_not_ae by (simp add: in_segment algebra_simps scaleR_conv_of_real flip: of_real_add of_real_mult)
  then have "open_segment (a - d) (a + e) ⊆ inside (path_image p)"
    using ada a aae Un_open_segment [of a "a-d" "a+e"] by blast
  then have "path_image q ∩ open_segment (a - d) (a + e) = {}"
    using inside_no_overlap by (fastforce simp: q_eq_p)
  with ad_ae_q have paq_Int_cs: "path_image q ∩ closed_segment (a - d) (a + e) = {a - d, a + e}"
    by (simp add: closed_segment_eq_open)
  obtain t where "0 ≤ t" "t ≤ 1" and qt: "q t = a + e"
    using a e_fro fro ad_ae_q by (auto simp: path_defs)
  then have "t ≠ 0"
    by (metis ad_not_ae pathstart_def q_ends(1))
  then have "t ≠ 1"
    by (metis ad_not_ae pathfinish_def q_ends(2) qt)
  have q01: "q 0 = a - d" "q 1 = a - d"
    using q_ends by (auto simp: pathstart_def pathfinish_def)
  obtain z where zin: "z ∈ inside (path_image (subpath t 0 q +++ linepath (a - d) (a + e)))"
             and z1: "cmod (winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z) = 1"
  proof (rule simple_closed_path_wn2 [of d e "subpath t 0 q" a], simp_all add: q01)
    show "simple_path (subpath t 0 q +++ linepath (a - d) (a + e))"
    proof (rule simple_path_join_loop, simp_all add: qt q01)
      have "inj_on q (closed_segment t 0)"
        using ‹0 ≤ t› ‹simple_path q› ‹t ≤ 1› ‹t ≠ 0› ‹t ≠ 1›
        by (fastforce simp: simple_path_def loop_free_def inj_on_def closed_segment_eq_real_ivl)
      then show "arc (subpath t 0 q)"
        using ‹0 ≤ t› ‹simple_path q› ‹t ≤ 1› ‹t ≠ 0›
        by (simp add: arc_subpath_eq simple_path_imp_path)
      show "arc (linepath (a - d) (a + e))"
        by (simp add: ad_not_ae)
      show "path_image (subpath t 0 q) ∩ closed_segment (a - d) (a + e) ⊆ {a + e, a - d}"
        using qt paq_Int_cs  ‹simple_path q› ‹0 ≤ t› ‹t ≤ 1›
        by (force simp: dest: rev_subsetD [OF _ path_image_subpath_subset] intro: simple_path_imp_path)
    qed
  qed (auto simp: ‹0 🚫› ‹0 🚫› qt)
  have pa01_Un: "path_image (subpath 0 t q) ∪ path_image (subpath 1 t q) = path_image q"
    unfolding path_image_subpath
    using ‹0 ≤ t› ‹t ≤ 1› by (force simp: path_image_def image_iff)
  with paq_Int_cs have pa_01q:
        "(path_image (subpath 0 t q) ∪ path_image (subpath 1 t q)) ∩ closed_segment (a - d) (a + e) = {a - d, a + e}"
    by metis
  have z_notin_ed: "z ∉ closed_segment (a + e) (a - d)"
    using zin q01 by (simp add: path_image_join closed_segment_commute inside_def)
  have z_notin_0t: "z ∉ path_image (subpath 0 t q)"
    by (metis (no_types, opaque_lifting) IntI Un_upper1 subsetD empty_iff inside_no_overlap path_image_join
        path_image_subpath_commute pathfinish_subpath pathstart_def pathstart_linepath q_ends(1) qt subpath_trivial zin)
  have [simp]: "- winding_number (subpath t 0 q) z = winding_number (subpath 0 t q) z"
    by (metis ‹0 ≤ t› ‹simple_path q› ‹t ≤ 1› atLeastAtMost_iff zero_le_one
              path_image_subpath_commute path_subpath real_eq_0_iff_le_ge_0
              reversepath_subpath simple_path_imp_path winding_number_reversepath z_notin_0t)
  obtain z_in_q: "z ∈ inside(path_image q)"
     and wn_q: "winding_number (subpath 0 t q +++ subpath t 1 q) z = - winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z"
  proof (rule winding_number_from_innerpath
          [of "subpath 0 t q" "a-d" "a+e" "subpath 1 t q" "linepath (a - d) (a + e)"
            z "- winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z"],
         simp_all add: q01 qt pa01_Un reversepath_subpath)
    show "simple_path (subpath 0 t q)" "simple_path (subpath 1 t q)"
      by (simp_all add: ‹0 ≤ t› ‹simple_path q› ‹t ≤ 1› ‹t ≠ 0› ‹t ≠ 1› simple_path_subpath)
    show "simple_path (linepath (a - d) (a + e))"
      using ad_not_ae by blast
    show "path_image (subpath 0 t q) ∩ path_image (subpath 1 t q) = {a - d, a + e}"  (is "?lhs = ?rhs")
    proof
      show "?lhs ⊆ ?rhs"
        using ‹0 ≤ t› ‹simple_path q› ‹t ≤ 1› ‹t ≠ 1› q_ends qt q01
        by (force simp: pathfinish_def qt simple_path_def loop_free_def path_image_subpath)
      show "?rhs ⊆ ?lhs"
        using ‹0 ≤ t› ‹t ≤ 1› q01 qt by (force simp: path_image_subpath)
    qed
    show "path_image (subpath 0 t q) ∩ closed_segment (a - d) (a + e) = {a - d, a + e}" (is "?lhs = ?rhs")
    proof
      show "?lhs ⊆ ?rhs"  using paq_Int_cs pa01_Un by fastforce
      show "?rhs ⊆ ?lhs"  using ‹0 ≤ t› ‹t ≤ 1› q01 qt by (force simp: path_image_subpath)
    qed
    show "path_image (subpath 1 t q) ∩ closed_segment (a - d) (a + e) = {a - d, a + e}" (is "?lhs = ?rhs")
    proof
      show "?lhs ⊆ ?rhs"  by (auto simp: pa_01q [symmetric])
      show "?rhs ⊆ ?lhs"  using ‹0 ≤ t› ‹t ≤ 1› q01 qt by (force simp: path_image_subpath)
    qed
    show "closed_segment (a - d) (a + e) ∩ inside (path_image q) ≠ {}"
      using a a_in_de open_closed_segment pa01_Un q_eq_p by fastforce
    show "z ∈ inside (path_image (subpath 0 t q) ∪ closed_segment (a - d) (a + e))"
      by (metis path_image_join path_image_linepath path_image_subpath_commute pathfinish_subpath pathstart_linepath q01(1) zin)
    show "winding_number (subpath 0 t q +++ linepath (a + e) (a - d)) z =
      - winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z"
      using z_notin_ed z_notin_0t ‹0 ≤ t› ‹simple_path q› ‹t ≤ 1›
      by (simp add: simple_path_imp_path qt q01 path_image_subpath_commute closed_segment_commute winding_number_join winding_number_reversepath [symmetric])
    show "- d ≠ e"
      using ad_not_ae by auto
    show "winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z ≠ 0"
      using z1 by auto
  qed
  show ?thesis
  proof
    show "z ∈ inside (path_image p)"
      using q_eq_p z_in_q by auto
    then have [simp]: "z ∉ path_image q"
      by (metis disjoint_iff_not_equal inside_no_overlap q_eq_p)
    have [simp]: "z ∉ path_image (subpath 1 t q)"
      using inside_def pa01_Un z_in_q by fastforce
    have "winding_number(subpath 0 t q +++ subpath t 1 q) z = winding_number(subpath 0 1 q) z"
      using z_notin_0t ‹0 ≤ t› ‹simple_path q› ‹t ≤ 1›
      by (simp add: simple_path_imp_path qt path_image_subpath_commute winding_number_join winding_number_subpath_combine)
    with wn_q have "winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z = - winding_number q z"
      by auto
    with z1 have "cmod (winding_number q z) = 1"
      by simp
    with z1 wn_q_eq_wn_p show "cmod (winding_number p z) = 1"
      using z1 wn_q_eq_wn_p  by (simp add: ‹z ∈ inside (path_image p)›)
    qed
qed

proposition simple_closed_path_winding_number_inside:
  assumes "simple_path γ"
  obtains "∧z. z ∈ inside(path_image γ) ==> winding_number γ z = 1"
        | "∧z. z ∈ inside(path_image γ) ==> winding_number γ z = -1"
proof (cases "pathfinish γ = pathstart γ")
  case True
  have "path γ"
    by (simp add: assms simple_path_imp_path)
  then have const: "winding_number γ constant_on inside(path_image γ)"
  proof (rule winding_number_constant)
    show "connected (inside(path_image γ))"
      by (simp add: Jordan_inside_outside True assms)
  qed (use inside_no_overlap True in auto)
  obtain z where zin: "z ∈ inside (path_image γ)" and z1: "cmod (winding_number γ z) = 1"
    using simple_closed_path_wn3 [of γ] True assms by blast
  have "winding_number γ z ∈ ℤ"
    using zin integer_winding_number [OF ‹path γ› True] inside_def by blast
  moreover have "real_of_int x = - 1 ⟷ x = -1" for x
    by linarith
  ultimately consider "winding_number γ z = 1" | "winding_number γ z = -1"
    using z1 by (auto simp: Ints_def abs_if split: if_split_asm)
  with that const zin show ?thesis
    unfolding constant_on_def by metis
next
  case False
  then show ?thesis
    using inside_simple_curve_imp_closed assms that(2) by blast
qed

lemma simple_closed_path_abs_winding_number_inside:
  assumes "simple_path γ" "z ∈ inside(path_image γ)"
    shows "∣Re (winding_number γ z)∣ = 1"
  by (metis assms norm_minus_cancel norm_one one_complex.simps(1) real_norm_def simple_closed_path_winding_number_inside uminus_complex.simps(1))

lemma simple_closed_path_norm_winding_number_inside:
  assumes "simple_path γ" "z ∈ inside(path_image γ)"
  shows "norm (winding_number γ z) = 1"
proof -
  have "pathfinish γ = pathstart γ"
    using assms inside_simple_curve_imp_closed by blast
  with assms integer_winding_number have "winding_number γ z ∈ ℤ"
    by (simp add: inside_def simple_path_def)
  then show ?thesis
    by (metis assms norm_minus_cancel norm_one simple_closed_path_winding_number_inside)
qed

lemma simple_closed_path_winding_number_cases:
  assumes "simple_path γ" "pathfinish γ = pathstart γ" "z ∉ path_image γ"
  shows "winding_number γ z ∈ {-1,0,1}"
proof -
  consider "z ∈ inside (path_image γ)" | "z ∈ outside (path_image γ)"
    by (metis ComplI UnE assms(3) inside_Un_outside)
  then show ?thesis
  proof cases
    case 1
    then show ?thesis
      using assms simple_closed_path_winding_number_inside by auto
  next
    case 2
    then show ?thesis
      using assms simple_path_def winding_number_zero_in_outside by blast
  qed
qed

lemma simple_closed_path_winding_number_pos:
   "[simple_path γ; pathfinish γ = pathstart γ; z ∉ path_image γ; 0 < Re(winding_number γ z)]
    ==> winding_number γ z = 1"
using simple_closed_path_winding_number_cases
  by fastforce

lemma simple_closed_path_winding_number_neg:
   "[simple_path γ; pathfinish γ = pathstart γ; z ∉ path_image γ; Re (winding_number γ z) < 0]
    ==> winding_number γ z = -1"
  using simple_closed_path_winding_number_cases by fastforce


subsection ‹Winding number for rectangular paths›

proposition winding_number_rectpath:
  assumes "z ∈ box a1 a3"
  shows   "winding_number (rectpath a1 a3) z = 1"
proof -
  from assms have less: "Re a1 < Re a3" "Im a1 < Im a3"
    by (auto simp: in_box_complex_iff)
  define a2 a4 where "a2 = Complex (Re a3) (Im a1)" and "a4 = Complex (Re a1) (Im a3)"
  let ?l1 = "linepath a1 a2" and ?l2 = "linepath a2 a3"
  and ?l3 = "linepath a3 a4" and ?l4 = "linepath a4 a1"
  from assms and less have "z ∉ path_image (rectpath a1 a3)"
    by (auto simp: path_image_rectpath_cbox_minus_box)
  also have "path_image (rectpath a1 a3) =
               path_image ?l1 ∪ path_image ?l2 ∪ path_image ?l3 ∪ path_image ?l4"
    by (simp add: rectpath_def Let_def path_image_join Un_assoc a2_def a4_def)
  finally have "z ∉ …" .
  moreover have "∀l∈{?l1,?l2,?l3,?l4}. Re (winding_number l z) > 0"
    unfolding ball_simps HOL.simp_thms a2_def a4_def
    by (intro conjI; (rule winding_number_linepath_pos_lt;
          (insert assms, auto simp: a2_def a4_def in_box_complex_iff mult_neg_neg))+)
  ultimately have "Re (winding_number (rectpath a1 a3) z) > 0"
    by (simp add: winding_number_join path_image_join rectpath_def Let_def a2_def a4_def)
  thus "winding_number (rectpath a1 a3) z = 1" using assms less
    by (intro simple_closed_path_winding_number_pos simple_path_rectpath)
       (auto simp: path_image_rectpath_cbox_minus_box)
qed

proposition winding_number_rectpath_outside:
  assumes "Re a1 ≤ Re a3" "Im a1 ≤ Im a3"
  assumes "z ∉ cbox a1 a3"
  shows   "winding_number (rectpath a1 a3) z = 0"
  using assms by (intro winding_number_zero_outside[OF _ _ _ assms(3)]
                     path_image_rectpath_subset_cbox) simp_all

text‹A per-function version for continuous logs, a kind of monodromy›
proposition🍋‹tag unimportant› winding_number_compose_exp:
  assumes "path p"
  shows "winding_number (exp ∘ p) 0 = (pathfinish p - pathstart p) / (2 * of_real pi * i)"
proof -
  obtain e where "0 < e" and e: "∧t. t ∈ {0..1} ==> e ≤ norm(exp(p t))"
  proof
    have "closed (path_image (exp ∘ p))"
      by (simp add: assms closed_path_image holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image)
    then show "0 < setdist {0} (path_image (exp ∘ p))"
      by (metis exp_not_eq_zero imageE image_comp infdist_eq_setdist infdist_pos_not_in_closed path_defs(4) path_image_nonempty)
  next
    fix t::real
    assume "t ∈ {0..1}"
    have "setdist {0} (path_image (exp ∘ p)) ≤ dist 0 (exp (p t))"
    proof (rule setdist_le_dist)
      show "exp (p t) ∈ path_image (exp ∘ p)"
        using ‹t ∈ {0..1}› path_image_def by fastforce+
    qed auto
    then show "setdist {0} (path_image (exp ∘ p)) ≤ cmod (exp (p t))"
      by simp
  qed
  have "bounded (path_image p)"
    by (simp add: assms bounded_path_image)
  then obtain B where "0 < B" and B: "path_image p ⊆ cball 0 B"
    by (meson bounded_pos mem_cball_0 subsetI)
  let ?B = "cball (0::complex) (B+1)"
  have "uniformly_continuous_on ?B exp"
    using holomorphic_on_exp holomorphic_on_imp_continuous_on
    by (force intro: compact_uniformly_continuous)
  then obtain d where "d > 0"
        and d: "∧x x'. [x∈?B; x'∈?B; dist x' x < d] ==> norm (exp x' - exp x) < e"
    using ‹e > 0› by (auto simp: uniformly_continuous_on_def dist_norm)
  then have "min 1 d > 0"
    by force
  then obtain g where pfg: "polynomial_function g"  and "g 0 = p 0" "g 1 = p 1"
           and gless: "∧t. t ∈ {0..1} ==> norm(g t - p t) < min 1 d"
    using path_approx_polynomial_function [OF ‹path p›] ‹d > 0› ‹0 🚫›
    unfolding pathfinish_def pathstart_def by blast
  have "winding_number (exp ∘ p) 0 = winding_number (exp ∘ g) 0"
  proof (rule winding_number_nearby_paths_eq [symmetric])
    show "path (exp ∘ p)" "path (exp ∘ g)"
      by (simp_all add: pfg assms holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image path_polynomial_function)
  next
    fix t :: "real"
    assume t: "t ∈ {0..1}"
    with gless have "norm(g t - p t) < 1"
      using min_less_iff_conj by blast
    moreover have ptB: "norm (p t) ≤ B"
      using B t by (force simp: path_image_def)
    ultimately have "cmod (g t) ≤ B + 1"
      by (meson add_mono_thms_linordered_field(4) le_less_trans less_imp_le norm_triangle_sub)
    with ptB gless t have "cmod ((exp ∘ g) t - (exp ∘ p) t) < e"
      by (auto simp: dist_norm d)
    with e t show "cmod ((exp ∘ g) t - (exp ∘ p) t) < cmod ((exp ∘ p) t - 0)"
      by fastforce
  qed (use ‹g 0 = p 0› ‹g 1 = p 1› in ‹auto simp: pathfinish_def pathstart_def›)
  also have "... = 1 / (of_real (2 * pi) * i) * contour_integral (exp ∘ g) (λw. 1 / (w - 0))"
  proof (rule winding_number_valid_path)
    have "continuous_on (path_image g) (deriv exp)"
      by (metis DERIV_exp DERIV_imp_deriv continuous_on_cong holomorphic_on_exp holomorphic_on_imp_continuous_on)
    then show "valid_path (exp ∘ g)"
      by (simp add: field_differentiable_within_exp pfg valid_path_compose valid_path_polynomial_function)
    show "0 ∉ path_image (exp ∘ g)"
      by (auto simp: path_image_def)
  qed
  also have "... = 1 / (of_real (2 * pi) * i) * integral {0..1} (λx. vector_derivative g (at x))"
  proof (simp add: contour_integral_integral, rule integral_cong)
    fix t :: "real"
    assume t: "t ∈ {0..1}"
    show "vector_derivative (exp ∘ g) (at t) / exp (g t) = vector_derivative g (at t)"
    proof -
      have "(exp ∘ g has_vector_derivative vector_derivative (exp ∘ g) (at t)) (at t)"
        by (meson DERIV_exp differentiable_def field_vector_diff_chain_at has_vector_derivative_def
            has_vector_derivative_polynomial_function pfg vector_derivative_works)
      moreover have "(exp ∘ g has_vector_derivative vector_derivative g (at t) * exp (g t)) (at t)"
        by (metis DERIV_exp field_vector_diff_chain_at has_vector_derivative_polynomial_function pfg vector_derivative_at)
      ultimately show ?thesis
        by (simp add: divide_simps, rule vector_derivative_unique_at)
    qed
  qed
  also have "... = (pathfinish p - pathstart p) / (2 * of_real pi * i)"
  proof -
    have "((λx. vector_derivative g (at x)) has_integral g 1 - g 0) {0..1}"
      by (meson differentiable_at_polynomial_function fundamental_theorem_of_calculus 
                has_vector_derivative_at_within pfg vector_derivative_works zero_le_one)
    then show ?thesis
      unfolding pathfinish_def pathstart_def
      using ‹g 0 = p 0› ‹g 1 = p 1› by auto
  qed
  finally show ?thesis .
qed

end