Theory HOL-Complex_Analysis.Riemann_Mapping

(*  Title:      HOL/Analysis/Riemann_Mapping.thy
    Authors:    LC Paulson, based on material from HOL Light
*)

section ‹Moebius functions, Equivalents of Simply Connected Sets, Riemann Mapping Theorem›

theory Riemann_Mapping
imports Great_Picard
begin

subsection‹Moebius functions are biholomorphisms of the unit disc›

definitiontag important› Moebius_function :: "[real,complex,complex]  complex" where
  "Moebius_function  λt w z. exp(𝗂 * of_real t) * (z - w) / (1 - cnj w * z)"

lemma Moebius_function_simple:
   "Moebius_function 0 w z = (z - w) / (1 - cnj w * z)"
  by (simp add: Moebius_function_def)

lemma Moebius_function_eq_zero:
   "Moebius_function t w w = 0"
  by (simp add: Moebius_function_def)

lemma Moebius_function_of_zero:
   "Moebius_function t w 0 = - exp(𝗂 * of_real t) * w"
  by (simp add: Moebius_function_def)

lemma Moebius_function_norm_lt_1:
  assumes w1: "norm w < 1" and z1: "norm z < 1"
  shows "norm (Moebius_function t w z) < 1"
proof -
  have "1 - cnj w * z  0"
    by (metis complex_cnj_cnj complex_mod_sqrt_Re_mult_cnj mult.commute mult_less_cancel_right1 norm_ge_zero norm_mult norm_one order.asym right_minus_eq w1 z1)
  then have VV: "1 - w * cnj z  0"
    by (metis complex_cnj_cnj complex_cnj_mult complex_cnj_one right_minus_eq)
  then have "1 - norm (Moebius_function t w z) ^ 2 =
         ((1 - norm w ^ 2) / (norm (1 - cnj w * z) ^ 2)) * (1 - norm z ^ 2)"
    apply (cases w)
    apply (cases z)
    apply (simp add: Moebius_function_def divide_simps norm_divide norm_mult)
    apply (simp add: complex_norm complex_diff complex_mult one_complex.code complex_cnj)
    apply (auto simp: algebra_simps power2_eq_square)
    done
  then have "1 - (cmod (Moebius_function t w z))2 = (1 - cmod (w * w)) / (cmod (1 - cnj w * z))2 * (1 - cmod (z * z))"
    by (simp add: norm_mult power2_eq_square)
  moreover have "0 < 1 - cmod (z * z)"
    by (metis (no_types) z1 diff_gt_0_iff_gt mult.left_neutral norm_mult_less)
  ultimately have "0 < 1 - norm (Moebius_function t w z) ^ 2"
    using 1 - cnj w * z  0 w1 norm_mult_less by fastforce
  then show ?thesis
    using linorder_not_less by fastforce
qed

lemma Moebius_function_holomorphic:
  assumes "norm w < 1"
  shows "Moebius_function t w holomorphic_on ball 0 1"
proof -
  have *: "1 - z * w  0" if "norm z < 1" for z
  proof -
    have "norm (1::complex)  norm (z * w)"
      using assms that norm_mult_less by fastforce
    then show ?thesis by auto
  qed
  show ?thesis
    unfolding Moebius_function_def
    apply (intro holomorphic_intros)
    by (metis "*" mult.commute complex_cnj_cnj complex_cnj_mult complex_cnj_one complex_mod_cnj mem_ball_0 right_minus_eq)
qed

lemma Moebius_function_compose:
  assumes meq: "-w1 = w2" and "norm w1 < 1" "norm z < 1"
  shows "Moebius_function 0 w1 (Moebius_function 0 w2 z) = z"
proof -
  have "norm w2 < 1"
    using assms by auto
  then have "-w1 = z" if "cnj w2 * z = 1"
    by (metis assms(3) complex_mod_cnj less_irrefl mult.right_neutral norm_mult_less norm_one that)
  moreover have "z=0" if "1 - cnj w2 * z = cnj w1 * (z - w2)"
  proof -
    have "w2 * cnj w2 = 1"
      using that meq by (auto simp: algebra_simps)
    then show "z = 0"
      by (metis (no_types) cmod w2 < 1 complex_mod_cnj less_irrefl mult.right_neutral norm_mult_less norm_one)
  qed
  moreover have "z - w2 - w1 * (1 - cnj w2 * z) = z * (1 - cnj w2 * z - cnj w1 * (z - w2))"
    using meq by (fastforce simp: algebra_simps)
  ultimately
  show ?thesis
    by (simp add: Moebius_function_def divide_simps norm_divide norm_mult)
qed

lemma ball_biholomorphism_exists:
  assumes "a  ball 0 1"
  obtains f g where "f a = 0"
                "f holomorphic_on ball 0 1" "f ` ball 0 1  ball 0 1"
                "g holomorphic_on ball 0 1" "g ` ball 0 1  ball 0 1"
                "z. z  ball 0 1  f (g z) = z"
                "z. z  ball 0 1  g (f z) = z"
proof
  show "Moebius_function 0 a holomorphic_on ball 0 1"  "Moebius_function 0 (-a) holomorphic_on ball 0 1"
    using Moebius_function_holomorphic assms mem_ball_0 by auto
  show "Moebius_function 0 a a = 0"
    by (simp add: Moebius_function_eq_zero)
  show "Moebius_function 0 a ` ball 0 1  ball 0 1"
       "Moebius_function 0 (- a) ` ball 0 1  ball 0 1"
    using Moebius_function_norm_lt_1 assms by auto
  show "Moebius_function 0 a (Moebius_function 0 (- a) z) = z"
       "Moebius_function 0 (- a) (Moebius_function 0 a z) = z" if "z  ball 0 1" for z
    using Moebius_function_compose assms that by auto
qed


subsection‹A big chain of equivalents of simple connectedness for an open set›

lemma biholomorphic_to_disc_aux:
  assumes "open S" "connected S" "0  S" and S01: "S  ball 0 1"
      and prev: "f. f holomorphic_on S; z. z  S  f z  0; inj_on f S
                g. g holomorphic_on S  (z  S. f z = (g z)2)"
  shows "f g. f holomorphic_on S  g holomorphic_on ball 0 1 
               (z  S. f z  ball 0 1  g(f z) = z) 
               (z  ball 0 1. g z  S  f(g z) = z)"
