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