src/HOL/Analysis/Riemann_Mapping.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (2 months ago) changeset 69981 3dced198b9ec parent 69922 4a9167f377b0 child 70136 f03a01a18c6e permissions -rw-r--r--
more strict AFP properties;
```     1 (*  Title:      HOL/Analysis/Riemann_Mapping.thy
```
```     2     Authors:    LC Paulson, based on material from HOL Light
```
```     3 *)
```
```     4
```
```     5 section \<open>Moebius functions, Equivalents of Simply Connected Sets, Riemann Mapping Theorem\<close>
```
```     6
```
```     7 theory Riemann_Mapping
```
```     8 imports Great_Picard
```
```     9 begin
```
```    10
```
```    11 subsection\<open>Moebius functions are biholomorphisms of the unit disc\<close>
```
```    12
```
```    13 definition%important Moebius_function :: "[real,complex,complex] \<Rightarrow> complex" where
```
```    14   "Moebius_function \<equiv> \<lambda>t w z. exp(\<i> * of_real t) * (z - w) / (1 - cnj w * z)"
```
```    15
```
```    16 lemma Moebius_function_simple:
```
```    17    "Moebius_function 0 w z = (z - w) / (1 - cnj w * z)"
```
```    18   by (simp add: Moebius_function_def)
```
```    19
```
```    20 lemma Moebius_function_eq_zero:
```
```    21    "Moebius_function t w w = 0"
```
```    22   by (simp add: Moebius_function_def)
```
```    23
```
```    24 lemma Moebius_function_of_zero:
```
```    25    "Moebius_function t w 0 = - exp(\<i> * of_real t) * w"
```
```    26   by (simp add: Moebius_function_def)
```
```    27
```
```    28 lemma Moebius_function_norm_lt_1:
```
```    29   assumes w1: "norm w < 1" and z1: "norm z < 1"
```
```    30   shows "norm (Moebius_function t w z) < 1"
```
```    31 proof -
```
```    32   have "1 - cnj w * z \<noteq> 0"
```
```    33     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)
```
```    34   then have VV: "1 - w * cnj z \<noteq> 0"
```
```    35     by (metis complex_cnj_cnj complex_cnj_mult complex_cnj_one right_minus_eq)
```
```    36   then have "1 - norm (Moebius_function t w z) ^ 2 =
```
```    37          ((1 - norm w ^ 2) / (norm (1 - cnj w * z) ^ 2)) * (1 - norm z ^ 2)"
```
```    38     apply (cases w)
```
```    39     apply (cases z)
```
```    40     apply (simp add: Moebius_function_def divide_simps norm_divide norm_mult)
```
```    41     apply (simp add: complex_norm complex_diff complex_mult one_complex.code complex_cnj)
```
```    42     apply (auto simp: algebra_simps power2_eq_square)
```
```    43     done
```
```    44   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))"
```
```    45     by (simp add: norm_mult power2_eq_square)
```
```    46   moreover have "0 < 1 - cmod (z * z)"
```
```    47     by (metis (no_types) z1 diff_gt_0_iff_gt mult.left_neutral norm_mult_less)
```
```    48   ultimately have "0 < 1 - norm (Moebius_function t w z) ^ 2"
```
```    49     using \<open>1 - cnj w * z \<noteq> 0\<close> w1 norm_mult_less by fastforce
```
```    50   then show ?thesis
```
```    51     using linorder_not_less by fastforce
```
```    52 qed
```
```    53
```
```    54 lemma Moebius_function_holomorphic:
```
```    55   assumes "norm w < 1"
```
```    56   shows "Moebius_function t w holomorphic_on ball 0 1"
```
```    57 proof -
```
```    58   have *: "1 - z * w \<noteq> 0" if "norm z < 1" for z
```
```    59   proof -
```
```    60     have "norm (1::complex) \<noteq> norm (z * w)"
```
```    61       using assms that norm_mult_less by fastforce
```
```    62     then show ?thesis by auto
```
```    63   qed
```
```    64   show ?thesis
```
```    65   apply (simp add: Moebius_function_def)
```
```    66   apply (intro holomorphic_intros)
```
```    67   using assms *
```
```    68   by (metis complex_cnj_cnj complex_cnj_mult complex_cnj_one complex_mod_cnj mem_ball_0 mult.commute right_minus_eq)
```
```    69 qed
```
```    70
```
```    71 lemma Moebius_function_compose:
```
```    72   assumes meq: "-w1 = w2" and "norm w1 < 1" "norm z < 1"
```
```    73   shows "Moebius_function 0 w1 (Moebius_function 0 w2 z) = z"
```
```    74 proof -
```
```    75   have "norm w2 < 1"
```
```    76     using assms by auto
```
```    77   then have "-w1 = z" if "cnj w2 * z = 1"
```
```    78     by (metis assms(3) complex_mod_cnj less_irrefl mult.right_neutral norm_mult_less norm_one that)
```
```    79   moreover have "z=0" if "1 - cnj w2 * z = cnj w1 * (z - w2)"
```
```    80   proof -
```
```    81     have "w2 * cnj w2 = 1"
```
```    82       using that meq by (auto simp: algebra_simps)
```
```    83     then show "z = 0"
```
```    84       by (metis (no_types) \<open>cmod w2 < 1\<close> complex_mod_cnj less_irrefl mult.right_neutral norm_mult_less norm_one)
```
```    85   qed
```
```    86   moreover have "z - w2 - w1 * (1 - cnj w2 * z) = z * (1 - cnj w2 * z - cnj w1 * (z - w2))"
```
```    87     using meq by (fastforce simp: algebra_simps)
```
```    88   ultimately
```
```    89   show ?thesis
```
```    90     by (simp add: Moebius_function_def divide_simps norm_divide norm_mult)
```
```    91 qed
```
```    92
```
```    93 lemma ball_biholomorphism_exists:
```
```    94   assumes "a \<in> ball 0 1"
```
```    95   obtains f g where "f a = 0"
```
```    96                 "f holomorphic_on ball 0 1" "f ` ball 0 1 \<subseteq> ball 0 1"
```
```    97                 "g holomorphic_on ball 0 1" "g ` ball 0 1 \<subseteq> ball 0 1"
```
```    98                 "\<And>z. z \<in> ball 0 1 \<Longrightarrow> f (g z) = z"
```
```    99                 "\<And>z. z \<in> ball 0 1 \<Longrightarrow> g (f z) = z"
```
```   100 proof
```
```   101   show "Moebius_function 0 a holomorphic_on ball 0 1"  "Moebius_function 0 (-a) holomorphic_on ball 0 1"
```
```   102     using Moebius_function_holomorphic assms mem_ball_0 by auto
```
```   103   show "Moebius_function 0 a a = 0"
```
```   104     by (simp add: Moebius_function_eq_zero)
```
```   105   show "Moebius_function 0 a ` ball 0 1 \<subseteq> ball 0 1"
```
```   106        "Moebius_function 0 (- a) ` ball 0 1 \<subseteq> ball 0 1"
```
```   107     using Moebius_function_norm_lt_1 assms by auto
```
```   108   show "Moebius_function 0 a (Moebius_function 0 (- a) z) = z"
```
```   109        "Moebius_function 0 (- a) (Moebius_function 0 a z) = z" if "z \<in> ball 0 1" for z
```
```   110     using Moebius_function_compose assms that by auto
```
```   111 qed
```
```   112
```
```   113
```
```   114 subsection\<open>A big chain of equivalents of simple connectedness for an open set\<close>
```
```   115
```
```   116 lemma biholomorphic_to_disc_aux:
```
```   117   assumes "open S" "connected S" "0 \<in> S" and S01: "S \<subseteq> ball 0 1"
```
```   118       and prev: "\<And>f. \<lbrakk>f holomorphic_on S; \<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0; inj_on f S\<rbrakk>
```
```   119                \<Longrightarrow> \<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S. f z = (g z)\<^sup>2)"
```
```   120   shows "\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
```
```   121                (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
```
```   122                (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z)"
```
```   123 proof -
```
```   124   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}"
```
```   125   have idF: "id \<in> F"
```
```   126     using S01 by (auto simp: F_def)
```
```   127   then have "F \<noteq> {}"
```
```   128     by blast
```
```   129   have imF_ne: "((\<lambda>h. norm(deriv h 0)) ` F) \<noteq> {}"
```
```   130     using idF by auto
```
```   131   have holF: "\<And>h. h \<in> F \<Longrightarrow> h holomorphic_on S"
```
```   132     by (auto simp: F_def)
```
```   133   obtain f where "f \<in> F" and normf: "\<And>h. h \<in> F \<Longrightarrow> norm(deriv h 0) \<le> norm(deriv f 0)"
```
```   134   proof -
```
```   135     obtain r where "r > 0" and r: "ball 0 r \<subseteq> S"
```
```   136       using \<open>open S\<close> \<open>0 \<in> S\<close> openE by auto
```
```   137     have bdd: "bdd_above ((\<lambda>h. norm(deriv h 0)) ` F)"
```
```   138     proof (intro bdd_aboveI exI ballI, clarify)
```
```   139       show "norm (deriv f 0) \<le> 1 / r" if "f \<in> F" for f
```
```   140       proof -
```
```   141         have r01: "(*) (complex_of_real r) ` ball 0 1 \<subseteq> S"
```
```   142           using that \<open>r > 0\<close> by (auto simp: norm_mult r [THEN subsetD])
```
```   143         then have "f holomorphic_on (*) (complex_of_real r) ` ball 0 1"
```
```   144           using holomorphic_on_subset [OF holF] by (simp add: that)
```
```   145         then have holf: "f \<circ> (\<lambda>z. (r * z)) holomorphic_on (ball 0 1)"
```
```   146           by (intro holomorphic_intros holomorphic_on_compose)
```
```   147         have f0: "(f \<circ> (*) (complex_of_real r)) 0 = 0"
```
```   148           using F_def that by auto
```
```   149         have "f ` S \<subseteq> ball 0 1"
```
```   150           using F_def that by blast
```
```   151         with r01 have fr1: "\<And>z. norm z < 1 \<Longrightarrow> norm ((f \<circ> (*)(of_real r))z) < 1"
```
```   152           by force
```
```   153         have *: "((\<lambda>w. f (r * w)) has_field_derivative deriv f (r * z) * r) (at z)"
```
```   154           if "z \<in> ball 0 1" for z::complex
```
```   155         proof (rule DERIV_chain' [where g=f])
```
```   156           show "(f has_field_derivative deriv f (of_real r * z)) (at (of_real r * z))"
```
```   157             apply (rule holomorphic_derivI [OF holF \<open>open S\<close>])
```
```   158              apply (rule \<open>f \<in> F\<close>)
```
```   159             by (meson imageI r01 subset_iff that)
```
```   160         qed simp
```
```   161         have df0: "((\<lambda>w. f (r * w)) has_field_derivative deriv f 0 * r) (at 0)"
```
```   162           using * [of 0] by simp
```
```   163         have deq: "deriv (\<lambda>x. f (complex_of_real r * x)) 0 = deriv f 0 * complex_of_real r"
```
```   164           using DERIV_imp_deriv df0 by blast
```
```   165         have "norm (deriv (f \<circ> (*) (complex_of_real r)) 0) \<le> 1"
```
```   166           by (auto intro: Schwarz_Lemma [OF holf f0 fr1, of 0])
```
```   167         with \<open>r > 0\<close> show ?thesis
```
```   168           by (simp add: deq norm_mult divide_simps o_def)
```
```   169       qed
```
```   170     qed
```
```   171     define l where "l \<equiv> SUP h\<in>F. norm (deriv h 0)"
```
```   172     have eql: "norm (deriv f 0) = l" if le: "l \<le> norm (deriv f 0)" and "f \<in> F" for f
```
```   173       apply (rule order_antisym [OF _ le])
```
```   174       using \<open>f \<in> F\<close> bdd cSUP_upper by (fastforce simp: l_def)
```
```   175     obtain \<F> where \<F>in: "\<And>n. \<F> n \<in> F" and \<F>lim: "(\<lambda>n. norm (deriv (\<F> n) 0)) \<longlonglongrightarrow> l"
```
```   176     proof -
```
```   177       have "\<exists>f. f \<in> F \<and> \<bar>norm (deriv f 0) - l\<bar> < 1 / (Suc n)" for n
```
```   178       proof -
```
```   179         obtain f where "f \<in> F" and f: "l < norm (deriv f 0) + 1/(Suc n)"
```
```   180           using cSup_least [OF imF_ne, of "l - 1/(Suc n)"] by (fastforce simp add: l_def)
```
```   181         then have "\<bar>norm (deriv f 0) - l\<bar> < 1 / (Suc n)"
```
```   182           by (fastforce simp add: abs_if not_less eql)
```
```   183         with \<open>f \<in> F\<close> show ?thesis
```
```   184           by blast
```
```   185       qed
```
```   186       then obtain \<F> where fF: "\<And>n. (\<F> n) \<in> F"
```
```   187         and fless:  "\<And>n. \<bar>norm (deriv (\<F> n) 0) - l\<bar> < 1 / (Suc n)"
```
```   188         by metis
```
```   189       have "(\<lambda>n. norm (deriv (\<F> n) 0)) \<longlonglongrightarrow> l"
```
```   190       proof (rule metric_LIMSEQ_I)
```
```   191         fix e::real
```
```   192         assume "e > 0"
```
```   193         then obtain N::nat where N: "e > 1/(Suc N)"
```
```   194           using nat_approx_posE by blast
```
```   195         show "\<exists>N. \<forall>n\<ge>N. dist (norm (deriv (\<F> n) 0)) l < e"
```
```   196         proof (intro exI allI impI)
```
```   197           fix n assume "N \<le> n"
```
```   198           have "dist (norm (deriv (\<F> n) 0)) l < 1 / (Suc n)"
```
```   199             using fless by (simp add: dist_norm)
```
```   200           also have "... < e"
```
```   201             using N \<open>N \<le> n\<close> inverse_of_nat_le le_less_trans by blast
```
```   202           finally show "dist (norm (deriv (\<F> n) 0)) l < e" .
```
```   203         qed
```
```   204       qed
```
```   205       with fF show ?thesis
```
```   206         using that by blast
```
```   207     qed
```
```   208     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"
```
```   209       by (rule_tac x=1 in exI) (force simp: F_def)
```
```   210     moreover have "range \<F> \<subseteq> F"
```
```   211       using \<open>\<And>n. \<F> n \<in> F\<close> by blast
```
```   212     ultimately obtain f and r :: "nat \<Rightarrow> nat"
```
```   213       where holf: "f holomorphic_on S" and r: "strict_mono r"
```
```   214         and limf: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. \<F> (r n) x) \<longlonglongrightarrow> f x"
```
```   215         and ulimf: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K (\<F> \<circ> r) f sequentially"
```
```   216       using Montel [of S F \<F>, OF \<open>open S\<close> holF] by auto+
```
```   217     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)"
```
```   218       using \<open>\<And>n. \<F> n \<in> F\<close> \<open>open S\<close> holF holomorphic_derivI by fastforce
```
```   219     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"
```
```   220       by (meson ulimf \<open>open S\<close> compact_cball open_contains_cball)
```
```   221     obtain f' :: "complex\<Rightarrow>complex" where f': "(f has_field_derivative f' 0) (at 0)"
```
```   222       and tof'0: "(\<lambda>n. ((\<lambda>n. deriv (\<F> n)) \<circ> r) n 0) \<longlonglongrightarrow> f' 0"
```
```   223       using has_complex_derivative_uniform_sequence [OF \<open>open S\<close> der ulim] \<open>0 \<in> S\<close> by metis
```
```   224     then have derf0: "deriv f 0 = f' 0"
```
```   225       by (simp add: DERIV_imp_deriv)
```
```   226     have "f field_differentiable (at 0)"
```
```   227       using field_differentiable_def f' by blast
```
```   228     have "(\<lambda>x.  (norm (deriv (\<F> (r x)) 0))) \<longlonglongrightarrow> norm (deriv f 0)"
```
```   229       using isCont_tendsto_compose [OF continuous_norm [OF continuous_ident] tof'0] derf0 by auto
```
```   230     with LIMSEQ_subseq_LIMSEQ [OF \<F>lim r] have no_df0: "norm(deriv f 0) = l"
```
```   231       by (force simp: o_def intro: tendsto_unique)
```
```   232     have nonconstf: "\<not> f constant_on S"
```
```   233     proof -
```
```   234       have False if "\<And>x. x \<in> S \<Longrightarrow> f x = c" for c
```
```   235       proof -
```
```   236         have "deriv f 0 = 0"
```
```   237           by (metis that \<open>open S\<close> \<open>0 \<in> S\<close> DERIV_imp_deriv [OF DERIV_transform_within_open [OF DERIV_const]])
```
```   238         with no_df0 have "l = 0"
```
```   239           by auto
```
```   240         with eql [OF _ idF] show False by auto
```
```   241       qed
```
```   242       then show ?thesis
```
```   243         by (meson constant_on_def)
```
```   244     qed
```
```   245     show ?thesis
```
```   246     proof
```
```   247       show "f \<in> F"
```
```   248         unfolding F_def
```
```   249       proof (intro CollectI conjI holf)
```
```   250         have "norm(f z) \<le> 1" if "z \<in> S" for z
```
```   251         proof (intro Lim_norm_ubound [OF _ limf] always_eventually allI that)
```
```   252           fix n
```
```   253           have "\<F> (r n) \<in> F"
```
```   254             by (simp add: \<F>in)
```
```   255           then show "norm (\<F> (r n) z) \<le> 1"
```
```   256             using that by (auto simp: F_def)
```
```   257         qed simp
```
```   258         then have fless1: "norm(f z) < 1" if "z \<in> S" for z
```
```   259           using maximum_modulus_principle [OF holf \<open>open S\<close> \<open>connected S\<close> \<open>open S\<close>] nonconstf that
```
```   260           by fastforce
```
```   261         then show "f ` S \<subseteq> ball 0 1"
```
```   262           by auto
```
```   263         have "(\<lambda>n. \<F> (r n) 0) \<longlonglongrightarrow> 0"
```
```   264           using \<F>in by (auto simp: F_def)
```
```   265         then show "f 0 = 0"
```
```   266           using tendsto_unique [OF _ limf ] \<open>0 \<in> S\<close> trivial_limit_sequentially by blast
```
```   267         show "inj_on f S"
```
```   268         proof (rule Hurwitz_injective [OF \<open>open S\<close> \<open>connected S\<close> _ holf])
```
```   269           show "\<And>n. (\<F> \<circ> r) n holomorphic_on S"
```
```   270             by (simp add: \<F>in holF)
```
```   271           show "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K(\<F> \<circ> r) f sequentially"
```
```   272             by (metis ulimf)
```
```   273           show "\<not> f constant_on S"
```
```   274             using nonconstf by auto
```
```   275           show "\<And>n. inj_on ((\<F> \<circ> r) n) S"
```
```   276             using \<F>in by (auto simp: F_def)
```
```   277         qed
```
```   278       qed
```
```   279       show "\<And>h. h \<in> F \<Longrightarrow> norm (deriv h 0) \<le> norm (deriv f 0)"
```
```   280         by (metis eql le_cases no_df0)
```
```   281     qed
```
```   282   qed
```
```   283   have holf: "f holomorphic_on S" and injf: "inj_on f S" and f01: "f ` S \<subseteq> ball 0 1"
```
```   284     using \<open>f \<in> F\<close> by (auto simp: F_def)
```
```   285   obtain g where holg: "g holomorphic_on (f ` S)"
```
```   286              and derg: "\<And>z. z \<in> S \<Longrightarrow> deriv f z * deriv g (f z) = 1"
```
```   287              and gf: "\<And>z. z \<in> S \<Longrightarrow> g(f z) = z"
```
```   288     using holomorphic_has_inverse [OF holf \<open>open S\<close> injf] by metis
```
```   289   have "ball 0 1 \<subseteq> f ` S"
```
```   290   proof
```
```   291     fix a::complex
```
```   292     assume a: "a \<in> ball 0 1"
```
```   293     have False if "\<And>x. x \<in> S \<Longrightarrow> f x \<noteq> a"
```
```   294     proof -
```
```   295       obtain h k where "h a = 0"
```
```   296         and holh: "h holomorphic_on ball 0 1" and h01: "h ` ball 0 1 \<subseteq> ball 0 1"
```
```   297         and holk: "k holomorphic_on ball 0 1" and k01: "k ` ball 0 1 \<subseteq> ball 0 1"
```
```   298         and hk: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> h (k z) = z"
```
```   299         and kh: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> k (h z) = z"
```
```   300         using ball_biholomorphism_exists [OF a] by blast
```
```   301       have nf1: "\<And>z. z \<in> S \<Longrightarrow> norm(f z) < 1"
```
```   302         using \<open>f \<in> F\<close> by (auto simp: F_def)
```
```   303       have 1: "h \<circ> f holomorphic_on S"
```
```   304         using F_def \<open>f \<in> F\<close> holh holomorphic_on_compose holomorphic_on_subset by blast
```
```   305       have 2: "\<And>z. z \<in> S \<Longrightarrow> (h \<circ> f) z \<noteq> 0"
```
```   306         by (metis \<open>h a = 0\<close> a comp_eq_dest_lhs nf1 kh mem_ball_0 that)
```
```   307       have 3: "inj_on (h \<circ> f) S"
```
```   308         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)
```
```   309       obtain \<psi> where hol\<psi>: "\<psi> holomorphic_on ((h \<circ> f) ` S)"
```
```   310         and \<psi>2: "\<And>z. z \<in> S  \<Longrightarrow> \<psi>(h (f z)) ^ 2 = h(f z)"
```
```   311       proof (rule exE [OF prev [OF 1 2 3]], safe)
```
```   312         fix \<theta>
```
```   313         assume hol\<theta>: "\<theta> holomorphic_on S" and \<theta>2: "(\<forall>z\<in>S. (h \<circ> f) z = (\<theta> z)\<^sup>2)"
```
```   314         show thesis
```
```   315         proof
```
```   316           show "(\<theta> \<circ> g \<circ> k) holomorphic_on (h \<circ> f) ` S"
```
```   317           proof (intro holomorphic_on_compose)
```
```   318             show "k holomorphic_on (h \<circ> f) ` S"
```
```   319               apply (rule holomorphic_on_subset [OF holk])
```
```   320               using f01 h01 by force
```
```   321             show "g holomorphic_on k ` (h \<circ> f) ` S"
```
```   322               apply (rule holomorphic_on_subset [OF holg])
```
```   323               by (auto simp: kh nf1)
```
```   324             show "\<theta> holomorphic_on g ` k ` (h \<circ> f) ` S"
```
```   325               apply (rule holomorphic_on_subset [OF hol\<theta>])
```
```   326               by (auto simp: gf kh nf1)
```
```   327           qed
```
```   328           show "((\<theta> \<circ> g \<circ> k) (h (f z)))\<^sup>2 = h (f z)" if "z \<in> S" for z
```
```   329           proof -
```
```   330             have "f z \<in> ball 0 1"
```
```   331               by (simp add: nf1 that)
```
```   332             then have "(\<theta> (g (k (h (f z)))))\<^sup>2 = (\<theta> (g (f z)))\<^sup>2"
```
```   333               by (metis kh)
```
```   334             also have "... = h (f z)"
```
```   335               using \<theta>2 gf that by auto
```
```   336             finally show ?thesis
```
```   337               by (simp add: o_def)
```
```   338           qed
```
```   339         qed
```
```   340       qed
```
```   341       have norm\<psi>1: "norm(\<psi> (h (f z))) < 1" if "z \<in> S" for z
```
```   342       proof -
```
```   343         have "norm (\<psi> (h (f z)) ^ 2) < 1"
```
```   344           by (metis (no_types) that DIM_complex \<psi>2 h01 image_subset_iff mem_ball_0 nf1)
```
```   345         then show ?thesis
```
```   346           by (metis le_less_trans mult_less_cancel_left2 norm_ge_zero norm_power not_le power2_eq_square)
```
```   347       qed
```
```   348       then have \<psi>01: "\<psi> (h (f 0)) \<in> ball 0 1"
```
```   349         by (simp add: \<open>0 \<in> S\<close>)
```
```   350       obtain p q where p0: "p (\<psi> (h (f 0))) = 0"
```
```   351         and holp: "p holomorphic_on ball 0 1" and p01: "p ` ball 0 1 \<subseteq> ball 0 1"
```
```   352         and holq: "q holomorphic_on ball 0 1" and q01: "q ` ball 0 1 \<subseteq> ball 0 1"
```
```   353         and pq: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> p (q z) = z"
```
```   354         and qp: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> q (p z) = z"
```
```   355         using ball_biholomorphism_exists [OF \<psi>01] by metis
```
```   356       have "p \<circ> \<psi> \<circ> h \<circ> f \<in> F"
```
```   357         unfolding F_def
```
```   358       proof (intro CollectI conjI holf)
```
```   359         show "p \<circ> \<psi> \<circ> h \<circ> f holomorphic_on S"
```
```   360         proof (intro holomorphic_on_compose holf)
```
```   361           show "h holomorphic_on f ` S"
```
```   362             apply (rule holomorphic_on_subset [OF holh])
```
```   363             using f01 by force
```
```   364           show "\<psi> holomorphic_on h ` f ` S"
```
```   365             apply (rule holomorphic_on_subset [OF hol\<psi>])
```
```   366             by auto
```
```   367           show "p holomorphic_on \<psi> ` h ` f ` S"
```
```   368             apply (rule holomorphic_on_subset [OF holp])
```
```   369             by (auto simp: norm\<psi>1)
```
```   370         qed
```
```   371         show "(p \<circ> \<psi> \<circ> h \<circ> f) ` S \<subseteq> ball 0 1"
```
```   372           apply clarsimp
```
```   373           by (meson norm\<psi>1 p01 image_subset_iff mem_ball_0)
```
```   374         show "(p \<circ> \<psi> \<circ> h \<circ> f) 0 = 0"
```
```   375           by (simp add: \<open>p (\<psi> (h (f 0))) = 0\<close>)
```
```   376         show "inj_on (p \<circ> \<psi> \<circ> h \<circ> f) S"
```
```   377           unfolding inj_on_def o_def
```
```   378           by (metis \<psi>2 dist_0_norm gf kh mem_ball nf1 norm\<psi>1 qp)
```
```   379       qed
```
```   380       then have le_norm_df0: "norm (deriv (p \<circ> \<psi> \<circ> h \<circ> f) 0) \<le> norm (deriv f 0)"
```
```   381         by (rule normf)
```
```   382       have 1: "k \<circ> power2 \<circ> q holomorphic_on ball 0 1"
```
```   383       proof (intro holomorphic_on_compose holq)
```
```   384         show "power2 holomorphic_on q ` ball 0 1"
```
```   385           using holomorphic_on_subset holomorphic_on_power
```
```   386           by (blast intro: holomorphic_on_ident)
```
```   387         show "k holomorphic_on power2 ` q ` ball 0 1"
```
```   388           apply (rule holomorphic_on_subset [OF holk])
```
```   389           using q01 by (auto simp: norm_power abs_square_less_1)
```
```   390       qed
```
```   391       have 2: "(k \<circ> power2 \<circ> q) 0 = 0"
```
```   392         using p0 F_def \<open>f \<in> F\<close> \<psi>01 \<psi>2 \<open>0 \<in> S\<close> kh qp by force
```
```   393       have 3: "norm ((k \<circ> power2 \<circ> q) z) < 1" if "norm z < 1" for z
```
```   394       proof -
```
```   395         have "norm ((power2 \<circ> q) z) < 1"
```
```   396           using that q01 by (force simp: norm_power abs_square_less_1)
```
```   397         with k01 show ?thesis
```
```   398           by fastforce
```
```   399       qed
```
```   400       have False if c: "\<forall>z. norm z < 1 \<longrightarrow> (k \<circ> power2 \<circ> q) z = c * z" and "norm c = 1" for c
```
```   401       proof -
```
```   402         have "c \<noteq> 0" using that by auto
```
```   403         have "norm (p(1/2)) < 1" "norm (p(-1/2)) < 1"
```
```   404           using p01 by force+
```
```   405         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)"
```
```   406           using c by force+
```
```   407         then have "p (1/2) = p (- (1/2))"
```
```   408           by (auto simp: \<open>c \<noteq> 0\<close> qp o_def)
```
```   409         then have "q (p (1/2)) = q (p (- (1/2)))"
```
```   410           by simp
```
```   411         then have "1/2 = - (1/2::complex)"
```
```   412           by (auto simp: qp)
```
```   413         then show False
```
```   414           by simp
```
```   415       qed
```
```   416       moreover
```
```   417       have False if "norm (deriv (k \<circ> power2 \<circ> q) 0) \<noteq> 1" "norm (deriv (k \<circ> power2 \<circ> q) 0) \<le> 1"
```
```   418         and le: "\<And>\<xi>. norm \<xi> < 1 \<Longrightarrow> norm ((k \<circ> power2 \<circ> q) \<xi>) \<le> norm \<xi>"
```
```   419       proof -
```
```   420         have "norm (deriv (k \<circ> power2 \<circ> q) 0) < 1"
```
```   421           using that by simp
```
```   422         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"
```
```   423         proof (intro DERIV_imp_deriv DERIV_transform_within_open [OF DERIV_chain])
```
```   424           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))"
```
```   425             using "1" holomorphic_derivI p0 by auto
```
```   426           show "(p \<circ> \<psi> \<circ> h \<circ> f has_field_derivative deriv (p \<circ> \<psi> \<circ> h \<circ> f) 0) (at 0)"
```
```   427             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
```
```   428           show "\<And>x. x \<in> S \<Longrightarrow> (k \<circ> power2 \<circ> q \<circ> (p \<circ> \<psi> \<circ> h \<circ> f)) x = f x"
```
```   429             using \<psi>2 f01 kh norm\<psi>1 qp by auto
```
```   430         qed (use assms in simp_all)
```
```   431         ultimately have "cmod (deriv (p \<circ> \<psi> \<circ> h \<circ> f) 0) \<le> 0"
```
```   432           using le_norm_df0
```
```   433           by (metis linorder_not_le mult.commute mult_less_cancel_left2 norm_mult)
```
```   434         moreover have "1 \<le> norm (deriv f 0)"
```
```   435           using normf [of id] by (simp add: idF)
```
```   436         ultimately show False
```
```   437           by (simp add: eq)
```
```   438       qed
```
```   439       ultimately show ?thesis
```
```   440         using Schwarz_Lemma [OF 1 2 3] norm_one by blast
```
```   441     qed
```
```   442     then show "a \<in> f ` S"
```
```   443       by blast
```
```   444   qed
```
```   445   then have "f ` S = ball 0 1"
```
```   446     using F_def \<open>f \<in> F\<close> by blast
```
```   447   then show ?thesis
```
```   448     apply (rule_tac x=f in exI)
```
```   449     apply (rule_tac x=g in exI)
```
```   450     using holf holg derg gf by safe force+
```
```   451 qed
```
```   452
```
```   453
```
```   454 locale SC_Chain =
```
```   455   fixes S :: "complex set"
```
```   456   assumes openS: "open S"
```
```   457 begin
```
```   458
```
```   459 lemma winding_number_zero:
```
```   460   assumes "simply_connected S"
```
```   461   shows "connected S \<and>
```
```   462          (\<forall>\<gamma> z. path \<gamma> \<and> path_image \<gamma> \<subseteq> S \<and>
```
```   463                    pathfinish \<gamma> = pathstart \<gamma> \<and> z \<notin> S \<longrightarrow> winding_number \<gamma> z = 0)"
```
```   464   using assms
```
```   465   by (auto simp: simply_connected_imp_connected simply_connected_imp_winding_number_zero)
```
```   466
```
```   467 lemma contour_integral_zero:
```
```   468   assumes "valid_path g" "path_image g \<subseteq> S" "pathfinish g = pathstart g" "f holomorphic_on S"
```
```   469          "\<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"
```
```   470   shows "(f has_contour_integral 0) g"
```
```   471   using assms by (meson Cauchy_theorem_global openS valid_path_imp_path)
```
```   472
```
```   473 lemma global_primitive:
```
```   474   assumes "connected S" and holf: "f holomorphic_on S"
```
```   475   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>"
```
```   476   shows "\<exists>h. \<forall>z \<in> S. (h has_field_derivative f z) (at z)"
```
```   477 proof (cases "S = {}")
```
```   478 case True then show ?thesis
```
```   479     by simp
```
```   480 next
```
```   481   case False
```
```   482   then obtain a where "a \<in> S"
```
```   483     by blast
```
```   484   show ?thesis
```
```   485   proof (intro exI ballI)
```
```   486     fix x assume "x \<in> S"
```
```   487     then obtain d where "d > 0" and d: "cball x d \<subseteq> S"
```
```   488       using openS open_contains_cball_eq by blast
```
```   489     let ?g = "\<lambda>z. (SOME g. polynomial_function g \<and> path_image g \<subseteq> S \<and> pathstart g = a \<and> pathfinish g = z)"
```
```   490     show "((\<lambda>z. contour_integral (?g z) f) has_field_derivative f x)
```
```   491           (at x)"
```
```   492     proof (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right, rule Lim_transform)
```
```   493       show "(\<lambda>y. inverse(norm(y - x)) *\<^sub>R (contour_integral(linepath x y) f - f x * (y - x))) \<midarrow>x\<rightarrow> 0"
```
```   494       proof (clarsimp simp add: Lim_at)
```
```   495         fix e::real assume "e > 0"
```
```   496         moreover have "continuous (at x) f"
```
```   497           using openS \<open>x \<in> S\<close> holf continuous_on_eq_continuous_at holomorphic_on_imp_continuous_on by auto
```
```   498         ultimately obtain d1 where "d1 > 0"
```
```   499              and d1: "\<And>x'. dist x' x < d1 \<Longrightarrow> dist (f x') (f x) < e/2"
```
```   500           unfolding continuous_at_eps_delta
```
```   501           by (metis less_divide_eq_numeral1(1) mult_zero_left)
```
```   502         obtain d2 where "d2 > 0" and d2: "ball x d2 \<subseteq> S"
```
```   503           using openS \<open>x \<in> S\<close> open_contains_ball_eq by blast
```
```   504         have "inverse (norm (y - x)) * norm (contour_integral (linepath x y) f - f x * (y - x)) < e"
```
```   505           if "0 < d1" "0 < d2" "y \<noteq> x" "dist y x < d1" "dist y x < d2" for y
```
```   506         proof -
```
```   507           have "f contour_integrable_on linepath x y"
```
```   508           proof (rule contour_integrable_continuous_linepath [OF continuous_on_subset])
```
```   509             show "continuous_on S f"
```
```   510               by (simp add: holf holomorphic_on_imp_continuous_on)
```
```   511             have "closed_segment x y \<subseteq> ball x d2"
```
```   512               by (meson dist_commute_lessI dist_in_closed_segment le_less_trans mem_ball subsetI that(5))
```
```   513             with d2 show "closed_segment x y \<subseteq> S"
```
```   514               by blast
```
```   515           qed
```
```   516           then obtain z where z: "(f has_contour_integral z) (linepath x y)"
```
```   517             by (force simp: contour_integrable_on_def)
```
```   518           have con: "((\<lambda>w. f x) has_contour_integral f x * (y - x)) (linepath x y)"
```
```   519             using has_contour_integral_const_linepath [of "f x" y x] by metis
```
```   520           have "norm (z - f x * (y - x)) \<le> (e/2) * norm (y - x)"
```
```   521           proof (rule has_contour_integral_bound_linepath)
```
```   522             show "((\<lambda>w. f w - f x) has_contour_integral z - f x * (y - x)) (linepath x y)"
```
```   523               by (rule has_contour_integral_diff [OF z con])
```
```   524             show "\<And>w. w \<in> closed_segment x y \<Longrightarrow> norm (f w - f x) \<le> e/2"
```
```   525               by (metis d1 dist_norm less_le_trans not_less not_less_iff_gr_or_eq segment_bound1 that(4))
```
```   526           qed (use \<open>e > 0\<close> in auto)
```
```   527           with \<open>e > 0\<close> have "inverse (norm (y - x)) * norm (z - f x * (y - x)) \<le> e/2"
```
```   528             by (simp add: divide_simps)
```
```   529           also have "... < e"
```
```   530             using \<open>e > 0\<close> by simp
```
```   531           finally show ?thesis
```
```   532             by (simp add: contour_integral_unique [OF z])
```
```   533         qed
```
```   534         with  \<open>d1 > 0\<close> \<open>d2 > 0\<close>
```
```   535         show "\<exists>d>0. \<forall>z. z \<noteq> x \<and> dist z x < d \<longrightarrow>
```
```   536                  inverse (norm (z - x)) * norm (contour_integral (linepath x z) f - f x * (z - x)) < e"
```
```   537           by (rule_tac x="min d1 d2" in exI) auto
```
```   538       qed
```
```   539     next
```
```   540       have *: "(1 / norm (y - x)) *\<^sub>R (contour_integral (?g y) f -
```
```   541                (contour_integral (?g x) f + f x * (y - x))) =
```
```   542                (contour_integral (linepath x y) f - f x * (y - x)) /\<^sub>R norm (y - x)"
```
```   543         if "0 < d" "y \<noteq> x" and yx: "dist y x < d" for y
```
```   544       proof -
```
```   545         have "y \<in> S"
```
```   546           by (metis subsetD d dist_commute less_eq_real_def mem_cball yx)
```
```   547         have gxy: "polynomial_function (?g x) \<and> path_image (?g x) \<subseteq> S \<and> pathstart (?g x) = a \<and> pathfinish (?g x) = x"
```
```   548                   "polynomial_function (?g y) \<and> path_image (?g y) \<subseteq> S \<and> pathstart (?g y) = a \<and> pathfinish (?g y) = y"
```
```   549           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>
```
```   550           by meson+
```
```   551         then have vp: "valid_path (?g x)" "valid_path (?g y)"
```
```   552           by (simp_all add: valid_path_polynomial_function)
```
```   553         have f0: "(f has_contour_integral 0) ((?g x) +++ linepath x y +++ reversepath (?g y))"
```
```   554         proof (rule prev)
```
```   555           show "valid_path ((?g x) +++ linepath x y +++ reversepath (?g y))"
```
```   556             using gxy vp by (auto simp: valid_path_join)
```
```   557           have "closed_segment x y \<subseteq> cball x d"
```
```   558             using  yx by (auto simp: dist_commute dest!: dist_in_closed_segment)
```
```   559           then have "closed_segment x y \<subseteq> S"
```
```   560             using d by blast
```
```   561           then show "path_image ((?g x) +++ linepath x y +++ reversepath (?g y)) \<subseteq> S"
```
```   562             using gxy by (auto simp: path_image_join)
```
```   563         qed (use gxy holf in auto)
```
```   564         then have fintxy: "f contour_integrable_on linepath x y"
```
```   565           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))
```
```   566         have fintgx: "f contour_integrable_on (?g x)" "f contour_integrable_on (?g y)"
```
```   567           using openS contour_integrable_holomorphic_simple gxy holf vp by blast+
```
```   568         show ?thesis
```
```   569           apply (clarsimp simp add: divide_simps)
```
```   570           using contour_integral_unique [OF f0]
```
```   571           apply (simp add: fintxy gxy contour_integrable_reversepath contour_integral_reversepath fintgx vp)
```
```   572           apply (simp add: algebra_simps)
```
```   573           done
```
```   574       qed
```
```   575       show "(\<lambda>z. (1 / norm (z - x)) *\<^sub>R
```
```   576                  (contour_integral (?g z) f - (contour_integral (?g x) f + f x * (z - x))) -
```
```   577                  (contour_integral (linepath x z) f - f x * (z - x)) /\<^sub>R norm (z - x))
```
```   578             \<midarrow>x\<rightarrow> 0"
```
```   579         apply (rule Lim_eventually)
```
```   580         apply (simp add: eventually_at)
```
```   581         apply (rule_tac x=d in exI)
```
```   582         using \<open>d > 0\<close> * by simp
```
```   583     qed
```
```   584   qed
```
```   585 qed
```
```   586
```
```   587 lemma holomorphic_log:
```
```   588   assumes "connected S" and holf: "f holomorphic_on S" and nz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
```
```   589   and prev: "\<And>f. f holomorphic_on S \<Longrightarrow> \<exists>h. \<forall>z \<in> S. (h has_field_derivative f z) (at z)"
```
```   590   shows "\<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S. f z = exp(g z))"
```
```   591 proof -
```
```   592   have "(\<lambda>z. deriv f z / f z) holomorphic_on S"
```
```   593     by (simp add: openS holf holomorphic_deriv holomorphic_on_divide nz)
```
```   594   then obtain g where g: "\<And>z. z \<in> S \<Longrightarrow> (g has_field_derivative deriv f z / f z) (at z)"
```
```   595     using prev [of "\<lambda>z. deriv f z / f z"] by metis
```
```   596   have hfd: "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>z. exp (g z) / f z) has_field_derivative 0) (at x)"
```
```   597     apply (rule derivative_eq_intros g| simp)+
```
```   598       apply (subst DERIV_deriv_iff_field_differentiable)
```
```   599     using openS holf holomorphic_on_imp_differentiable_at nz apply auto
```
```   600     done
```
```   601   obtain c where c: "\<And>x. x \<in> S \<Longrightarrow> exp (g x) / f x = c"
```
```   602   proof (rule DERIV_zero_connected_constant[OF \<open>connected S\<close> openS finite.emptyI])
```
```   603     show "continuous_on S (\<lambda>z. exp (g z) / f z)"
```
```   604       by (metis (full_types) openS g continuous_on_divide continuous_on_exp holf holomorphic_on_imp_continuous_on holomorphic_on_open nz)
```
```   605     then show "\<forall>x\<in>S - {}. ((\<lambda>z. exp (g z) / f z) has_field_derivative 0) (at x)"
```
```   606       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"])
```
```   607   qed auto
```
```   608   show ?thesis
```
```   609   proof (intro exI ballI conjI)
```
```   610     show "(\<lambda>z. Ln(inverse c) + g z) holomorphic_on S"
```
```   611       apply (intro holomorphic_intros)
```
```   612       using openS g holomorphic_on_open by blast
```
```   613     fix z :: complex
```
```   614     assume "z \<in> S"
```
```   615     then have "exp (g z) / c = f z"
```
```   616       by (metis c divide_divide_eq_right exp_not_eq_zero nonzero_mult_div_cancel_left)
```
```   617     moreover have "1 / c \<noteq> 0"
```
```   618       using \<open>z \<in> S\<close> c nz by fastforce
```
```   619     ultimately show "f z = exp (Ln (inverse c) + g z)"
```
```   620       by (simp add: exp_add inverse_eq_divide)
```
```   621   qed
```
```   622 qed
```
```   623
```
```   624 lemma holomorphic_sqrt:
```
```   625   assumes holf: "f holomorphic_on S" and nz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
```
```   626   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))"
```
```   627   shows "\<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S. f z = (g z)\<^sup>2)"
```
```   628 proof -
```
```   629   obtain g where holg: "g holomorphic_on S" and g: "\<And>z. z \<in> S \<Longrightarrow> f z = exp (g z)"
```
```   630     using prev [of f] holf nz by metis
```
```   631   show ?thesis
```
```   632   proof (intro exI ballI conjI)
```
```   633     show "(\<lambda>z. exp(g z/2)) holomorphic_on S"
```
```   634       by (intro holomorphic_intros) (auto simp: holg)
```
```   635     show "\<And>z. z \<in> S \<Longrightarrow> f z = (exp (g z/2))\<^sup>2"
```
```   636       by (metis (no_types) g exp_double nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral)
```
```   637   qed
```
```   638 qed
```
```   639
```
```   640 lemma biholomorphic_to_disc:
```
```   641   assumes "connected S" and S: "S \<noteq> {}" "S \<noteq> UNIV"
```
```   642   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)"
```
```   643   shows "\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
```
```   644                    (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
```
```   645                    (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z)"
```
```   646 proof -
```
```   647   obtain a b where "a \<in> S" "b \<notin> S"
```
```   648     using S by blast
```
```   649   then obtain \<delta> where "\<delta> > 0" and \<delta>: "ball a \<delta> \<subseteq> S"
```
```   650     using openS openE by blast
```
```   651   obtain g where holg: "g holomorphic_on S" and eqg: "\<And>z. z \<in> S \<Longrightarrow> z - b = (g z)\<^sup>2"
```
```   652   proof (rule exE [OF prev [of "\<lambda>z. z - b"]])
```
```   653     show "(\<lambda>z. z - b) holomorphic_on S"
```
```   654       by (intro holomorphic_intros)
```
```   655   qed (use \<open>b \<notin> S\<close> in auto)
```
```   656   have "\<not> g constant_on S"
```
```   657   proof -
```
```   658     have "(a + \<delta>/2) \<in> ball a \<delta>" "a + (\<delta>/2) \<noteq> a"
```
```   659       using \<open>\<delta> > 0\<close> by (simp_all add: dist_norm)
```
```   660     then show ?thesis
```
```   661       unfolding constant_on_def
```
```   662       using eqg [of a] eqg [of "a + \<delta>/2"] \<open>a \<in> S\<close> \<delta>
```
```   663       by (metis diff_add_cancel subset_eq)
```
```   664   qed
```
```   665   then have "open (g ` ball a \<delta>)"
```
```   666     using open_mapping_thm [of g S "ball a \<delta>", OF holg openS \<open>connected S\<close>] \<delta> by blast
```
```   667   then obtain r where "r > 0" and r: "ball (g a) r \<subseteq> (g ` ball a \<delta>)"
```
```   668     by (metis \<open>0 < \<delta>\<close> centre_in_ball imageI openE)
```
```   669   have g_not_r: "g z \<notin> ball (-(g a)) r" if "z \<in> S" for z
```
```   670   proof
```
```   671     assume "g z \<in> ball (-(g a)) r"
```
```   672     then have "- g z \<in> ball (g a) r"
```
```   673       by (metis add.inverse_inverse dist_minus mem_ball)
```
```   674     with r have "- g z \<in> (g ` ball a \<delta>)"
```
```   675       by blast
```
```   676     then obtain w where w: "- g z = g w" "dist a w < \<delta>"
```
```   677       by auto
```
```   678     then have "w \<in> ball a \<delta>"
```
```   679       by simp
```
```   680     then have "w \<in> S"
```
```   681       using \<delta> by blast
```
```   682     then have "w = z"
```
```   683       by (metis diff_add_cancel eqg power_minus_Bit0 that w(1))
```
```   684     then have "g z = 0"
```
```   685       using \<open>- g z = g w\<close> by auto
```
```   686     with eqg [OF that] have "z = b"
```
```   687       by auto
```
```   688     with that \<open>b \<notin> S\<close> show False
```
```   689       by simp
```
```   690   qed
```
```   691   then have nz: "\<And>z. z \<in> S \<Longrightarrow> g z + g a \<noteq> 0"
```
```   692     by (metis \<open>0 < r\<close> add.commute add_diff_cancel_left' centre_in_ball diff_0)
```
```   693   let ?f = "\<lambda>z. (r/3) / (g z + g a) - (r/3) / (g a + g a)"
```
```   694   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"
```
```   695   proof
```
```   696     show "?f holomorphic_on S"
```
```   697       by (intro holomorphic_intros holg nz)
```
```   698     have 3: "\<lbrakk>norm x \<le> 1/3; norm y \<le> 1/3\<rbrakk> \<Longrightarrow> norm(x - y) < 1" for x y::complex
```
```   699       using norm_triangle_ineq4 [of x y] by simp
```
```   700     have "norm ((r/3) / (g z + g a) - (r/3) / (g a + g a)) < 1" if "z \<in> S" for z
```
```   701       apply (rule 3)
```
```   702       unfolding norm_divide
```
```   703       using \<open>r > 0\<close> g_not_r [OF \<open>z \<in> S\<close>] g_not_r [OF \<open>a \<in> S\<close>]
```
```   704       by (simp_all add: divide_simps dist_commute dist_norm)
```
```   705   then show "?f ` S \<subseteq> ball 0 1"
```
```   706     by auto
```
```   707     show "inj_on ?f S"
```
```   708       using \<open>r > 0\<close> eqg apply (clarsimp simp: inj_on_def)
```
```   709       by (metis diff_add_cancel)
```
```   710   qed auto
```
```   711   obtain k where holk: "k holomorphic_on (h ` S)"
```
```   712              and derk: "\<And>z. z \<in> S \<Longrightarrow> deriv h z * deriv k (h z) = 1"
```
```   713              and kh: "\<And>z. z \<in> S \<Longrightarrow> k(h z) = z"
```
```   714     using holomorphic_has_inverse [OF holh openS \<open>inj_on h S\<close>] by metis
```
```   715
```
```   716   have 1: "open (h ` S)"
```
```   717     by (simp add: \<open>inj_on h S\<close> holh openS open_mapping_thm3)
```
```   718   have 2: "connected (h ` S)"
```
```   719     by (simp add: connected_continuous_image \<open>connected S\<close> holh holomorphic_on_imp_continuous_on)
```
```   720   have 3: "0 \<in> h ` S"
```
```   721     using \<open>a \<in> S\<close> \<open>h a = 0\<close> by auto
```
```   722   have 4: "\<exists>g. g holomorphic_on h ` S \<and> (\<forall>z\<in>h ` S. f z = (g z)\<^sup>2)"
```
```   723     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
```
```   724   proof -
```
```   725     obtain g where holg: "g holomorphic_on S" and eqg: "\<And>z. z \<in> S \<Longrightarrow> (f \<circ> h) z = (g z)\<^sup>2"
```
```   726     proof -
```
```   727       have "f \<circ> h holomorphic_on S"
```
```   728         by (simp add: holh holomorphic_on_compose holf)
```
```   729       moreover have "\<forall>z\<in>S. (f \<circ> h) z \<noteq> 0"
```
```   730         by (simp add: nz)
```
```   731       ultimately show thesis
```
```   732         using prev that by blast
```
```   733     qed
```
```   734     show ?thesis
```
```   735     proof (intro exI conjI)
```
```   736       show "g \<circ> k holomorphic_on h ` S"
```
```   737       proof -
```
```   738         have "k ` h ` S \<subseteq> S"
```
```   739           by (simp add: \<open>\<And>z. z \<in> S \<Longrightarrow> k (h z) = z\<close> image_subset_iff)
```
```   740         then show ?thesis
```
```   741           by (meson holg holk holomorphic_on_compose holomorphic_on_subset)
```
```   742       qed
```
```   743       show "\<forall>z\<in>h ` S. f z = ((g \<circ> k) z)\<^sup>2"
```
```   744         using eqg kh by auto
```
```   745     qed
```
```   746   qed
```
```   747   obtain f g where f: "f holomorphic_on h ` S" and g: "g holomorphic_on ball 0 1"
```
```   748        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"
```
```   749     using biholomorphic_to_disc_aux [OF 1 2 3 h01 4] by blast
```
```   750   show ?thesis
```
```   751   proof (intro exI conjI)
```
```   752     show "f \<circ> h holomorphic_on S"
```
```   753       by (simp add: f holh holomorphic_on_compose)
```
```   754     show "k \<circ> g holomorphic_on ball 0 1"
```
```   755       by (metis holomorphic_on_subset image_subset_iff fg holk g holomorphic_on_compose)
```
```   756   qed (use fg gf kh in auto)
```
```   757 qed
```
```   758
```
```   759 lemma homeomorphic_to_disc:
```
```   760   assumes S: "S \<noteq> {}"
```
```   761     and prev: "S = UNIV \<or>
```
```   762                (\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
```
```   763                      (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
```
```   764                      (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z))" (is "_ \<or> ?P")
```
```   765   shows "S homeomorphic ball (0::complex) 1"
```
```   766   using prev
```
```   767 proof
```
```   768   assume "S = UNIV" then show ?thesis
```
```   769     using homeomorphic_ball01_UNIV homeomorphic_sym by blast
```
```   770 next
```
```   771   assume ?P
```
```   772   then show ?thesis
```
```   773     unfolding homeomorphic_minimal
```
```   774     using holomorphic_on_imp_continuous_on by blast
```
```   775 qed
```
```   776
```
```   777 lemma homeomorphic_to_disc_imp_simply_connected:
```
```   778   assumes "S = {} \<or> S homeomorphic ball (0::complex) 1"
```
```   779   shows "simply_connected S"
```
```   780   using assms homeomorphic_simply_connected_eq convex_imp_simply_connected by auto
```
```   781
```
```   782 end
```
```   783
```
```   784 proposition
```
```   785   assumes "open S"
```
```   786   shows simply_connected_eq_winding_number_zero:
```
```   787          "simply_connected S \<longleftrightarrow>
```
```   788            connected S \<and>
```
```   789            (\<forall>g z. path g \<and> path_image g \<subseteq> S \<and>
```
```   790                  pathfinish g = pathstart g \<and> (z \<notin> S)
```
```   791                  \<longrightarrow> winding_number g z = 0)" (is "?wn0")
```
```   792     and simply_connected_eq_contour_integral_zero:
```
```   793          "simply_connected S \<longleftrightarrow>
```
```   794            connected S \<and>
```
```   795            (\<forall>g f. valid_path g \<and> path_image g \<subseteq> S \<and>
```
```   796                  pathfinish g = pathstart g \<and> f holomorphic_on S
```
```   797                \<longrightarrow> (f has_contour_integral 0) g)" (is "?ci0")
```
```   798     and simply_connected_eq_global_primitive:
```
```   799          "simply_connected S \<longleftrightarrow>
```
```   800            connected S \<and>
```
```   801            (\<forall>f. f holomorphic_on S \<longrightarrow>
```
```   802                 (\<exists>h. \<forall>z. z \<in> S \<longrightarrow> (h has_field_derivative f z) (at z)))" (is "?gp")
```
```   803     and simply_connected_eq_holomorphic_log:
```
```   804          "simply_connected S \<longleftrightarrow>
```
```   805            connected S \<and>
```
```   806            (\<forall>f. f holomorphic_on S \<and> (\<forall>z \<in> S. f z \<noteq> 0)
```
```   807                \<longrightarrow> (\<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S. f z = exp(g z))))" (is "?log")
```
```   808     and simply_connected_eq_holomorphic_sqrt:
```
```   809          "simply_connected S \<longleftrightarrow>
```
```   810            connected S \<and>
```
```   811            (\<forall>f. f holomorphic_on S \<and> (\<forall>z \<in> S. f z \<noteq> 0)
```
```   812                 \<longrightarrow> (\<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S.  f z = (g z)\<^sup>2)))" (is "?sqrt")
```
```   813     and simply_connected_eq_biholomorphic_to_disc:
```
```   814          "simply_connected S \<longleftrightarrow>
```
```   815            S = {} \<or> S = UNIV \<or>
```
```   816            (\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
```
```   817                  (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
```
```   818                  (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z))" (is "?bih")
```
```   819     and simply_connected_eq_homeomorphic_to_disc:
```
```   820           "simply_connected S \<longleftrightarrow> S = {} \<or> S homeomorphic ball (0::complex) 1" (is "?disc")
```
```   821 proof -
```
```   822   interpret SC_Chain
```
```   823     using assms by (simp add: SC_Chain_def)
```
```   824   have "?wn0 \<and> ?ci0 \<and> ?gp \<and> ?log \<and> ?sqrt \<and> ?bih \<and> ?disc"
```
```   825 proof -
```
```   826   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>
```
```   827         \<Longrightarrow> (\<alpha> \<longleftrightarrow> \<beta>) \<and> (\<alpha> \<longleftrightarrow> \<gamma>) \<and> (\<alpha> \<longleftrightarrow> \<delta>) \<and> (\<alpha> \<longleftrightarrow> \<zeta>) \<and>
```
```   828             (\<alpha> \<longleftrightarrow> \<eta>) \<and> (\<alpha> \<longleftrightarrow> \<theta>) \<and> (\<alpha> \<longleftrightarrow> \<xi>)" for \<alpha> \<beta> \<gamma> \<delta> \<zeta> \<eta> \<theta> \<xi>
```
```   829     by blast
```
```   830   show ?thesis
```
```   831     apply (rule *)
```
```   832     using winding_number_zero apply metis
```
```   833     using contour_integral_zero apply metis
```
```   834     using global_primitive apply metis
```
```   835     using holomorphic_log apply metis
```
```   836     using holomorphic_sqrt apply simp
```
```   837     using biholomorphic_to_disc apply blast
```
```   838     using homeomorphic_to_disc apply blast
```
```   839     using homeomorphic_to_disc_imp_simply_connected apply blast
```
```   840     done
```
```   841 qed
```
```   842   then show ?wn0 ?ci0 ?gp ?log ?sqrt ?bih ?disc
```
```   843     by safe
```
```   844 qed
```
```   845
```
```   846 corollary contractible_eq_simply_connected_2d:
```
```   847   fixes S :: "complex set"
```
```   848   shows "open S \<Longrightarrow> (contractible S \<longleftrightarrow> simply_connected S)"
```
```   849   apply safe
```
```   850    apply (simp add: contractible_imp_simply_connected)
```
```   851   using convex_imp_contractible homeomorphic_contractible_eq simply_connected_eq_homeomorphic_to_disc by auto
```
```   852
```
```   853 subsection\<open>A further chain of equivalences about components of the complement of a simply connected set\<close>
```
```   854
```
```   855 text\<open>(following 1.35 in Burckel'S book)\<close>
```
```   856
```
```   857 context SC_Chain
```
```   858 begin
```
```   859
```
```   860 lemma frontier_properties:
```
```   861   assumes "simply_connected S"
```
```   862   shows "if bounded S then connected(frontier S)
```
```   863          else \<forall>C \<in> components(frontier S). \<not> bounded C"
```
```   864 proof -
```
```   865   have "S = {} \<or> S homeomorphic ball (0::complex) 1"
```
```   866     using simply_connected_eq_homeomorphic_to_disc assms openS by blast
```
```   867   then show ?thesis
```
```   868   proof
```
```   869     assume "S = {}"
```
```   870     then have "bounded S"
```
```   871       by simp
```
```   872     with \<open>S = {}\<close> show ?thesis
```
```   873       by simp
```
```   874   next
```
```   875     assume S01: "S homeomorphic ball (0::complex) 1"
```
```   876     then obtain g f
```
```   877       where gim: "g ` S = ball 0 1" and fg: "\<And>x. x \<in> S \<Longrightarrow> f(g x) = x"
```
```   878         and fim: "f ` ball 0 1 = S" and gf: "\<And>y. cmod y < 1 \<Longrightarrow> g(f y) = y"
```
```   879         and contg: "continuous_on S g" and contf: "continuous_on (ball 0 1) f"
```
```   880       by (fastforce simp: homeomorphism_def homeomorphic_def)
```
```   881     define D where "D \<equiv> \<lambda>n. ball (0::complex) (1 - 1/(of_nat n + 2))"
```
```   882     define A where "A \<equiv> \<lambda>n. {z::complex. 1 - 1/(of_nat n + 2) < norm z \<and> norm z < 1}"
```
```   883     define X where "X \<equiv> \<lambda>n::nat. closure(f ` A n)"
```
```   884     have D01: "D n \<subseteq> ball 0 1" for n
```
```   885       by (simp add: D_def ball_subset_ball_iff)
```
```   886     have A01: "A n \<subseteq> ball 0 1" for n
```
```   887       by (auto simp: A_def)
```
```   888     have cloX: "closed(X n)" for n
```
```   889       by (simp add: X_def)
```
```   890     have Xsubclo: "X n \<subseteq> closure S" for n
```
```   891       unfolding X_def by (metis A01 closure_mono fim image_mono)
```
```   892     have connX: "connected(X n)" for n
```
```   893       unfolding X_def
```
```   894       apply (rule connected_imp_connected_closure)
```
```   895       apply (rule connected_continuous_image)
```
```   896       apply (simp add: continuous_on_subset [OF contf A01])
```
```   897       using connected_annulus [of _ "0::complex"] by (simp add: A_def)
```
```   898     have nestX: "X n \<subseteq> X m" if "m \<le> n" for m n
```
```   899     proof -
```
```   900       have "1 - 1 / (real m + 2) \<le> 1 - 1 / (real n + 2)"
```
```   901         using that by (auto simp: field_simps)
```
```   902       then show ?thesis
```
```   903         by (auto simp: X_def A_def intro!: closure_mono)
```
```   904     qed
```
```   905     have "closure S - S \<subseteq> (\<Inter>n. X n)"
```
```   906     proof
```
```   907       fix x
```
```   908       assume "x \<in> closure S - S"
```
```   909       then have "x \<in> closure S" "x \<notin> S" by auto
```
```   910       show "x \<in> (\<Inter>n. X n)"
```
```   911       proof
```
```   912         fix n
```
```   913         have "ball 0 1 = closure (D n) \<union> A n"
```
```   914           by (auto simp: D_def A_def le_less_trans)
```
```   915         with fim have Seq: "S = f ` (closure (D n)) \<union> f ` (A n)"
```
```   916           by (simp add: image_Un)
```
```   917         have "continuous_on (closure (D n)) f"
```
```   918           by (simp add: D_def cball_subset_ball_iff continuous_on_subset [OF contf])
```
```   919         moreover have "compact (closure (D n))"
```
```   920           by (simp add: D_def)
```
```   921         ultimately have clo_fim: "closed (f ` closure (D n))"
```
```   922           using compact_continuous_image compact_imp_closed by blast
```
```   923         have *: "(f ` cball 0 (1 - 1 / (real n + 2))) \<subseteq> S"
```
```   924           by (force simp: D_def Seq)
```
```   925         show "x \<in> X n"
```
```   926           using \<open>x \<in> closure S\<close> unfolding X_def Seq
```
```   927           using \<open>x \<notin> S\<close> * D_def clo_fim by auto
```
```   928       qed
```
```   929     qed
```
```   930     moreover have "(\<Inter>n. X n) \<subseteq> closure S - S"
```
```   931     proof -
```
```   932       have "(\<Inter>n. X n) \<subseteq> closure S"
```
```   933       proof -
```
```   934         have "(\<Inter>n. X n) \<subseteq> X 0"
```
```   935           by blast
```
```   936         also have "... \<subseteq> closure S"
```
```   937           apply (simp add: X_def fim [symmetric])
```
```   938           apply (rule closure_mono)
```
```   939           by (auto simp: A_def)
```
```   940         finally show "(\<Inter>n. X n) \<subseteq> closure S" .
```
```   941       qed
```
```   942       moreover have "(\<Inter>n. X n) \<inter> S \<subseteq> {}"
```
```   943       proof (clarify, clarsimp simp: X_def fim [symmetric])
```
```   944         fix x assume x [rule_format]: "\<forall>n. f x \<in> closure (f ` A n)" and "cmod x < 1"
```
```   945         then obtain n where n: "1 / (1 - norm x) < of_nat n"
```
```   946           using reals_Archimedean2 by blast
```
```   947         with \<open>cmod x < 1\<close> gr0I have XX: "1 / of_nat n < 1 - norm x" and "n > 0"
```
```   948           by (fastforce simp: divide_simps algebra_simps)+
```
```   949         have "f x \<in> f ` (D n)"
```
```   950           using n \<open>cmod x < 1\<close> by (auto simp: divide_simps algebra_simps D_def)
```
```   951         moreover have " f ` D n \<inter> closure (f ` A n) = {}"
```
```   952         proof -
```
```   953           have op_fDn: "open(f ` (D n))"
```
```   954           proof (rule invariance_of_domain)
```
```   955             show "continuous_on (D n) f"
```
```   956               by (rule continuous_on_subset [OF contf D01])
```
```   957             show "open (D n)"
```
```   958               by (simp add: D_def)
```
```   959             show "inj_on f (D n)"
```
```   960               unfolding inj_on_def using D01 by (metis gf mem_ball_0 subsetCE)
```
```   961           qed
```
```   962           have injf: "inj_on f (ball 0 1)"
```
```   963             by (metis mem_ball_0 inj_on_def gf)
```
```   964           have "D n \<union> A n \<subseteq> ball 0 1"
```
```   965             using D01 A01 by simp
```
```   966           moreover have "D n \<inter> A n = {}"
```
```   967             by (auto simp: D_def A_def)
```
```   968           ultimately have "f ` D n \<inter> f ` A n = {}"
```
```   969             by (metis A01 D01 image_is_empty inj_on_image_Int injf)
```
```   970           then show ?thesis
```
```   971             by (simp add: open_Int_closure_eq_empty [OF op_fDn])
```
```   972         qed
```
```   973         ultimately show False
```
```   974           using x [of n] by blast
```
```   975       qed
```
```   976       ultimately
```
```   977       show "(\<Inter>n. X n) \<subseteq> closure S - S"
```
```   978         using closure_subset disjoint_iff_not_equal by blast
```
```   979     qed
```
```   980     ultimately have "closure S - S = (\<Inter>n. X n)" by blast
```
```   981     then have frontierS: "frontier S = (\<Inter>n. X n)"
```
```   982       by (simp add: frontier_def openS interior_open)
```
```   983     show ?thesis
```
```   984     proof (cases "bounded S")
```
```   985       case True
```
```   986       have bouX: "bounded (X n)" for n
```
```   987         apply (simp add: X_def)
```
```   988         apply (rule bounded_closure)
```
```   989         by (metis A01 fim image_mono bounded_subset [OF True])
```
```   990       have compaX: "compact (X n)" for n
```
```   991         apply (simp add: compact_eq_bounded_closed bouX)
```
```   992         apply (auto simp: X_def)
```
```   993         done
```
```   994       have "connected (\<Inter>n. X n)"
```
```   995         by (metis nestX compaX connX connected_nest)
```
```   996       then show ?thesis
```
```   997         by (simp add: True \<open>frontier S = (\<Inter>n. X n)\<close>)
```
```   998     next
```
```   999       case False
```
```  1000       have unboundedX: "\<not> bounded(X n)" for n
```
```  1001       proof
```
```  1002         assume bXn: "bounded(X n)"
```
```  1003         have "continuous_on (cball 0 (1 - 1 / (2 + real n))) f"
```
```  1004           by (simp add: cball_subset_ball_iff continuous_on_subset [OF contf])
```
```  1005         then have "bounded (f ` cball 0 (1 - 1 / (2 + real n)))"
```
```  1006           by (simp add: compact_imp_bounded [OF compact_continuous_image])
```
```  1007         moreover have "bounded (f ` A n)"
```
```  1008           by (auto simp: X_def closure_subset image_subset_iff bounded_subset [OF bXn])
```
```  1009         ultimately have "bounded (f ` (cball 0 (1 - 1/(2 + real n)) \<union> A n))"
```
```  1010           by (simp add: image_Un)
```
```  1011         then have "bounded (f ` ball 0 1)"
```
```  1012           apply (rule bounded_subset)
```
```  1013           apply (auto simp: A_def algebra_simps)
```
```  1014           done
```
```  1015         then show False
```
```  1016           using False by (simp add: fim [symmetric])
```
```  1017       qed
```
```  1018       have clo_INTX: "closed(\<Inter>(range X))"
```
```  1019         by (metis cloX closed_INT)
```
```  1020       then have lcX: "locally compact (\<Inter>(range X))"
```
```  1021         by (metis closed_imp_locally_compact)
```
```  1022       have False if C: "C \<in> components (frontier S)" and boC: "bounded C" for C
```
```  1023       proof -
```
```  1024         have "closed C"
```
```  1025           by (metis C closed_components frontier_closed)
```
```  1026         then have "compact C"
```
```  1027           by (metis boC compact_eq_bounded_closed)
```
```  1028         have Cco: "C \<in> components (\<Inter>(range X))"
```
```  1029           by (metis frontierS C)
```
```  1030         obtain K where "C \<subseteq> K" "compact K"
```
```  1031                    and Ksub: "K \<subseteq> \<Inter>(range X)" and clo: "closed(\<Inter>(range X) - K)"
```
```  1032         proof (cases "{k. C \<subseteq> k \<and> compact k \<and> openin (top_of_set (\<Inter>(range X))) k} = {}")
```
```  1033           case True
```
```  1034           then show ?thesis
```
```  1035             using Sura_Bura [OF lcX Cco \<open>compact C\<close>] boC
```
```  1036             by (simp add: True)
```
```  1037         next
```
```  1038           case False
```
```  1039           then obtain L where "compact L" "C \<subseteq> L" and K: "openin (top_of_set (\<Inter>x. X x)) L"
```
```  1040             by blast
```
```  1041           show ?thesis
```
```  1042           proof
```
```  1043             show "L \<subseteq> \<Inter>(range X)"
```
```  1044               by (metis K openin_imp_subset)
```
```  1045             show "closed (\<Inter>(range X) - L)"
```
```  1046               by (metis closedin_diff closedin_self closedin_closed_trans [OF _ clo_INTX] K)
```
```  1047           qed (use \<open>compact L\<close> \<open>C \<subseteq> L\<close> in auto)
```
```  1048         qed
```
```  1049         obtain U V where "open U" and "compact (closure U)" and "open V" "K \<subseteq> U"
```
```  1050                      and V: "\<Inter>(range X) - K \<subseteq> V" and "U \<inter> V = {}"
```
```  1051           using separation_normal_compact [OF \<open>compact K\<close> clo] by blast
```
```  1052         then have "U \<inter> (\<Inter> (range X) - K) = {}"
```
```  1053           by blast
```
```  1054         have "(closure U - U) \<inter> (\<Inter>n. X n \<inter> closure U) \<noteq> {}"
```
```  1055         proof (rule compact_imp_fip)
```
```  1056           show "compact (closure U - U)"
```
```  1057             by (metis \<open>compact (closure U)\<close> \<open>open U\<close> compact_diff)
```
```  1058           show "\<And>T. T \<in> range (\<lambda>n. X n \<inter> closure U) \<Longrightarrow> closed T"
```
```  1059             by clarify (metis cloX closed_Int closed_closure)
```
```  1060           show "(closure U - U) \<inter> \<Inter>\<F> \<noteq> {}"
```
```  1061             if "finite \<F>" and \<F>: "\<F> \<subseteq> range (\<lambda>n. X n \<inter> closure U)" for \<F>
```
```  1062           proof
```
```  1063             assume empty: "(closure U - U) \<inter> \<Inter>\<F> = {}"
```
```  1064             obtain J where "finite J" and J: "\<F> = (\<lambda>n. X n \<inter> closure U) ` J"
```
```  1065               using finite_subset_image [OF \<open>finite \<F>\<close> \<F>] by auto
```
```  1066             show False
```
```  1067             proof (cases "J = {}")
```
```  1068               case True
```
```  1069               with J empty have "closed U"
```
```  1070                 by (simp add: closure_subset_eq)
```
```  1071               have "C \<noteq> {}"
```
```  1072                 using C in_components_nonempty by blast
```
```  1073               then have "U \<noteq> {}"
```
```  1074                 using \<open>K \<subseteq> U\<close> \<open>C \<subseteq> K\<close> by blast
```
```  1075               moreover have "U \<noteq> UNIV"
```
```  1076                 using \<open>compact (closure U)\<close> by auto
```
```  1077               ultimately show False
```
```  1078                 using \<open>open U\<close> \<open>closed U\<close> clopen by blast
```
```  1079             next
```
```  1080               case False
```
```  1081               define j where "j \<equiv> Max J"
```
```  1082               have "j \<in> J"
```
```  1083                 by (simp add: False \<open>finite J\<close> j_def)
```
```  1084               have jmax: "\<And>m. m \<in> J \<Longrightarrow> m \<le> j"
```
```  1085                 by (simp add: j_def \<open>finite J\<close>)
```
```  1086               have "\<Inter> ((\<lambda>n. X n \<inter> closure U) ` J) = X j \<inter> closure U"
```
```  1087                 using False jmax nestX \<open>j \<in> J\<close> by auto
```
```  1088               then have "X j \<inter> closure U = X j \<inter> U"
```
```  1089                 apply safe
```
```  1090                 using DiffI J empty apply auto
```
```  1091                 using closure_subset by blast
```
```  1092               then have "openin (top_of_set (X j)) (X j \<inter> closure U)"
```
```  1093                 by (simp add: openin_open_Int \<open>open U\<close>)
```
```  1094               moreover have "closedin (top_of_set (X j)) (X j \<inter> closure U)"
```
```  1095                 by (simp add: closedin_closed_Int)
```
```  1096               moreover have "X j \<inter> closure U \<noteq> X j"
```
```  1097                 by (metis unboundedX \<open>compact (closure U)\<close> bounded_subset compact_eq_bounded_closed inf.order_iff)
```
```  1098               moreover have "X j \<inter> closure U \<noteq> {}"
```
```  1099               proof -
```
```  1100                 have "C \<noteq> {}"
```
```  1101                   using C in_components_nonempty by blast
```
```  1102                 moreover have "C \<subseteq> X j \<inter> closure U"
```
```  1103                   using \<open>C \<subseteq> K\<close> \<open>K \<subseteq> U\<close> Ksub closure_subset by blast
```
```  1104                 ultimately show ?thesis by blast
```
```  1105               qed
```
```  1106               ultimately show False
```
```  1107                 using connX [of j] by (force simp: connected_clopen)
```
```  1108             qed
```
```  1109           qed
```
```  1110         qed
```
```  1111         moreover have "(\<Inter>n. X n \<inter> closure U) = (\<Inter>n. X n) \<inter> closure U"
```
```  1112           by blast
```
```  1113         moreover have "x \<in> U" if "\<And>n. x \<in> X n" "x \<in> closure U" for x
```
```  1114         proof -
```
```  1115           have "x \<notin> V"
```
```  1116             using \<open>U \<inter> V = {}\<close> \<open>open V\<close> closure_iff_nhds_not_empty that(2) by blast
```
```  1117           then show ?thesis
```
```  1118             by (metis (no_types) Diff_iff INT_I V \<open>K \<subseteq> U\<close> contra_subsetD that(1))
```
```  1119         qed
```
```  1120         ultimately show False
```
```  1121           by (auto simp: open_Int_closure_eq_empty [OF \<open>open V\<close>, of U])
```
```  1122       qed
```
```  1123       then show ?thesis
```
```  1124         by (auto simp: False)
```
```  1125     qed
```
```  1126   qed
```
```  1127 qed
```
```  1128
```
```  1129
```
```  1130 lemma unbounded_complement_components:
```
```  1131   assumes C: "C \<in> components (- S)" and S: "connected S"
```
```  1132     and prev: "if bounded S then connected(frontier S)
```
```  1133                else \<forall>C \<in> components(frontier S). \<not> bounded C"
```
```  1134   shows "\<not> bounded C"
```
```  1135 proof (cases "bounded S")
```
```  1136   case True
```
```  1137   with prev have "S \<noteq> UNIV" and confr: "connected(frontier S)"
```
```  1138     by auto
```
```  1139   obtain w where C_ccsw: "C = connected_component_set (- S) w" and "w \<notin> S"
```
```  1140     using C by (auto simp: components_def)
```
```  1141   show ?thesis
```
```  1142   proof (cases "S = {}")
```
```  1143     case True with C show ?thesis by auto
```
```  1144   next
```
```  1145     case False
```
```  1146     show ?thesis
```
```  1147     proof
```
```  1148       assume "bounded C"
```
```  1149       then have "outside C \<noteq> {}"
```
```  1150         using outside_bounded_nonempty by metis
```
```  1151       then obtain z where z: "\<not> bounded (connected_component_set (- C) z)" and "z \<notin> C"
```
```  1152         by (auto simp: outside_def)
```
```  1153       have clo_ccs: "closed (connected_component_set (- S) x)" for x
```
```  1154         by (simp add: closed_Compl closed_connected_component openS)
```
```  1155       have "connected_component_set (- S) w = connected_component_set (- S) z"
```
```  1156       proof (rule joinable_connected_component_eq [OF confr])
```
```  1157         show "frontier S \<subseteq> - S"
```
```  1158           using openS by (auto simp: frontier_def interior_open)
```
```  1159         have False if "connected_component_set (- S) w \<inter> frontier (- S) = {}"
```
```  1160         proof -
```
```  1161           have "C \<inter> frontier S = {}"
```
```  1162             using that by (simp add: C_ccsw)
```
```  1163           then show False
```
```  1164             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)
```
```  1165         qed
```
```  1166         then show "connected_component_set (- S) w \<inter> frontier S \<noteq> {}"
```
```  1167           by auto
```
```  1168         have *: "\<lbrakk>frontier C \<subseteq> C; frontier C \<subseteq> F; frontier C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<inter> F \<noteq> {}" for C F::"complex set"
```
```  1169           by blast
```
```  1170         have "connected_component_set (- S) z \<inter> frontier (- S) \<noteq> {}"
```
```  1171         proof (rule *)
```
```  1172           show "frontier (connected_component_set (- S) z) \<subseteq> connected_component_set (- S) z"
```
```  1173             by (auto simp: closed_Compl closed_connected_component frontier_def openS)
```
```  1174           show "frontier (connected_component_set (- S) z) \<subseteq> frontier (- S)"
```
```  1175             using frontier_of_connected_component_subset by fastforce
```
```  1176           have "\<not> bounded (-S)"
```
```  1177             by (simp add: True cobounded_imp_unbounded)
```
```  1178           then have "connected_component_set (- S) z \<noteq> {}"
```
```  1179             apply (simp only: connected_component_eq_empty)
```
```  1180             using confr openS \<open>bounded C\<close> \<open>w \<notin> S\<close>
```
```  1181             apply (simp add: frontier_def interior_open C_ccsw)
```
```  1182             by (metis ComplI Compl_eq_Diff_UNIV connected_UNIV closed_closure closure_subset connected_component_eq_self
```
```  1183                       connected_diff_open_from_closed subset_UNIV)
```
```  1184           then show "frontier (connected_component_set (- S) z) \<noteq> {}"
```
```  1185             apply (simp add: frontier_eq_empty connected_component_eq_UNIV)
```
```  1186             apply (metis False compl_top_eq double_compl)
```
```  1187             done
```
```  1188         qed
```
```  1189         then show "connected_component_set (- S) z \<inter> frontier S \<noteq> {}"
```
```  1190           by auto
```
```  1191       qed
```
```  1192       then show False
```
```  1193         by (metis C_ccsw Compl_iff \<open>w \<notin> S\<close> \<open>z \<notin> C\<close> connected_component_eq_empty connected_component_idemp)
```
```  1194     qed
```
```  1195   qed
```
```  1196 next
```
```  1197   case False
```
```  1198   obtain w where C_ccsw: "C = connected_component_set (- S) w" and "w \<notin> S"
```
```  1199     using C by (auto simp: components_def)
```
```  1200   have "frontier (connected_component_set (- S) w) \<subseteq> connected_component_set (- S) w"
```
```  1201     by (simp add: closed_Compl closed_connected_component frontier_subset_eq openS)
```
```  1202   moreover have "frontier (connected_component_set (- S) w) \<subseteq> frontier S"
```
```  1203     using frontier_complement frontier_of_connected_component_subset by blast
```
```  1204   moreover have "frontier (connected_component_set (- S) w) \<noteq> {}"
```
```  1205     by (metis C C_ccsw False bounded_empty compl_top_eq connected_component_eq_UNIV double_compl frontier_not_empty in_components_nonempty)
```
```  1206   ultimately obtain z where zin: "z \<in> frontier S" and z: "z \<in> connected_component_set (- S) w"
```
```  1207     by blast
```
```  1208   have *: "connected_component_set (frontier S) z \<in> components(frontier S)"
```
```  1209     by (simp add: \<open>z \<in> frontier S\<close> componentsI)
```
```  1210   with prev False have "\<not> bounded (connected_component_set (frontier S) z)"
```
```  1211     by simp
```
```  1212   moreover have "connected_component (- S) w = connected_component (- S) z"
```
```  1213     using connected_component_eq [OF z] by force
```
```  1214   ultimately show ?thesis
```
```  1215     by (metis C_ccsw * zin bounded_subset closed_Compl closure_closed connected_component_maximal
```
```  1216               connected_component_refl connected_connected_component frontier_closures in_components_subset le_inf_iff mem_Collect_eq openS)
```
```  1217 qed
```
```  1218
```
```  1219 lemma empty_inside:
```
```  1220   assumes "connected S" "\<And>C. C \<in> components (- S) \<Longrightarrow> \<not> bounded C"
```
```  1221   shows "inside S = {}"
```
```  1222   using assms by (auto simp: components_def inside_def)
```
```  1223
```
```  1224 lemma empty_inside_imp_simply_connected:
```
```  1225   "\<lbrakk>connected S; inside S = {}\<rbrakk> \<Longrightarrow> simply_connected S"
```
```  1226   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)
```
```  1227
```
```  1228 end
```
```  1229
```
```  1230 proposition
```
```  1231   fixes S :: "complex set"
```
```  1232   assumes "open S"
```
```  1233   shows simply_connected_eq_frontier_properties:
```
```  1234          "simply_connected S \<longleftrightarrow>
```
```  1235           connected S \<and>
```
```  1236              (if bounded S then connected(frontier S)
```
```  1237              else (\<forall>C \<in> components(frontier S). \<not>bounded C))" (is "?fp")
```
```  1238     and simply_connected_eq_unbounded_complement_components:
```
```  1239          "simply_connected S \<longleftrightarrow>
```
```  1240           connected S \<and> (\<forall>C \<in> components(- S). \<not>bounded C)" (is "?ucc")
```
```  1241     and simply_connected_eq_empty_inside:
```
```  1242          "simply_connected S \<longleftrightarrow>
```
```  1243           connected S \<and> inside S = {}" (is "?ei")
```
```  1244 proof -
```
```  1245   interpret SC_Chain
```
```  1246     using assms by (simp add: SC_Chain_def)
```
```  1247   have "?fp \<and> ?ucc \<and> ?ei"
```
```  1248 proof -
```
```  1249   have *: "\<lbrakk>\<alpha> \<Longrightarrow> \<beta>; \<beta> \<Longrightarrow> \<gamma>; \<gamma> \<Longrightarrow> \<delta>; \<delta> \<Longrightarrow> \<alpha>\<rbrakk>
```
```  1250            \<Longrightarrow> (\<alpha> \<longleftrightarrow> \<beta>) \<and> (\<alpha> \<longleftrightarrow> \<gamma>) \<and> (\<alpha> \<longleftrightarrow> \<delta>)" for \<alpha> \<beta> \<gamma> \<delta>
```
```  1251     by blast
```
```  1252   show ?thesis
```
```  1253     apply (rule *)
```
```  1254     using frontier_properties simply_connected_imp_connected apply blast
```
```  1255 apply clarify
```
```  1256     using unbounded_complement_components simply_connected_imp_connected apply blast
```
```  1257     using empty_inside apply blast
```
```  1258     using empty_inside_imp_simply_connected apply blast
```
```  1259     done
```
```  1260 qed
```
```  1261   then show ?fp ?ucc ?ei
```
```  1262     by safe
```
```  1263 qed
```
```  1264
```
```  1265 lemma simply_connected_iff_simple:
```
```  1266   fixes S :: "complex set"
```
```  1267   assumes "open S" "bounded S"
```
```  1268   shows "simply_connected S \<longleftrightarrow> connected S \<and> connected(- S)"
```
```  1269   apply (simp add: simply_connected_eq_unbounded_complement_components assms, safe)
```
```  1270    apply (metis DIM_complex assms(2) cobounded_has_bounded_component double_compl order_refl)
```
```  1271   by (meson assms inside_bounded_complement_connected_empty simply_connected_eq_empty_inside simply_connected_eq_unbounded_complement_components)
```
```  1272
```
```  1273 subsection\<open>Further equivalences based on continuous logs and sqrts\<close>
```
```  1274
```
```  1275 context SC_Chain
```
```  1276 begin
```
```  1277
```
```  1278 lemma continuous_log:
```
```  1279   fixes f :: "complex\<Rightarrow>complex"
```
```  1280   assumes S: "simply_connected S"
```
```  1281     and contf: "continuous_on S f" and nz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
```
```  1282   shows "\<exists>g. continuous_on S g \<and> (\<forall>z \<in> S. f z = exp(g z))"
```
```  1283 proof -
```
```  1284   consider "S = {}" | "S homeomorphic ball (0::complex) 1"
```
```  1285     using simply_connected_eq_homeomorphic_to_disc [OF openS] S by metis
```
```  1286   then show ?thesis
```
```  1287   proof cases
```
```  1288     case 1 then show ?thesis
```
```  1289       by simp
```
```  1290   next
```
```  1291     case 2
```
```  1292     then obtain h k :: "complex\<Rightarrow>complex"
```
```  1293       where kh: "\<And>x. x \<in> S \<Longrightarrow> k(h x) = x" and him: "h ` S = ball 0 1"
```
```  1294       and conth: "continuous_on S h"
```
```  1295       and hk: "\<And>y. y \<in> ball 0 1 \<Longrightarrow> h(k y) = y" and kim: "k ` ball 0 1 = S"
```
```  1296       and contk: "continuous_on (ball 0 1) k"
```
```  1297       unfolding homeomorphism_def homeomorphic_def by metis
```
```  1298     obtain g where contg: "continuous_on (ball 0 1) g"
```
```  1299              and expg: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> (f \<circ> k) z = exp (g z)"
```
```  1300     proof (rule continuous_logarithm_on_ball)
```
```  1301       show "continuous_on (ball 0 1) (f \<circ> k)"
```
```  1302         apply (rule continuous_on_compose [OF contk])
```
```  1303         using kim continuous_on_subset [OF contf]
```
```  1304         by blast
```
```  1305       show "\<And>z. z \<in> ball 0 1 \<Longrightarrow> (f \<circ> k) z \<noteq> 0"
```
```  1306         using kim nz by auto
```
```  1307     qed auto
```
```  1308     then show ?thesis
```
```  1309       by (metis comp_apply conth continuous_on_compose him imageI kh)
```
```  1310   qed
```
```  1311 qed
```
```  1312
```
```  1313 lemma continuous_sqrt:
```
```  1314   fixes f :: "complex\<Rightarrow>complex"
```
```  1315   assumes contf: "continuous_on S f" and nz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
```
```  1316   and prev: "\<And>f::complex\<Rightarrow>complex.
```
```  1317                 \<lbrakk>continuous_on S f; \<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0\<rbrakk>
```
```  1318                   \<Longrightarrow> \<exists>g. continuous_on S g \<and> (\<forall>z \<in> S. f z = exp(g z))"
```
```  1319   shows "\<exists>g. continuous_on S g \<and> (\<forall>z \<in> S. f z = (g z)\<^sup>2)"
```
```  1320 proof -
```
```  1321   obtain g where contg: "continuous_on S g" and geq: "\<And>z. z \<in> S \<Longrightarrow> f z = exp(g z)"
```
```  1322     using contf nz prev by metis
```
```  1323   show ?thesis
```
```  1324 proof (intro exI ballI conjI)
```
```  1325   show "continuous_on S (\<lambda>z. exp(g z/2))"
```
```  1326       by (intro continuous_intros) (auto simp: contg)
```
```  1327     show "\<And>z. z \<in> S \<Longrightarrow> f z = (exp (g z/2))\<^sup>2"
```
```  1328       by (metis (no_types, lifting) divide_inverse exp_double geq mult.left_commute mult.right_neutral right_inverse zero_neq_numeral)
```
```  1329   qed
```
```  1330 qed
```
```  1331
```
```  1332 lemma continuous_sqrt_imp_simply_connected:
```
```  1333   assumes "connected S"
```
```  1334     and prev: "\<And>f::complex\<Rightarrow>complex. \<lbrakk>continuous_on S f; \<forall>z \<in> S. f z \<noteq> 0\<rbrakk>
```
```  1335                 \<Longrightarrow> \<exists>g. continuous_on S g \<and> (\<forall>z \<in> S. f z = (g z)\<^sup>2)"
```
```  1336   shows "simply_connected S"
```
```  1337 proof (clarsimp simp add: simply_connected_eq_holomorphic_sqrt [OF openS] \<open>connected S\<close>)
```
```  1338   fix f
```
```  1339   assume "f holomorphic_on S" and nz: "\<forall>z\<in>S. f z \<noteq> 0"
```
```  1340   then obtain g where contg: "continuous_on S g" and geq: "\<And>z. z \<in> S \<Longrightarrow> f z = (g z)\<^sup>2"
```
```  1341     by (metis holomorphic_on_imp_continuous_on prev)
```
```  1342   show "\<exists>g. g holomorphic_on S \<and> (\<forall>z\<in>S. f z = (g z)\<^sup>2)"
```
```  1343   proof (intro exI ballI conjI)
```
```  1344     show "g holomorphic_on S"
```
```  1345     proof (clarsimp simp add: holomorphic_on_open [OF openS])
```
```  1346       fix z
```
```  1347       assume "z \<in> S"
```
```  1348       with nz geq have "g z \<noteq> 0"
```
```  1349         by auto
```
```  1350       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)"
```
```  1351         using contg [unfolded continuous_on_iff] by (metis \<open>g z \<noteq> 0\<close> \<open>z \<in> S\<close> zero_less_norm_iff)
```
```  1352       then have \<delta>: "\<And>w. \<lbrakk>w \<in> S; w \<in> ball z \<delta>\<rbrakk> \<Longrightarrow> g w + g z \<noteq> 0"
```
```  1353         apply (clarsimp simp: dist_norm)
```
```  1354         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)
```
```  1355       have *: "(\<lambda>x. (f x - f z) / (x - z) / (g x + g z)) \<midarrow>z\<rightarrow> deriv f z / (g z + g z)"
```
```  1356         apply (intro tendsto_intros)
```
```  1357         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
```
```  1358         using \<open>z \<in> S\<close> contg continuous_on_eq_continuous_at isCont_def openS apply blast
```
```  1359         by (simp add: \<open>g z \<noteq> 0\<close>)
```
```  1360       then have "(g has_field_derivative deriv f z / (g z + g z)) (at z)"
```
```  1361         unfolding has_field_derivative_iff
```
```  1362       proof (rule Lim_transform_within_open)
```
```  1363         show "open (ball z \<delta> \<inter> S)"
```
```  1364           by (simp add: openS open_Int)
```
```  1365         show "z \<in> ball z \<delta> \<inter> S"
```
```  1366           using \<open>z \<in> S\<close> \<open>0 < \<delta>\<close> by simp
```
```  1367         show "\<And>x. \<lbrakk>x \<in> ball z \<delta> \<inter> S; x \<noteq> z\<rbrakk>
```
```  1368                   \<Longrightarrow> (f x - f z) / (x - z) / (g x + g z) = (g x - g z) / (x - z)"
```
```  1369           using \<delta>
```
```  1370           apply (simp add: geq \<open>z \<in> S\<close> divide_simps)
```
```  1371           apply (auto simp: algebra_simps power2_eq_square)
```
```  1372           done
```
```  1373       qed
```
```  1374       then show "\<exists>f'. (g has_field_derivative f') (at z)" ..
```
```  1375     qed
```
```  1376   qed (use geq in auto)
```
```  1377 qed
```
```  1378
```
```  1379 end
```
```  1380
```
```  1381 proposition
```
```  1382   fixes S :: "complex set"
```
```  1383   assumes "open S"
```
```  1384   shows simply_connected_eq_continuous_log:
```
```  1385          "simply_connected S \<longleftrightarrow>
```
```  1386           connected S \<and>
```
```  1387           (\<forall>f::complex\<Rightarrow>complex. continuous_on S f \<and> (\<forall>z \<in> S. f z \<noteq> 0)
```
```  1388             \<longrightarrow> (\<exists>g. continuous_on S g \<and> (\<forall>z \<in> S. f z = exp (g z))))" (is "?log")
```
```  1389     and simply_connected_eq_continuous_sqrt:
```
```  1390          "simply_connected S \<longleftrightarrow>
```
```  1391           connected S \<and>
```
```  1392           (\<forall>f::complex\<Rightarrow>complex. continuous_on S f \<and> (\<forall>z \<in> S. f z \<noteq> 0)
```
```  1393             \<longrightarrow> (\<exists>g. continuous_on S g \<and> (\<forall>z \<in> S. f z = (g z)\<^sup>2)))" (is "?sqrt")
```
```  1394 proof -
```
```  1395   interpret SC_Chain
```
```  1396     using assms by (simp add: SC_Chain_def)
```
```  1397   have "?log \<and> ?sqrt"
```
```  1398 proof -
```
```  1399   have *: "\<lbrakk>\<alpha> \<Longrightarrow> \<beta>; \<beta> \<Longrightarrow> \<gamma>; \<gamma> \<Longrightarrow> \<alpha>\<rbrakk>
```
```  1400            \<Longrightarrow> (\<alpha> \<longleftrightarrow> \<beta>) \<and> (\<alpha> \<longleftrightarrow> \<gamma>)" for \<alpha> \<beta> \<gamma>
```
```  1401     by blast
```
```  1402   show ?thesis
```
```  1403     apply (rule *)
```
```  1404     apply (simp add: local.continuous_log winding_number_zero)
```
```  1405     apply (simp add: continuous_sqrt)
```
```  1406     apply (simp add: continuous_sqrt_imp_simply_connected)
```
```  1407     done
```
```  1408 qed
```
```  1409   then show ?log ?sqrt
```
```  1410     by safe
```
```  1411 qed
```
```  1412
```
```  1413
```
```  1414 subsection%unimportant \<open>More Borsukian results\<close>
```
```  1415
```
```  1416 lemma Borsukian_componentwise_eq:
```
```  1417   fixes S :: "'a::euclidean_space set"
```
```  1418   assumes S: "locally connected S \<or> compact S"
```
```  1419   shows "Borsukian S \<longleftrightarrow> (\<forall>C \<in> components S. Borsukian C)"
```
```  1420 proof -
```
```  1421   have *: "ANR(-{0::complex})"
```
```  1422     by (simp add: ANR_delete open_Compl open_imp_ANR)
```
```  1423   show ?thesis
```
```  1424     using cohomotopically_trivial_on_components [OF assms *] by (auto simp: Borsukian_alt)
```
```  1425 qed
```
```  1426
```
```  1427 lemma Borsukian_componentwise:
```
```  1428   fixes S :: "'a::euclidean_space set"
```
```  1429   assumes "locally connected S \<or> compact S" "\<And>C. C \<in> components S \<Longrightarrow> Borsukian C"
```
```  1430   shows "Borsukian S"
```
```  1431   by (metis Borsukian_componentwise_eq assms)
```
```  1432
```
```  1433 lemma simply_connected_eq_Borsukian:
```
```  1434   fixes S :: "complex set"
```
```  1435   shows "open S \<Longrightarrow> (simply_connected S \<longleftrightarrow> connected S \<and> Borsukian S)"
```
```  1436   by (auto simp: simply_connected_eq_continuous_log Borsukian_continuous_logarithm)
```
```  1437
```
```  1438 lemma Borsukian_eq_simply_connected:
```
```  1439   fixes S :: "complex set"
```
```  1440   shows "open S \<Longrightarrow> Borsukian S \<longleftrightarrow> (\<forall>C \<in> components S. simply_connected C)"
```
```  1441 apply (auto simp: Borsukian_componentwise_eq open_imp_locally_connected)
```
```  1442   using in_components_connected open_components simply_connected_eq_Borsukian apply blast
```
```  1443   using open_components simply_connected_eq_Borsukian by blast
```
```  1444
```
```  1445 lemma Borsukian_separation_open_closed:
```
```  1446   fixes S :: "complex set"
```
```  1447   assumes S: "open S \<or> closed S" and "bounded S"
```
```  1448   shows "Borsukian S \<longleftrightarrow> connected(- S)"
```
```  1449   using S
```
```  1450 proof
```
```  1451   assume "open S"
```
```  1452   show ?thesis
```
```  1453     unfolding Borsukian_eq_simply_connected [OF \<open>open S\<close>]
```
```  1454     by (meson \<open>open S\<close> \<open>bounded S\<close> bounded_subset in_components_connected in_components_subset nonseparation_by_component_eq open_components simply_connected_iff_simple)
```
```  1455 next
```
```  1456   assume "closed S"
```
```  1457   with \<open>bounded S\<close> show ?thesis
```
```  1458     by (simp add: Borsukian_separation_compact compact_eq_bounded_closed)
```
```  1459 qed
```
```  1460
```
```  1461
```
```  1462 subsection\<open>Finally, the Riemann Mapping Theorem\<close>
```
```  1463
```
```  1464 theorem Riemann_mapping_theorem:
```
```  1465     "open S \<and> simply_connected S \<longleftrightarrow>
```
```  1466      S = {} \<or> S = UNIV \<or>
```
```  1467      (\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
```
```  1468            (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
```
```  1469            (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z))"
```
```  1470     (is "_ = ?rhs")
```
```  1471 proof -
```
```  1472   have "simply_connected S \<longleftrightarrow> ?rhs" if "open S"
```
```  1473     by (simp add: simply_connected_eq_biholomorphic_to_disc that)
```
```  1474   moreover have "open S" if "?rhs"
```
```  1475   proof -
```
```  1476     { fix f g
```
```  1477       assume g: "g holomorphic_on ball 0 1" "\<forall>z\<in>ball 0 1. g z \<in> S \<and> f (g z) = z"
```
```  1478         and "\<forall>z\<in>S. cmod (f z) < 1 \<and> g (f z) = z"
```
```  1479       then have "S = g ` (ball 0 1)"
```
```  1480         by (force simp:)
```
```  1481       then have "open S"
```
```  1482         by (metis open_ball g inj_on_def open_mapping_thm3)
```
```  1483     }
```
```  1484     with that show "open S" by auto
```
```  1485   qed
```
```  1486   ultimately show ?thesis by metis
```
```  1487 qed
```
```  1488
```
```  1489 end
```