proof -
  define F where "F  {h. h holomorphic_on S  h ` S  ball 0 1  h 0 = 0  inj_on h S}"
  have idF: "id  F"
    using S01 by (auto simp: F_def)
  then have "F  {}"
    by blast
  have imF_ne: "((λh. norm(deriv h 0)) ` F)  {}"
    using idF by auto
  have holF: "h. h  F  h holomorphic_on S"
    by (auto simp: F_def)
  obtain f where "f  F" and normf: "h. h  F  norm(deriv h 0)  norm(deriv f 0)"
  proof -
    obtain r where "r > 0" and r: "ball 0 r  S"
      using open S 0  S openE by auto
    have bdd: "bdd_above ((λh. norm(deriv h 0)) ` F)"
    proof (intro bdd_aboveI exI ballI, clarify)
      show "norm (deriv f 0)  1 / r" if "f  F" for f
      proof -
        have r01: "(*) (complex_of_real r) ` ball 0 1  S"
          using that r > 0 by (auto simp: norm_mult r [THEN subsetD])
        then have "f holomorphic_on (*) (complex_of_real r) ` ball 0 1"
          using holomorphic_on_subset [OF holF] by (simp add: that)
        then have holf: "f  (λz. (r * z)) holomorphic_on (ball 0 1)"
          by (intro holomorphic_intros holomorphic_on_compose)
        have f0: "(f  (*) (complex_of_real r)) 0 = 0"
          using F_def that by auto
        have "f ` S  ball 0 1"
          using F_def that by blast
        with r01 have fr1: "z. norm z < 1  norm ((f  (*)(of_real r))z) < 1"
          by force
        have *: "((λw. f (r * w)) has_field_derivative deriv f (r * z) * r) (at z)"
          if "z  ball 0 1" for z::complex
        proof (rule DERIV_chain' [where g=f])
          show "(f has_field_derivative deriv f (of_real r * z)) (at (of_real r * z))"
            by (metis holomorphic_derivI [OF holF open S] f  F image_subset_iff r01 that)
        qed simp
        have df0: "((λw. f (r * w)) has_field_derivative deriv f 0 * r) (at 0)"
          using * [of 0] by simp
        have deq: "deriv (λx. f (complex_of_real r * x)) 0 = deriv f 0 * complex_of_real r"
          using DERIV_imp_deriv df0 by blast
        have "norm (deriv (f  (*) (complex_of_real r)) 0)  1"
          by (auto intro: Schwarz_Lemma [OF holf f0 fr1, of 0])
        with r > 0 show ?thesis
          by (simp add: deq norm_mult divide_simps o_def)
      qed
    qed
    define l where "l  SUP hF. norm (deriv h 0)"
    have eql: "norm (deriv f 0) = l" if le: "l  norm (deriv f 0)" and "f  F" for f
    proof (rule order_antisym [OF _ le])
      show "cmod (deriv f 0)  l"
        using f  F bdd cSUP_upper by (fastforce simp: l_def)
    qed
    obtain  where ℱin: "n.  n  F" and ℱlim: "(λn. norm (deriv ( n) 0))  l"
    proof -
      have "f. f  F  ¦norm (deriv f 0) - l¦ < 1 / (Suc n)" for n
      proof -
        obtain f where "f  F" and f: "l < norm (deriv f 0) + 1/(Suc n)"
          using cSup_least [OF imF_ne, of "l - 1/(Suc n)"] by (fastforce simp: l_def)
        then have "¦norm (deriv f 0) - l¦ < 1 / (Suc n)"
          by (fastforce simp: abs_if not_less eql)
        with f  F show ?thesis
          by blast
      qed
      then obtain  where fF: "n. ( n)  F"
        and fless:  "n. ¦norm (deriv ( n) 0) - l¦ < 1 / (Suc n)"
        by metis
      have "(λn. norm (deriv ( n) 0))  l"
      proof (rule metric_LIMSEQ_I)
        fix e::real
        assume "e > 0"
        then obtain N::nat where N: "e > 1/(Suc N)"
          using nat_approx_posE by blast
        show "N. nN. dist (norm (deriv ( n) 0)) l < e"
        proof (intro exI allI impI)
          fix n assume "N  n"
          have "dist (norm (deriv ( n) 0)) l < 1 / (Suc n)"
            using fless by (simp add: dist_norm)
          also have " < e"
            using N N  n inverse_of_nat_le le_less_trans by blast
          finally show "dist (norm (deriv ( n) 0)) l < e" .
        qed
      qed
      with fF show ?thesis
        using that by blast
    qed
    have "K. compact K; K  S  B. hF. zK. norm (h z)  B"
      by (rule_tac x=1 in exI) (force simp: F_def)
    moreover have "range   F"
      using n.  n  F by blast
    ultimately obtain f and r :: "nat  nat"
      where holf: "f holomorphic_on S" and r: "strict_mono r"
        and limf: "x. x  S  (λn.  (r n) x)  f x"
        and ulimf: "K. compact K; K  S  uniform_limit K (  r) f sequentially"
      using Montel [of S F , OF open S holF] by auto+
    have der: "n x. x  S  ((  r) n has_field_derivative ((λn. deriv ( n))  r) n x) (at x)"
      using n.  n  F open S holF holomorphic_derivI by fastforce
    have ulim: "x. x  S  d>0. cball x d  S  uniform_limit (cball x d) (  r) f sequentially"
      by (meson ulimf open S compact_cball open_contains_cball)
    obtain f' :: "complexcomplex" where f': "(f has_field_derivative f' 0) (at 0)"
      and tof'0: "(λn. ((λn. deriv ( n))  r) n 0)  f' 0"
      using has_complex_derivative_uniform_sequence [OF open S der ulim] 0  S by metis
    then have derf0: "deriv f 0 = f' 0"
      by (simp add: DERIV_imp_deriv)
    have "f field_differentiable (at 0)"
      using field_differentiable_def f' by blast
    have "(λx.  (norm (deriv ( (r x)) 0)))  norm (deriv f 0)"
      using isCont_tendsto_compose [OF continuous_norm [OF continuous_ident] tof'0] derf0 by auto
    with LIMSEQ_subseq_LIMSEQ [OF ℱlim r] have no_df0: "norm(deriv f 0) = l"
      by (force simp: o_def intro: tendsto_unique)
    have nonconstf: "¬ f constant_on S"
      using open S 0  S no_df0 holomorphic_nonconstant [OF holf] eql [OF _ idF]
      by force
    show ?thesis
    proof
      show "f  F"
        unfolding F_def
      proof (intro CollectI conjI holf)
        have "norm(f z)  1" if "z  S" for z
        proof (intro Lim_norm_ubound [OF _ limf] always_eventually allI that)
          fix n
          have " (r n)  F"
            by (simp add: ℱin)
          then show "norm ( (r n) z)  1"
            using that by (auto simp: F_def)
        qed simp
        then have fless1: "norm(f z) < 1" if "z  S" for z
          using maximum_modulus_principle [OF holf open S connected S open S] nonconstf that
          by fastforce
        then show "f ` S  ball 0 1"
          by auto
        have "(λn.  (r n) 0)  0"
          using ℱin by (auto simp: F_def)
        then show "f 0 = 0"
          using tendsto_unique [OF _ limf ] 0  S trivial_limit_sequentially by blast
        show "inj_on f S"
        proof (rule Hurwitz_injective [OF open S connected S _ holf])
          show "n. (  r) n holomorphic_on S"
            by (simp add: ℱin holF)
          show "K. compact K; K  S  uniform_limit K(  r) f sequentially"
            by (metis ulimf)
          show "¬ f constant_on S"
            using nonconstf by auto
          show "n. inj_on ((  r) n) S"
            using ℱin by (auto simp: F_def)
        qed
      qed
      show "h. h  F  norm (deriv h 0)  norm (deriv f 0)"
        by (metis eql le_cases no_df0)
    qed
  qed
  have holf: "f holomorphic_on S" and injf: "inj_on f S" and f01: "f ` S  ball 0 1"
    using f  F by (auto simp: F_def)
  obtain g where holg: "g holomorphic_on (f ` S)"
             and derg: "z. z  S  deriv f z * deriv g (f z) = 1"
             and gf: "z. z  S  g(f z) = z"
    using holomorphic_has_inverse [OF holf open S injf] by metis
  have "ball 0 1  f ` S"
  proof
    fix a::complex
    assume a: "a  ball 0 1"
    have False if "x. x  S  f x  a"
    proof -
      obtain h k where "h a = 0"
        and holh: "h holomorphic_on ball 0 1" and h01: "h ` ball 0 1  ball 0 1"
        and holk: "k holomorphic_on ball 0 1" and k01: "k ` ball 0 1  ball 0 1"
        and hk: "z. z  ball 0 1  h (k z) = z"
        and kh: "z. z  ball 0 1  k (h z) = z"
        using ball_biholomorphism_exists [OF a] by blast
      have nf1: "z. z  S  norm(f z) < 1"
        using f  F by (auto simp: F_def)
      have 1: "h  f holomorphic_on S"
        using F_def f  F holh holomorphic_on_compose holomorphic_on_subset by blast
      have 2: "z. z  S  (h  f) z  0"
        by (metis h a = 0 a comp_eq_dest_lhs nf1 kh mem_ball_0 that)
      have 3: "inj_on (h  f) S"
        by (metis (no_types, lifting) F_def f  F comp_inj_on inj_on_inverseI injf kh mem_Collect_eq subset_inj_on)
      obtain ψ where holψ: "ψ holomorphic_on ((h  f) ` S)"
        and ψ2: "z. z  S   ψ(h (f z)) ^ 2 = h(f z)"
      proof (rule exE [OF prev [OF 1 2 3]], safe)
        fix θ
        assume holθ: "θ holomorphic_on S" and θ2: "(zS. (h  f) z = (θ z)2)"
        show thesis
        proof
          show "(θ  g  k) holomorphic_on (h  f) ` S"
          proof (intro holomorphic_on_compose)
            show "k holomorphic_on (h  f) ` S"
              using holomorphic_on_subset [OF holk] f01 h01 by force
            show "g holomorphic_on k ` (h  f) ` S"
              using holomorphic_on_subset [OF holg] by (force simp: kh nf1)
            show "θ holomorphic_on g ` k ` (h  f) ` S"
              using holomorphic_on_subset [OF holθ] by (force simp: gf kh nf1)
          qed
          show "((θ  g  k) (h (f z)))2 = h (f z)" if "z  S" for z
            using θ2 gf kh nf1 that by fastforce
        qed
      qed
      have normψ1: "norm(ψ (h (f z))) < 1" if "z  S" for z
      proof -
        have "norm (ψ (h (f z)) ^ 2) < 1"
          by (metis (no_types) that DIM_complex ψ2 h01 image_subset_iff mem_ball_0 nf1)
        then show ?thesis
          by (metis le_less_trans mult_less_cancel_left2 norm_ge_zero norm_power not_le power2_eq_square)
      qed
      then have ψ01: "ψ (h (f 0))  ball 0 1"
        by (simp add: 0  S)
      obtain p q where p0: "p (ψ (h (f 0))) = 0"
        and holp: "p holomorphic_on ball 0 1" and p01: "p ` ball 0 1  ball 0 1"
        and holq: "q holomorphic_on ball 0 1" and q01: "q ` ball 0 1  ball 0 1"
        and pq: "z. z  ball 0 1  p (q z) = z"
        and qp: "z. z  ball 0 1  q (p z) = z"
        using ball_biholomorphism_exists [OF ψ01] by metis
      have "p  ψ  h  f  F"
        unfolding F_def
      proof (intro CollectI conjI holf)
        show "p  ψ  h  f holomorphic_on S"
        proof (intro holomorphic_on_compose holf)
          show "h holomorphic_on f ` S"
            using holomorphic_on_subset [OF holh] f01 by fastforce
          show "ψ holomorphic_on h ` f ` S"
            using holomorphic_on_subset [OF holψ] by fastforce
          show "p holomorphic_on ψ ` h ` f ` S"
            using holomorphic_on_subset [OF holp] by (simp add: image_subset_iff normψ1)
        qed
        show "(p  ψ  h  f) ` S  ball 0 1"
          using normψ1 p01 by fastforce
        show "(p  ψ  h  f) 0 = 0"
          by (simp add: p (ψ (h (f 0))) = 0)
        show "inj_on (p  ψ  h  f) S"
          unfolding inj_on_def o_def
          by (metis ψ2 dist_0_norm gf kh mem_ball nf1 normψ1 qp)
      qed
      then have le_norm_df0: "norm (deriv (p  ψ  h  f) 0)  norm (deriv f 0)"
        by (rule normf)
      have 1: "k  power2  q holomorphic_on ball 0 1"
      proof (intro holomorphic_on_compose holq)
        show "power2 holomorphic_on q ` ball 0 1"
          using holomorphic_on_subset holomorphic_on_power
          by (blast intro: holomorphic_on_ident)
        show "k holomorphic_on power2 ` q ` ball 0 1"
          using q01  holomorphic_on_subset [OF holk] 
          by (force simp: norm_power abs_square_less_1)
      qed
      have 2: "(k  power2  q) 0 = 0"
        using p0 F_def f  F ψ01 ψ2 0  S kh qp by force
      have 3: "norm ((k  power2  q) z) < 1" if "norm z < 1" for z
      proof -
        have "norm ((power2  q) z) < 1"
          using that q01 by (force simp: norm_power abs_square_less_1)
        with k01 show ?thesis
          by fastforce
      qed
      have False if c: "z. norm z < 1  (k  power2  q) z = c * z" and "norm c = 1" for c
      proof -
        have "c  0" using that by auto
        have "norm (p(1/2)) < 1" "norm (p(-1/2)) < 1"
          using p01 by force+
        then have "(k  power2  q) (p(1/2)) = c * p(1/2)" "(k  power2  q) (p(-1/2)) = c * p(-1/2)"
          using c by force+
        then have "p (1/2) = p (- (1/2))"
          by (auto simp: c  0 qp o_def)
        then have "q (p (1/2)) = q (p (- (1/2)))"
          by simp
        then have "1/2 = - (1/2::complex)"
          by (auto simp: qp)
        then show False
          by simp
      qed
      moreover
      have False if "norm (deriv (k  power2  q) 0)  1" "norm (deriv (k  power2  q) 0)  1"
        and le: "ξ. norm ξ < 1  norm ((k  power2  q) ξ)  norm ξ"
      proof -
        have "norm (deriv (k  power2  q) 0) < 1"
          using that by simp
        moreover have eq: "deriv f 0 = deriv (k  (λz. z ^ 2)  q) 0 * deriv (p  ψ  h  f) 0"
        proof (intro DERIV_imp_deriv has_field_derivative_transform_within_open [OF DERIV_chain])
          show "(k  power2  q has_field_derivative deriv (k  power2  q) 0) (at ((p  ψ  h  f) 0))"
            using "1" holomorphic_derivI p0 by auto
          show "(p  ψ  h  f has_field_derivative deriv (p  ψ  h  f) 0) (at 0)"
            using p  ψ  h  f  F open S 0  S holF holomorphic_derivI by blast
          show "x. x  S  (k  power2  q  (p  ψ  h  f)) x = f x"
            using ψ2 f01 kh normψ1 qp by auto
        qed (use assms in simp_all)
        ultimately have "cmod (deriv (p  ψ  h  f) 0)  0"
          using le_norm_df0
          by (metis linorder_not_le mult.commute mult_less_cancel_left2 norm_mult)
        moreover have "1  norm (deriv f 0)"
          using normf [of id] by (simp add: idF)
        ultimately show False
          by (simp add: eq)
      qed
      ultimately show ?thesis
        using Schwarz_Lemma [OF 1 2 3] norm_one by blast
    qed
    then show "a  f ` S"
      by blast
  qed
  then have fS: "f ` S = ball 0 1"
    using F_def f  F by blast
  then have "zball 0 1. g z  S  f (g z) = z"
    by (metis  gf imageE)
  with fS show ?thesis
    by (metis gf holf holg image_eqI)
qed


locale SC_Chain =
  fixes S :: "complex set"
  assumes openS: "open S"
begin

lemma winding_number_zero:
  assumes "simply_connected S"
  shows "connected S 
         (γ z. path γ  path_image γ  S 
                   pathfinish γ = pathstart γ  z  S  winding_number γ z = 0)"
  using assms
  by (auto simp: simply_connected_imp_connected simply_connected_imp_winding_number_zero)

lemma contour_integral_zero:
  assumes "valid_path g" "path_image g  S" "pathfinish g = pathstart g" "f holomorphic_on S"
         "γ z. path γ; path_image γ  S; pathfinish γ = pathstart γ; z  S  winding_number γ z = 0"
  shows "(f has_contour_integral 0) g"
  using assms by (meson Cauchy_theorem_global openS valid_path_imp_path)

lemma global_primitive:
  assumes "connected S" and holf: "f holomorphic_on S"
  and prev: "γ f. valid_path γ; path_image γ  S; pathfinish γ = pathstart γ; f holomorphic_on S  (f has_contour_integral 0) γ"
  shows "h. z  S. (h has_field_derivative f z) (at z)"
proof (cases "S = {}")
case True then show ?thesis
    by simp
next
  case False
  then obtain a where "a  S"
    by blast
  show ?thesis
  proof (intro exI ballI)
    fix x assume "x  S"
    then obtain d where "d > 0" and d: "cball x d  S"
      using openS open_contains_cball_eq by blast
    let ?g = "λz. (SOME g. polynomial_function g  path_image g  S  pathstart g = a  pathfinish g = z)"
    show "((λz. contour_integral (?g z) f) has_field_derivative f x)
          (at x)"
    proof (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right, rule Lim_transform)
      show "(λy. inverse(norm(y - x)) *R (contour_integral(linepath x y) f - f x * (y - x))) x 0"
      proof (clarsimp simp add: Lim_at)
        fix e::real assume "e > 0"
        moreover have "continuous (at x) f"
          using openS x  S holf continuous_on_eq_continuous_at holomorphic_on_imp_continuous_on by auto
        ultimately obtain d1 where "d1 > 0"
             and d1: "x'. dist x' x < d1  dist (f x') (f x) < e/2"
          unfolding continuous_at_eps_delta
          by (metis less_divide_eq_numeral1(1) mult_zero_left)
        obtain d2 where "d2 > 0" and d2: "ball x d2  S"
          using openS x  S open_contains_ball_eq by blast
        have "inverse (norm (y - x)) * norm (contour_integral (linepath x y) f - f x * (y - x)) < e"
          if "0 < d1" "0 < d2" "y  x" "dist y x < d1" "dist y x < d2" for y
        proof -
          have "f contour_integrable_on linepath x y"
          proof (rule contour_integrable_continuous_linepath [OF continuous_on_subset])
            show "continuous_on S f"
              by (simp add: holf holomorphic_on_imp_continuous_on)
            have "closed_segment x y  ball x d2"
              by (meson dist_commute_lessI dist_in_closed_segment le_less_trans mem_ball subsetI that(5))
            with d2 show "closed_segment x y  S"
              by blast
          qed
          then obtain z where z: "(f has_contour_integral z) (linepath x y)"
            by (force simp: contour_integrable_on_def)
          have con: "((λw. f x) has_contour_integral f x * (y - x)) (linepath x y)"
            using has_contour_integral_const_linepath [of "f x" y x] by metis
          have "norm (z - f x * (y - x))  (e/2) * norm (y - x)"
          proof (rule has_contour_integral_bound_linepath)
            show "((λw. f w - f x) has_contour_integral z - f x * (y - x)) (linepath x y)"
              by (rule has_contour_integral_diff [OF z con])
            show "w. w  closed_segment x y  norm (f w - f x)  e/2"
              by (metis d1 dist_norm less_le_trans not_less not_less_iff_gr_or_eq segment_bound1 that(4))
          qed (use e > 0 in auto)
          with e > 0 have "inverse (norm (y - x)) * norm (z - f x * (y - x))  e/2"
            by (simp add: field_split_simps)
          also have " < e"
            using e > 0 by simp
          finally show ?thesis
            by (simp add: contour_integral_unique [OF z])
        qed
        with  d1 > 0 d2 > 0
        show "d>0. z. z  x  dist z x < d 
                 inverse (norm (z - x)) * norm (contour_integral (linepath x z) f - f x * (z - x)) < e"
          by (rule_tac x="min d1 d2" in exI) auto
      qed
    next
      have *: "(1 / norm (y - x)) *R (contour_integral (?g y) f -
               (contour_integral (?g x) f + f x * (y - x))) =
               (contour_integral (linepath x y) f - f x * (y - x)) /R norm (y - x)"
        if "0 < d" "y  x" and yx: "dist y x < d" for y
      proof -
        have "y  S"
          by (metis subsetD d dist_commute less_eq_real_def mem_cball yx)
        have gxy: "polynomial_function (?g x)  path_image (?g x)  S  pathstart (?g x) = a  pathfinish (?g x) = x"
                  "polynomial_function (?g y)  path_image (?g y)  S  pathstart (?g y) = a  pathfinish (?g y) = y"
          using someI_ex [OF connected_open_polynomial_connected [OF openS connected S a  S]] x  S y  S
          by meson+
        then have vp: "valid_path (?g x)" "valid_path (?g y)"
          by (simp_all add: valid_path_polynomial_function)
        have f0: "(f has_contour_integral 0) ((?g x) +++ linepath x y +++ reversepath (?g y))"
        proof (rule prev)
          show "valid_path ((?g x) +++ linepath x y +++ reversepath (?g y))"
            using gxy vp by (auto simp: valid_path_join)
          have "closed_segment x y  cball x d"
            using  yx by (auto simp: dist_commute dest!: dist_in_closed_segment)
          then have "closed_segment x y  S"
            using d by blast
          then show "path_image ((?g x) +++ linepath x y +++ reversepath (?g y))  S"
            using gxy by (auto simp: path_image_join)
        qed (use gxy holf in auto)
        then have fintxy: "f contour_integrable_on linepath x y"
          by (metis (no_types, lifting) contour_integrable_joinD1 contour_integrable_joinD2 gxy(2) has_contour_integral_integrable pathfinish_linepath pathstart_reversepath valid_path_imp_reverse valid_path_join valid_path_linepath vp(2))
        have fintgx: "f contour_integrable_on (?g x)" "f contour_integrable_on (?g y)"
          using openS contour_integrable_holomorphic_simple gxy holf vp by blast+
        show ?thesis
          apply (clarsimp simp add: divide_simps)
          using contour_integral_unique [OF f0]
          apply (simp add: fintxy gxy contour_integrable_reversepath contour_integral_reversepath fintgx vp)
          apply (simp add: algebra_simps)
          done
      qed
      show "(λz. (1 / norm (z - x)) *R
                 (contour_integral (?g z) f - (contour_integral (?g x) f + f x * (z - x))) -
                 (contour_integral (linepath x z) f - f x * (z - x)) /R norm (z - x))
            x 0"
        apply (rule tendsto_eventually)
        apply (simp add: eventually_at)
        apply (rule_tac x=d in exI)
        using d > 0 * by simp
    qed
  qed
