Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.
authorpaulson <lp15@cam.ac.uk>
Tue Oct 10 14:03:51 2017 +0100 (19 months ago)
changeset 668260d60d2118544
parent 66825 9f6ec65f7a6e
child 66827 c94531b5007d
Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.
NEWS
src/HOL/Analysis/Analysis.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Riemann_Mapping.thy
src/HOL/Analysis/Winding_Numbers.thy
     1.1 --- a/NEWS	Mon Oct 09 22:08:05 2017 +0200
     1.2 +++ b/NEWS	Tue Oct 10 14:03:51 2017 +0100
     1.3 @@ -59,6 +59,7 @@
     1.4  * Predicate pairwise_coprime abolished, use "pairwise coprime" instead.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.
     1.8  
     1.9  *** System ***
    1.10  
     2.1 --- a/src/HOL/Analysis/Analysis.thy	Mon Oct 09 22:08:05 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Analysis.thy	Tue Oct 10 14:03:51 2017 +0100
     2.3 @@ -16,7 +16,7 @@
     2.4    Polytope
     2.5    Jordan_Curve
     2.6    Winding_Numbers
     2.7 -  Great_Picard
     2.8 +  Riemann_Mapping
     2.9    Poly_Roots
    2.10    Conformal_Mappings
    2.11    FPS_Convergence
     3.1 --- a/src/HOL/Analysis/Path_Connected.thy	Mon Oct 09 22:08:05 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Tue Oct 10 14:03:51 2017 +0100
     3.3 @@ -5485,6 +5485,275 @@
     3.4    shows "\<lbrakk>locally compact S; locally compact T\<rbrakk> \<Longrightarrow> locally compact (S \<times> T)"
     3.5    by (auto simp: compact_Times locally_Times)
     3.6  
     3.7 +lemma locally_compact_compact_subopen:
     3.8 +  fixes S :: "'a :: heine_borel set"
     3.9 +  shows
    3.10 +   "locally compact S \<longleftrightarrow>
    3.11 +    (\<forall>K T. K \<subseteq> S \<and> compact K \<and> open T \<and> K \<subseteq> T
    3.12 +          \<longrightarrow> (\<exists>U V. K \<subseteq> U \<and> U \<subseteq> V \<and> U \<subseteq> T \<and> V \<subseteq> S \<and>
    3.13 +                     openin (subtopology euclidean S) U \<and> compact V))"
    3.14 +   (is "?lhs = ?rhs")
    3.15 +proof
    3.16 +  assume L: ?lhs
    3.17 +  show ?rhs
    3.18 +  proof clarify
    3.19 +    fix K :: "'a set" and T :: "'a set"
    3.20 +    assume "K \<subseteq> S" and "compact K" and "open T" and "K \<subseteq> T"
    3.21 +    obtain U V where "K \<subseteq> U" "U \<subseteq> V" "V \<subseteq> S" "compact V"
    3.22 +                 and ope: "openin (subtopology euclidean S) U"
    3.23 +      using L unfolding locally_compact_compact by (meson \<open>K \<subseteq> S\<close> \<open>compact K\<close>)
    3.24 +    show "\<exists>U V. K \<subseteq> U \<and> U \<subseteq> V \<and> U \<subseteq> T \<and> V \<subseteq> S \<and>
    3.25 +                openin (subtopology euclidean S) U \<and> compact V"
    3.26 +    proof (intro exI conjI)
    3.27 +      show "K \<subseteq> U \<inter> T"
    3.28 +        by (simp add: \<open>K \<subseteq> T\<close> \<open>K \<subseteq> U\<close>)
    3.29 +      show "U \<inter> T \<subseteq> closure(U \<inter> T)"
    3.30 +        by (rule closure_subset)
    3.31 +      show "closure (U \<inter> T) \<subseteq> S"
    3.32 +        by (metis \<open>U \<subseteq> V\<close> \<open>V \<subseteq> S\<close> \<open>compact V\<close> closure_closed closure_mono compact_imp_closed inf.cobounded1 subset_trans)
    3.33 +      show "openin (subtopology euclidean S) (U \<inter> T)"
    3.34 +        by (simp add: \<open>open T\<close> ope openin_Int_open)
    3.35 +      show "compact (closure (U \<inter> T))"
    3.36 +        by (meson Int_lower1 \<open>U \<subseteq> V\<close> \<open>compact V\<close> bounded_subset compact_closure compact_eq_bounded_closed)
    3.37 +    qed auto
    3.38 +  qed
    3.39 +next
    3.40 +  assume ?rhs then show ?lhs
    3.41 +    unfolding locally_compact_compact
    3.42 +    by (metis open_openin openin_topspace subtopology_superset top.extremum topspace_euclidean_subtopology)
    3.43 +qed
    3.44 +
    3.45 +subsection\<open>Sura-Bura's results about compact components of sets.\<close>
    3.46 +
    3.47 +proposition Sura_Bura_compact:
    3.48 +  fixes S :: "'a::euclidean_space set"
    3.49 +  assumes "compact S" and C: "C \<in> components S"
    3.50 +  shows "C = \<Inter>{T. C \<subseteq> T \<and> openin (subtopology euclidean S) T \<and>
    3.51 +                           closedin (subtopology euclidean S) T}"
    3.52 +         (is "C = \<Inter>?\<T>")
    3.53 +proof
    3.54 +  obtain x where x: "C = connected_component_set S x" and "x \<in> S"
    3.55 +    using C by (auto simp: components_def)
    3.56 +  have "C \<subseteq> S"
    3.57 +    by (simp add: C in_components_subset)
    3.58 +  have "\<Inter>?\<T> \<subseteq> connected_component_set S x"
    3.59 +  proof (rule connected_component_maximal)
    3.60 +    have "x \<in> C"
    3.61 +      by (simp add: \<open>x \<in> S\<close> x)
    3.62 +    then show "x \<in> \<Inter>?\<T>"
    3.63 +      by blast
    3.64 +    have clo: "closed (\<Inter>?\<T>)"
    3.65 +      by (simp add: \<open>compact S\<close> closed_Inter closedin_compact_eq compact_imp_closed)
    3.66 +    have False
    3.67 +      if K1: "closedin (subtopology euclidean (\<Inter>?\<T>)) K1" and
    3.68 +         K2: "closedin (subtopology euclidean (\<Inter>?\<T>)) K2" and
    3.69 +         K12_Int: "K1 \<inter> K2 = {}" and K12_Un: "K1 \<union> K2 = \<Inter>?\<T>" and "K1 \<noteq> {}" "K2 \<noteq> {}"
    3.70 +       for K1 K2
    3.71 +    proof -
    3.72 +      have "closed K1" "closed K2"
    3.73 +        using closedin_closed_trans clo K1 K2 by blast+
    3.74 +      then obtain V1 V2 where "open V1" "open V2" "K1 \<subseteq> V1" "K2 \<subseteq> V2" and V12: "V1 \<inter> V2 = {}"
    3.75 +        using separation_normal \<open>K1 \<inter> K2 = {}\<close> by metis
    3.76 +      have SV12_ne: "(S - (V1 \<union> V2)) \<inter> (\<Inter>?\<T>) \<noteq> {}"
    3.77 +      proof (rule compact_imp_fip)
    3.78 +        show "compact (S - (V1 \<union> V2))"
    3.79 +          by (simp add: \<open>open V1\<close> \<open>open V2\<close> \<open>compact S\<close> compact_diff open_Un)
    3.80 +        show clo\<T>: "closed T" if "T \<in> ?\<T>" for T
    3.81 +          using that \<open>compact S\<close>
    3.82 +          by (force intro: closedin_closed_trans simp add: compact_imp_closed)
    3.83 +        show "(S - (V1 \<union> V2)) \<inter> \<Inter>\<F> \<noteq> {}" if "finite \<F>" and \<F>: "\<F> \<subseteq> ?\<T>" for \<F>
    3.84 +        proof
    3.85 +          assume djo: "(S - (V1 \<union> V2)) \<inter> \<Inter>\<F> = {}"
    3.86 +          obtain D where opeD: "openin (subtopology euclidean S) D"
    3.87 +                   and cloD: "closedin (subtopology euclidean S) D"
    3.88 +                   and "C \<subseteq> D" and DV12: "D \<subseteq> V1 \<union> V2"
    3.89 +          proof (cases "\<F> = {}")
    3.90 +            case True
    3.91 +            with \<open>C \<subseteq> S\<close> djo that show ?thesis
    3.92 +              by force
    3.93 +          next
    3.94 +            case False show ?thesis
    3.95 +            proof
    3.96 +              show ope: "openin (subtopology euclidean S) (\<Inter>\<F>)"
    3.97 +                using openin_Inter \<open>finite \<F>\<close> False \<F> by blast
    3.98 +              then show "closedin (subtopology euclidean S) (\<Inter>\<F>)"
    3.99 +                by (meson clo\<T> \<F> closed_Inter closed_subset openin_imp_subset subset_eq)
   3.100 +              show "C \<subseteq> \<Inter>\<F>"
   3.101 +                using \<F> by auto
   3.102 +              show "\<Inter>\<F> \<subseteq> V1 \<union> V2"
   3.103 +                using ope djo openin_imp_subset by fastforce
   3.104 +            qed
   3.105 +          qed
   3.106 +          have "connected C"
   3.107 +            by (simp add: x)
   3.108 +          have "closed D"
   3.109 +            using \<open>compact S\<close> cloD closedin_closed_trans compact_imp_closed by blast
   3.110 +          have cloV1: "closedin (subtopology euclidean D) (D \<inter> closure V1)"
   3.111 +            and cloV2: "closedin (subtopology euclidean D) (D \<inter> closure V2)"
   3.112 +            by (simp_all add: closedin_closed_Int)
   3.113 +          moreover have "D \<inter> closure V1 = D \<inter> V1" "D \<inter> closure V2 = D \<inter> V2"
   3.114 +            apply safe
   3.115 +            using \<open>D \<subseteq> V1 \<union> V2\<close> \<open>open V1\<close> \<open>open V2\<close> V12
   3.116 +               apply (simp_all add: closure_subset [THEN subsetD] closure_iff_nhds_not_empty, blast+)
   3.117 +            done
   3.118 +          ultimately have cloDV1: "closedin (subtopology euclidean D) (D \<inter> V1)"
   3.119 +                      and cloDV2:  "closedin (subtopology euclidean D) (D \<inter> V2)"
   3.120 +            by metis+
   3.121 +          then obtain U1 U2 where "closed U1" "closed U2"
   3.122 +               and D1: "D \<inter> V1 = D \<inter> U1" and D2: "D \<inter> V2 = D \<inter> U2"
   3.123 +            by (auto simp: closedin_closed)
   3.124 +          have "D \<inter> U1 \<inter> C \<noteq> {}"
   3.125 +          proof
   3.126 +            assume "D \<inter> U1 \<inter> C = {}"
   3.127 +            then have *: "C \<subseteq> D \<inter> V2"
   3.128 +              using D1 DV12 \<open>C \<subseteq> D\<close> by auto
   3.129 +            have "\<Inter>?\<T> \<subseteq> D \<inter> V2"
   3.130 +              apply (rule Inter_lower)
   3.131 +              using * apply simp
   3.132 +              by (meson cloDV2 \<open>open V2\<close> cloD closedin_trans le_inf_iff opeD openin_Int_open)
   3.133 +            then show False
   3.134 +              using K1 V12 \<open>K1 \<noteq> {}\<close> \<open>K1 \<subseteq> V1\<close> closedin_imp_subset by blast
   3.135 +          qed
   3.136 +          moreover have "D \<inter> U2 \<inter> C \<noteq> {}"
   3.137 +          proof
   3.138 +            assume "D \<inter> U2 \<inter> C = {}"
   3.139 +            then have *: "C \<subseteq> D \<inter> V1"
   3.140 +              using D2 DV12 \<open>C \<subseteq> D\<close> by auto
   3.141 +            have "\<Inter>?\<T> \<subseteq> D \<inter> V1"
   3.142 +              apply (rule Inter_lower)
   3.143 +              using * apply simp
   3.144 +              by (meson cloDV1 \<open>open V1\<close> cloD closedin_trans le_inf_iff opeD openin_Int_open)
   3.145 +            then show False
   3.146 +              using K2 V12 \<open>K2 \<noteq> {}\<close> \<open>K2 \<subseteq> V2\<close> closedin_imp_subset by blast
   3.147 +          qed
   3.148 +          ultimately show False
   3.149 +            using \<open>connected C\<close> unfolding connected_closed
   3.150 +            apply (simp only: not_ex)
   3.151 +            apply (drule_tac x="D \<inter> U1" in spec)
   3.152 +            apply (drule_tac x="D \<inter> U2" in spec)
   3.153 +            using \<open>C \<subseteq> D\<close> D1 D2 V12 DV12 \<open>closed U1\<close> \<open>closed U2\<close> \<open>closed D\<close>
   3.154 +            by blast
   3.155 +        qed
   3.156 +      qed
   3.157 +      show False
   3.158 +        by (metis (full_types) DiffE UnE Un_upper2 SV12_ne \<open>K1 \<subseteq> V1\<close> \<open>K2 \<subseteq> V2\<close> disjoint_iff_not_equal subsetCE sup_ge1 K12_Un)
   3.159 +    qed
   3.160 +    then show "connected (\<Inter>?\<T>)"
   3.161 +      by (auto simp: connected_closedin_eq)
   3.162 +    show "\<Inter>?\<T> \<subseteq> S"
   3.163 +      by (fastforce simp: C in_components_subset)
   3.164 +  qed
   3.165 +  with x show "\<Inter>?\<T> \<subseteq> C" by simp
   3.166 +qed auto
   3.167 +
   3.168 +
   3.169 +corollary Sura_Bura_clopen_subset:
   3.170 +  fixes S :: "'a::euclidean_space set"
   3.171 +  assumes S: "locally compact S" and C: "C \<in> components S" and "compact C"
   3.172 +      and U: "open U" "C \<subseteq> U"
   3.173 +  obtains K where "openin (subtopology euclidean S) K" "compact K" "C \<subseteq> K" "K \<subseteq> U"
   3.174 +proof (rule ccontr)
   3.175 +  assume "\<not> thesis"
   3.176 +  with that have neg: "\<nexists>K. openin (subtopology euclidean S) K \<and> compact K \<and> C \<subseteq> K \<and> K \<subseteq> U"
   3.177 +    by metis
   3.178 +  obtain V K where "C \<subseteq> V" "V \<subseteq> U" "V \<subseteq> K" "K \<subseteq> S" "compact K"
   3.179 +               and opeSV: "openin (subtopology euclidean S) V"
   3.180 +    using S U \<open>compact C\<close>
   3.181 +    apply (simp add: locally_compact_compact_subopen)
   3.182 +    by (meson C in_components_subset)
   3.183 +  let ?\<T> = "{T. C \<subseteq> T \<and> openin (subtopology euclidean K) T \<and> compact T \<and> T \<subseteq> K}"
   3.184 +  have CK: "C \<in> components K"
   3.185 +    by (meson C \<open>C \<subseteq> V\<close> \<open>K \<subseteq> S\<close> \<open>V \<subseteq> K\<close> components_intermediate_subset subset_trans)
   3.186 +  with \<open>compact K\<close>
   3.187 +  have "C = \<Inter>{T. C \<subseteq> T \<and> openin (subtopology euclidean K) T \<and> closedin (subtopology euclidean K) T}"
   3.188 +    by (simp add: Sura_Bura_compact)
   3.189 +  then have Ceq: "C = \<Inter>?\<T>"
   3.190 +    by (simp add: closedin_compact_eq \<open>compact K\<close>)
   3.191 +  obtain W where "open W" and W: "V = S \<inter> W"
   3.192 +    using opeSV by (auto simp: openin_open)
   3.193 +  have "-(U \<inter> W) \<inter> \<Inter>?\<T> \<noteq> {}"
   3.194 +  proof (rule closed_imp_fip_compact)
   3.195 +    show "- (U \<inter> W) \<inter> \<Inter>\<F> \<noteq> {}"
   3.196 +      if "finite \<F>" and \<F>: "\<F> \<subseteq> ?\<T>" for \<F>
   3.197 +    proof (cases "\<F> = {}")
   3.198 +      case True
   3.199 +      have False if "U = UNIV" "W = UNIV"
   3.200 +      proof -
   3.201 +        have "V = S"
   3.202 +          by (simp add: W \<open>W = UNIV\<close>)
   3.203 +        with neg show False
   3.204 +          using \<open>C \<subseteq> V\<close> \<open>K \<subseteq> S\<close> \<open>V \<subseteq> K\<close> \<open>V \<subseteq> U\<close> \<open>compact K\<close> by auto
   3.205 +      qed
   3.206 +      with True show ?thesis
   3.207 +        by auto
   3.208 +    next
   3.209 +      case False
   3.210 +      show ?thesis
   3.211 +      proof
   3.212 +        assume "- (U \<inter> W) \<inter> \<Inter>\<F> = {}"
   3.213 +        then have FUW: "\<Inter>\<F> \<subseteq> U \<inter> W"
   3.214 +          by blast
   3.215 +        have "C \<subseteq> \<Inter>\<F>"
   3.216 +          using \<F> by auto
   3.217 +        moreover have "compact (\<Inter>\<F>)"
   3.218 +          by (metis (no_types, lifting) compact_Inter False mem_Collect_eq subsetCE \<F>)
   3.219 +        moreover have "\<Inter>\<F> \<subseteq> K"
   3.220 +          using False that(2) by fastforce
   3.221 +        moreover have opeKF: "openin (subtopology euclidean K) (\<Inter>\<F>)"
   3.222 +          using False \<F> \<open>finite \<F>\<close> by blast
   3.223 +        then have opeVF: "openin (subtopology euclidean V) (\<Inter>\<F>)"
   3.224 +          using W \<open>K \<subseteq> S\<close> \<open>V \<subseteq> K\<close> opeKF \<open>\<Inter>\<F> \<subseteq> K\<close> FUW openin_subset_trans by fastforce
   3.225 +        then have "openin (subtopology euclidean S) (\<Inter>\<F>)"
   3.226 +          by (metis opeSV openin_trans)
   3.227 +        moreover have "\<Inter>\<F> \<subseteq> U"
   3.228 +          by (meson \<open>V \<subseteq> U\<close> opeVF dual_order.trans openin_imp_subset)
   3.229 +        ultimately show False
   3.230 +          using neg by blast
   3.231 +      qed
   3.232 +    qed
   3.233 +  qed (use \<open>open W\<close> \<open>open U\<close> in auto)
   3.234 +  with W Ceq \<open>C \<subseteq> V\<close> \<open>C \<subseteq> U\<close> show False
   3.235 +    by auto
   3.236 +qed
   3.237 +
   3.238 +
   3.239 +corollary Sura_Bura_clopen_subset_alt:
   3.240 +  fixes S :: "'a::euclidean_space set"
   3.241 +  assumes S: "locally compact S" and C: "C \<in> components S" and "compact C"
   3.242 +      and opeSU: "openin (subtopology euclidean S) U" and "C \<subseteq> U"
   3.243 +  obtains K where "openin (subtopology euclidean S) K" "compact K" "C \<subseteq> K" "K \<subseteq> U"
   3.244 +proof -
   3.245 +  obtain V where "open V" "U = S \<inter> V"
   3.246 +    using opeSU by (auto simp: openin_open)
   3.247 +  with \<open>C \<subseteq> U\<close> have "C \<subseteq> V"
   3.248 +    by auto
   3.249 +  then show ?thesis
   3.250 +    using Sura_Bura_clopen_subset [OF S C \<open>compact C\<close> \<open>open V\<close>]
   3.251 +    by (metis \<open>U = S \<inter> V\<close> inf.bounded_iff openin_imp_subset that)
   3.252 +qed
   3.253 +
   3.254 +corollary Sura_Bura:
   3.255 +  fixes S :: "'a::euclidean_space set"
   3.256 +  assumes "locally compact S" "C \<in> components S" "compact C"
   3.257 +  shows "C = \<Inter> {K. C \<subseteq> K \<and> compact K \<and> openin (subtopology euclidean S) K}"
   3.258 +         (is "C = ?rhs")
   3.259 +proof
   3.260 +  show "?rhs \<subseteq> C"
   3.261 +  proof (clarsimp, rule ccontr)
   3.262 +    fix x
   3.263 +    assume *: "\<forall>X. C \<subseteq> X \<and> compact X \<and> openin (subtopology euclidean S) X \<longrightarrow> x \<in> X"
   3.264 +      and "x \<notin> C"
   3.265 +    obtain U V where "open U" "open V" "{x} \<subseteq> U" "C \<subseteq> V" "U \<inter> V = {}"
   3.266 +      using separation_normal [of "{x}" C]
   3.267 +      by (metis Int_empty_left \<open>x \<notin> C\<close> \<open>compact C\<close> closed_empty closed_insert compact_imp_closed insert_disjoint(1))
   3.268 +    have "x \<notin> V"
   3.269 +      using \<open>U \<inter> V = {}\<close> \<open>{x} \<subseteq> U\<close> by blast
   3.270 +    then show False
   3.271 +      by (meson "*" Sura_Bura_clopen_subset \<open>C \<subseteq> V\<close> \<open>open V\<close> assms(1) assms(2) assms(3) subsetCE)
   3.272 +  qed
   3.273 +qed blast
   3.274 +
   3.275 +
   3.276  subsection\<open>Important special cases of local connectedness and path connectedness\<close>
   3.277  
   3.278  lemma locally_connected_1:
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Analysis/Riemann_Mapping.thy	Tue Oct 10 14:03:51 2017 +0100
     4.3 @@ -0,0 +1,1445 @@
     4.4 +(*  Title:      HOL/Analysis/Riemann_Mapping.thy
     4.5 +    Authors:    LC Paulson, based on material from HOL Light
     4.6 +*)
     4.7 +
     4.8 +section \<open>Moebius functions, Equivalents of Simply Connected Sets, Riemann Mapping Theorem\<close>
     4.9 +
    4.10 +theory Riemann_Mapping
    4.11 +imports Great_Picard
    4.12 +begin
    4.13 +
    4.14 +subsection\<open>Moebius functions are biholomorphisms of the unit disc.\<close>
    4.15 +
    4.16 +definition Moebius_function :: "[real,complex,complex] \<Rightarrow> complex" where
    4.17 +  "Moebius_function \<equiv> \<lambda>t w z. exp(\<i> * of_real t) * (z - w) / (1 - cnj w * z)"
    4.18 +
    4.19 +lemma Moebius_function_simple:
    4.20 +   "Moebius_function 0 w z = (z - w) / (1 - cnj w * z)"
    4.21 +  by (simp add: Moebius_function_def)
    4.22 +
    4.23 +lemma Moebius_function_eq_zero:
    4.24 +   "Moebius_function t w w = 0"
    4.25 +  by (simp add: Moebius_function_def)
    4.26 +
    4.27 +lemma Moebius_function_of_zero:
    4.28 +   "Moebius_function t w 0 = - exp(\<i> * of_real t) * w"
    4.29 +  by (simp add: Moebius_function_def)
    4.30 +
    4.31 +lemma Moebius_function_norm_lt_1:
    4.32 +  assumes w1: "norm w < 1" and z1: "norm z < 1"
    4.33 +  shows "norm (Moebius_function t w z) < 1"
    4.34 +proof -
    4.35 +  have "1 - cnj w * z \<noteq> 0"
    4.36 +    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)
    4.37 +  then have VV: "1 - w * cnj z \<noteq> 0"
    4.38 +    by (metis complex_cnj_cnj complex_cnj_mult complex_cnj_one right_minus_eq)
    4.39 +  then have "1 - norm (Moebius_function t w z) ^ 2 =
    4.40 +         ((1 - norm w ^ 2) / (norm (1 - cnj w * z) ^ 2)) * (1 - norm z ^ 2)"
    4.41 +    apply (cases w)
    4.42 +    apply (cases z)
    4.43 +    apply (simp add: Moebius_function_def divide_simps norm_divide norm_mult)
    4.44 +    apply (simp add: complex_norm complex_diff complex_mult one_complex.code complex_cnj)
    4.45 +    apply (auto simp: algebra_simps power2_eq_square)
    4.46 +    done
    4.47 +  then have "1 - (cmod (Moebius_function t w z))\<^sup>2 = (1 - cmod (w * w)) / (cmod (1 - cnj w * z))\<^sup>2 * (1 - cmod (z * z))"
    4.48 +    by (simp add: norm_mult power2_eq_square)
    4.49 +  moreover have "0 < 1 - cmod (z * z)"
    4.50 +    by (metis (no_types) z1 diff_gt_0_iff_gt mult.left_neutral norm_mult_less)
    4.51 +  ultimately have "0 < 1 - norm (Moebius_function t w z) ^ 2"
    4.52 +    using \<open>1 - cnj w * z \<noteq> 0\<close> w1 norm_mult_less by fastforce
    4.53 +  then show ?thesis
    4.54 +    using linorder_not_less by fastforce
    4.55 +qed
    4.56 +
    4.57 +lemma Moebius_function_holomorphic:
    4.58 +  assumes "norm w < 1"
    4.59 +  shows "Moebius_function t w holomorphic_on ball 0 1"
    4.60 +proof -
    4.61 +  have *: "1 - z * w \<noteq> 0" if "norm z < 1" for z
    4.62 +  proof -
    4.63 +    have "norm (1::complex) \<noteq> norm (z * w)"
    4.64 +      using assms that norm_mult_less by fastforce
    4.65 +    then show ?thesis by auto
    4.66 +  qed
    4.67 +  show ?thesis
    4.68 +  apply (simp add: Moebius_function_def)
    4.69 +  apply (intro holomorphic_intros)
    4.70 +  using assms *
    4.71 +  by (metis complex_cnj_cnj complex_cnj_mult complex_cnj_one complex_mod_cnj mem_ball_0 mult.commute right_minus_eq)
    4.72 +qed
    4.73 +
    4.74 +lemma Moebius_function_compose:
    4.75 +  assumes meq: "-w1 = w2" and "norm w1 < 1" "norm z < 1"
    4.76 +  shows "Moebius_function 0 w1 (Moebius_function 0 w2 z) = z"
    4.77 +proof -
    4.78 +  have "norm w2 < 1"
    4.79 +    using assms by auto
    4.80 +  then have "-w1 = z" if "cnj w2 * z = 1"
    4.81 +    by (metis assms(3) complex_mod_cnj less_irrefl mult.right_neutral norm_mult_less norm_one that)
    4.82 +  moreover have "z=0" if "1 - cnj w2 * z = cnj w1 * (z - w2)"
    4.83 +  proof -
    4.84 +    have "w2 * cnj w2 = 1"
    4.85 +      using that meq by (auto simp: algebra_simps)
    4.86 +    then show "z = 0"
    4.87 +      by (metis (no_types) \<open>cmod w2 < 1\<close> complex_mod_cnj less_irrefl mult.right_neutral norm_mult_less norm_one)
    4.88 +  qed
    4.89 +  moreover have "z - w2 - w1 * (1 - cnj w2 * z) = z * (1 - cnj w2 * z - cnj w1 * (z - w2))"
    4.90 +    using meq by (fastforce simp: algebra_simps)
    4.91 +  ultimately
    4.92 +  show ?thesis
    4.93 +    by (simp add: Moebius_function_def divide_simps norm_divide norm_mult)
    4.94 +qed
    4.95 +
    4.96 +lemma ball_biholomorphism_exists:
    4.97 +  assumes "a \<in> ball 0 1"
    4.98 +  obtains f g where "f a = 0"
    4.99 +                "f holomorphic_on ball 0 1" "f ` ball 0 1 \<subseteq> ball 0 1"
   4.100 +                "g holomorphic_on ball 0 1" "g ` ball 0 1 \<subseteq> ball 0 1"
   4.101 +                "\<And>z. z \<in> ball 0 1 \<Longrightarrow> f (g z) = z"
   4.102 +                "\<And>z. z \<in> ball 0 1 \<Longrightarrow> g (f z) = z"
   4.103 +proof
   4.104 +  show "Moebius_function 0 a holomorphic_on ball 0 1"  "Moebius_function 0 (-a) holomorphic_on ball 0 1"
   4.105 +    using Moebius_function_holomorphic assms mem_ball_0 by auto
   4.106 +  show "Moebius_function 0 a a = 0"
   4.107 +    by (simp add: Moebius_function_eq_zero)
   4.108 +  show "Moebius_function 0 a ` ball 0 1 \<subseteq> ball 0 1"
   4.109 +       "Moebius_function 0 (- a) ` ball 0 1 \<subseteq> ball 0 1"
   4.110 +    using Moebius_function_norm_lt_1 assms by auto
   4.111 +  show "Moebius_function 0 a (Moebius_function 0 (- a) z) = z"
   4.112 +       "Moebius_function 0 (- a) (Moebius_function 0 a z) = z" if "z \<in> ball 0 1" for z
   4.113 +    using Moebius_function_compose assms that by auto
   4.114 +qed
   4.115 +
   4.116 +
   4.117 +subsection\<open>A big chain of equivalents of simple connectedness for an open set\<close>
   4.118 +
   4.119 +lemma biholomorphic_to_disc_aux:
   4.120 +  assumes "open S" "connected S" "0 \<in> S" and S01: "S \<subseteq> ball 0 1"
   4.121 +      and prev: "\<And>f. \<lbrakk>f holomorphic_on S; \<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0; inj_on f S\<rbrakk>
   4.122 +               \<Longrightarrow> \<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S. f z = (g z)\<^sup>2)"
   4.123 +  shows "\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
   4.124 +               (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
   4.125 +               (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z)"
   4.126 +proof -
   4.127 +  define F where "F \<equiv> {h. h holomorphic_on S \<and> h ` S \<subseteq> ball 0 1 \<and> h 0 = 0 \<and> inj_on h S}"
   4.128 +  have idF: "id \<in> F"
   4.129 +    using S01 by (auto simp: F_def)
   4.130 +  then have "F \<noteq> {}"
   4.131 +    by blast
   4.132 +  have imF_ne: "((\<lambda>h. norm(deriv h 0)) ` F) \<noteq> {}"
   4.133 +    using idF by auto
   4.134 +  have holF: "\<And>h. h \<in> F \<Longrightarrow> h holomorphic_on S"
   4.135 +    by (auto simp: F_def)
   4.136 +  obtain f where "f \<in> F" and normf: "\<And>h. h \<in> F \<Longrightarrow> norm(deriv h 0) \<le> norm(deriv f 0)"
   4.137 +  proof -
   4.138 +    obtain r where "r > 0" and r: "ball 0 r \<subseteq> S"
   4.139 +      using \<open>open S\<close> \<open>0 \<in> S\<close> openE by auto
   4.140 +    have bdd: "bdd_above ((\<lambda>h. norm(deriv h 0)) ` F)"
   4.141 +    proof (intro bdd_aboveI exI ballI, clarify)
   4.142 +      show "norm (deriv f 0) \<le> 1 / r" if "f \<in> F" for f
   4.143 +      proof -
   4.144 +        have r01: "op * (complex_of_real r) ` ball 0 1 \<subseteq> S"
   4.145 +          using that \<open>r > 0\<close> by (auto simp: norm_mult r [THEN subsetD])
   4.146 +        then have "f holomorphic_on op * (complex_of_real r) ` ball 0 1"
   4.147 +          using holomorphic_on_subset [OF holF] by (simp add: that)
   4.148 +        then have holf: "f \<circ> (\<lambda>z. (r * z)) holomorphic_on (ball 0 1)"
   4.149 +          by (intro holomorphic_intros holomorphic_on_compose)
   4.150 +        have f0: "(f \<circ> op * (complex_of_real r)) 0 = 0"
   4.151 +          using F_def that by auto
   4.152 +        have "f ` S \<subseteq> ball 0 1"
   4.153 +          using F_def that by blast
   4.154 +        with r01 have fr1: "\<And>z. norm z < 1 \<Longrightarrow> norm ((f \<circ> op*(of_real r))z) < 1"
   4.155 +          by force
   4.156 +        have *: "((\<lambda>w. f (r * w)) has_field_derivative deriv f (r * z) * r) (at z)"
   4.157 +          if "z \<in> ball 0 1" for z::complex
   4.158 +        proof (rule DERIV_chain' [where g=f])
   4.159 +          show "(f has_field_derivative deriv f (of_real r * z)) (at (of_real r * z))"
   4.160 +            apply (rule holomorphic_derivI [OF holF \<open>open S\<close>])
   4.161 +             apply (rule \<open>f \<in> F\<close>)
   4.162 +            by (meson imageI r01 subset_iff that)
   4.163 +        qed simp
   4.164 +        have df0: "((\<lambda>w. f (r * w)) has_field_derivative deriv f 0 * r) (at 0)"
   4.165 +          using * [of 0] by simp
   4.166 +        have deq: "deriv (\<lambda>x. f (complex_of_real r * x)) 0 = deriv f 0 * complex_of_real r"
   4.167 +          using DERIV_imp_deriv df0 by blast
   4.168 +        have "norm (deriv (f \<circ> op * (complex_of_real r)) 0) \<le> 1"
   4.169 +          by (auto intro: Schwarz_Lemma [OF holf f0 fr1, of 0])
   4.170 +        with \<open>r > 0\<close> show ?thesis
   4.171 +          by (simp add: deq norm_mult divide_simps o_def)
   4.172 +      qed
   4.173 +    qed
   4.174 +    define l where "l \<equiv> SUP h:F. norm (deriv h 0)"
   4.175 +    have eql: "norm (deriv f 0) = l" if le: "l \<le> norm (deriv f 0)" and "f \<in> F" for f
   4.176 +      apply (rule order_antisym [OF _ le])
   4.177 +      using \<open>f \<in> F\<close> bdd cSUP_upper by (fastforce simp: l_def)
   4.178 +    obtain \<F> where \<F>in: "\<And>n. \<F> n \<in> F" and \<F>lim: "(\<lambda>n. norm (deriv (\<F> n) 0)) \<longlonglongrightarrow> l"
   4.179 +    proof -
   4.180 +      have "\<exists>f. f \<in> F \<and> \<bar>norm (deriv f 0) - l\<bar> < 1 / (Suc n)" for n
   4.181 +      proof -
   4.182 +        obtain f where "f \<in> F" and f: "l < norm (deriv f 0) + 1/(Suc n)"
   4.183 +          using cSup_least [OF imF_ne, of "l - 1/(Suc n)"] by (fastforce simp add: l_def)
   4.184 +        then have "\<bar>norm (deriv f 0) - l\<bar> < 1 / (Suc n)"
   4.185 +          by (fastforce simp add: abs_if not_less eql)
   4.186 +        with \<open>f \<in> F\<close> show ?thesis
   4.187 +          by blast
   4.188 +      qed
   4.189 +      then obtain \<F> where fF: "\<And>n. (\<F> n) \<in> F"
   4.190 +        and fless:  "\<And>n. \<bar>norm (deriv (\<F> n) 0) - l\<bar> < 1 / (Suc n)"
   4.191 +        by metis
   4.192 +      have "(\<lambda>n. norm (deriv (\<F> n) 0)) \<longlonglongrightarrow> l"
   4.193 +      proof (rule metric_LIMSEQ_I)
   4.194 +        fix e::real
   4.195 +        assume "e > 0"
   4.196 +        then obtain N::nat where N: "e > 1/(Suc N)"
   4.197 +          using nat_approx_posE by blast
   4.198 +        show "\<exists>N. \<forall>n\<ge>N. dist (norm (deriv (\<F> n) 0)) l < e"
   4.199 +        proof (intro exI allI impI)
   4.200 +          fix n assume "N \<le> n"
   4.201 +          have "dist (norm (deriv (\<F> n) 0)) l < 1 / (Suc n)"
   4.202 +            using fless by (simp add: dist_norm)
   4.203 +          also have "... < e"
   4.204 +            using N \<open>N \<le> n\<close> inverse_of_nat_le le_less_trans by blast
   4.205 +          finally show "dist (norm (deriv (\<F> n) 0)) l < e" .
   4.206 +        qed
   4.207 +      qed
   4.208 +      with fF show ?thesis
   4.209 +        using that by blast
   4.210 +    qed
   4.211 +    have "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>B. \<forall>h\<in>F. \<forall>z\<in>K. norm (h z) \<le> B"
   4.212 +      by (rule_tac x=1 in exI) (force simp: F_def)
   4.213 +    moreover have "range \<F> \<subseteq> F"
   4.214 +      using \<open>\<And>n. \<F> n \<in> F\<close> by blast
   4.215 +    ultimately obtain f and r :: "nat \<Rightarrow> nat"
   4.216 +      where holf: "f holomorphic_on S" and r: "strict_mono r"
   4.217 +        and limf: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. \<F> (r n) x) \<longlonglongrightarrow> f x"
   4.218 +        and ulimf: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K (\<F> \<circ> r) f sequentially"
   4.219 +      using Montel [of S F \<F>, OF \<open>open S\<close> holF] by auto+
   4.220 +    have der: "\<And>n x. x \<in> S \<Longrightarrow> ((\<F> \<circ> r) n has_field_derivative ((\<lambda>n. deriv (\<F> n)) \<circ> r) n x) (at x)"
   4.221 +      using \<open>\<And>n. \<F> n \<in> F\<close> \<open>open S\<close> holF holomorphic_derivI by fastforce
   4.222 +    have ulim: "\<And>x. x \<in> S \<Longrightarrow> \<exists>d>0. cball x d \<subseteq> S \<and> uniform_limit (cball x d) (\<F> \<circ> r) f sequentially"
   4.223 +      by (meson ulimf \<open>open S\<close> compact_cball open_contains_cball)
   4.224 +    obtain f' :: "complex\<Rightarrow>complex" where f': "(f has_field_derivative f' 0) (at 0)"
   4.225 +      and tof'0: "(\<lambda>n. ((\<lambda>n. deriv (\<F> n)) \<circ> r) n 0) \<longlonglongrightarrow> f' 0"
   4.226 +      using has_complex_derivative_uniform_sequence [OF \<open>open S\<close> der ulim] \<open>0 \<in> S\<close> by metis
   4.227 +    then have derf0: "deriv f 0 = f' 0"
   4.228 +      by (simp add: DERIV_imp_deriv)
   4.229 +    have "f field_differentiable (at 0)"
   4.230 +      using field_differentiable_def f' by blast
   4.231 +    have "(\<lambda>x.  (norm (deriv (\<F> (r x)) 0))) \<longlonglongrightarrow> norm (deriv f 0)"
   4.232 +      using isCont_tendsto_compose [OF continuous_norm [OF continuous_ident] tof'0] derf0 by auto
   4.233 +    with LIMSEQ_subseq_LIMSEQ [OF \<F>lim r] have no_df0: "norm(deriv f 0) = l"
   4.234 +      by (force simp: o_def intro: tendsto_unique)
   4.235 +    have nonconstf: "\<not> f constant_on S"
   4.236 +    proof -
   4.237 +      have False if "\<And>x. x \<in> S \<Longrightarrow> f x = c" for c
   4.238 +      proof -
   4.239 +        have "deriv f 0 = 0"
   4.240 +          by (metis that \<open>open S\<close> \<open>0 \<in> S\<close> DERIV_imp_deriv [OF DERIV_transform_within_open [OF DERIV_const]])
   4.241 +        with no_df0 have "l = 0"
   4.242 +          by auto
   4.243 +        with eql [OF _ idF] show False by auto
   4.244 +      qed
   4.245 +      then show ?thesis
   4.246 +        by (meson constant_on_def)
   4.247 +    qed
   4.248 +    show ?thesis
   4.249 +    proof
   4.250 +      show "f \<in> F"
   4.251 +        unfolding F_def
   4.252 +      proof (intro CollectI conjI holf)
   4.253 +        have "norm(f z) \<le> 1" if "z \<in> S" for z
   4.254 +        proof (intro Lim_norm_ubound [OF _ limf] always_eventually allI that)
   4.255 +          fix n
   4.256 +          have "\<F> (r n) \<in> F"
   4.257 +            by (simp add: \<F>in)
   4.258 +          then show "norm (\<F> (r n) z) \<le> 1"
   4.259 +            using that by (auto simp: F_def)
   4.260 +        qed simp
   4.261 +        then have fless1: "norm(f z) < 1" if "z \<in> S" for z
   4.262 +          using maximum_modulus_principle [OF holf \<open>open S\<close> \<open>connected S\<close> \<open>open S\<close>] nonconstf that
   4.263 +          by fastforce
   4.264 +        then show "f ` S \<subseteq> ball 0 1"
   4.265 +          by auto
   4.266 +        have "(\<lambda>n. \<F> (r n) 0) \<longlonglongrightarrow> 0"
   4.267 +          using \<F>in by (auto simp: F_def)
   4.268 +        then show "f 0 = 0"
   4.269 +          using tendsto_unique [OF _ limf ] \<open>0 \<in> S\<close> trivial_limit_sequentially by blast
   4.270 +        show "inj_on f S"
   4.271 +        proof (rule Hurwitz_injective [OF \<open>open S\<close> \<open>connected S\<close> _ holf])
   4.272 +          show "\<And>n. (\<F> \<circ> r) n holomorphic_on S"
   4.273 +            by (simp add: \<F>in holF)
   4.274 +          show "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K(\<F> \<circ> r) f sequentially"
   4.275 +            by (metis ulimf)
   4.276 +          show "\<not> f constant_on S"
   4.277 +            using nonconstf by auto
   4.278 +          show "\<And>n. inj_on ((\<F> \<circ> r) n) S"
   4.279 +            using \<F>in by (auto simp: F_def)
   4.280 +        qed
   4.281 +      qed
   4.282 +      show "\<And>h. h \<in> F \<Longrightarrow> norm (deriv h 0) \<le> norm (deriv f 0)"
   4.283 +        by (metis eql le_cases no_df0)
   4.284 +    qed
   4.285 +  qed
   4.286 +  have holf: "f holomorphic_on S" and injf: "inj_on f S" and f01: "f ` S \<subseteq> ball 0 1"
   4.287 +    using \<open>f \<in> F\<close> by (auto simp: F_def)
   4.288 +  obtain g where holg: "g holomorphic_on (f ` S)"
   4.289 +             and derg: "\<And>z. z \<in> S \<Longrightarrow> deriv f z * deriv g (f z) = 1"
   4.290 +             and gf: "\<And>z. z \<in> S \<Longrightarrow> g(f z) = z"
   4.291 +    using holomorphic_has_inverse [OF holf \<open>open S\<close> injf] by metis
   4.292 +  have "ball 0 1 \<subseteq> f ` S"
   4.293 +  proof
   4.294 +    fix a::complex
   4.295 +    assume a: "a \<in> ball 0 1"
   4.296 +    have False if "\<And>x. x \<in> S \<Longrightarrow> f x \<noteq> a"
   4.297 +    proof -
   4.298 +      obtain h k where "h a = 0"
   4.299 +        and holh: "h holomorphic_on ball 0 1" and h01: "h ` ball 0 1 \<subseteq> ball 0 1"
   4.300 +        and holk: "k holomorphic_on ball 0 1" and k01: "k ` ball 0 1 \<subseteq> ball 0 1"
   4.301 +        and hk: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> h (k z) = z"
   4.302 +        and kh: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> k (h z) = z"
   4.303 +        using ball_biholomorphism_exists [OF a] by blast
   4.304 +      have nf1: "\<And>z. z \<in> S \<Longrightarrow> norm(f z) < 1"
   4.305 +        using \<open>f \<in> F\<close> by (auto simp: F_def)
   4.306 +      have 1: "h \<circ> f holomorphic_on S"
   4.307 +        using F_def \<open>f \<in> F\<close> holh holomorphic_on_compose holomorphic_on_subset by blast
   4.308 +      have 2: "\<And>z. z \<in> S \<Longrightarrow> (h \<circ> f) z \<noteq> 0"
   4.309 +        by (metis \<open>h a = 0\<close> a comp_eq_dest_lhs nf1 kh mem_ball_0 that)
   4.310 +      have 3: "inj_on (h \<circ> f) S"
   4.311 +        by (metis (no_types, lifting) F_def \<open>f \<in> F\<close> comp_inj_on inj_on_inverseI injf kh mem_Collect_eq subset_inj_on)
   4.312 +      obtain \<psi> where hol\<psi>: "\<psi> holomorphic_on ((h \<circ> f) ` S)"
   4.313 +        and \<psi>2: "\<And>z. z \<in> S  \<Longrightarrow> \<psi>(h (f z)) ^ 2 = h(f z)"
   4.314 +      proof (rule exE [OF prev [OF 1 2 3]], safe)
   4.315 +        fix \<theta>
   4.316 +        assume hol\<theta>: "\<theta> holomorphic_on S" and \<theta>2: "(\<forall>z\<in>S. (h \<circ> f) z = (\<theta> z)\<^sup>2)"
   4.317 +        show thesis
   4.318 +        proof
   4.319 +          show "(\<theta> \<circ> g \<circ> k) holomorphic_on (h \<circ> f) ` S"
   4.320 +          proof (intro holomorphic_on_compose)
   4.321 +            show "k holomorphic_on (h \<circ> f) ` S"
   4.322 +              apply (rule holomorphic_on_subset [OF holk])
   4.323 +              using f01 h01 by force
   4.324 +            show "g holomorphic_on k ` (h \<circ> f) ` S"
   4.325 +              apply (rule holomorphic_on_subset [OF holg])
   4.326 +              by (auto simp: kh nf1)
   4.327 +            show "\<theta> holomorphic_on g ` k ` (h \<circ> f) ` S"
   4.328 +              apply (rule holomorphic_on_subset [OF hol\<theta>])
   4.329 +              by (auto simp: gf kh nf1)
   4.330 +          qed
   4.331 +          show "((\<theta> \<circ> g \<circ> k) (h (f z)))\<^sup>2 = h (f z)" if "z \<in> S" for z
   4.332 +          proof -
   4.333 +            have "f z \<in> ball 0 1"
   4.334 +              by (simp add: nf1 that)
   4.335 +            then have "(\<theta> (g (k (h (f z)))))\<^sup>2 = (\<theta> (g (f z)))\<^sup>2"
   4.336 +              by (metis kh)
   4.337 +            also have "... = h (f z)"
   4.338 +              using \<theta>2 gf that by auto
   4.339 +            finally show ?thesis
   4.340 +              by (simp add: o_def)
   4.341 +          qed
   4.342 +        qed
   4.343 +      qed
   4.344 +      have norm\<psi>1: "norm(\<psi> (h (f z))) < 1" if "z \<in> S" for z
   4.345 +      proof -
   4.346 +        have "norm (\<psi> (h (f z)) ^ 2) < 1"
   4.347 +          by (metis (no_types) that DIM_complex \<psi>2 h01 image_subset_iff mem_ball_0 nf1)
   4.348 +        then show ?thesis
   4.349 +          by (metis le_less_trans mult_less_cancel_left2 norm_ge_zero norm_power not_le power2_eq_square)
   4.350 +      qed
   4.351 +      then have \<psi>01: "\<psi> (h (f 0)) \<in> ball 0 1"
   4.352 +        by (simp add: \<open>0 \<in> S\<close>)
   4.353 +      obtain p q where p0: "p (\<psi> (h (f 0))) = 0"
   4.354 +        and holp: "p holomorphic_on ball 0 1" and p01: "p ` ball 0 1 \<subseteq> ball 0 1"
   4.355 +        and holq: "q holomorphic_on ball 0 1" and q01: "q ` ball 0 1 \<subseteq> ball 0 1"
   4.356 +        and pq: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> p (q z) = z"
   4.357 +        and qp: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> q (p z) = z"
   4.358 +        using ball_biholomorphism_exists [OF \<psi>01] by metis
   4.359 +      have "p \<circ> \<psi> \<circ> h \<circ> f \<in> F"
   4.360 +        unfolding F_def
   4.361 +      proof (intro CollectI conjI holf)
   4.362 +        show "p \<circ> \<psi> \<circ> h \<circ> f holomorphic_on S"
   4.363 +        proof (intro holomorphic_on_compose holf)
   4.364 +          show "h holomorphic_on f ` S"
   4.365 +            apply (rule holomorphic_on_subset [OF holh])
   4.366 +            using f01 by force
   4.367 +          show "\<psi> holomorphic_on h ` f ` S"
   4.368 +            apply (rule holomorphic_on_subset [OF hol\<psi>])
   4.369 +            by auto
   4.370 +          show "p holomorphic_on \<psi> ` h ` f ` S"
   4.371 +            apply (rule holomorphic_on_subset [OF holp])
   4.372 +            by (auto simp: norm\<psi>1)
   4.373 +        qed
   4.374 +        show "(p \<circ> \<psi> \<circ> h \<circ> f) ` S \<subseteq> ball 0 1"
   4.375 +          apply clarsimp
   4.376 +          by (meson norm\<psi>1 p01 image_subset_iff mem_ball_0)
   4.377 +        show "(p \<circ> \<psi> \<circ> h \<circ> f) 0 = 0"
   4.378 +          by (simp add: \<open>p (\<psi> (h (f 0))) = 0\<close>)
   4.379 +        show "inj_on (p \<circ> \<psi> \<circ> h \<circ> f) S"
   4.380 +          unfolding inj_on_def o_def
   4.381 +          by (metis \<psi>2 dist_0_norm gf kh mem_ball nf1 norm\<psi>1 qp)
   4.382 +      qed
   4.383 +      then have le_norm_df0: "norm (deriv (p \<circ> \<psi> \<circ> h \<circ> f) 0) \<le> norm (deriv f 0)"
   4.384 +        by (rule normf)
   4.385 +      have 1: "k \<circ> power2 \<circ> q holomorphic_on ball 0 1"
   4.386 +      proof (intro holomorphic_on_compose holq)
   4.387 +        show "power2 holomorphic_on q ` ball 0 1"
   4.388 +          using holomorphic_on_subset holomorphic_on_power
   4.389 +          by (blast intro: holomorphic_on_ident)
   4.390 +        show "k holomorphic_on power2 ` q ` ball 0 1"
   4.391 +          apply (rule holomorphic_on_subset [OF holk])
   4.392 +          using q01 by (auto simp: norm_power abs_square_less_1)
   4.393 +      qed
   4.394 +      have 2: "(k \<circ> power2 \<circ> q) 0 = 0"
   4.395 +        using p0 F_def \<open>f \<in> F\<close> \<psi>01 \<psi>2 \<open>0 \<in> S\<close> kh qp by force
   4.396 +      have 3: "norm ((k \<circ> power2 \<circ> q) z) < 1" if "norm z < 1" for z
   4.397 +      proof -
   4.398 +        have "norm ((power2 \<circ> q) z) < 1"
   4.399 +          using that q01 by (force simp: norm_power abs_square_less_1)
   4.400 +        with k01 show ?thesis
   4.401 +          by fastforce
   4.402 +      qed
   4.403 +      have False if c: "\<forall>z. norm z < 1 \<longrightarrow> (k \<circ> power2 \<circ> q) z = c * z" and "norm c = 1" for c
   4.404 +      proof -
   4.405 +        have "c \<noteq> 0" using that by auto
   4.406 +        have "norm (p(1/2)) < 1" "norm (p(-1/2)) < 1"
   4.407 +          using p01 by force+
   4.408 +        then have "(k \<circ> power2 \<circ> q) (p(1/2)) = c * p(1/2)" "(k \<circ> power2 \<circ> q) (p(-1/2)) = c * p(-1/2)"
   4.409 +          using c by force+
   4.410 +        then have "p (1/2) = p (- (1/2))"
   4.411 +          by (auto simp: \<open>c \<noteq> 0\<close> qp o_def)
   4.412 +        then have "q (p (1/2)) = q (p (- (1/2)))"
   4.413 +          by simp
   4.414 +        then have "1/2 = - (1/2::complex)"
   4.415 +          by (auto simp: qp)
   4.416 +        then show False
   4.417 +          by simp
   4.418 +      qed
   4.419 +      moreover
   4.420 +      have False if "norm (deriv (k \<circ> power2 \<circ> q) 0) \<noteq> 1" "norm (deriv (k \<circ> power2 \<circ> q) 0) \<le> 1"
   4.421 +        and le: "\<And>\<xi>. norm \<xi> < 1 \<Longrightarrow> norm ((k \<circ> power2 \<circ> q) \<xi>) \<le> norm \<xi>"
   4.422 +      proof -
   4.423 +        have "norm (deriv (k \<circ> power2 \<circ> q) 0) < 1"
   4.424 +          using that by simp
   4.425 +        moreover have eq: "deriv f 0 = deriv (k \<circ> (\<lambda>z. z ^ 2) \<circ> q) 0 * deriv (p \<circ> \<psi> \<circ> h \<circ> f) 0"
   4.426 +        proof (intro DERIV_imp_deriv DERIV_transform_within_open [OF DERIV_chain])
   4.427 +          show "(k \<circ> power2 \<circ> q has_field_derivative deriv (k \<circ> power2 \<circ> q) 0) (at ((p \<circ> \<psi> \<circ> h \<circ> f) 0))"
   4.428 +            using "1" holomorphic_derivI p0 by auto
   4.429 +          show "(p \<circ> \<psi> \<circ> h \<circ> f has_field_derivative deriv (p \<circ> \<psi> \<circ> h \<circ> f) 0) (at 0)"
   4.430 +            using \<open>p \<circ> \<psi> \<circ> h \<circ> f \<in> F\<close> \<open>open S\<close> \<open>0 \<in> S\<close> holF holomorphic_derivI by blast
   4.431 +          show "\<And>x. x \<in> S \<Longrightarrow> (k \<circ> power2 \<circ> q \<circ> (p \<circ> \<psi> \<circ> h \<circ> f)) x = f x"
   4.432 +            using \<psi>2 f01 kh norm\<psi>1 qp by auto
   4.433 +        qed (use assms in simp_all)
   4.434 +        ultimately have "cmod (deriv (p \<circ> \<psi> \<circ> h \<circ> f) 0) \<le> 0"
   4.435 +          using le_norm_df0
   4.436 +          by (metis linorder_not_le mult.commute mult_less_cancel_left2 norm_mult)
   4.437 +        moreover have "1 \<le> norm (deriv f 0)"
   4.438 +          using normf [of id] by (simp add: idF)
   4.439 +        ultimately show False
   4.440 +          by (simp add: eq)
   4.441 +      qed
   4.442 +      ultimately show ?thesis
   4.443 +        using Schwarz_Lemma [OF 1 2 3] norm_one by blast
   4.444 +    qed
   4.445 +    then show "a \<in> f ` S"
   4.446 +      by blast
   4.447 +  qed
   4.448 +  then have "f ` S = ball 0 1"
   4.449 +    using F_def \<open>f \<in> F\<close> by blast
   4.450 +  then show ?thesis
   4.451 +    apply (rule_tac x=f in exI)
   4.452 +    apply (rule_tac x=g in exI)
   4.453 +    using holf holg derg gf by safe force+
   4.454 +qed
   4.455 +
   4.456 +
   4.457 +locale SC_Chain =
   4.458 +  fixes S :: "complex set"
   4.459 +  assumes openS: "open S"
   4.460 +begin
   4.461 +
   4.462 +lemma winding_number_zero:
   4.463 +  assumes "simply_connected S"
   4.464 +  shows "connected S \<and>
   4.465 +         (\<forall>\<gamma> z. path \<gamma> \<and> path_image \<gamma> \<subseteq> S \<and>
   4.466 +                   pathfinish \<gamma> = pathstart \<gamma> \<and> z \<notin> S \<longrightarrow> winding_number \<gamma> z = 0)"
   4.467 +  using assms
   4.468 +  by (auto simp: simply_connected_imp_connected simply_connected_imp_winding_number_zero)
   4.469 +
   4.470 +lemma contour_integral_zero:
   4.471 +  assumes "valid_path g" "path_image g \<subseteq> S" "pathfinish g = pathstart g" "f holomorphic_on S"
   4.472 +         "\<And>\<gamma> z. \<lbrakk>path \<gamma>; path_image \<gamma> \<subseteq> S; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> S\<rbrakk> \<Longrightarrow> winding_number \<gamma> z = 0"
   4.473 +  shows "(f has_contour_integral 0) g"
   4.474 +  using assms by (meson Cauchy_theorem_global openS valid_path_imp_path)
   4.475 +
   4.476 +lemma global_primitive:
   4.477 +  assumes "connected S" and holf: "f holomorphic_on S"
   4.478 +  and prev: "\<And>\<gamma> f. \<lbrakk>valid_path \<gamma>; path_image \<gamma> \<subseteq> S; pathfinish \<gamma> = pathstart \<gamma>; f holomorphic_on S\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) \<gamma>"
   4.479 +  shows "\<exists>h. \<forall>z \<in> S. (h has_field_derivative f z) (at z)"
   4.480 +proof (cases "S = {}")
   4.481 +case True then show ?thesis
   4.482 +    by simp
   4.483 +next
   4.484 +  case False
   4.485 +  then obtain a where "a \<in> S"
   4.486 +    by blast
   4.487 +  show ?thesis
   4.488 +  proof (intro exI ballI)
   4.489 +    fix x assume "x \<in> S"
   4.490 +    then obtain d where "d > 0" and d: "cball x d \<subseteq> S"
   4.491 +      using openS open_contains_cball_eq by blast
   4.492 +    let ?g = "\<lambda>z. (SOME g. polynomial_function g \<and> path_image g \<subseteq> S \<and> pathstart g = a \<and> pathfinish g = z)"
   4.493 +    show "((\<lambda>z. contour_integral (?g z) f) has_field_derivative f x)
   4.494 +          (at x)"
   4.495 +    proof (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right, rule Lim_transform)
   4.496 +      show "(\<lambda>y. inverse(norm(y - x)) *\<^sub>R (contour_integral(linepath x y) f - f x * (y - x))) \<midarrow>x\<rightarrow> 0"
   4.497 +      proof (clarsimp simp add: Lim_at)
   4.498 +        fix e::real assume "e > 0"
   4.499 +        moreover have "continuous (at x) f"
   4.500 +          using openS \<open>x \<in> S\<close> holf continuous_on_eq_continuous_at holomorphic_on_imp_continuous_on by auto
   4.501 +        ultimately obtain d1 where "d1 > 0"
   4.502 +             and d1: "\<And>x'. dist x' x < d1 \<Longrightarrow> dist (f x') (f x) < e/2"
   4.503 +          unfolding continuous_at_eps_delta
   4.504 +          by (metis less_divide_eq_numeral1(1) mult_zero_left)
   4.505 +        obtain d2 where "d2 > 0" and d2: "ball x d2 \<subseteq> S"
   4.506 +          using openS \<open>x \<in> S\<close> open_contains_ball_eq by blast
   4.507 +        have "inverse (norm (y - x)) * norm (contour_integral (linepath x y) f - f x * (y - x)) < e"
   4.508 +          if "0 < d1" "0 < d2" "y \<noteq> x" "dist y x < d1" "dist y x < d2" for y
   4.509 +        proof -
   4.510 +          have "f contour_integrable_on linepath x y"
   4.511 +          proof (rule contour_integrable_continuous_linepath [OF continuous_on_subset])
   4.512 +            show "continuous_on S f"
   4.513 +              by (simp add: holf holomorphic_on_imp_continuous_on)
   4.514 +            have "closed_segment x y \<subseteq> ball x d2"
   4.515 +              by (meson dist_commute_lessI dist_in_closed_segment le_less_trans mem_ball subsetI that(5))
   4.516 +            with d2 show "closed_segment x y \<subseteq> S"
   4.517 +              by blast
   4.518 +          qed
   4.519 +          then obtain z where z: "(f has_contour_integral z) (linepath x y)"
   4.520 +            by (force simp: contour_integrable_on_def)
   4.521 +          have con: "((\<lambda>w. f x) has_contour_integral f x * (y - x)) (linepath x y)"
   4.522 +            using has_contour_integral_const_linepath [of "f x" y x] by metis
   4.523 +          have "norm (z - f x * (y - x)) \<le> (e/2) * norm (y - x)"
   4.524 +          proof (rule has_contour_integral_bound_linepath)
   4.525 +            show "((\<lambda>w. f w - f x) has_contour_integral z - f x * (y - x)) (linepath x y)"
   4.526 +              by (rule has_contour_integral_diff [OF z con])
   4.527 +            show "\<And>w. w \<in> closed_segment x y \<Longrightarrow> norm (f w - f x) \<le> e/2"
   4.528 +              by (metis d1 dist_norm less_le_trans not_less not_less_iff_gr_or_eq segment_bound1 that(4))
   4.529 +          qed (use \<open>e > 0\<close> in auto)
   4.530 +          with \<open>e > 0\<close> have "inverse (norm (y - x)) * norm (z - f x * (y - x)) \<le> e/2"
   4.531 +            by (simp add: divide_simps)
   4.532 +          also have "... < e"
   4.533 +            using \<open>e > 0\<close> by simp
   4.534 +          finally show ?thesis
   4.535 +            by (simp add: contour_integral_unique [OF z])
   4.536 +        qed
   4.537 +        with  \<open>d1 > 0\<close> \<open>d2 > 0\<close>
   4.538 +        show "\<exists>d>0. \<forall>z. z \<noteq> x \<and> dist z x < d \<longrightarrow>
   4.539 +                 inverse (norm (z - x)) * norm (contour_integral (linepath x z) f - f x * (z - x)) < e"
   4.540 +          by (rule_tac x="min d1 d2" in exI) auto
   4.541 +      qed
   4.542 +    next
   4.543 +      have *: "(1 / norm (y - x)) *\<^sub>R (contour_integral (?g y) f -
   4.544 +               (contour_integral (?g x) f + f x * (y - x))) =
   4.545 +               (contour_integral (linepath x y) f - f x * (y - x)) /\<^sub>R norm (y - x)"
   4.546 +        if "0 < d" "y \<noteq> x" and yx: "dist y x < d" for y
   4.547 +      proof -
   4.548 +        have "y \<in> S"
   4.549 +          by (metis subsetD d dist_commute less_eq_real_def mem_cball yx)
   4.550 +        have gxy: "polynomial_function (?g x) \<and> path_image (?g x) \<subseteq> S \<and> pathstart (?g x) = a \<and> pathfinish (?g x) = x"
   4.551 +                  "polynomial_function (?g y) \<and> path_image (?g y) \<subseteq> S \<and> pathstart (?g y) = a \<and> pathfinish (?g y) = y"
   4.552 +          using someI_ex [OF connected_open_polynomial_connected [OF openS \<open>connected S\<close> \<open>a \<in> S\<close>]] \<open>x \<in> S\<close> \<open>y \<in> S\<close>
   4.553 +          by meson+
   4.554 +        then have vp: "valid_path (?g x)" "valid_path (?g y)"
   4.555 +          by (simp_all add: valid_path_polynomial_function)
   4.556 +        have f0: "(f has_contour_integral 0) ((?g x) +++ linepath x y +++ reversepath (?g y))"
   4.557 +        proof (rule prev)
   4.558 +          show "valid_path ((?g x) +++ linepath x y +++ reversepath (?g y))"
   4.559 +            using gxy vp by (auto simp: valid_path_join)
   4.560 +          have "closed_segment x y \<subseteq> cball x d"
   4.561 +            using  yx by (auto simp: dist_commute dest!: dist_in_closed_segment)
   4.562 +          then have "closed_segment x y \<subseteq> S"
   4.563 +            using d by blast
   4.564 +          then show "path_image ((?g x) +++ linepath x y +++ reversepath (?g y)) \<subseteq> S"
   4.565 +            using gxy by (auto simp: path_image_join)
   4.566 +        qed (use gxy holf in auto)
   4.567 +        then have fintxy: "f contour_integrable_on linepath x y"
   4.568 +          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))
   4.569 +        have fintgx: "f contour_integrable_on (?g x)" "f contour_integrable_on (?g y)"
   4.570 +          using openS contour_integrable_holomorphic_simple gxy holf vp by blast+
   4.571 +        show ?thesis
   4.572 +          apply (clarsimp simp add: divide_simps)
   4.573 +          using contour_integral_unique [OF f0]
   4.574 +          apply (simp add: fintxy gxy contour_integrable_reversepath contour_integral_reversepath fintgx vp)
   4.575 +          apply (simp add: algebra_simps)
   4.576 +          done
   4.577 +      qed
   4.578 +      show "(\<lambda>z. (1 / norm (z - x)) *\<^sub>R
   4.579 +                 (contour_integral (?g z) f - (contour_integral (?g x) f + f x * (z - x))) -
   4.580 +                 (contour_integral (linepath x z) f - f x * (z - x)) /\<^sub>R norm (z - x))
   4.581 +            \<midarrow>x\<rightarrow> 0"
   4.582 +        apply (rule Lim_eventually)
   4.583 +        apply (simp add: eventually_at)
   4.584 +        apply (rule_tac x=d in exI)
   4.585 +        using \<open>d > 0\<close> * by simp
   4.586 +    qed
   4.587 +  qed
   4.588 +qed
   4.589 +
   4.590 +lemma holomorphic_log:
   4.591 +  assumes "connected S" and holf: "f holomorphic_on S" and nz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
   4.592 +  and prev: "\<And>f. f holomorphic_on S \<Longrightarrow> \<exists>h. \<forall>z \<in> S. (h has_field_derivative f z) (at z)"
   4.593 +  shows "\<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S. f z = exp(g z))"
   4.594 +proof -
   4.595 +  have "(\<lambda>z. deriv f z / f z) holomorphic_on S"
   4.596 +    by (simp add: openS holf holomorphic_deriv holomorphic_on_divide nz)
   4.597 +  then obtain g where g: "\<And>z. z \<in> S \<Longrightarrow> (g has_field_derivative deriv f z / f z) (at z)"
   4.598 +    using prev [of "\<lambda>z. deriv f z / f z"] by metis
   4.599 +  have hfd: "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>z. exp (g z) / f z) has_field_derivative 0) (at x)"
   4.600 +    apply (rule derivative_eq_intros g| simp)+
   4.601 +      apply (subst DERIV_deriv_iff_field_differentiable)
   4.602 +    using openS holf holomorphic_on_imp_differentiable_at nz apply auto
   4.603 +    done
   4.604 +  obtain c where c: "\<And>x. x \<in> S \<Longrightarrow> exp (g x) / f x = c"
   4.605 +  proof (rule DERIV_zero_connected_constant[OF \<open>connected S\<close> openS finite.emptyI])
   4.606 +    show "continuous_on S (\<lambda>z. exp (g z) / f z)"
   4.607 +      by (metis (full_types) openS g continuous_on_divide continuous_on_exp holf holomorphic_on_imp_continuous_on holomorphic_on_open nz)
   4.608 +    then show "\<forall>x\<in>S - {}. ((\<lambda>z. exp (g z) / f z) has_field_derivative 0) (at x)"
   4.609 +      using hfd by (blast intro: DERIV_zero_connected_constant [OF \<open>connected S\<close> openS finite.emptyI, of "\<lambda>z. exp(g z) / f z"])
   4.610 +  qed auto
   4.611 +  show ?thesis
   4.612 +  proof (intro exI ballI conjI)
   4.613 +    show "(\<lambda>z. Ln(inverse c) + g z) holomorphic_on S"
   4.614 +      apply (intro holomorphic_intros)
   4.615 +      using openS g holomorphic_on_open by blast
   4.616 +    fix z :: complex
   4.617 +    assume "z \<in> S"
   4.618 +    then have "exp (g z) / c = f z"
   4.619 +      by (metis c divide_divide_eq_right exp_not_eq_zero nonzero_mult_div_cancel_left)
   4.620 +    moreover have "1 / c \<noteq> 0"
   4.621 +      using \<open>z \<in> S\<close> c nz by fastforce
   4.622 +    ultimately show "f z = exp (Ln (inverse c) + g z)"
   4.623 +      by (simp add: exp_add inverse_eq_divide)
   4.624 +  qed
   4.625 +qed
   4.626 +
   4.627 +lemma holomorphic_sqrt:
   4.628 +  assumes holf: "f holomorphic_on S" and nz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
   4.629 +  and prev: "\<And>f. \<lbrakk>f holomorphic_on S; \<forall>z \<in> S. f z \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S. f z = exp(g z))"
   4.630 +  shows "\<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S. f z = (g z)\<^sup>2)"
   4.631 +proof -
   4.632 +  obtain g where holg: "g holomorphic_on S" and g: "\<And>z. z \<in> S \<Longrightarrow> f z = exp (g z)"
   4.633 +    using prev [of f] holf nz by metis
   4.634 +  show ?thesis
   4.635 +  proof (intro exI ballI conjI)
   4.636 +    show "(\<lambda>z. exp(g z/2)) holomorphic_on S"
   4.637 +      by (intro holomorphic_intros) (auto simp: holg)
   4.638 +    show "\<And>z. z \<in> S \<Longrightarrow> f z = (exp (g z/2))\<^sup>2"
   4.639 +      by (metis (no_types) g exp_double nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral)
   4.640 +  qed
   4.641 +qed
   4.642 +
   4.643 +lemma biholomorphic_to_disc:
   4.644 +  assumes "connected S" and S: "S \<noteq> {}" "S \<noteq> UNIV"
   4.645 +  and prev: "\<And>f. \<lbrakk>f holomorphic_on S; \<forall>z \<in> S. f z \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S. f z = (g z)\<^sup>2)"
   4.646 +  shows "\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
   4.647 +                   (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
   4.648 +                   (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z)"
   4.649 +proof -
   4.650 +  obtain a b where "a \<in> S" "b \<notin> S"
   4.651 +    using S by blast
   4.652 +  then obtain \<delta> where "\<delta> > 0" and \<delta>: "ball a \<delta> \<subseteq> S"
   4.653 +    using openS openE by blast
   4.654 +  obtain g where holg: "g holomorphic_on S" and eqg: "\<And>z. z \<in> S \<Longrightarrow> z - b = (g z)\<^sup>2"
   4.655 +  proof (rule exE [OF prev [of "\<lambda>z. z - b"]])
   4.656 +    show "(\<lambda>z. z - b) holomorphic_on S"
   4.657 +      by (intro holomorphic_intros)
   4.658 +  qed (use \<open>b \<notin> S\<close> in auto)
   4.659 +  have "\<not> g constant_on S"
   4.660 +  proof -
   4.661 +    have "(a + \<delta>/2) \<in> ball a \<delta>" "a + (\<delta>/2) \<noteq> a"
   4.662 +      using \<open>\<delta> > 0\<close> by (simp_all add: dist_norm)
   4.663 +    then show ?thesis
   4.664 +      unfolding constant_on_def
   4.665 +      using eqg [of a] eqg [of "a + \<delta>/2"] \<open>a \<in> S\<close> \<delta>
   4.666 +      by (metis diff_add_cancel subset_eq)
   4.667 +  qed
   4.668 +  then have "open (g ` ball a \<delta>)"
   4.669 +    using open_mapping_thm [of g S "ball a \<delta>", OF holg openS \<open>connected S\<close>] \<delta> by blast
   4.670 +  then obtain r where "r > 0" and r: "ball (g a) r \<subseteq> (g ` ball a \<delta>)"
   4.671 +    by (metis \<open>0 < \<delta>\<close> centre_in_ball imageI openE)
   4.672 +  have g_not_r: "g z \<notin> ball (-(g a)) r" if "z \<in> S" for z
   4.673 +  proof
   4.674 +    assume "g z \<in> ball (-(g a)) r"
   4.675 +    then have "- g z \<in> ball (g a) r"
   4.676 +      by (metis add.inverse_inverse dist_minus mem_ball)
   4.677 +    with r have "- g z \<in> (g ` ball a \<delta>)"
   4.678 +      by blast
   4.679 +    then obtain w where w: "- g z = g w" "dist a w < \<delta>"
   4.680 +      by auto
   4.681 +    then have "w \<in> ball a \<delta>"
   4.682 +      by simp
   4.683 +    then have "w \<in> S"
   4.684 +      using \<delta> by blast
   4.685 +    then have "w = z"
   4.686 +      by (metis diff_add_cancel eqg power_minus_Bit0 that w(1))
   4.687 +    then have "g z = 0"
   4.688 +      using \<open>- g z = g w\<close> by auto
   4.689 +    with eqg [OF that] have "z = b"
   4.690 +      by auto
   4.691 +    with that \<open>b \<notin> S\<close> show False
   4.692 +      by simp
   4.693 +  qed
   4.694 +  then have nz: "\<And>z. z \<in> S \<Longrightarrow> g z + g a \<noteq> 0"
   4.695 +    by (metis \<open>0 < r\<close> add.commute add_diff_cancel_left' centre_in_ball diff_0)
   4.696 +  let ?f = "\<lambda>z. (r/3) / (g z + g a) - (r/3) / (g a + g a)"
   4.697 +  obtain h where holh: "h holomorphic_on S" and "h a = 0" and h01: "h ` S \<subseteq> ball 0 1" and "inj_on h S"
   4.698 +  proof
   4.699 +    show "?f holomorphic_on S"
   4.700 +      by (intro holomorphic_intros holg nz)
   4.701 +    have 3: "\<lbrakk>norm x \<le> 1/3; norm y \<le> 1/3\<rbrakk> \<Longrightarrow> norm(x - y) < 1" for x y::complex
   4.702 +      using norm_triangle_ineq4 [of x y] by simp
   4.703 +    have "norm ((r/3) / (g z + g a) - (r/3) / (g a + g a)) < 1" if "z \<in> S" for z
   4.704 +      apply (rule 3)
   4.705 +      unfolding norm_divide
   4.706 +      using \<open>r > 0\<close> g_not_r [OF \<open>z \<in> S\<close>] g_not_r [OF \<open>a \<in> S\<close>]
   4.707 +      by (simp_all add: divide_simps dist_commute dist_norm)
   4.708 +  then show "?f ` S \<subseteq> ball 0 1"
   4.709 +    by auto
   4.710 +    show "inj_on ?f S"
   4.711 +      using \<open>r > 0\<close> eqg apply (clarsimp simp: inj_on_def)
   4.712 +      by (metis diff_add_cancel)
   4.713 +  qed auto
   4.714 +  obtain k where holk: "k holomorphic_on (h ` S)"
   4.715 +             and derk: "\<And>z. z \<in> S \<Longrightarrow> deriv h z * deriv k (h z) = 1"
   4.716 +             and kh: "\<And>z. z \<in> S \<Longrightarrow> k(h z) = z"
   4.717 +    using holomorphic_has_inverse [OF holh openS \<open>inj_on h S\<close>] by metis
   4.718 +
   4.719 +  have 1: "open (h ` S)"
   4.720 +    by (simp add: \<open>inj_on h S\<close> holh openS open_mapping_thm3)
   4.721 +  have 2: "connected (h ` S)"
   4.722 +    by (simp add: connected_continuous_image \<open>connected S\<close> holh holomorphic_on_imp_continuous_on)
   4.723 +  have 3: "0 \<in> h ` S"
   4.724 +    using \<open>a \<in> S\<close> \<open>h a = 0\<close> by auto
   4.725 +  have 4: "\<exists>g. g holomorphic_on h ` S \<and> (\<forall>z\<in>h ` S. f z = (g z)\<^sup>2)"
   4.726 +    if holf: "f holomorphic_on h ` S" and nz: "\<And>z. z \<in> h ` S \<Longrightarrow> f z \<noteq> 0" "inj_on f (h ` S)" for f
   4.727 +  proof -
   4.728 +    obtain g where holg: "g holomorphic_on S" and eqg: "\<And>z. z \<in> S \<Longrightarrow> (f \<circ> h) z = (g z)\<^sup>2"
   4.729 +    proof -
   4.730 +      have "f \<circ> h holomorphic_on S"
   4.731 +        by (simp add: holh holomorphic_on_compose holf)
   4.732 +      moreover have "\<forall>z\<in>S. (f \<circ> h) z \<noteq> 0"
   4.733 +        by (simp add: nz)
   4.734 +      ultimately show thesis
   4.735 +        using prev that by blast
   4.736 +    qed
   4.737 +    show ?thesis
   4.738 +    proof (intro exI conjI)
   4.739 +      show "g \<circ> k holomorphic_on h ` S"
   4.740 +      proof -
   4.741 +        have "k ` h ` S \<subseteq> S"
   4.742 +          by (simp add: \<open>\<And>z. z \<in> S \<Longrightarrow> k (h z) = z\<close> image_subset_iff)
   4.743 +        then show ?thesis
   4.744 +          by (meson holg holk holomorphic_on_compose holomorphic_on_subset)
   4.745 +      qed
   4.746 +      show "\<forall>z\<in>h ` S. f z = ((g \<circ> k) z)\<^sup>2"
   4.747 +        using eqg kh by auto
   4.748 +    qed
   4.749 +  qed
   4.750 +  obtain f g where f: "f holomorphic_on h ` S" and g: "g holomorphic_on ball 0 1"
   4.751 +       and gf: "\<forall>z\<in>h ` S. f z \<in> ball 0 1 \<and> g (f z) = z"  and fg:"\<forall>z\<in>ball 0 1. g z \<in> h ` S \<and> f (g z) = z"
   4.752 +    using biholomorphic_to_disc_aux [OF 1 2 3 h01 4] by blast
   4.753 +  show ?thesis
   4.754 +  proof (intro exI conjI)
   4.755 +    show "f \<circ> h holomorphic_on S"
   4.756 +      by (simp add: f holh holomorphic_on_compose)
   4.757 +    show "k \<circ> g holomorphic_on ball 0 1"
   4.758 +      by (metis holomorphic_on_subset image_subset_iff fg holk g holomorphic_on_compose)
   4.759 +  qed (use fg gf kh in auto)
   4.760 +qed
   4.761 +
   4.762 +lemma homeomorphic_to_disc:
   4.763 +  assumes S: "S \<noteq> {}"
   4.764 +    and prev: "S = UNIV \<or>
   4.765 +               (\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
   4.766 +                     (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
   4.767 +                     (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z))" (is "_ \<or> ?P")
   4.768 +  shows "S homeomorphic ball (0::complex) 1"
   4.769 +  using prev
   4.770 +proof
   4.771 +  assume "S = UNIV" then show ?thesis
   4.772 +    using homeomorphic_ball01_UNIV homeomorphic_sym by blast
   4.773 +next
   4.774 +  assume ?P
   4.775 +  then show ?thesis
   4.776 +    unfolding homeomorphic_minimal
   4.777 +    using holomorphic_on_imp_continuous_on by blast
   4.778 +qed
   4.779 +
   4.780 +lemma homeomorphic_to_disc_imp_simply_connected:
   4.781 +  assumes "S = {} \<or> S homeomorphic ball (0::complex) 1"
   4.782 +  shows "simply_connected S"
   4.783 +  using assms homeomorphic_simply_connected_eq convex_imp_simply_connected by auto
   4.784 +
   4.785 +end
   4.786 +
   4.787 +
   4.788 +proposition
   4.789 +  assumes "open S"
   4.790 +  shows simply_connected_eq_winding_number_zero:
   4.791 +         "simply_connected S \<longleftrightarrow>
   4.792 +           connected S \<and>
   4.793 +           (\<forall>g z. path g \<and> path_image g \<subseteq> S \<and>
   4.794 +                 pathfinish g = pathstart g \<and> (z \<notin> S)
   4.795 +                 \<longrightarrow> winding_number g z = 0)" (is "?wn0")
   4.796 +    and simply_connected_eq_contour_integral_zero:
   4.797 +         "simply_connected S \<longleftrightarrow>
   4.798 +           connected S \<and>
   4.799 +           (\<forall>g f. valid_path g \<and> path_image g \<subseteq> S \<and>
   4.800 +                 pathfinish g = pathstart g \<and> f holomorphic_on S
   4.801 +               \<longrightarrow> (f has_contour_integral 0) g)" (is "?ci0")
   4.802 +    and simply_connected_eq_global_primitive:
   4.803 +         "simply_connected S \<longleftrightarrow>
   4.804 +           connected S \<and>
   4.805 +           (\<forall>f. f holomorphic_on S \<longrightarrow>
   4.806 +                (\<exists>h. \<forall>z. z \<in> S \<longrightarrow> (h has_field_derivative f z) (at z)))" (is "?gp")
   4.807 +    and simply_connected_eq_holomorphic_log:
   4.808 +         "simply_connected S \<longleftrightarrow>
   4.809 +           connected S \<and>
   4.810 +           (\<forall>f. f holomorphic_on S \<and> (\<forall>z \<in> S. f z \<noteq> 0)
   4.811 +               \<longrightarrow> (\<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S. f z = exp(g z))))" (is "?log")
   4.812 +    and simply_connected_eq_holomorphic_sqrt:
   4.813 +         "simply_connected S \<longleftrightarrow>
   4.814 +           connected S \<and>
   4.815 +           (\<forall>f. f holomorphic_on S \<and> (\<forall>z \<in> S. f z \<noteq> 0)
   4.816 +                \<longrightarrow> (\<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S.  f z = (g z)\<^sup>2)))" (is "?sqrt")
   4.817 +    and simply_connected_eq_biholomorphic_to_disc:
   4.818 +         "simply_connected S \<longleftrightarrow>
   4.819 +           S = {} \<or> S = UNIV \<or>
   4.820 +           (\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
   4.821 +                 (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
   4.822 +                 (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z))" (is "?bih")
   4.823 +    and simply_connected_eq_homeomorphic_to_disc:
   4.824 +          "simply_connected S \<longleftrightarrow> S = {} \<or> S homeomorphic ball (0::complex) 1" (is "?disc")
   4.825 +proof -
   4.826 +  interpret SC_Chain
   4.827 +    using assms by (simp add: SC_Chain_def)
   4.828 +  have "?wn0 \<and> ?ci0 \<and> ?gp \<and> ?log \<and> ?sqrt \<and> ?bih \<and> ?disc"
   4.829 +proof -
   4.830 +  have *: "\<lbrakk>\<alpha> \<Longrightarrow> \<beta>; \<beta> \<Longrightarrow> \<gamma>; \<gamma> \<Longrightarrow> \<delta>; \<delta> \<Longrightarrow> \<zeta>; \<zeta> \<Longrightarrow> \<eta>; \<eta> \<Longrightarrow> \<theta>; \<theta> \<Longrightarrow> \<xi>; \<xi> \<Longrightarrow> \<alpha>\<rbrakk>
   4.831 +        \<Longrightarrow> (\<alpha> \<longleftrightarrow> \<beta>) \<and> (\<alpha> \<longleftrightarrow> \<gamma>) \<and> (\<alpha> \<longleftrightarrow> \<delta>) \<and> (\<alpha> \<longleftrightarrow> \<zeta>) \<and>
   4.832 +            (\<alpha> \<longleftrightarrow> \<eta>) \<and> (\<alpha> \<longleftrightarrow> \<theta>) \<and> (\<alpha> \<longleftrightarrow> \<xi>)" for \<alpha> \<beta> \<gamma> \<delta> \<zeta> \<eta> \<theta> \<xi>
   4.833 +    by blast
   4.834 +  show ?thesis
   4.835 +    apply (rule *)
   4.836 +    using winding_number_zero apply metis
   4.837 +    using contour_integral_zero apply metis
   4.838 +    using global_primitive apply metis
   4.839 +    using holomorphic_log apply metis
   4.840 +    using holomorphic_sqrt apply simp
   4.841 +    using biholomorphic_to_disc apply blast
   4.842 +    using homeomorphic_to_disc apply blast
   4.843 +    using homeomorphic_to_disc_imp_simply_connected apply blast
   4.844 +    done
   4.845 +qed
   4.846 +  then show ?wn0 ?ci0 ?gp ?log ?sqrt ?bih ?disc
   4.847 +    by safe
   4.848 +qed
   4.849 +
   4.850 +
   4.851 +corollary contractible_eq_simply_connected_2d:
   4.852 +  fixes S :: "complex set"
   4.853 +  shows "open S \<Longrightarrow> (contractible S \<longleftrightarrow> simply_connected S)"
   4.854 +  apply safe
   4.855 +   apply (simp add: contractible_imp_simply_connected)
   4.856 +  using convex_imp_contractible homeomorphic_contractible_eq simply_connected_eq_homeomorphic_to_disc by auto
   4.857 +
   4.858 +
   4.859 +subsection\<open>A further chain of equivalences about components of the complement of a simply connected set.\<close>
   4.860 +
   4.861 +text\<open>(following 1.35 in Burckel'S book)\<close>
   4.862 +
   4.863 +context SC_Chain
   4.864 +begin
   4.865 +
   4.866 +lemma frontier_properties:
   4.867 +  assumes "simply_connected S"
   4.868 +  shows "if bounded S then connected(frontier S)
   4.869 +         else \<forall>C \<in> components(frontier S). ~bounded C"
   4.870 +proof -
   4.871 +  have "S = {} \<or> S homeomorphic ball (0::complex) 1"
   4.872 +    using simply_connected_eq_homeomorphic_to_disc assms openS by blast
   4.873 +  then show ?thesis
   4.874 +  proof
   4.875 +    assume "S = {}"
   4.876 +    then have "bounded S"
   4.877 +      by simp
   4.878 +    with \<open>S = {}\<close> show ?thesis
   4.879 +      by simp
   4.880 +  next
   4.881 +    assume S01: "S homeomorphic ball (0::complex) 1"
   4.882 +    then obtain g f
   4.883 +      where gim: "g ` S = ball 0 1" and fg: "\<And>x. x \<in> S \<Longrightarrow> f(g x) = x"
   4.884 +        and fim: "f ` ball 0 1 = S" and gf: "\<And>y. cmod y < 1 \<Longrightarrow> g(f y) = y"
   4.885 +        and contg: "continuous_on S g" and contf: "continuous_on (ball 0 1) f"
   4.886 +      by (fastforce simp: homeomorphism_def homeomorphic_def)
   4.887 +    define D where "D \<equiv> \<lambda>n. ball (0::complex) (1 - 1/(of_nat n + 2))"
   4.888 +    define A where "A \<equiv> \<lambda>n. {z::complex. 1 - 1/(of_nat n + 2) < norm z \<and> norm z < 1}"
   4.889 +    define X where "X \<equiv> \<lambda>n::nat. closure(f ` A n)"
   4.890 +    have D01: "D n \<subseteq> ball 0 1" for n
   4.891 +      by (simp add: D_def ball_subset_ball_iff)
   4.892 +    have A01: "A n \<subseteq> ball 0 1" for n
   4.893 +      by (auto simp: A_def)
   4.894 +    have cloX: "closed(X n)" for n
   4.895 +      by (simp add: X_def)
   4.896 +    have Xsubclo: "X n \<subseteq> closure S" for n
   4.897 +      unfolding X_def by (metis A01 closure_mono fim image_mono)
   4.898 +    have connX: "connected(X n)" for n
   4.899 +      unfolding X_def
   4.900 +      apply (rule connected_imp_connected_closure)
   4.901 +      apply (rule connected_continuous_image)
   4.902 +      apply (simp add: continuous_on_subset [OF contf A01])
   4.903 +      using connected_annulus [of _ "0::complex"] by (simp add: A_def)
   4.904 +    have nestX: "X n \<subseteq> X m" if "m \<le> n" for m n
   4.905 +    proof -
   4.906 +      have "1 - 1 / (real m + 2) \<le> 1 - 1 / (real n + 2)"
   4.907 +        using that by (auto simp: field_simps)
   4.908 +      then show ?thesis
   4.909 +        by (auto simp: X_def A_def intro!: closure_mono)
   4.910 +    qed
   4.911 +    have "closure S - S \<subseteq> (\<Inter>n. X n)"
   4.912 +    proof
   4.913 +      fix x
   4.914 +      assume "x \<in> closure S - S"
   4.915 +      then have "x \<in> closure S" "x \<notin> S" by auto
   4.916 +      show "x \<in> (\<Inter>n. X n)"
   4.917 +      proof
   4.918 +        fix n
   4.919 +        have "ball 0 1 = closure (D n) \<union> A n"
   4.920 +          by (auto simp: D_def A_def le_less_trans)
   4.921 +        with fim have Seq: "S = f ` (closure (D n)) \<union> f ` (A n)"
   4.922 +          by (simp add: image_Un)
   4.923 +        have "continuous_on (closure (D n)) f"
   4.924 +          by (simp add: D_def cball_subset_ball_iff continuous_on_subset [OF contf])
   4.925 +        moreover have "compact (closure (D n))"
   4.926 +          by (simp add: D_def)
   4.927 +        ultimately have clo_fim: "closed (f ` closure (D n))"
   4.928 +          using compact_continuous_image compact_imp_closed by blast
   4.929 +        have *: "(f ` cball 0 (1 - 1 / (real n + 2))) \<subseteq> S"
   4.930 +          by (force simp: D_def Seq)
   4.931 +        show "x \<in> X n"
   4.932 +          using \<open>x \<in> closure S\<close> unfolding X_def Seq
   4.933 +          using \<open>x \<notin> S\<close> * D_def clo_fim by auto
   4.934 +      qed
   4.935 +    qed
   4.936 +    moreover have "(\<Inter>n. X n) \<subseteq> closure S - S"
   4.937 +    proof -
   4.938 +      have "(\<Inter>n. X n) \<subseteq> closure S"
   4.939 +      proof -
   4.940 +        have "(\<Inter>n. X n) \<subseteq> X 0"
   4.941 +          by blast
   4.942 +        also have "... \<subseteq> closure S"
   4.943 +          apply (simp add: X_def fim [symmetric])
   4.944 +          apply (rule closure_mono)
   4.945 +          by (auto simp: A_def)
   4.946 +        finally show "(\<Inter>n. X n) \<subseteq> closure S" .
   4.947 +      qed
   4.948 +      moreover have "(\<Inter>n. X n) \<inter> S \<subseteq> {}"
   4.949 +      proof (clarify, clarsimp simp: X_def fim [symmetric])
   4.950 +        fix x assume x [rule_format]: "\<forall>n. f x \<in> closure (f ` A n)" and "cmod x < 1"
   4.951 +        then obtain n where n: "1 / (1 - norm x) < of_nat n"
   4.952 +          using reals_Archimedean2 by blast
   4.953 +        with \<open>cmod x < 1\<close> gr0I have XX: "1 / of_nat n < 1 - norm x" and "n > 0"
   4.954 +          by (fastforce simp: divide_simps algebra_simps)+
   4.955 +        have "f x \<in> f ` (D n)"
   4.956 +          using n \<open>cmod x < 1\<close> by (auto simp: divide_simps algebra_simps D_def)
   4.957 +        moreover have " f ` D n \<inter> closure (f ` A n) = {}"
   4.958 +        proof -
   4.959 +          have op_fDn: "open(f ` (D n))"
   4.960 +          proof (rule invariance_of_domain)
   4.961 +            show "continuous_on (D n) f"
   4.962 +              by (rule continuous_on_subset [OF contf D01])
   4.963 +            show "open (D n)"
   4.964 +              by (simp add: D_def)
   4.965 +            show "inj_on f (D n)"
   4.966 +              unfolding inj_on_def using D01 by (metis gf mem_ball_0 subsetCE)
   4.967 +          qed
   4.968 +          have injf: "inj_on f (ball 0 1)"
   4.969 +            by (metis mem_ball_0 inj_on_def gf)
   4.970 +          have "D n \<union> A n \<subseteq> ball 0 1"
   4.971 +            using D01 A01 by simp
   4.972 +          moreover have "D n \<inter> A n = {}"
   4.973 +            by (auto simp: D_def A_def)
   4.974 +          ultimately have "f ` D n \<inter> f ` A n = {}"
   4.975 +            by (metis A01 D01 image_is_empty inj_on_image_Int injf)
   4.976 +          then show ?thesis
   4.977 +            by (simp add: open_Int_closure_eq_empty [OF op_fDn])
   4.978 +        qed
   4.979 +        ultimately show False
   4.980 +          using x [of n] by blast
   4.981 +      qed
   4.982 +      ultimately
   4.983 +      show "(\<Inter>n. X n) \<subseteq> closure S - S"
   4.984 +        using closure_subset disjoint_iff_not_equal by blast
   4.985 +    qed
   4.986 +    ultimately have "closure S - S = (\<Inter>n. X n)" by blast
   4.987 +    then have frontierS: "frontier S = (\<Inter>n. X n)"
   4.988 +      by (simp add: frontier_def openS interior_open)
   4.989 +    show ?thesis
   4.990 +    proof (cases "bounded S")
   4.991 +      case True
   4.992 +      have bouX: "bounded (X n)" for n
   4.993 +        apply (simp add: X_def)
   4.994 +        apply (rule bounded_closure)
   4.995 +        by (metis A01 fim image_mono bounded_subset [OF True])
   4.996 +      have compaX: "compact (X n)" for n
   4.997 +        apply (simp add: compact_eq_bounded_closed bouX)
   4.998 +        apply (auto simp: X_def)
   4.999 +        done
  4.1000 +      have "connected (\<Inter>n. X n)"
  4.1001 +        by (metis nestX compaX connX connected_nest)
  4.1002 +      then show ?thesis
  4.1003 +        by (simp add: True \<open>frontier S = (\<Inter>n. X n)\<close>)
  4.1004 +    next
  4.1005 +      case False
  4.1006 +      have unboundedX: "\<not> bounded(X n)" for n
  4.1007 +      proof
  4.1008 +        assume bXn: "bounded(X n)"
  4.1009 +        have "continuous_on (cball 0 (1 - 1 / (2 + real n))) f"
  4.1010 +          by (simp add: cball_subset_ball_iff continuous_on_subset [OF contf])
  4.1011 +        then have "bounded (f ` cball 0 (1 - 1 / (2 + real n)))"
  4.1012 +          by (simp add: compact_imp_bounded [OF compact_continuous_image])
  4.1013 +        moreover have "bounded (f ` A n)"
  4.1014 +          by (auto simp: X_def closure_subset image_subset_iff bounded_subset [OF bXn])
  4.1015 +        ultimately have "bounded (f ` (cball 0 (1 - 1/(2 + real n)) \<union> A n))"
  4.1016 +          by (simp add: image_Un)
  4.1017 +        then have "bounded (f ` ball 0 1)"
  4.1018 +          apply (rule bounded_subset)
  4.1019 +          apply (auto simp: A_def algebra_simps)
  4.1020 +          done
  4.1021 +        then show False
  4.1022 +          using False by (simp add: fim [symmetric])
  4.1023 +      qed
  4.1024 +      have clo_INTX: "closed(\<Inter>(range X))"
  4.1025 +        by (metis cloX closed_INT)
  4.1026 +      then have lcX: "locally compact (\<Inter>(range X))"
  4.1027 +        by (metis closed_imp_locally_compact)
  4.1028 +      have False if C: "C \<in> components (frontier S)" and boC: "bounded C" for C
  4.1029 +      proof -
  4.1030 +        have "closed C"
  4.1031 +          by (metis C closed_components frontier_closed)
  4.1032 +        then have "compact C"
  4.1033 +          by (metis boC compact_eq_bounded_closed)
  4.1034 +        have Cco: "C \<in> components (\<Inter>(range X))"
  4.1035 +          by (metis frontierS C)
  4.1036 +        obtain K where "C \<subseteq> K" "compact K"
  4.1037 +                   and Ksub: "K \<subseteq> \<Inter>(range X)" and clo: "closed(\<Inter>(range X) - K)"
  4.1038 +        proof (cases "{k. C \<subseteq> k \<and> compact k \<and> openin (subtopology euclidean (\<Inter>(range X))) k} = {}")
  4.1039 +          case True
  4.1040 +          then show ?thesis
  4.1041 +            using Sura_Bura [OF lcX Cco \<open>compact C\<close>] boC
  4.1042 +            by (simp add: True)
  4.1043 +        next
  4.1044 +          case False
  4.1045 +          then obtain L where "compact L" "C \<subseteq> L" and K: "openin (subtopology euclidean (\<Inter>x. X x)) L"
  4.1046 +            by blast
  4.1047 +          show ?thesis
  4.1048 +          proof
  4.1049 +            show "L \<subseteq> \<Inter>(range X)"
  4.1050 +              by (metis K openin_imp_subset)
  4.1051 +            show "closed (\<Inter>(range X) - L)"
  4.1052 +              by (metis closedin_diff closedin_self closedin_closed_trans [OF _ clo_INTX] K)
  4.1053 +          qed (use \<open>compact L\<close> \<open>C \<subseteq> L\<close> in auto)
  4.1054 +        qed
  4.1055 +        obtain U V where "open U" and "compact (closure U)" and "open V" "K \<subseteq> U"
  4.1056 +                     and V: "\<Inter>(range X) - K \<subseteq> V" and "U \<inter> V = {}"
  4.1057 +          using separation_normal_compact [OF \<open>compact K\<close> clo] by blast
  4.1058 +        then have "U \<inter> (\<Inter> (range X) - K) = {}"
  4.1059 +          by blast
  4.1060 +        have "(closure U - U) \<inter> (\<Inter>n. X n \<inter> closure U) \<noteq> {}"
  4.1061 +        proof (rule compact_imp_fip)
  4.1062 +          show "compact (closure U - U)"
  4.1063 +            by (metis \<open>compact (closure U)\<close> \<open>open U\<close> compact_diff)
  4.1064 +          show "\<And>T. T \<in> range (\<lambda>n. X n \<inter> closure U) \<Longrightarrow> closed T"
  4.1065 +            by clarify (metis cloX closed_Int closed_closure)
  4.1066 +          show "(closure U - U) \<inter> \<Inter>\<F> \<noteq> {}"
  4.1067 +            if "finite \<F>" and \<F>: "\<F> \<subseteq> range (\<lambda>n. X n \<inter> closure U)" for \<F>
  4.1068 +          proof
  4.1069 +            assume empty: "(closure U - U) \<inter> \<Inter>\<F> = {}"
  4.1070 +            obtain J where "finite J" and J: "\<F> = (\<lambda>n. X n \<inter> closure U) ` J"
  4.1071 +              using finite_subset_image [OF \<open>finite \<F>\<close> \<F>] by auto
  4.1072 +            show False
  4.1073 +            proof (cases "J = {}")
  4.1074 +              case True
  4.1075 +              with J empty have "closed U"
  4.1076 +                by (simp add: closure_subset_eq)
  4.1077 +              have "C \<noteq> {}"
  4.1078 +                using C in_components_nonempty by blast
  4.1079 +              then have "U \<noteq> {}"
  4.1080 +                using \<open>K \<subseteq> U\<close> \<open>C \<subseteq> K\<close> by blast
  4.1081 +              moreover have "U \<noteq> UNIV"
  4.1082 +                using \<open>compact (closure U)\<close> by auto
  4.1083 +              ultimately show False
  4.1084 +                using \<open>open U\<close> \<open>closed U\<close> clopen by blast
  4.1085 +            next
  4.1086 +              case False
  4.1087 +              define j where "j \<equiv> Max J"
  4.1088 +              have "j \<in> J"
  4.1089 +                by (simp add: False \<open>finite J\<close> j_def)
  4.1090 +              have jmax: "\<And>m. m \<in> J \<Longrightarrow> m \<le> j"
  4.1091 +                by (simp add: j_def \<open>finite J\<close>)
  4.1092 +              have "\<Inter> ((\<lambda>n. X n \<inter> closure U) ` J) = X j \<inter> closure U"
  4.1093 +                using False jmax nestX \<open>j \<in> J\<close> by auto
  4.1094 +              then have "X j \<inter> closure U = X j \<inter> U"
  4.1095 +                apply safe
  4.1096 +                using DiffI J empty apply auto[1]
  4.1097 +                using closure_subset by blast
  4.1098 +              then have "openin (subtopology euclidean (X j)) (X j \<inter> closure U)"
  4.1099 +                by (simp add: openin_open_Int \<open>open U\<close>)
  4.1100 +              moreover have "closedin (subtopology euclidean (X j)) (X j \<inter> closure U)"
  4.1101 +                by (simp add: closedin_closed_Int)
  4.1102 +              moreover have "X j \<inter> closure U \<noteq> X j"
  4.1103 +                by (metis unboundedX \<open>compact (closure U)\<close> bounded_subset compact_eq_bounded_closed inf.order_iff)
  4.1104 +              moreover have "X j \<inter> closure U \<noteq> {}"
  4.1105 +              proof -
  4.1106 +                have "C \<noteq> {}"
  4.1107 +                  using C in_components_nonempty by blast
  4.1108 +                moreover have "C \<subseteq> X j \<inter> closure U"
  4.1109 +                  using \<open>C \<subseteq> K\<close> \<open>K \<subseteq> U\<close> Ksub closure_subset by blast
  4.1110 +                ultimately show ?thesis by blast
  4.1111 +              qed
  4.1112 +              ultimately show False
  4.1113 +                using connX [of j] by (force simp: connected_clopen)
  4.1114 +            qed
  4.1115 +          qed
  4.1116 +        qed
  4.1117 +        moreover have "(\<Inter>n. X n \<inter> closure U) = (\<Inter>n. X n) \<inter> closure U"
  4.1118 +          by blast
  4.1119 +        moreover have "x \<in> U" if "\<And>n. x \<in> X n" "x \<in> closure U" for x
  4.1120 +        proof -
  4.1121 +          have "x \<notin> V"
  4.1122 +            using \<open>U \<inter> V = {}\<close> \<open>open V\<close> closure_iff_nhds_not_empty that(2) by blast
  4.1123 +          then show ?thesis
  4.1124 +            by (metis (no_types) Diff_iff INT_I V \<open>K \<subseteq> U\<close> contra_subsetD that(1))
  4.1125 +        qed
  4.1126 +        ultimately show False
  4.1127 +          by (auto simp: open_Int_closure_eq_empty [OF \<open>open V\<close>, of U])
  4.1128 +      qed
  4.1129 +      then show ?thesis
  4.1130 +        by (auto simp: False)
  4.1131 +    qed
  4.1132 +  qed
  4.1133 +qed
  4.1134 +
  4.1135 +
  4.1136 +lemma unbounded_complement_components:
  4.1137 +  assumes C: "C \<in> components (- S)" and S: "connected S"
  4.1138 +    and prev: "if bounded S then connected(frontier S)
  4.1139 +               else \<forall>C \<in> components(frontier S). \<not> bounded C"
  4.1140 +  shows "\<not> bounded C"
  4.1141 +proof (cases "bounded S")
  4.1142 +  case True
  4.1143 +  with prev have "S \<noteq> UNIV" and confr: "connected(frontier S)"
  4.1144 +    by auto
  4.1145 +  obtain w where C_ccsw: "C = connected_component_set (- S) w" and "w \<notin> S"
  4.1146 +    using C by (auto simp: components_def)
  4.1147 +  show ?thesis
  4.1148 +  proof (cases "S = {}")
  4.1149 +    case True with C show ?thesis by auto
  4.1150 +  next
  4.1151 +    case False
  4.1152 +    show ?thesis
  4.1153 +    proof
  4.1154 +      assume "bounded C"
  4.1155 +      then have "outside C \<noteq> {}"
  4.1156 +        using outside_bounded_nonempty by metis
  4.1157 +      then obtain z where z: "\<not> bounded (connected_component_set (- C) z)" and "z \<notin> C"
  4.1158 +        by (auto simp: outside_def)
  4.1159 +      have clo_ccs: "closed (connected_component_set (- S) x)" for x
  4.1160 +        by (simp add: closed_Compl closed_connected_component openS)
  4.1161 +      have "connected_component_set (- S) w = connected_component_set (- S) z"
  4.1162 +      proof (rule joinable_connected_component_eq [OF confr])
  4.1163 +        show "frontier S \<subseteq> - S"
  4.1164 +          using openS by (auto simp: frontier_def interior_open)
  4.1165 +        have False if "connected_component_set (- S) w \<inter> frontier (- S) = {}"
  4.1166 +        proof -
  4.1167 +          have "C \<inter> frontier S = {}"
  4.1168 +            using that by (simp add: C_ccsw)
  4.1169 +          then show False
  4.1170 +            by (metis C_ccsw ComplI Compl_eq_Compl_iff Diff_subset False \<open>w \<notin> S\<close> clo_ccs closure_closed compl_bot_eq connected_component_eq_UNIV connected_component_eq_empty empty_subsetI frontier_complement frontier_def frontier_not_empty frontier_of_connected_component_subset le_inf_iff subset_antisym)
  4.1171 +        qed
  4.1172 +        then show "connected_component_set (- S) w \<inter> frontier S \<noteq> {}"
  4.1173 +          by auto
  4.1174 +        have *: "\<lbrakk>frontier C \<subseteq> C; frontier C \<subseteq> F; frontier C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<inter> F \<noteq> {}" for C F::"complex set"
  4.1175 +          by blast
  4.1176 +        have "connected_component_set (- S) z \<inter> frontier (- S) \<noteq> {}"
  4.1177 +        proof (rule *)
  4.1178 +          show "frontier (connected_component_set (- S) z) \<subseteq> connected_component_set (- S) z"
  4.1179 +            by (auto simp: closed_Compl closed_connected_component frontier_def openS)
  4.1180 +          show "frontier (connected_component_set (- S) z) \<subseteq> frontier (- S)"
  4.1181 +            using frontier_of_connected_component_subset by fastforce
  4.1182 +          have "\<not> bounded (-S)"
  4.1183 +            by (simp add: True cobounded_imp_unbounded)
  4.1184 +          then have "connected_component_set (- S) z \<noteq> {}"
  4.1185 +            apply (simp only: connected_component_eq_empty)
  4.1186 +            using confr openS \<open>bounded C\<close> \<open>w \<notin> S\<close>
  4.1187 +            apply (simp add: frontier_def interior_open C_ccsw)
  4.1188 +            by (metis ComplI Compl_eq_Diff_UNIV connected_UNIV closed_closure closure_subset connected_component_eq_self
  4.1189 +                      connected_diff_open_from_closed subset_UNIV)
  4.1190 +          then show "frontier (connected_component_set (- S) z) \<noteq> {}"
  4.1191 +            apply (simp add: frontier_eq_empty connected_component_eq_UNIV)
  4.1192 +            apply (metis False compl_top_eq double_compl)
  4.1193 +            done
  4.1194 +        qed
  4.1195 +        then show "connected_component_set (- S) z \<inter> frontier S \<noteq> {}"
  4.1196 +          by auto
  4.1197 +      qed
  4.1198 +      then show False
  4.1199 +        by (metis C_ccsw Compl_iff \<open>w \<notin> S\<close> \<open>z \<notin> C\<close> connected_component_eq_empty connected_component_idemp)
  4.1200 +    qed
  4.1201 +  qed
  4.1202 +next
  4.1203 +  case False
  4.1204 +  obtain w where C_ccsw: "C = connected_component_set (- S) w" and "w \<notin> S"
  4.1205 +    using C by (auto simp: components_def)
  4.1206 +  have "frontier (connected_component_set (- S) w) \<subseteq> connected_component_set (- S) w"
  4.1207 +    by (simp add: closed_Compl closed_connected_component frontier_subset_eq openS)
  4.1208 +  moreover have "frontier (connected_component_set (- S) w) \<subseteq> frontier S"
  4.1209 +    using frontier_complement frontier_of_connected_component_subset by blast
  4.1210 +  moreover have "frontier (connected_component_set (- S) w) \<noteq> {}"
  4.1211 +    by (metis C C_ccsw False bounded_empty compl_top_eq connected_component_eq_UNIV double_compl frontier_not_empty in_components_nonempty)
  4.1212 +  ultimately obtain z where zin: "z \<in> frontier S" and z: "z \<in> connected_component_set (- S) w"
  4.1213 +    by blast
  4.1214 +  have *: "connected_component_set (frontier S) z \<in> components(frontier S)"
  4.1215 +    by (simp add: \<open>z \<in> frontier S\<close> componentsI)
  4.1216 +  with prev False have "\<not> bounded (connected_component_set (frontier S) z)"
  4.1217 +    by simp
  4.1218 +  moreover have "connected_component (- S) w = connected_component (- S) z"
  4.1219 +    using connected_component_eq [OF z] by force
  4.1220 +  ultimately show ?thesis
  4.1221 +    by (metis C_ccsw * zin bounded_subset closed_Compl closure_closed connected_component_maximal
  4.1222 +              connected_component_refl connected_connected_component frontier_closures in_components_subset le_inf_iff mem_Collect_eq openS)
  4.1223 +qed
  4.1224 +
  4.1225 +lemma empty_inside:
  4.1226 +  assumes "connected S" "\<And>C. C \<in> components (- S) \<Longrightarrow> ~bounded C"
  4.1227 +  shows "inside S = {}"
  4.1228 +  using assms by (auto simp: components_def inside_def)
  4.1229 +
  4.1230 +lemma empty_inside_imp_simply_connected:
  4.1231 +  "\<lbrakk>connected S; inside S = {}\<rbrakk> \<Longrightarrow> simply_connected S"
  4.1232 +  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)
  4.1233 +
  4.1234 +end
  4.1235 +
  4.1236 +proposition
  4.1237 +  fixes S :: "complex set"
  4.1238 +  assumes "open S"
  4.1239 +  shows simply_connected_eq_frontier_properties:
  4.1240 +         "simply_connected S \<longleftrightarrow>
  4.1241 +          connected S \<and>
  4.1242 +             (if bounded S then connected(frontier S)
  4.1243 +             else (\<forall>C \<in> components(frontier S). \<not>bounded C))" (is "?fp")
  4.1244 +    and simply_connected_eq_unbounded_complement_components:
  4.1245 +         "simply_connected S \<longleftrightarrow>
  4.1246 +          connected S \<and> (\<forall>C \<in> components(- S). \<not>bounded C)" (is "?ucc")
  4.1247 +    and simply_connected_eq_empty_inside:
  4.1248 +         "simply_connected S \<longleftrightarrow>
  4.1249 +          connected S \<and> inside S = {}" (is "?ei")
  4.1250 +proof -
  4.1251 +  interpret SC_Chain
  4.1252 +    using assms by (simp add: SC_Chain_def)
  4.1253 +  have "?fp \<and> ?ucc \<and> ?ei"
  4.1254 +proof -
  4.1255 +  have *: "\<lbrakk>\<alpha> \<Longrightarrow> \<beta>; \<beta> \<Longrightarrow> \<gamma>; \<gamma> \<Longrightarrow> \<delta>; \<delta> \<Longrightarrow> \<alpha>\<rbrakk>
  4.1256 +           \<Longrightarrow> (\<alpha> \<longleftrightarrow> \<beta>) \<and> (\<alpha> \<longleftrightarrow> \<gamma>) \<and> (\<alpha> \<longleftrightarrow> \<delta>)" for \<alpha> \<beta> \<gamma> \<delta>
  4.1257 +    by blast
  4.1258 +  show ?thesis
  4.1259 +    apply (rule *)
  4.1260 +    using frontier_properties simply_connected_imp_connected apply blast
  4.1261 +apply clarify
  4.1262 +    using unbounded_complement_components simply_connected_imp_connected apply blast
  4.1263 +    using empty_inside apply blast
  4.1264 +    using empty_inside_imp_simply_connected apply blast
  4.1265 +    done
  4.1266 +qed
  4.1267 +  then show ?fp ?ucc ?ei
  4.1268 +    by safe
  4.1269 +qed
  4.1270 +
  4.1271 +
  4.1272 +lemma simply_connected_iff_simple:
  4.1273 +  fixes S :: "complex set"
  4.1274 +  assumes "open S" "bounded S"
  4.1275 +  shows "simply_connected S \<longleftrightarrow> connected S \<and> connected(- S)"
  4.1276 +  apply (simp add: simply_connected_eq_unbounded_complement_components assms, safe)
  4.1277 +   apply (metis DIM_complex assms(2) cobounded_has_bounded_component double_compl order_refl)
  4.1278 +  by (meson assms inside_bounded_complement_connected_empty simply_connected_eq_empty_inside simply_connected_eq_unbounded_complement_components)
  4.1279 +
  4.1280 +subsection\<open>Further equivalences based on continuous logs and sqrts\<close>
  4.1281 +
  4.1282 +context SC_Chain
  4.1283 +begin
  4.1284 +
  4.1285 +lemma continuous_log:
  4.1286 +  fixes f :: "complex\<Rightarrow>complex"
  4.1287 +  assumes S: "simply_connected S"
  4.1288 +    and contf: "continuous_on S f" and nz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
  4.1289 +  shows "\<exists>g. continuous_on S g \<and> (\<forall>z \<in> S. f z = exp(g z))"
  4.1290 +proof -
  4.1291 +  consider "S = {}" | "S homeomorphic ball (0::complex) 1"
  4.1292 +    using simply_connected_eq_homeomorphic_to_disc [OF openS] S by metis
  4.1293 +  then show ?thesis
  4.1294 +  proof cases
  4.1295 +    case 1 then show ?thesis
  4.1296 +      by simp
  4.1297 +  next
  4.1298 +    case 2
  4.1299 +    then obtain h k :: "complex\<Rightarrow>complex"
  4.1300 +      where kh: "\<And>x. x \<in> S \<Longrightarrow> k(h x) = x" and him: "h ` S = ball 0 1"
  4.1301 +      and conth: "continuous_on S h"
  4.1302 +      and hk: "\<And>y. y \<in> ball 0 1 \<Longrightarrow> h(k y) = y" and kim: "k ` ball 0 1 = S"
  4.1303 +      and contk: "continuous_on (ball 0 1) k"
  4.1304 +      unfolding homeomorphism_def homeomorphic_def by metis
  4.1305 +    obtain g where contg: "continuous_on (ball 0 1) g"
  4.1306 +             and expg: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> (f \<circ> k) z = exp (g z)"
  4.1307 +    proof (rule continuous_logarithm_on_ball)
  4.1308 +      show "continuous_on (ball 0 1) (f \<circ> k)"
  4.1309 +        apply (rule continuous_on_compose [OF contk])
  4.1310 +        using kim continuous_on_subset [OF contf]
  4.1311 +        by blast
  4.1312 +      show "\<And>z. z \<in> ball 0 1 \<Longrightarrow> (f \<circ> k) z \<noteq> 0"
  4.1313 +        using kim nz by auto
  4.1314 +    qed auto
  4.1315 +    then show ?thesis
  4.1316 +      by (metis comp_apply conth continuous_on_compose him imageI kh)
  4.1317 +  qed
  4.1318 +qed
  4.1319 +
  4.1320 +lemma continuous_sqrt:
  4.1321 +  fixes f :: "complex\<Rightarrow>complex"
  4.1322 +  assumes contf: "continuous_on S f" and nz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
  4.1323 +  and prev: "\<And>f::complex\<Rightarrow>complex.
  4.1324 +                \<lbrakk>continuous_on S f; \<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0\<rbrakk>
  4.1325 +                  \<Longrightarrow> \<exists>g. continuous_on S g \<and> (\<forall>z \<in> S. f z = exp(g z))"
  4.1326 +  shows "\<exists>g. continuous_on S g \<and> (\<forall>z \<in> S. f z = (g z)\<^sup>2)"
  4.1327 +proof -
  4.1328 +  obtain g where contg: "continuous_on S g" and geq: "\<And>z. z \<in> S \<Longrightarrow> f z = exp(g z)"
  4.1329 +    using contf nz prev by metis
  4.1330 +  show ?thesis
  4.1331 +proof (intro exI ballI conjI)
  4.1332 +  show "continuous_on S (\<lambda>z. exp(g z/2))"
  4.1333 +      by (intro continuous_intros) (auto simp: contg)
  4.1334 +    show "\<And>z. z \<in> S \<Longrightarrow> f z = (exp (g z/2))\<^sup>2"
  4.1335 +      by (metis (no_types, lifting) divide_inverse exp_double geq mult.left_commute mult.right_neutral right_inverse zero_neq_numeral)
  4.1336 +  qed
  4.1337 +qed
  4.1338 +
  4.1339 +
  4.1340 +lemma continuous_sqrt_imp_simply_connected:
  4.1341 +  assumes "connected S"
  4.1342 +    and prev: "\<And>f::complex\<Rightarrow>complex. \<lbrakk>continuous_on S f; \<forall>z \<in> S. f z \<noteq> 0\<rbrakk>
  4.1343 +                \<Longrightarrow> \<exists>g. continuous_on S g \<and> (\<forall>z \<in> S. f z = (g z)\<^sup>2)"
  4.1344 +  shows "simply_connected S"
  4.1345 +proof (clarsimp simp add: simply_connected_eq_holomorphic_sqrt [OF openS] \<open>connected S\<close>)
  4.1346 +  fix f
  4.1347 +  assume "f holomorphic_on S" and nz: "\<forall>z\<in>S. f z \<noteq> 0"
  4.1348 +  then obtain g where contg: "continuous_on S g" and geq: "\<And>z. z \<in> S \<Longrightarrow> f z = (g z)\<^sup>2"
  4.1349 +    by (metis holomorphic_on_imp_continuous_on prev)
  4.1350 +  show "\<exists>g. g holomorphic_on S \<and> (\<forall>z\<in>S. f z = (g z)\<^sup>2)"
  4.1351 +  proof (intro exI ballI conjI)
  4.1352 +    show "g holomorphic_on S"
  4.1353 +    proof (clarsimp simp add: holomorphic_on_open [OF openS])
  4.1354 +      fix z
  4.1355 +      assume "z \<in> S"
  4.1356 +      with nz geq have "g z \<noteq> 0"
  4.1357 +        by auto
  4.1358 +      obtain \<delta> where "0 < \<delta>" "\<And>w. \<lbrakk>w \<in> S; dist w z < \<delta>\<rbrakk> \<Longrightarrow> dist (g w) (g z) < cmod (g z)"
  4.1359 +        using contg [unfolded continuous_on_iff] by (metis \<open>g z \<noteq> 0\<close> \<open>z \<in> S\<close> zero_less_norm_iff)
  4.1360 +      then have \<delta>: "\<And>w. \<lbrakk>w \<in> S; w \<in> ball z \<delta>\<rbrakk> \<Longrightarrow> g w + g z \<noteq> 0"
  4.1361 +        apply (clarsimp simp: dist_norm)
  4.1362 +        by (metis \<open>g z \<noteq> 0\<close> add_diff_cancel_left' diff_0_right norm_eq_zero norm_increases_online norm_minus_commute norm_not_less_zero not_less_iff_gr_or_eq)
  4.1363 +      have *: "(\<lambda>x. (f x - f z) / (x - z) / (g x + g z)) \<midarrow>z\<rightarrow> deriv f z / (g z + g z)"
  4.1364 +        apply (intro tendsto_intros)
  4.1365 +        using SC_Chain.openS SC_Chain_axioms \<open>f holomorphic_on S\<close> \<open>z \<in> S\<close> has_field_derivativeD holomorphic_derivI apply fastforce
  4.1366 +        using \<open>z \<in> S\<close> contg continuous_on_eq_continuous_at isCont_def openS apply blast
  4.1367 +        by (simp add: \<open>g z \<noteq> 0\<close>)
  4.1368 +      then have "(g has_field_derivative deriv f z / (g z + g z)) (at z)"
  4.1369 +        unfolding DERIV_iff2
  4.1370 +      proof (rule Lim_transform_within_open)
  4.1371 +        show "open (ball z \<delta> \<inter> S)"
  4.1372 +          by (simp add: openS open_Int)
  4.1373 +        show "z \<in> ball z \<delta> \<inter> S"
  4.1374 +          using \<open>z \<in> S\<close> \<open>0 < \<delta>\<close> by simp
  4.1375 +        show "\<And>x. \<lbrakk>x \<in> ball z \<delta> \<inter> S; x \<noteq> z\<rbrakk>
  4.1376 +                  \<Longrightarrow> (f x - f z) / (x - z) / (g x + g z) = (g x - g z) / (x - z)"
  4.1377 +          using \<delta>
  4.1378 +          apply (simp add: geq \<open>z \<in> S\<close> divide_simps)
  4.1379 +          apply (auto simp: algebra_simps power2_eq_square)
  4.1380 +          done
  4.1381 +      qed
  4.1382 +      then show "\<exists>f'. (g has_field_derivative f') (at z)" ..
  4.1383 +    qed
  4.1384 +  qed (use geq in auto)
  4.1385 +qed
  4.1386 +
  4.1387 +end
  4.1388 +
  4.1389 +proposition
  4.1390 +  fixes S :: "complex set"
  4.1391 +  assumes "open S"
  4.1392 +  shows simply_connected_eq_continuous_log:
  4.1393 +         "simply_connected S \<longleftrightarrow>
  4.1394 +          connected S \<and>
  4.1395 +          (\<forall>f::complex\<Rightarrow>complex. continuous_on S f \<and> (\<forall>z \<in> S. f z \<noteq> 0)
  4.1396 +            \<longrightarrow> (\<exists>g. continuous_on S g \<and> (\<forall>z \<in> S. f z = exp (g z))))" (is "?log")
  4.1397 +    and simply_connected_eq_continuous_sqrt:
  4.1398 +         "simply_connected S \<longleftrightarrow>
  4.1399 +          connected S \<and>
  4.1400 +          (\<forall>f::complex\<Rightarrow>complex. continuous_on S f \<and> (\<forall>z \<in> S. f z \<noteq> 0)
  4.1401 +            \<longrightarrow> (\<exists>g. continuous_on S g \<and> (\<forall>z \<in> S. f z = (g z)\<^sup>2)))" (is "?sqrt")
  4.1402 +proof -
  4.1403 +  interpret SC_Chain
  4.1404 +    using assms by (simp add: SC_Chain_def)
  4.1405 +  have "?log \<and> ?sqrt"
  4.1406 +proof -
  4.1407 +  have *: "\<lbrakk>\<alpha> \<Longrightarrow> \<beta>; \<beta> \<Longrightarrow> \<gamma>; \<gamma> \<Longrightarrow> \<alpha>\<rbrakk>
  4.1408 +           \<Longrightarrow> (\<alpha> \<longleftrightarrow> \<beta>) \<and> (\<alpha> \<longleftrightarrow> \<gamma>)" for \<alpha> \<beta> \<gamma>
  4.1409 +    by blast
  4.1410 +  show ?thesis
  4.1411 +    apply (rule *)
  4.1412 +    apply (simp add: local.continuous_log winding_number_zero)
  4.1413 +    apply (simp add: continuous_sqrt)
  4.1414 +    apply (simp add: continuous_sqrt_imp_simply_connected)
  4.1415 +    done
  4.1416 +qed
  4.1417 +  then show ?log ?sqrt
  4.1418 +    by safe
  4.1419 +qed
  4.1420 +
  4.1421 +
  4.1422 +text\<open>Finally, pick out the Riemann Mapping Theorem from the earlier chain\<close>
  4.1423 +theorem Riemann_mapping_theorem:
  4.1424 +    "open S \<and> simply_connected S \<longleftrightarrow>
  4.1425 +     S = {} \<or> S = UNIV \<or>
  4.1426 +     (\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
  4.1427 +           (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
  4.1428 +           (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z))"
  4.1429 +    (is "_ = ?rhs")
  4.1430 +proof -
  4.1431 +  have "simply_connected S \<longleftrightarrow> ?rhs" if "open S"
  4.1432 +    by (simp add: simply_connected_eq_biholomorphic_to_disc that)
  4.1433 +  moreover have "open S" if "?rhs"
  4.1434 +  proof -
  4.1435 +    { fix f g
  4.1436 +      assume g: "g holomorphic_on ball 0 1" "\<forall>z\<in>ball 0 1. g z \<in> S \<and> f (g z) = z"
  4.1437 +        and "\<forall>z\<in>S. cmod (f z) < 1 \<and> g (f z) = z"
  4.1438 +      then have "S = g ` (ball 0 1)"
  4.1439 +        by (force simp:)
  4.1440 +      then have "open S"
  4.1441 +        by (metis Topology_Euclidean_Space.open_ball g inj_on_def open_mapping_thm3)
  4.1442 +    }
  4.1443 +    with that show "open S" by auto
  4.1444 +  qed
  4.1445 +  ultimately show ?thesis by metis
  4.1446 +qed
  4.1447 +
  4.1448 +end
     5.1 --- a/src/HOL/Analysis/Winding_Numbers.thy	Mon Oct 09 22:08:05 2017 +0200
     5.2 +++ b/src/HOL/Analysis/Winding_Numbers.thy	Tue Oct 10 14:03:51 2017 +0100
     5.3 @@ -3,9 +3,21 @@
     5.4  text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2017)\<close>
     5.5  
     5.6  theory Winding_Numbers
     5.7 -imports Polytope Jordan_Curve Cauchy_Integral_Theorem
     5.8 +imports Polytope Jordan_Curve Riemann_Mapping
     5.9  begin
    5.10  
    5.11 +lemma simply_connected_inside_simple_path:
    5.12 +  fixes p :: "real \<Rightarrow> complex"
    5.13 +  shows "simple_path p \<Longrightarrow> simply_connected(inside(path_image p))"
    5.14 +  using Jordan_inside_outside connected_simple_path_image inside_simple_curve_imp_closed simply_connected_eq_frontier_properties
    5.15 +  by fastforce
    5.16 +
    5.17 +lemma simply_connected_Int:
    5.18 +  fixes S :: "complex set"
    5.19 +  assumes "open S" "open T" "simply_connected S" "simply_connected T" "connected (S \<inter> T)"
    5.20 +  shows "simply_connected (S \<inter> T)"
    5.21 +  using assms by (force simp: simply_connected_eq_winding_number_zero open_Int)
    5.22 +
    5.23  subsection\<open>Winding number for a triangle\<close>
    5.24  
    5.25  lemma wn_triangle1:
    5.26 @@ -926,5 +938,338 @@
    5.27    using assms by (intro winding_number_zero_outside[OF _ _ _ assms(3)] 
    5.28                       path_image_rectpath_subset_cbox) simp_all
    5.29  
    5.30 +
    5.31 +text\<open>A per-function version for continuous logs, a kind of monodromy\<close>
    5.32 +
    5.33 +proposition winding_number_compose_exp:
    5.34 +  assumes "path p"
    5.35 +  shows "winding_number (exp \<circ> p) 0 = (pathfinish p - pathstart p) / (2 * of_real pi * \<i>)"
    5.36 +proof -
    5.37 +  obtain e where "0 < e" and e: "\<And>t. t \<in> {0..1} \<Longrightarrow> e \<le> norm(exp(p t))"
    5.38 +  proof
    5.39 +     have "closed (path_image (exp \<circ> p))"
    5.40 +       by (simp add: assms closed_path_image holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image)
    5.41 +    then show "0 < setdist {0} (path_image (exp \<circ> p))"
    5.42 +      by (metis (mono_tags, lifting) compact_sing exp_not_eq_zero imageE path_image_compose
    5.43 +               path_image_nonempty setdist_eq_0_compact_closed setdist_gt_0_compact_closed setdist_eq_0_closed)
    5.44 +  next
    5.45 +    fix t::real
    5.46 +    assume "t \<in> {0..1}"
    5.47 +    have "setdist {0} (path_image (exp \<circ> p)) \<le> dist 0 (exp (p t))"
    5.48 +      apply (rule setdist_le_dist)
    5.49 +      using \<open>t \<in> {0..1}\<close> path_image_def by fastforce+
    5.50 +    then show "setdist {0} (path_image (exp \<circ> p)) \<le> cmod (exp (p t))"
    5.51 +      by simp
    5.52 +  qed
    5.53 +  have "bounded (path_image p)"
    5.54 +    by (simp add: assms bounded_path_image)
    5.55 +  then obtain B where "0 < B" and B: "path_image p \<subseteq> cball 0 B"
    5.56 +    by (meson bounded_pos mem_cball_0 subsetI)
    5.57 +  let ?B = "cball (0::complex) (B+1)"
    5.58 +  have "uniformly_continuous_on ?B exp"
    5.59 +    using holomorphic_on_exp holomorphic_on_imp_continuous_on
    5.60 +    by (force intro: compact_uniformly_continuous)
    5.61 +  then obtain d where "d > 0"
    5.62 +        and d: "\<And>x x'. \<lbrakk>x\<in>?B; x'\<in>?B; dist x' x < d\<rbrakk> \<Longrightarrow> norm (exp x' - exp x) < e"
    5.63 +    using \<open>e > 0\<close> by (auto simp: uniformly_continuous_on_def dist_norm)
    5.64 +  then have "min 1 d > 0"
    5.65 +    by force
    5.66 +  then obtain g where pfg: "polynomial_function g"  and "g 0 = p 0" "g 1 = p 1"
    5.67 +           and gless: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm(g t - p t) < min 1 d"
    5.68 +    using path_approx_polynomial_function [OF \<open>path p\<close>] \<open>d > 0\<close> \<open>0 < e\<close>
    5.69 +    unfolding pathfinish_def pathstart_def by meson
    5.70 +  have "winding_number (exp \<circ> p) 0 = winding_number (exp \<circ> g) 0"
    5.71 +  proof (rule winding_number_nearby_paths_eq [symmetric])
    5.72 +    show "path (exp \<circ> p)" "path (exp \<circ> g)"
    5.73 +      by (simp_all add: pfg assms holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image path_polynomial_function)
    5.74 +  next
    5.75 +    fix t :: "real"
    5.76 +    assume t: "t \<in> {0..1}"
    5.77 +    with gless have "norm(g t - p t) < 1"
    5.78 +      using min_less_iff_conj by blast
    5.79 +    moreover have ptB: "norm (p t) \<le> B"
    5.80 +      using B t by (force simp: path_image_def)
    5.81 +    ultimately have "cmod (g t) \<le> B + 1"
    5.82 +      by (meson add_mono_thms_linordered_field(4) le_less_trans less_imp_le norm_triangle_sub)
    5.83 +    with ptB gless t have "cmod ((exp \<circ> g) t - (exp \<circ> p) t) < e"
    5.84 +      by (auto simp: dist_norm d)
    5.85 +    with e t show "cmod ((exp \<circ> g) t - (exp \<circ> p) t) < cmod ((exp \<circ> p) t - 0)"
    5.86 +      by fastforce
    5.87 +  qed (use \<open>g 0 = p 0\<close> \<open>g 1 = p 1\<close> in \<open>auto simp: pathfinish_def pathstart_def\<close>)
    5.88 +  also have "... = 1 / (of_real (2 * pi) * \<i>) * contour_integral (exp \<circ> g) (\<lambda>w. 1 / (w - 0))"
    5.89 +  proof (rule winding_number_valid_path)
    5.90 +    have "continuous_on (path_image g) (deriv exp)"
    5.91 +      by (metis DERIV_exp DERIV_imp_deriv continuous_on_cong holomorphic_on_exp holomorphic_on_imp_continuous_on)
    5.92 +    then show "valid_path (exp \<circ> g)"
    5.93 +      by (simp add: field_differentiable_within_exp pfg valid_path_compose valid_path_polynomial_function)
    5.94 +    show "0 \<notin> path_image (exp \<circ> g)"
    5.95 +      by (auto simp: path_image_def)
    5.96 +  qed
    5.97 +  also have "... = 1 / (of_real (2 * pi) * \<i>) * integral {0..1} (\<lambda>x. vector_derivative g (at x))"
    5.98 +  proof (simp add: contour_integral_integral, rule integral_cong)
    5.99 +    fix t :: "real"
   5.100 +    assume t: "t \<in> {0..1}"
   5.101 +    show "vector_derivative (exp \<circ> g) (at t) / exp (g t) = vector_derivative g (at t)"
   5.102 +    proof (simp add: divide_simps, rule vector_derivative_unique_at)
   5.103 +      show "(exp \<circ> g has_vector_derivative vector_derivative (exp \<circ> g) (at t)) (at t)"
   5.104 +        by (meson DERIV_exp differentiable_def field_vector_diff_chain_at has_vector_derivative_def
   5.105 +            has_vector_derivative_polynomial_function pfg vector_derivative_works)
   5.106 +      show "(exp \<circ> g has_vector_derivative vector_derivative g (at t) * exp (g t)) (at t)"
   5.107 +        apply (rule field_vector_diff_chain_at)
   5.108 +        apply (metis has_vector_derivative_polynomial_function pfg vector_derivative_at)
   5.109 +        using DERIV_exp has_field_derivative_def apply blast
   5.110 +        done
   5.111 +    qed
   5.112 +  qed
   5.113 +  also have "... = (pathfinish p - pathstart p) / (2 * of_real pi * \<i>)"
   5.114 +  proof -
   5.115 +    have "((\<lambda>x. vector_derivative g (at x)) has_integral g 1 - g 0) {0..1}"
   5.116 +      apply (rule fundamental_theorem_of_calculus [OF zero_le_one])
   5.117 +      by (metis has_vector_derivative_at_within has_vector_derivative_polynomial_function pfg vector_derivative_at)
   5.118 +    then show ?thesis
   5.119 +    apply (simp add: pathfinish_def pathstart_def)
   5.120 +      using \<open>g 0 = p 0\<close> \<open>g 1 = p 1\<close> by auto
   5.121 +  qed
   5.122 +  finally show ?thesis .
   5.123 +qed
   5.124 +
   5.125 +
   5.126 +
   5.127 +subsection\<open>The winding number defines a continuous logarithm for the path itself\<close>
   5.128 +
   5.129 +lemma winding_number_as_continuous_log:
   5.130 +  assumes "path p" and \<zeta>: "\<zeta> \<notin> path_image p"
   5.131 +  obtains q where "path q"
   5.132 +                  "pathfinish q - pathstart q = 2 * of_real pi * \<i> * winding_number p \<zeta>"
   5.133 +                  "\<And>t. t \<in> {0..1} \<Longrightarrow> p t = \<zeta> + exp(q t)"
   5.134 +proof -
   5.135 +  let ?q = "\<lambda>t. 2 * of_real pi * \<i> * winding_number(subpath 0 t p) \<zeta> + Ln(pathstart p - \<zeta>)"
   5.136 +  show ?thesis
   5.137 +  proof
   5.138 +    have *: "continuous (at t within {0..1}) (\<lambda>x. winding_number (subpath 0 x p) \<zeta>)"
   5.139 +      if t: "t \<in> {0..1}" for t
   5.140 +    proof -
   5.141 +      let ?B = "ball (p t) (norm(p t - \<zeta>))"
   5.142 +      have "p t \<noteq> \<zeta>"
   5.143 +        using path_image_def that \<zeta> by blast
   5.144 +      then have "simply_connected ?B"
   5.145 +        by (simp add: convex_imp_simply_connected)
   5.146 +      then have "\<And>f::complex\<Rightarrow>complex. continuous_on ?B f \<and> (\<forall>\<zeta> \<in> ?B. f \<zeta> \<noteq> 0)
   5.147 +                  \<longrightarrow> (\<exists>g. continuous_on ?B g \<and> (\<forall>\<zeta> \<in> ?B. f \<zeta> = exp (g \<zeta>)))"
   5.148 +        by (simp add: simply_connected_eq_continuous_log)
   5.149 +      moreover have "continuous_on ?B (\<lambda>w. w - \<zeta>)"
   5.150 +        by (intro continuous_intros)
   5.151 +      moreover have "(\<forall>z \<in> ?B. z - \<zeta> \<noteq> 0)"
   5.152 +        by (auto simp: dist_norm)
   5.153 +      ultimately obtain g where contg: "continuous_on ?B g"
   5.154 +        and geq: "\<And>z. z \<in> ?B \<Longrightarrow> z - \<zeta> = exp (g z)" by blast
   5.155 +      obtain d where "0 < d" and d:
   5.156 +        "\<And>x. \<lbrakk>x \<in> {0..1}; dist x t < d\<rbrakk> \<Longrightarrow> dist (p x) (p t) < cmod (p t - \<zeta>)"
   5.157 +        using \<open>path p\<close> t unfolding path_def continuous_on_iff
   5.158 +        by (metis \<open>p t \<noteq> \<zeta>\<close> right_minus_eq zero_less_norm_iff)
   5.159 +      have "((\<lambda>x. winding_number (\<lambda>w. subpath 0 x p w - \<zeta>) 0 -
   5.160 +                  winding_number (\<lambda>w. subpath 0 t p w - \<zeta>) 0) \<longlongrightarrow> 0)
   5.161 +            (at t within {0..1})"
   5.162 +      proof (rule Lim_transform_within [OF _ \<open>d > 0\<close>])
   5.163 +        have "continuous (at t within {0..1}) (g o p)"
   5.164 +          apply (rule continuous_within_compose)
   5.165 +          using \<open>path p\<close> continuous_on_eq_continuous_within path_def that apply blast
   5.166 +          by (metis (no_types, lifting) Topology_Euclidean_Space.open_ball UNIV_I \<open>p t \<noteq> \<zeta>\<close> centre_in_ball contg continuous_on_eq_continuous_at continuous_within_topological right_minus_eq zero_less_norm_iff)
   5.167 +        with LIM_zero have "((\<lambda>u. (g (subpath t u p 1) - g (subpath t u p 0))) \<longlongrightarrow> 0) (at t within {0..1})"
   5.168 +          by (auto simp: subpath_def continuous_within o_def)
   5.169 +        then show "((\<lambda>u.  (g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * \<i>)) \<longlongrightarrow> 0)
   5.170 +           (at t within {0..1})"
   5.171 +          by (simp add: tendsto_divide_zero)
   5.172 +        show "(g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * \<i>) =
   5.173 +              winding_number (\<lambda>w. subpath 0 u p w - \<zeta>) 0 - winding_number (\<lambda>w. subpath 0 t p w - \<zeta>) 0"
   5.174 +          if "u \<in> {0..1}" "0 < dist u t" "dist u t < d" for u
   5.175 +        proof -
   5.176 +          have "closed_segment t u \<subseteq> {0..1}"
   5.177 +            using closed_segment_eq_real_ivl t that by auto
   5.178 +          then have piB: "path_image(subpath t u p) \<subseteq> ?B"
   5.179 +            apply (clarsimp simp add: path_image_subpath_gen)
   5.180 +            by (metis subsetD le_less_trans \<open>dist u t < d\<close> d dist_commute dist_in_closed_segment)
   5.181 +          have *: "path (g \<circ> subpath t u p)"
   5.182 +            apply (rule path_continuous_image)
   5.183 +            using \<open>path p\<close> t that apply auto[1]
   5.184 +            using piB contg continuous_on_subset by blast
   5.185 +          have "(g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * \<i>)
   5.186 +              =  winding_number (exp \<circ> g \<circ> subpath t u p) 0"
   5.187 +            using winding_number_compose_exp [OF *]
   5.188 +            by (simp add: pathfinish_def pathstart_def o_assoc)
   5.189 +          also have "... = winding_number (\<lambda>w. subpath t u p w - \<zeta>) 0"
   5.190 +          proof (rule winding_number_cong)
   5.191 +            have "exp(g y) = y - \<zeta>" if "y \<in> (subpath t u p) ` {0..1}" for y
   5.192 +              by (metis that geq path_image_def piB subset_eq)
   5.193 +            then show "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> (exp \<circ> g \<circ> subpath t u p) x = subpath t u p x - \<zeta>"
   5.194 +              by auto
   5.195 +          qed
   5.196 +          also have "... = winding_number (\<lambda>w. subpath 0 u p w - \<zeta>) 0 -
   5.197 +                           winding_number (\<lambda>w. subpath 0 t p w - \<zeta>) 0"
   5.198 +            apply (simp add: winding_number_offset [symmetric])
   5.199 +            using winding_number_subpath_combine [OF \<open>path p\<close> \<zeta>, of 0 t u] \<open>t \<in> {0..1}\<close> \<open>u \<in> {0..1}\<close>
   5.200 +            by (simp add: add.commute eq_diff_eq)
   5.201 +          finally show ?thesis .
   5.202 +        qed
   5.203 +      qed
   5.204 +      then show ?thesis
   5.205 +        by (subst winding_number_offset) (simp add: continuous_within LIM_zero_iff)
   5.206 +    qed
   5.207 +    show "path ?q"
   5.208 +      unfolding path_def
   5.209 +      by (intro continuous_intros) (simp add: continuous_on_eq_continuous_within *)
   5.210 +
   5.211 +    have "\<zeta> \<noteq> p 0"
   5.212 +      by (metis \<zeta> pathstart_def pathstart_in_path_image)
   5.213 +    then show "pathfinish ?q - pathstart ?q = 2 * of_real pi * \<i> * winding_number p \<zeta>"
   5.214 +      by (simp add: pathfinish_def pathstart_def)
   5.215 +    show "p t = \<zeta> + exp (?q t)" if "t \<in> {0..1}" for t
   5.216 +    proof -
   5.217 +      have "path (subpath 0 t p)"
   5.218 +        using \<open>path p\<close> that by auto
   5.219 +      moreover
   5.220 +      have "\<zeta> \<notin> path_image (subpath 0 t p)"
   5.221 +        using \<zeta> [unfolded path_image_def] that by (auto simp: path_image_subpath)
   5.222 +      ultimately show ?thesis
   5.223 +        using winding_number_exp_2pi [of "subpath 0 t p" \<zeta>] \<open>\<zeta> \<noteq> p 0\<close>
   5.224 +        by (auto simp: exp_add algebra_simps pathfinish_def pathstart_def subpath_def)
   5.225 +    qed
   5.226 +  qed
   5.227 +qed
   5.228 +
   5.229 +
   5.230 +subsection\<open>Winding number equality is the same as path/loop homotopy in C - {0}\<close>
   5.231 +
   5.232 +lemma winding_number_homotopic_loops_null_eq:
   5.233 +  assumes "path p" and \<zeta>: "\<zeta> \<notin> path_image p"
   5.234 +  shows "winding_number p \<zeta> = 0 \<longleftrightarrow> (\<exists>a. homotopic_loops (-{\<zeta>}) p (\<lambda>t. a))"
   5.235 +    (is "?lhs = ?rhs")
   5.236 +proof
   5.237 +  assume [simp]: ?lhs
   5.238 +  obtain q where "path q"
   5.239 +             and qeq:  "pathfinish q - pathstart q = 2 * of_real pi * \<i> * winding_number p \<zeta>"
   5.240 +             and peq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p t = \<zeta> + exp(q t)"
   5.241 +    using winding_number_as_continuous_log [OF assms] by blast
   5.242 +  have *: "homotopic_with (\<lambda>r. pathfinish r = pathstart r)
   5.243 +                       {0..1} (-{\<zeta>}) ((\<lambda>w. \<zeta> + exp w) \<circ> q) ((\<lambda>w. \<zeta> + exp w) \<circ> (\<lambda>t. 0))"
   5.244 +  proof (rule homotopic_with_compose_continuous_left)
   5.245 +    show "homotopic_with (\<lambda>f. pathfinish ((\<lambda>w. \<zeta> + exp w) \<circ> f) = pathstart ((\<lambda>w. \<zeta> + exp w) \<circ> f))
   5.246 +              {0..1} UNIV q (\<lambda>t. 0)"
   5.247 +    proof (rule homotopic_with_mono, simp_all add: pathfinish_def pathstart_def)
   5.248 +      have "homotopic_loops UNIV q (\<lambda>t. 0)"
   5.249 +        by (rule homotopic_loops_linear) (use qeq \<open>path q\<close> in \<open>auto simp: continuous_on_const path_defs\<close>)
   5.250 +      then show "homotopic_with (\<lambda>h. exp (h 1) = exp (h 0)) {0..1} UNIV q (\<lambda>t. 0)"
   5.251 +        by (simp add: homotopic_loops_def homotopic_with_mono pathfinish_def pathstart_def)
   5.252 +    qed
   5.253 +    show "continuous_on UNIV (\<lambda>w. \<zeta> + exp w)"
   5.254 +      by (rule continuous_intros)+
   5.255 +    show "range (\<lambda>w. \<zeta> + exp w) \<subseteq> -{\<zeta>}"
   5.256 +      by auto
   5.257 +  qed
   5.258 +  then have "homotopic_with (\<lambda>r. pathfinish r = pathstart r) {0..1} (-{\<zeta>}) p (\<lambda>x. \<zeta> + 1)"
   5.259 +    by (rule homotopic_with_eq) (auto simp: o_def peq pathfinish_def pathstart_def)
   5.260 +  then have "homotopic_loops (-{\<zeta>}) p (\<lambda>t. \<zeta> + 1)"
   5.261 +    by (simp add: homotopic_loops_def)
   5.262 +  then show ?rhs ..
   5.263 +next
   5.264 +  assume ?rhs
   5.265 +  then obtain a where "homotopic_loops (-{\<zeta>}) p (\<lambda>t. a)" ..
   5.266 +  then have "winding_number p \<zeta> = winding_number (\<lambda>t. a) \<zeta>" "a \<noteq> \<zeta>"
   5.267 +    using winding_number_homotopic_loops homotopic_loops_imp_subset by (force simp:)+
   5.268 +  moreover have "winding_number (\<lambda>t. a) \<zeta> = 0"
   5.269 +    by (metis winding_number_zero_const \<open>a \<noteq> \<zeta>\<close>)
   5.270 +  ultimately show ?lhs by metis
   5.271 +qed
   5.272 +
   5.273 +
   5.274 +lemma winding_number_homotopic_paths_null_explicit_eq:
   5.275 +  assumes "path p" and \<zeta>: "\<zeta> \<notin> path_image p"
   5.276 +  shows "winding_number p \<zeta> = 0 \<longleftrightarrow> homotopic_paths (-{\<zeta>}) p (linepath (pathstart p) (pathstart p))"
   5.277 +        (is "?lhs = ?rhs")
   5.278 +proof
   5.279 +  assume ?lhs
   5.280 +  then show ?rhs
   5.281 +    apply (auto simp: winding_number_homotopic_loops_null_eq [OF assms])
   5.282 +    apply (rule homotopic_loops_imp_homotopic_paths_null)
   5.283 +    apply (simp add: linepath_refl)
   5.284 +    done
   5.285 +next
   5.286 +  assume ?rhs
   5.287 +  then show ?lhs
   5.288 +    by (metis \<zeta> pathstart_in_path_image winding_number_homotopic_paths winding_number_trivial)
   5.289 +qed
   5.290 +
   5.291 +
   5.292 +lemma winding_number_homotopic_paths_null_eq:
   5.293 +  assumes "path p" and \<zeta>: "\<zeta> \<notin> path_image p"
   5.294 +  shows "winding_number p \<zeta> = 0 \<longleftrightarrow> (\<exists>a. homotopic_paths (-{\<zeta>}) p (\<lambda>t. a))"
   5.295 +    (is "?lhs = ?rhs")
   5.296 +proof
   5.297 +  assume ?lhs
   5.298 +  then show ?rhs
   5.299 +    by (auto simp: winding_number_homotopic_paths_null_explicit_eq [OF assms] linepath_refl)
   5.300 +next
   5.301 +  assume ?rhs
   5.302 +  then show ?lhs
   5.303 +    by (metis \<zeta> homotopic_paths_imp_pathfinish pathfinish_def pathfinish_in_path_image winding_number_homotopic_paths winding_number_zero_const)
   5.304 +qed
   5.305 +
   5.306 +
   5.307 +lemma winding_number_homotopic_paths_eq:
   5.308 +  assumes "path p" and \<zeta>p: "\<zeta> \<notin> path_image p"
   5.309 +      and "path q" and \<zeta>q: "\<zeta> \<notin> path_image q"
   5.310 +      and qp: "pathstart q = pathstart p" "pathfinish q = pathfinish p"
   5.311 +    shows "winding_number p \<zeta> = winding_number q \<zeta> \<longleftrightarrow> homotopic_paths (-{\<zeta>}) p q"
   5.312 +    (is "?lhs = ?rhs")
   5.313 +proof
   5.314 +  assume ?lhs
   5.315 +  then have "winding_number (p +++ reversepath q) \<zeta> = 0"
   5.316 +    using assms by (simp add: winding_number_join winding_number_reversepath)
   5.317 +  moreover
   5.318 +  have "path (p +++ reversepath q)" "\<zeta> \<notin> path_image (p +++ reversepath q)"
   5.319 +    using assms by (auto simp: not_in_path_image_join)
   5.320 +  ultimately obtain a where "homotopic_paths (- {\<zeta>}) (p +++ reversepath q) (linepath a a)"
   5.321 +    using winding_number_homotopic_paths_null_explicit_eq by blast
   5.322 +  then show ?rhs
   5.323 +    using homotopic_paths_imp_pathstart assms
   5.324 +    by (fastforce simp add: dest: homotopic_paths_imp_homotopic_loops homotopic_paths_loop_parts)
   5.325 +next
   5.326 +  assume ?rhs
   5.327 +  then show ?lhs
   5.328 +    by (simp add: winding_number_homotopic_paths)
   5.329 +qed
   5.330 +
   5.331 +
   5.332 +lemma winding_number_homotopic_loops_eq:
   5.333 +  assumes "path p" and \<zeta>p: "\<zeta> \<notin> path_image p"
   5.334 +      and "path q" and \<zeta>q: "\<zeta> \<notin> path_image q"
   5.335 +      and loops: "pathfinish p = pathstart p" "pathfinish q = pathstart q"
   5.336 +    shows "winding_number p \<zeta> = winding_number q \<zeta> \<longleftrightarrow> homotopic_loops (-{\<zeta>}) p q"
   5.337 +    (is "?lhs = ?rhs")
   5.338 +proof
   5.339 +  assume L: ?lhs
   5.340 +  have "pathstart p \<noteq> \<zeta>" "pathstart q \<noteq> \<zeta>"
   5.341 +    using \<zeta>p \<zeta>q by blast+
   5.342 +  moreover have "path_connected (-{\<zeta>})"
   5.343 +    by (simp add: path_connected_punctured_universe)
   5.344 +  ultimately obtain r where "path r" and rim: "path_image r \<subseteq> -{\<zeta>}"
   5.345 +                        and pas: "pathstart r = pathstart p" and paf: "pathfinish r = pathstart q"
   5.346 +    by (auto simp: path_connected_def)
   5.347 +  then have "pathstart r \<noteq> \<zeta>" by blast
   5.348 +  have "homotopic_loops (- {\<zeta>}) p (r +++ q +++ reversepath r)"
   5.349 +    apply (rule homotopic_paths_imp_homotopic_loops)
   5.350 +    apply (metis (mono_tags, hide_lams) \<open>path r\<close> L \<zeta>p \<zeta>q \<open>path p\<close> \<open>path q\<close> homotopic_loops_conjugate loops not_in_path_image_join paf pas path_image_reversepath path_imp_reversepath path_join_eq pathfinish_join pathfinish_reversepath  pathstart_join pathstart_reversepath rim subset_Compl_singleton winding_number_homotopic_loops winding_number_homotopic_paths_eq)
   5.351 +    using loops pas apply auto
   5.352 +    done
   5.353 +  moreover have "homotopic_loops (- {\<zeta>}) (r +++ q +++ reversepath r) q"
   5.354 +    using rim \<zeta>q by (auto simp: homotopic_loops_conjugate paf \<open>path q\<close> \<open>path r\<close> loops)
   5.355 +  ultimately show ?rhs
   5.356 +    using homotopic_loops_trans by metis
   5.357 +next
   5.358 +  assume ?rhs
   5.359 +  then show ?lhs
   5.360 +    by (simp add: winding_number_homotopic_loops)
   5.361 +qed
   5.362 +
   5.363  end
   5.364