qed

lemma holomorphic_log:
  assumes "connected S" and holf: "f holomorphic_on S" and nz: "z. z  S  f z  0"
  and prev: "f. f holomorphic_on S  h. z  S. (h has_field_derivative f z) (at z)"
  shows "g. g holomorphic_on S  (z  S. f z = exp(g z))"
proof -
  have "(λz. deriv f z / f z) holomorphic_on S"
    by (simp add: openS holf holomorphic_deriv holomorphic_on_divide nz)
  then obtain g where g: "z. z  S  (g has_field_derivative deriv f z / f z) (at z)"
    using prev [of "λz. deriv f z / f z"] by metis
  have Df: "x. x  S  DERIV f x :> deriv f x"
    using holf holomorphic_derivI openS by force
  have hfd: "x. x  S  ((λz. exp (g z) / f z) has_field_derivative 0) (at x)"
    by (rule derivative_eq_intros Df g nz| simp)+
  obtain c where c: "x. x  S  exp (g x) / f x = c"
  proof (rule DERIV_zero_connected_constant[OF connected S openS finite.emptyI])
    show "continuous_on S (λz. exp (g z) / f z)"
      by (metis (full_types) openS g continuous_on_divide continuous_on_exp holf holomorphic_on_imp_continuous_on holomorphic_on_open nz)
    then show "xS - {}. ((λz. exp (g z) / f z) has_field_derivative 0) (at x)"
      using hfd by (blast intro: DERIV_zero_connected_constant [OF connected S openS finite.emptyI, of "λz. exp(g z) / f z"])
  qed auto
  show ?thesis
  proof (intro exI ballI conjI)
    have "g holomorphic_on S"
      using openS g holomorphic_on_open by blast
    then show "(λz. Ln(inverse c) + g z) holomorphic_on S"
      by (intro holomorphic_intros)
    fix z :: complex
    assume "z  S"
    then have "exp (g z) / c = f z"
      by (metis c divide_divide_eq_right exp_not_eq_zero nonzero_mult_div_cancel_left)
    moreover have "1 / c  0"
      using z  S c nz by fastforce
    ultimately show "f z = exp (Ln (inverse c) + g z)"
      by (simp add: exp_add inverse_eq_divide)
  qed
qed

lemma holomorphic_sqrt:
  assumes holf: "f holomorphic_on S" and nz: "z. z  S  f z  0"
  and prev: "f. f holomorphic_on S; z  S. f z  0  g. g holomorphic_on S  (z  S. f z = exp(g z))"
  shows "g. g holomorphic_on S  (z  S. f z = (g z)2)"
proof -
  obtain g where holg: "g holomorphic_on S" and g: "z. z  S  f z = exp (g z)"
    using prev [of f] holf nz by metis
  show ?thesis
  proof (intro exI ballI conjI)
    show "(λz. exp(g z/2)) holomorphic_on S"
      by (intro holomorphic_intros) (auto simp: holg)
    show "z. z  S  f z = (exp (g z/2))2"
      by (metis (no_types) g exp_double nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral)
  qed
qed

lemma biholomorphic_to_disc:
  assumes "connected S" and S: "S  {}" "S  UNIV"
  and prev: "f. f holomorphic_on S; z  S. f z  0  g. g holomorphic_on S  (z  S. f z = (g z)2)"
  shows "f g. f holomorphic_on S  g holomorphic_on ball 0 1 
                   (z  S. f z  ball 0 1  g(f z) = z) 
                   (z  ball 0 1. g z  S  f(g z) = z)"
proof -
  obtain a b where "a  S" "b  S"
    using S by blast
  then obtain δ where "δ > 0" and δ: "ball a δ  S"
    using openS openE by blast
  obtain g where holg: "g holomorphic_on S" and eqg: "z. z  S  z - b = (g z)2"
  proof (rule exE [OF prev [of "λz. z - b"]])
    show "(λz. z - b) holomorphic_on S"
      by (intro holomorphic_intros)
  qed (use b  S in auto)
  have "¬ g constant_on S"
  proof -
    have "(a + δ/2)  ball a δ" "a + (δ/2)  a"
      using δ > 0 by (simp_all add: dist_norm)
    then show ?thesis
      unfolding constant_on_def
      using eqg [of a] eqg [of "a + δ/2"] a  S δ
      by (metis diff_add_cancel subset_eq)
  qed
  then have "open (g ` ball a δ)"
    using open_mapping_thm [of g S "ball a δ", OF holg openS connected S] δ by blast
  then obtain r where "r > 0" and r: "ball (g a) r  (g ` ball a δ)"
    by (metis 0 < δ centre_in_ball imageI openE)
  have g_not_r: "g z  ball (-(g a)) r" if "z  S" for z
  proof
    assume "g z  ball (-(g a)) r"
    then have "- g z  ball (g a) r"
      by (metis add.inverse_inverse dist_minus mem_ball)
    with r have "- g z  (g ` ball a δ)"
      by blast
    then obtain w where w: "- g z = g w" "dist a w < δ"
      by auto
    with δ have "w  S"
      by force
    then have "w = z"
      by (metis diff_add_cancel eqg power_minus_Bit0 that w(1))
    then have "g z = 0"
      using - g z = g w by auto
    with eqg that b  S show False
      by force
  qed
  then have nz: "z. z  S  g z + g a  0"
    by (metis 0 < r add.commute add_diff_cancel_left' centre_in_ball diff_0)
  let ?f = "λz. (r/3) / (g z + g a) - (r/3) / (g a + g a)"
  obtain h where holh: "h holomorphic_on S" and "h a = 0" and h01: "h ` S  ball 0 1" and "inj_on h S"
  proof
    show "?f holomorphic_on S"
      by (intro holomorphic_intros holg nz)
    have 3: "norm x  1/3; norm y  1/3  norm(x - y) < 1" for x y::complex
      using norm_triangle_ineq4 [of x y] by simp
    have "norm ((r/3) / (g z + g a) - (r/3) / (g a + g a)) < 1" if "z  S" for z
      apply (rule 3)
      unfolding norm_divide
      using r > 0 g_not_r [OF z  S] g_not_r [OF a  S]
      by (simp_all add: field_split_simps dist_commute dist_norm)
  then show "?f ` S  ball 0 1"
    by auto
    show "inj_on ?f S"
      using r > 0 eqg apply (clarsimp simp: inj_on_def)
      by (metis diff_add_cancel)
  qed auto
  obtain k where holk: "k holomorphic_on (h ` S)"
             and derk: "z. z  S  deriv h z * deriv k (h z) = 1"
             and kh: "z. z  S  k(h z) = z"
    using holomorphic_has_inverse [OF holh openS inj_on h S] by metis

  have 1: "open (h ` S)"
    by (simp add: inj_on h S holh openS open_mapping_thm3)
  have 2: "connected (h ` S)"
    by (simp add: connected_continuous_image connected S holh holomorphic_on_imp_continuous_on)
  have 3: "0  h ` S"
    using a  S h a = 0 by auto
  have 4: "g. g holomorphic_on h ` S  (zh ` S. f z = (g z)2)"
    if holf: "f holomorphic_on h ` S" and nz: "z. z  h ` S  f z  0" "inj_on f (h ` S)" for f
  proof -
    obtain g where holg: "g holomorphic_on S" and eqg: "z. z  S  (f  h) z = (g z)2"
      by (smt (verit) comp_def holf holh holomorphic_on_compose image_eqI nz(1) prev)
    show ?thesis
    proof (intro exI conjI)
      show "g  k holomorphic_on h ` S"
        by (smt (verit) holg holk holomorphic_on_compose holomorphic_on_subset imageE image_subset_iff kh)
      show "zh ` S. f z = ((g  k) z)2"
        using eqg kh by auto
    qed
  qed
  obtain f g where f: "f holomorphic_on h ` S" and g: "g holomorphic_on ball 0 1"
       and gf: "zh ` S. f z  ball 0 1  g (f z) = z"  and fg:"zball 0 1. g z  h ` S  f (g z) = z"
    using biholomorphic_to_disc_aux [OF 1 2 3 h01 4] by blast
  show ?thesis
  proof (intro exI conjI)
    show "f  h holomorphic_on S"
      by (simp add: f holh holomorphic_on_compose)
    show "k  g holomorphic_on ball 0 1"
      by (metis holomorphic_on_subset image_subset_iff fg holk g holomorphic_on_compose)
  qed (use fg gf kh in auto)
qed

lemma homeomorphic_to_disc:
  assumes S: "S  {}"
    and prev: "S = UNIV 
               (f g. f holomorphic_on S  g holomorphic_on ball 0 1 
                     (z  S. f z  ball 0 1  g(f z) = z) 
                     (z  ball 0 1. g z  S  f(g z) = z))" (is "_  ?P")
  shows "S homeomorphic ball (0::complex) 1"
  using prev
proof
  assume "S = UNIV" then show ?thesis
    using homeomorphic_ball01_UNIV homeomorphic_sym by blast
next
  assume ?P
  then show ?thesis
    unfolding homeomorphic_minimal
    using holomorphic_on_imp_continuous_on by blast
qed

lemma homeomorphic_to_disc_imp_simply_connected:
  assumes "S = {}  S homeomorphic ball (0::complex) 1"
  shows "simply_connected S"
  using assms homeomorphic_simply_connected_eq convex_imp_simply_connected by auto

end

proposition
  assumes "open S"
  shows simply_connected_eq_winding_number_zero:
         "simply_connected S 
           connected S 
           (g z. path g  path_image g  S 
                 pathfinish g = pathstart g  (z  S)
                  winding_number g z = 0)" (is "?wn0")
    and simply_connected_eq_contour_integral_zero:
         "simply_connected S 
           connected S 
           (g f. valid_path g  path_image g  S 
                 pathfinish g = pathstart g  f holomorphic_on S
                (f has_contour_integral 0) g)" (is "?ci0")
    and simply_connected_eq_global_primitive:
         "simply_connected S 
           connected S 
           (f. f holomorphic_on S 
                (h. z. z  S  (h has_field_derivative f z) (at z)))" (is "?gp")
    and simply_connected_eq_holomorphic_log:
         "simply_connected S 
           connected S 
           (f. f holomorphic_on S  (z  S. f z  0)
                (g. g holomorphic_on S  (z  S. f z = exp(g z))))" (is "?log")
    and simply_connected_eq_holomorphic_sqrt:
         "simply_connected S 
           connected S 
           (f. f holomorphic_on S  (z  S. f z  0)
                 (g. g holomorphic_on S  (z  S.  f z = (g z)2)))" (is "?sqrt")
    and simply_connected_eq_biholomorphic_to_disc:
         "simply_connected S 
           S = {}  S = UNIV 
           (f g. f holomorphic_on S  g holomorphic_on ball 0 1 
                 (z  S. f z  ball 0 1  g(f z) = z) 
                 (z  ball 0 1. g z  S  f(g z) = z))" (is "?bih")
    and simply_connected_eq_homeomorphic_to_disc:
          "simply_connected S  S = {}  S homeomorphic ball (0::complex) 1" (is "?disc")
proof -
  interpret SC_Chain
    using assms by (simp add: SC_Chain_def)
  have "?wn0  ?ci0  ?gp  ?log  ?sqrt  ?bih  ?disc"
proof -
  have *: "α  β; β  γ; γ  δ; δ  ζ; ζ  η; η  θ; θ  ξ; ξ  α
         (α  β)  (α  γ)  (α  δ)  (α  ζ) 
            (α  η)  (α  θ)  (α  ξ)" for α β γ δ ζ η θ ξ
    by blast
  show ?thesis
    apply (rule *)
    using winding_number_zero apply metis
    using contour_integral_zero apply metis
    using global_primitive apply metis
    using holomorphic_log apply metis
    using holomorphic_sqrt apply simp
    using biholomorphic_to_disc apply blast
    using homeomorphic_to_disc apply blast
    using homeomorphic_to_disc_imp_simply_connected apply blast
    done
qed
  then show ?wn0 ?ci0 ?gp ?log ?sqrt ?bih ?disc
    by safe
qed

corollary contractible_eq_simply_connected_2d:
  fixes S :: "complex set"
  assumes "open S"
  shows "contractible S  simply_connected S"
proof
  show "contractible S  simply_connected S"
    by (simp add: contractible_imp_simply_connected)
  show "simply_connected S  contractible S"
    using assms convex_imp_contractible homeomorphic_contractible_eq 
      simply_connected_eq_homeomorphic_to_disc by auto
qed

subsection‹A further chain of equivalences about components of the complement of a simply connected set›

text‹(following 1.35 in Burckel'S book)›

context SC_Chain
begin

lemma frontier_properties:
  assumes "simply_connected S"
  shows "if bounded S then connected(frontier S)
         else C  components(frontier S). ¬ bounded C"
proof -
  have "S = {}  S homeomorphic ball (0::complex) 1"
    using simply_connected_eq_homeomorphic_to_disc assms openS by blast
  then show ?thesis
  proof
    assume "S = {}"
    then show ?thesis
      by simp
  next
    assume S01: "S homeomorphic ball (0::complex) 1"
    then obtain g f
      where gim: "g ` S = ball 0 1" and fg: "x. x  S  f(g x) = x"
        and fim: "f ` ball 0 1 = S" and gf: "y. cmod y < 1  g(f y) = y"
        and contg: "continuous_on S g" and contf: "continuous_on (ball 0 1) f"
      by (fastforce simp: homeomorphism_def homeomorphic_def)
    define D where "D  λn. ball (0::complex) (1 - 1/(of_nat n + 2))"
    define A where "A  λn. {z::complex. 1 - 1/(of_nat n + 2) < norm z  norm z < 1}"
    define X where "X  λn::nat. closure(f ` A n)"
    have D01: "D n  ball 0 1" for n
      by (simp add: D_def ball_subset_ball_iff)
    have A01: "A n  ball 0 1" for n
      by (auto simp: A_def)
    have cloX: "closed(X n)" for n
      by (simp add: X_def)
    have Xsubclo: "X n  closure S" for n
      unfolding X_def by (metis A01 closure_mono fim image_mono)
    have "connected (A n)" for n
      using connected_annulus [of _ "0::complex"] by (simp add: A_def)
    then have connX: "connected(X n)" for n
      unfolding X_def
      by (metis A01 connected_continuous_image connected_imp_connected_closure contf continuous_on_subset)
    have nestX: "X n  X m" if "m  n" for m n
    proof -
      have "1 - 1 / (real m + 2)  1 - 1 / (real n + 2)"
        using that by (auto simp: field_simps)
      then show ?thesis
        by (auto simp: X_def A_def intro!: closure_mono)
    qed
    have "closure S - S  (n. X n)"
    proof
      fix x
      assume "x  closure S - S"
      then have "x  closure S" "x  S" by auto
      show "x  (n. X n)"
      proof
        fix n
        have "ball 0 1 = closure (D n)  A n"
          by (auto simp: D_def A_def le_less_trans)
        with fim have Seq: "S = f ` (closure (D n))  f ` (A n)"
          by (simp add: image_Un)
        have "continuous_on (closure (D n)) f"
          by (simp add: D_def cball_subset_ball_iff continuous_on_subset [OF contf])
        moreover have "compact (closure (D n))"
          by (simp add: D_def)
        ultimately have clo_fim: "closed (f ` closure (D n))"
          using compact_continuous_image compact_imp_closed by blast
        have *: "(f ` cball 0 (1 - 1 / (real n + 2)))  S"
          by (force simp: D_def Seq)
        show "x  X n"
          using Seq X_def x  closure S x  S clo_fim by fastforce
      qed
    qed
    moreover have "(n. X n)  closure S - S"
    proof -
      have "(n. X n)  closure S"
        using Xsubclo by blast
      moreover have "(n. X n)  S  {}"
      proof (clarify, clarsimp simp: X_def fim [symmetric])
        fix x assume x [rule_format]: "n. f x  closure (f ` A n)" and "cmod x < 1"
        then obtain n where n: "1 / (1 - norm x) < of_nat n"
          using reals_Archimedean2 by blast
        with cmod x < 1 gr0I have XX: "1 / of_nat n < 1 - norm x" and "n > 0"
          by (fastforce simp: field_split_simps algebra_simps)+
        have "f x  f ` (D n)"
          using n cmod x < 1 by (auto simp: field_split_simps algebra_simps D_def)
        moreover have " f ` D n  closure (f ` A n) = {}"
        proof -
          have op_fDn: "open(f ` (D n))"
          proof (rule invariance_of_domain)
            show "continuous_on (D n) f"
              by (rule continuous_on_subset [OF contf D01])
            show "open (D n)"
              by (simp add: D_def)
            show "inj_on f (D n)"
              unfolding inj_on_def using D01 by (metis gf mem_ball_0 subsetCE)
          qed
          have injf: "inj_on f (ball 0 1)"
            by (metis mem_ball_0 inj_on_def gf)
          have "D n  A n  ball 0 1"
            using D01 A01 by simp
          moreover have "D n  A n = {}"
            by (auto simp: D_def A_def)
          ultimately have "f ` D n  f ` A n = {}"
            by (metis A01 D01 image_is_empty inj_on_image_Int injf)
          then show ?thesis
            by (simp add: open_Int_closure_eq_empty [OF op_fDn])
        qed
        ultimately show False
          using x [of n] by blast
      qed
      ultimately
      show "(n. X n)  closure S - S"
        using closure_subset disjoint_iff_not_equal by blast
    qed
    ultimately have "closure S - S = (n. X n)" by blast
    then have frontierS: "frontier S = (n. X n)"
      by (simp add: frontier_def openS interior_open)
    show ?thesis
    proof (cases "bounded S")
      case True
      have bouX: "bounded (X n)" for n
        by (meson True Xsubclo bounded_closure bounded_subset)
      have compaX: "compact (X n)" for n
        by (simp add: bouX cloX compact_eq_bounded_closed)
      have "connected (n. X n)"
        by (metis nestX compaX connX connected_nest)
      then show ?thesis
        by (simp add: True frontier S = (n. X n))
    next
      case False
      have unboundedX: "¬ bounded(X n)" for n
      proof
        assume bXn: "bounded(X n)"
        have "continuous_on (cball 0 (1 - 1 / (2 + real n))) f"
          by (simp add: cball_subset_ball_iff continuous_on_subset [OF contf])
        then have "bounded (f ` cball 0 (1 - 1 / (2 + real n)))"
          by (simp add: compact_imp_bounded [OF compact_continuous_image])
        moreover have "bounded (f ` A n)"
          by (auto simp: X_def closure_subset image_subset_iff bounded_subset [OF bXn])
        ultimately have "bounded (f ` (cball 0 (1 - 1/(2 + real n))  A n))"
          by (simp add: image_Un)
        then have "bounded (f ` ball 0 1)"
          apply (rule bounded_subset)
          apply (auto simp: A_def algebra_simps)
          done
        then show False
          using False by (simp add: fim [symmetric])
      qed
      have clo_INTX: "closed((range X))"
        by (metis cloX closed_INT)
      then have lcX: "locally compact ((range X))"
        by (metis closed_imp_locally_compact)
      have False if C: "C  components (frontier S)" and boC: "bounded C" for C
      proof -
        have "closed C"
          by (metis C closed_components frontier_closed)
        then have "compact C"
          by (metis boC compact_eq_bounded_closed)
        have Cco: "C  components ((range X))"
          by (metis frontierS C)
        obtain K where "C  K" "compact K"
                   and Ksub: "K  (range X)" and clo: "closed((range X) - K)"
        proof (cases "{k. C  k  compact k  openin (top_of_set ((range X))) k} = {}")
          case True
          then show ?thesis
            using Sura_Bura [OF lcX Cco compact C] boC
            by (simp add: True)
        next
          case False
          then obtain L where "compact L" "C  L" and K: "openin (top_of_set (x. X x)) L"
            by blast
          show ?thesis
          proof
            show "L  (range X)"
              by (metis K openin_imp_subset)
            show "closed ((range X) - L)"
              by (metis closedin_diff closedin_self closedin_closed_trans [OF _ clo_INTX] K)
          qed (use compact L C  L in auto)
        qed
        obtain U V where "open U" and "compact (closure U)" and "open V" "K  U"
                     and V: "(range X) - K  V" and "U  V = {}"
          using separation_normal_compact [OF compact K clo] by blast
        then have "U  ( (range X) - K) = {}"
          by blast
        have "(closure U - U)  (n. X n  closure U)  {}"
        proof (rule compact_imp_fip)
          show "compact (closure U - U)"
            by (metis compact (closure U) open U compact_diff)
          show "T. T  range (λn. X n  closure U)  closed T"
            by clarify (metis cloX closed_Int closed_closure)
          show "(closure U - U)    {}"
            if "finite " and : "  range (λn. X n  closure U)" for 
          proof
            assume empty: "(closure U - U)   = {}"
            obtain J where "finite J" and J: " = (λn. X n  closure U) ` J"
              using finite_subset_image [OF finite  ] by auto
            show False
            proof (cases "J = {}")
              case True
              with J empty have "closed U"
                by (simp add: closure_subset_eq)
              have "C  {}"
                using C in_components_nonempty by blast
              then have "U  {}"
                using K  U C  K by blast
              moreover have "U  UNIV"
                using compact (closure U) by auto
              ultimately show False
                using open U closed U clopen by blast
            next
              case False
              define j where "j  Max J"
              have "j  J"
                by (simp add: False finite J j_def)
              have jmax: "m. m  J  m  j"
                by (simp add: j_def finite J)
              have " ((λn. X n  closure U) ` J) = X j  closure U"
                using False jmax nestX j  J by auto
              then have XU: "X j  closure U = X j  U"
                using J closure_subset empty by fastforce
              then have "openin (top_of_set (X j)) (X j  closure U)"
                by (simp add: openin_open_Int open U)
              moreover have "closedin (top_of_set (X j)) (X j  closure U)"
                by (simp add: closedin_closed_Int)
              moreover have "X j  closure U  X j"
                by (metis unboundedX compact (closure U) bounded_subset compact_eq_bounded_closed inf.order_iff)
              moreover have "X j  closure U  {}"
                by (metis Cco Ksub UNIV_I C  K K  U XU bot.extremum_uniqueI in_components_maximal le_INF_iff le_inf_iff)
              ultimately show False
                using connX [of j] by (force simp: connected_clopen)
            qed
          qed
        qed
        moreover have "(n. X n  closure U) = (n. X n)  closure U"
          by blast
        moreover have "x  U" if "n. x  X n" "x  closure U" for x
        proof -
          have "x  V"
            using U  V = {} open V closure_iff_nhds_not_empty that(2) by blast
          then show ?thesis
            by (metis (no_types) Diff_iff INT_I V K  U subsetD that(1))
        qed
        ultimately show False
          by (auto simp: open_Int_closure_eq_empty [OF open V, of U])
      qed
      then show ?thesis
        by (auto simp: False)
    qed
  qed
qed


lemma unbounded_complement_components:
  assumes C: "C  components (- S)" and S: "connected S"
    and prev: "if bounded S then connected(frontier S)
               else C  components(frontier S). ¬ bounded C"
  shows "¬ bounded C"
proof (cases "bounded S")
  case True
  with prev have "S  UNIV" and confr: "connected(frontier S)"
    by auto
  obtain w where C_ccsw: "C = connected_component_set (- S) w" and "w  S"
    using C by (auto simp: components_def)
  show ?thesis
  proof (cases "S = {}")
    case True with C show ?thesis by auto
  next
    case False
    show ?thesis
    proof
      assume "bounded C"
      then have "outside C  {}"
        using outside_bounded_nonempty by metis
      then obtain z where z: "¬ bounded (connected_component_set (- C) z)" and "z  C"
        by (auto simp: outside_def)
      have clo_ccs: "closed (connected_component_set (- S) x)" for x
        by (simp add: closed_Compl closed_connected_component openS)
      have "connected_component_set (- S) w = connected_component_set (- S) z"
      proof (rule joinable_connected_component_eq [OF confr])
        show "frontier S  - S"
          using openS by (auto simp: frontier_def interior_open)
        have False if "connected_component_set (- S) w  frontier (- S) = {}"
        proof -
          have "C  frontier S = {}"
            using that by (simp add: C_ccsw)
          moreover have "closed C"
            using C_ccsw clo_ccs by blast
          ultimately show False
            by (metis C False S  UNIV C_ccsw bot_eq_sup_iff connected_component_eq_UNIV frontier_Int_closed
                frontier_closed frontier_complement frontier_eq_empty frontier_of_components_subset in_components_maximal inf.orderE)
        qed
        then show "connected_component_set (- S) w  frontier S  {}"
          by auto
        have *: "frontier C  C; frontier C  F; frontier C  {}  C  F  {}" for C F::"complex set"
          by blast
        have "connected_component_set (- S) z  frontier (- S)  {}"
        proof (rule *)
          show "frontier (connected_component_set (- S) z)  connected_component_set (- S) z"
            by (auto simp: closed_Compl closed_connected_component frontier_def openS)
          show "frontier (connected_component_set (- S) z)  frontier (- S)"
            using frontier_of_connected_component_subset by fastforce
          have "¬ bounded (-S)"
            by (simp add: True cobounded_imp_unbounded)
          then have "connected_component_set (- S) z  {}"
            unfolding connected_component_eq_empty
            using confr openS bounded C w  S
            apply (simp add: frontier_def interior_open C_ccsw)
            by (metis ComplI Compl_eq_Diff_UNIV connected_UNIV closed_closure closure_subset connected_component_eq_self
                      connected_diff_open_from_closed subset_UNIV)
          then show "frontier (connected_component_set (- S) z)  {}"
            by (metis False S  UNIV connected_component_eq_UNIV frontier_complement frontier_eq_empty)
        qed
        then show "connected_component_set (- S) z  frontier S  {}"
          by auto
      qed
      then show False
        by (metis C_ccsw Compl_iff w  S z  C connected_component_eq_empty connected_component_idemp)
    qed
  qed
next
  case False
  obtain w where C_ccsw: "C = connected_component_set (- S) w" and "w  S"
    using C by (auto simp: components_def)
  have "frontier (connected_component_set (- S) w)  connected_component_set (- S) w"
    by (simp add: closed_Compl closed_connected_component frontier_subset_eq openS)
  moreover have "frontier (connected_component_set (- S) w)  frontier S"
    using frontier_complement frontier_of_connected_component_subset by blast
  moreover have "frontier (connected_component_set (- S) w)  {}"
    by (metis C C_ccsw False bounded_empty compl_top_eq connected_component_eq_UNIV double_compl frontier_not_empty in_components_nonempty)
  ultimately obtain z where zin: "z  frontier S" and z: "z  connected_component_set (- S) w"
    by blast
  have "connected_component_set (frontier S) z  components(frontier S)"
    by (simp add: z  frontier S componentsI)
  with prev False have "¬ bounded (connected_component_set (frontier S) z)"
    by simp
  moreover have "connected_component (- S) w = connected_component (- S) z"
    using connected_component_eq [OF z] by force
  ultimately show ?thesis
    by (metis C_ccsw SC_Chain.openS SC_Chain_axioms bounded_subset closed_Compl connected_component_mono frontier_complement frontier_subset_eq)
qed

lemma empty_inside:
  assumes "connected S" "C. C  components (- S)  ¬ bounded C"
  shows "inside S = {}"
  using assms by (auto simp: components_def inside_def)

lemma empty_inside_imp_simply_connected:
  "connected S; inside S = {}  simply_connected S"
  by (metis ComplI inside_Un_outside openS outside_mono simply_connected_eq_winding_number_zero subsetCE sup_bot.left_neutral winding_number_zero_in_outside)

end

proposition
  fixes S :: "complex set"
  assumes "open S"
  shows simply_connected_eq_frontier_properties:
         "simply_connected S 
          connected S 
             (if bounded S then connected(frontier S)
             else (C  components(frontier S). ¬bounded C))" (is "?fp")
    and simply_connected_eq_unbounded_complement_components:
         "simply_connected S 
          connected S  (C  components(- S). ¬bounded C)" (is "?ucc")
    and simply_connected_eq_empty_inside:
         "simply_connected S 
          connected S  inside S = {}" (is "?ei")
proof -
  interpret SC_Chain
    using assms by (simp add: SC_Chain_def)
  have "?fp  ?ucc  ?ei"
    using empty_inside empty_inside_imp_simply_connected frontier_properties 
      unbounded_complement_components winding_number_zero by blast
  then show ?fp ?ucc ?ei
    by blast+
qed

lemma simply_connected_iff_simple:
  fixes S :: "complex set"
  assumes "open S" "bounded S"
  shows "simply_connected S  connected S  connected(- S)" (is "?lhs = ?rhs")
proof
  show "?lhs  ?rhs"
    by (metis DIM_complex assms cobounded_has_bounded_component double_complement dual_order.order_iff_strict
        simply_connected_eq_unbounded_complement_components)
  show "?rhs  ?lhs"
    by (simp add: assms connected_frontier_simple simply_connected_eq_frontier_properties)
qed

lemma subset_simply_connected_imp_inside_subset:
  fixes A :: "complex set"
  assumes "simply_connected A" "open A" "B  A"
  shows   "inside B  A" 
  by (metis assms Diff_eq_empty_iff inside_mono subset_empty simply_connected_eq_empty_inside)

subsection‹Further equivalences based on continuous logs and sqrts›

context SC_Chain
begin

lemma continuous_log:
  fixes f :: "complexcomplex"
  assumes S: "simply_connected S"
    and contf: "continuous_on S f" and nz: "z. z  S  f z  0"
  shows "g. continuous_on S g  (z  S. f z = exp(g z))"
proof -
  consider "S = {}" | "S homeomorphic ball (0::complex) 1"
    using simply_connected_eq_homeomorphic_to_disc [OF openS] S by metis
  then show ?thesis
  proof cases
    case 1 then show ?thesis
      by simp
  next
    case 2
    then obtain h k :: "complexcomplex"
      where kh: "x. x  S  k(h x) = x" and him: "h ` S = ball 0 1"
      and conth: "continuous_on S h"
      and hk: "y. y  ball 0 1  h(k y) = y" and kim: "k ` ball 0 1 = S"
      and contk: "continuous_on (ball 0 1) k"
      unfolding homeomorphism_def homeomorphic_def by metis
    obtain g where contg: "continuous_on (ball 0 1) g"
             and expg: "z. z  ball 0 1  (f  k) z = exp (g z)"
    proof (rule continuous_logarithm_on_ball)
      show "continuous_on (ball 0 1) (f  k)"
        using contf continuous_on_compose contk kim by blast
      show "z. z  ball 0 1  (f  k) z  0"
        using kim nz by auto
    qed auto
    then show ?thesis
      by (metis comp_apply conth continuous_on_compose him imageI kh)
  qed
qed

lemma continuous_sqrt:
  fixes f :: "complexcomplex"
  assumes contf: "continuous_on S f" and nz: "z. z  S  f z  0"
    and prev: "f::complexcomplex.
                continuous_on S f; z. z  S  f z  0
                   g. continuous_on S g  (z  S. f z = exp(g z))"
  shows "g. continuous_on S g  (z  S. f z = (g z)2)"
proof -
  obtain g where contg: "continuous_on S g" and geq: "z. z  S  f z = exp(g z)"
    using contf nz prev by metis
  show ?thesis
  proof (intro exI ballI conjI)
    show "continuous_on S (λz. exp(g z/2))"
      by (intro continuous_intros) (auto simp: contg)
    show "z. z  S  f z = (exp (g z/2))2"
      by (metis (no_types, lifting) divide_inverse exp_double geq mult.left_commute mult.right_neutral right_inverse zero_neq_numeral)
  qed
qed

lemma continuous_sqrt_imp_simply_connected:
  assumes "connected S"
    and prev: "f::complexcomplex. continuous_on S f; z  S. f z  0
                 g. continuous_on S g  (z  S. f z = (g z)2)"
  shows "simply_connected S"
proof (clarsimp simp add: simply_connected_eq_holomorphic_sqrt [OF openS] connected S)
  fix f
  assume "f holomorphic_on S" and nz: "zS. f z  0"
  then obtain g where contg: "continuous_on S g" and geq: "z. z  S  f z = (g z)2"
    by (metis holomorphic_on_imp_continuous_on prev)
  show "g. g holomorphic_on S  (zS. f z = (g z)2)"
  proof (intro exI ballI conjI)
    show "g holomorphic_on S"
    proof (clarsimp simp add: holomorphic_on_open [OF openS])
      fix z
      assume "z  S"
      with nz geq have "g z  0"
        by auto
      obtain δ where "0 < δ" "w. w  S; dist w z < δ  dist (g w) (g z) < cmod (g z)"
        using contg [unfolded continuous_on_iff] by (metis g z  0 z  S zero_less_norm_iff)
      then have δ: "w. w  S; w  ball z δ  g w + g z  0"
        apply (clarsimp simp: dist_norm)
        by (metis add_diff_cancel_left' dist_0_norm dist_complex_def less_le_not_le norm_increases_online norm_minus_commute)
      have *: "(λx. (f x - f z) / (x - z) / (g x + g z)) z deriv f z / (g z + g z)"
      proof (intro tendsto_intros)
        show "(λx. (f x - f z) / (x - z)) z deriv f z"
          using f holomorphic_on S z  S has_field_derivative_iff holomorphic_derivI openS by blast
        show "g z g z"
          using z  S contg continuous_on_eq_continuous_at isCont_def openS by blast
      qed (simp add: g z  0)
      then have "(g has_field_derivative deriv f z / (g z + g z)) (at z)"
        unfolding has_field_derivative_iff
      proof (rule Lim_transform_within_open)
        show "open (ball z δ  S)"
          by (simp add: openS open_Int)
        show "z  ball z δ  S"
          using z  S 0 < δ by simp
        show "x. x  ball z δ  S; x  z
                   (f x - f z) / (x - z) / (g x + g z) = (g x - g z) / (x - z)"
          using δ
          apply (simp add: geq z  S divide_simps)
          apply (auto simp: algebra_simps power2_eq_square)
          done
      qed
      then show "f'. (g has_field_derivative f') (at z)" ..
    qed
  qed (use geq in auto)
qed

end

proposition
  fixes S :: "complex set"
  assumes "open S"
  shows simply_connected_eq_continuous_log:
         "simply_connected S 
          connected S 
          (f::complexcomplex. continuous_on S f  (z  S. f z  0)
             (g. continuous_on S g  (z  S. f z = exp (g z))))" (is "?log")
    and simply_connected_eq_continuous_sqrt:
         "simply_connected S 
          connected S 
          (f::complexcomplex. continuous_on S f  (z  S. f z  0)
             (g. continuous_on S g  (z  S. f z = (g z)2)))" (is "?sqrt")
proof -
  interpret SC_Chain
    using assms by (simp add: SC_Chain_def)
  show ?log ?sqrt
    using local.continuous_log winding_number_zero continuous_sqrt continuous_sqrt_imp_simply_connected 
    by auto
qed


subsectiontag unimportant› ‹More Borsukian results›

lemma Borsukian_componentwise_eq:
  fixes S :: "'a::euclidean_space set"
  assumes S: "locally connected S  compact S"
  shows "Borsukian S  (C  components S. Borsukian C)"
proof -
  have *: "ANR(-{0::complex})"
    by (simp add: ANR_delete open_Compl open_imp_ANR)
  show ?thesis
    using cohomotopically_trivial_on_components [OF assms *] by (auto simp: Borsukian_alt)
qed

lemma Borsukian_componentwise:
  fixes S :: "'a::euclidean_space set"
  assumes "locally connected S  compact S" "C. C  components S  Borsukian C"
  shows "Borsukian S"
  by (metis Borsukian_componentwise_eq assms)

lemma simply_connected_eq_Borsukian:
  fixes S :: "complex set"
  shows "open S  (simply_connected S  connected S  Borsukian S)"
  by (auto simp: simply_connected_eq_continuous_log Borsukian_continuous_logarithm)

lemma Borsukian_eq_simply_connected:
  fixes S :: "complex set"
  shows "open S  Borsukian S  (C  components S. simply_connected C)"
  by (meson Borsukian_componentwise_eq in_components_connected open_components open_imp_locally_connected simply_connected_eq_Borsukian)

lemma Borsukian_separation_open_closed:
  fixes S :: "complex set"
  assumes S: "open S  closed S" and "bounded S"
  shows "Borsukian S  connected(- S)"
  using S
proof
  assume "open S"
  show ?thesis
    unfolding Borsukian_eq_simply_connected [OF open S]
    by (metis open S bounded S bounded_subset in_components_maximal nonseparation_by_component_eq open_components simply_connected_iff_simple)
next
  assume "closed S"
  with bounded S show ?thesis
    by (simp add: Borsukian_separation_compact compact_eq_bounded_closed)
qed


subsection‹Finally, the Riemann Mapping Theorem›

theorem Riemann_mapping_theorem:
    "open S  simply_connected S 
     S = {}  S = UNIV 
     (f g. f holomorphic_on S  g holomorphic_on ball 0 1 
           (z  S. f z  ball 0 1  g(f z) = z) 
           (z  ball 0 1. g z  S  f(g z) = z))"
    (is "_ = ?rhs")
proof -
  have "simply_connected S  ?rhs" if "open S"
    by (simp add: simply_connected_eq_biholomorphic_to_disc that)
  moreover have "open S" if "?rhs"
  proof -
    { fix f g
      assume g: "g holomorphic_on ball 0 1" "zball 0 1. g z  S  f (g z) = z"
        and "zS. cmod (f z) < 1  g (f z) = z"
      then have "S = g ` (ball 0 1)"
        by (force simp:)
      then have "open S"
        by (metis open_ball g inj_on_def open_mapping_thm3)
    }
    with that show "open S" by auto
  qed
  ultimately show ?thesis by metis
qed


subsection ‹Applications to Winding Numbers›

lemma simply_connected_inside_simple_path:
  fixes p :: "real  complex"
  shows "simple_path p  simply_connected(inside(path_image p))"
  using Jordan_inside_outside connected_simple_path_image inside_simple_curve_imp_closed simply_connected_eq_frontier_properties
  by fastforce

lemma simply_connected_Int:
  fixes S :: "complex set"
  assumes "open S" "open T" "simply_connected S" "simply_connected T" "connected (S  T)"
  shows "simply_connected (S  T)"
  using assms by (force simp: simply_connected_eq_winding_number_zero open_Int)


subsectiontag unimportant› ‹The winding number defines a continuous logarithm for the path itself›

lemma winding_number_as_continuous_log:
  assumes "path p" and ζ: "ζ  path_image p"
  obtains q where "path q"
                  "pathfinish q - pathstart q = 2 * of_real pi * 𝗂 * winding_number p ζ"
                  "t. t  {0..1}  p t = ζ + exp(q t)"
proof -
  let ?q = "λt. 2 * of_real pi * 𝗂 * winding_number(subpath 0 t p) ζ + Ln(pathstart p - ζ)"
  show ?thesis
  proof
    have *: "continuous (at t within {0..1}) (λx. winding_number (subpath 0 x p) ζ)"
      if t: "t  {0..1}" for t
    proof -
      let ?B = "ball (p t) (norm(p t - ζ))"
      have "p t  ζ"
        using path_image_def that ζ by blast
      then have "simply_connected ?B"
        by (simp add: convex_imp_simply_connected)
      then have "f::complexcomplex. continuous_on ?B f  (ζ  ?B. f ζ  0)
                   (g. continuous_on ?B g  (ζ  ?B. f ζ = exp (g ζ)))"
        by (simp add: simply_connected_eq_continuous_log)
      moreover have "continuous_on ?B (λw. w - ζ)"
        by (intro continuous_intros)
      moreover have "(z  ?B. z - ζ  0)"
        by (auto simp: dist_norm)
      ultimately obtain g where contg: "continuous_on ?B g"
        and geq: "z. z  ?B  z - ζ = exp (g z)" by blast
      obtain d where "0 < d" and d:
        "x. x  {0..1}; dist x t < d  dist (p x) (p t) < cmod (p t - ζ)"
        using path p t unfolding path_def continuous_on_iff
        by (metis p t  ζ right_minus_eq zero_less_norm_iff)
      have "((λx. winding_number (λw. subpath 0 x p w - ζ) 0 -
                  winding_number (λw. subpath 0 t p w - ζ) 0)  0)
            (at t within {0..1})"
      proof (rule Lim_transform_within [OF _ d > 0])
        have "continuous (at t within {0..1}) (g o p)"
        proof (rule continuous_within_compose)
          show "continuous (at t within {0..1}) p"
            using path p continuous_on_eq_continuous_within path_def that by blast
          show "continuous (at (p t) within p ` {0..1}) g"
            by (metis (no_types, lifting) open_ball UNIV_I p t  ζ centre_in_ball contg continuous_on_eq_continuous_at continuous_within_topological right_minus_eq zero_less_norm_iff)
        qed
        with LIM_zero have "((λu. (g (subpath t u p 1) - g (subpath t u p 0)))  0) (at t within {0..1})"
          by (auto simp: subpath_def continuous_within o_def)
        then show "((λu.  (g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * 𝗂))  0)
           (at t within {0..1})"
          by (simp add: tendsto_divide_zero)
        show "(g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * 𝗂) =
              winding_number (λw. subpath 0 u p w - ζ) 0 - winding_number (λw. subpath 0 t p w - ζ) 0"
          if "u  {0..1}" "0 < dist u t" "dist u t < d" for u
        proof -
          have "closed_segment t u  {0..1}"
            using closed_segment_eq_real_ivl t that by auto
          then have piB: "path_image(subpath t u p)  ?B"
            apply (clarsimp simp add: path_image_subpath_gen)
            by (metis subsetD le_less_trans dist u t < d d dist_commute dist_in_closed_segment)
          have *: "path (g  subpath t u p)"
          proof (rule path_continuous_image)
            show "path (subpath t u p)"
              using path p t that by auto
            show "continuous_on (path_image (subpath t u p)) g"
              using piB contg continuous_on_subset by blast
          qed
          have "(g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * 𝗂)
              =  winding_number (exp  g  subpath t u p) 0"
            using winding_number_compose_exp [OF *]
            by (simp add: pathfinish_def pathstart_def o_assoc)
          also have " = winding_number (λw. subpath t u p w - ζ) 0"
          proof (rule winding_number_cong)
            have "exp(g y) = y - ζ" if "y  (subpath t u p) ` {0..1}" for y
              by (metis that geq path_image_def piB subset_eq)
            then show "x. 0  x; x  1  (exp  g  subpath t u p) x = subpath t u p x - ζ"
              by auto
          qed
          also have " = winding_number (λw. subpath 0 u p w - ζ) 0 -
                           winding_number (λw. subpath 0 t p w - ζ) 0"
            apply (simp add: winding_number_offset [symmetric])
            using winding_number_subpath_combine [OF path p ζ, of 0 t u] t  {0..1} u  {0..1}
            by (simp add: add.commute eq_diff_eq)
          finally show ?thesis .
        qed
      qed
      then show ?thesis
        by (subst winding_number_offset) (simp add: continuous_within LIM_zero_iff)
    qed
    show "path ?q"
      unfolding path_def
      by (intro continuous_intros) (simp add: continuous_on_eq_continuous_within *)

    have "ζ  p 0"
      by (metis ζ pathstart_def pathstart_in_path_image)
    then show "pathfinish ?q - pathstart ?q = 2 * of_real pi * 𝗂 * winding_number p ζ"
      by (simp add: pathfinish_def pathstart_def)
    show "p t = ζ + exp (?q t)" if "t  {0..1}" for t
    proof -
      have "path (subpath 0 t p)"
        using path p that by auto
      moreover
      have "ζ  path_image (subpath 0 t p)"
        using ζ [unfolded path_image_def] that by (auto simp: path_image_subpath)
      ultimately show ?thesis
        using winding_number_exp_2pi [of "subpath 0 t p" ζ] ζ  p 0
        by (auto simp: exp_add algebra_simps pathfinish_def pathstart_def subpath_def)
    qed
  qed
qed

subsection ‹Winding number equality is the same as path/loop homotopy in C - {0}›

lemma winding_number_homotopic_loops_null_eq:
  assumes "path p" and ζ: "ζ  path_image p"
  shows "winding_number p ζ = 0  (a. homotopic_loops (-{ζ}) p (λt. a))"
    (is "?lhs = ?rhs")
proof
  assume [simp]: ?lhs
  obtain q where "path q"
             and qeq:  "pathfinish q - pathstart q = 2 * of_real pi * 𝗂 * winding_number p ζ"
             and peq: "t. t  {0..1}  p t = ζ + exp(q t)"
    using winding_number_as_continuous_log [OF assms] by blast
  have *: "homotopic_with_canon (λr. pathfinish r = pathstart r)
                       {0..1} (-{ζ}) ((λw. ζ + exp w)  q) ((λw. ζ + exp w)  (λt. 0))"
  proof (rule homotopic_with_compose_continuous_left)
    show "homotopic_with_canon (λf. pathfinish ((λw. ζ + exp w)  f) = pathstart ((λw. ζ + exp w)  f))
              {0..1} UNIV q (λt. 0)"
    proof (rule homotopic_with_mono, simp_all add: pathfinish_def pathstart_def)
      have "homotopic_loops UNIV q (λt. 0)"
        by (rule homotopic_loops_linear) (use qeq path q in auto simp: path_defs)
      then have "homotopic_with (λr. r 1 = r 0) (top_of_set {0..1}) euclidean q (λt. 0)"
        by (simp add: homotopic_loops_def pathfinish_def pathstart_def)
      then show "homotopic_with (λh. exp (h 1) = exp (h 0)) (top_of_set {0..1}) euclidean q (λt. 0)"
        by (rule homotopic_with_mono) simp
    qed
    show "continuous_on UNIV (λw. ζ + exp w)"
      by (rule continuous_intros)+
    show "(λw. ζ + exp w)  UNIV  -{ζ}"
      by auto
  qed
  then have "homotopic_with_canon (λr. pathfinish r = pathstart r) {0..1} (-{ζ}) p (λx. ζ + 1)"
    by (rule homotopic_with_eq) (auto simp: o_def peq pathfinish_def pathstart_def)
  then have "homotopic_loops (-{ζ}) p (λt. ζ + 1)"
    by (simp add: homotopic_loops_def)
  then show ?rhs ..
next
  assume ?rhs
  then obtain a where "homotopic_loops (-{ζ}) p (λt. a)" ..
  then have "winding_number p ζ = winding_number (λt. a) ζ" "a  ζ"
    using winding_number_homotopic_loops homotopic_loops_imp_subset by (force simp:)+
  then show ?lhs
    using winding_number_zero_const by auto
qed

lemma winding_number_homotopic_paths_null_explicit_eq:
  assumes "path p" and ζ: "ζ  path_image p"
  shows "winding_number p ζ = 0  homotopic_paths (-{ζ}) p (linepath (pathstart p) (pathstart p))"
        (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    using homotopic_loops_imp_homotopic_paths_null 
    by (force simp: linepath_refl winding_number_homotopic_loops_null_eq [OF assms])
next
  assume ?rhs
  then show ?lhs
    by (metis ζ pathstart_in_path_image winding_number_homotopic_paths winding_number_trivial)
qed

lemma winding_number_homotopic_paths_null_eq:
  assumes "path p" and ζ: "ζ  path_image p"
  shows "winding_number p ζ = 0  (a. homotopic_paths (-{ζ}) p (λt. a))"
    (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (auto simp: winding_number_homotopic_paths_null_explicit_eq [OF assms] linepath_refl)
next
  assume ?rhs
  then show ?lhs
    by (metis ζ homotopic_paths_imp_pathfinish pathfinish_def pathfinish_in_path_image winding_number_homotopic_paths winding_number_zero_const)
qed

proposition winding_number_homotopic_paths_eq:
  assumes "path p" and ζp: "ζ  path_image p"
      and "path q" and ζq: "ζ  path_image q"
      and qp: "pathstart q = pathstart p" "pathfinish q = pathfinish p"
    shows "winding_number p ζ = winding_number q ζ  homotopic_paths (-{ζ}) p q"
    (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have "winding_number (p +++ reversepath q) ζ = 0"
    using assms by (simp add: winding_number_join winding_number_reversepath)
  moreover
  have "path (p +++ reversepath q)" "ζ  path_image (p +++ reversepath q)"
    using assms by (auto simp: not_in_path_image_join)
  ultimately obtain a where "homotopic_paths (- {ζ}) (p +++ reversepath q) (linepath a a)"
    using winding_number_homotopic_paths_null_explicit_eq by blast
  then show ?rhs
    using homotopic_paths_imp_pathstart assms
    by (fastforce simp: dest: homotopic_paths_imp_homotopic_loops homotopic_paths_loop_parts)
qed (simp add: winding_number_homotopic_paths)

lemma winding_number_homotopic_loops_eq:
  assumes "path p" and ζp: "ζ  path_image p"
      and "path q" and ζq: "ζ  path_image q"
      and loops: "pathfinish p = pathstart p" "pathfinish q = pathstart q"
    shows "winding_number p ζ = winding_number q ζ  homotopic_loops (-{ζ}) p q"
    (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  have "pathstart p  ζ" "pathstart q  ζ"
    using ζp ζq by blast+
  moreover have "path_connected (-{ζ})"
    by (simp add: path_connected_punctured_universe)
  ultimately obtain r where "path r" and rim: "path_image r  -{ζ}"
                        and pas: "pathstart r = pathstart p" and paf: "pathfinish r = pathstart q"
    by (auto simp: path_connected_def)
  then have "pathstart r  ζ" by blast
  have "homotopic_loops (- {ζ}) p (r +++ q +++ reversepath r)"
  proof (rule homotopic_paths_imp_homotopic_loops)
    have "path (r +++ q +++ reversepath r)"
      by (simp add: path r path q loops paf)
    moreover have "ζ  path_image (r +++ q +++ reversepath r)"
      by (metis ζq not_in_path_image_join path_image_reversepath rim subset_Compl_singleton)
    moreover have "homotopic_loops (- {ζ}) (r +++ q +++ reversepath r) q"
      using path q path r ζq homotopic_loops_conjugate loops(2) paf rim by blast
    ultimately show "homotopic_paths (- {ζ}) p (r +++ q +++ reversepath r)"
      using loops pathfinish_join pathfinish_reversepath pathstart_join
      by (metis L ζp path p pas winding_number_homotopic_loops winding_number_homotopic_paths_eq)
  qed (use loops pas in auto)
  moreover have "homotopic_loops (- {ζ}) (r +++ q +++ reversepath r) q"
    using rim ζq by (auto simp: homotopic_loops_conjugate paf path q path r loops)
  ultimately show ?rhs
    using homotopic_loops_trans by metis
qed (simp add: winding_number_homotopic_loops)

end