Quelle Riemann_Mapping.thy Sprache: Isabelle

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

section \<open>Moebius functions, Equivalents of Simply Connected Sets, Riemann Mapping Theorem\<close>

theory Riemann_Mapping
imports Great_Picard
begin

subsection\<open>Moebius functions are biholomorphisms of the unit disc\<close>

definition\<^marker>\<open>tag important\<close> Moebius_function :: "[real,complex,complex] \<Rightarrow> complex" where
  "Moebius_function \ \t w z. exp(\ * of_real t) * (z - w) / (1 - cnj w * z)"

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

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

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

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

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

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

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

subsection\<open>A big chain of equivalents of simple connectedness for an open set\<close>

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

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

lemma winding_number_zero:
  assumes "simply_connected S"
  shows "connected S \
         (\<forall>\<gamma> z. path \<gamma> \<and> path_image \<gamma> \<subseteq> S \<and>
                   pathfinish \<gamma> = pathstart \<gamma> \<and> z \<notin> S \<longrightarrow> winding_number \<gamma> z = 0)"
  using assms
  by (auto simp: simply_connected_imp_connected simply_connected_imp_winding_number_zero)

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

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

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

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

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

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

lemma homeomorphic_to_disc:
  assumes "S = UNIV \
               (\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
                      (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
                      (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z))" (is "_ \<or> ?P")
  shows "S homeomorphic ball (0::complex) 1"
  by (smt (verit, ccfv_SIG) holomorphic_on_imp_continuous_on homeomorphic_ball01_UNIV
      homeomorphic_minimal assms)

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

end

proposition
  assumes "open S"
  shows simply_connected_eq_winding_number_zero:
         "simply_connected S \
           connected S \<and>
           (\<forall>g z. path g \<and> path_image g \<subseteq> S \<and>
                 pathfinish g = pathstart g \<and> (z \<notin> S)
                 \<longrightarrow> winding_number g z = 0)" (is "?wn0")
    and simply_connected_eq_contour_integral_zero:
         "simply_connected S \
           connected S \<and>
           (\<forall>g f. valid_path g \<and> path_image g \<subseteq> S \<and>
                 pathfinish g = pathstart g \<and> f holomorphic_on S
               \<longrightarrow> (f has_contour_integral 0) g)" (is "?ci0")
    and simply_connected_eq_global_primitive:
         "simply_connected S \
           connected S \<and>
           (\<forall>f. f holomorphic_on S \<longrightarrow>
                (\<exists>h. \<forall>z. z \<in> S \<longrightarrow> (h has_field_derivative f z) (at z)))" (is "?gp")
    and simply_connected_eq_holomorphic_log:
         "simply_connected S \
           connected S \<and>
           (\<forall>f. f holomorphic_on S \<and> (\<forall>z \<in> S. f z \<noteq> 0)
               \<longrightarrow> (\<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S. f z = exp(g z))))" (is "?log")
    and simply_connected_eq_holomorphic_sqrt:
         "simply_connected S \
           connected S \<and>
           (\<forall>f. f holomorphic_on S \<and> (\<forall>z \<in> S. f z \<noteq> 0)
                \<longrightarrow> (\<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S.  f z = (g z)\<^sup>2)))" (is "?sqrt")
    and simply_connected_eq_biholomorphic_to_disc:
         "simply_connected S \
           S = {} \<or> S = UNIV \<or>
           (\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
                 (\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
                 (\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z))" (is "?bih")
    and simply_connected_eq_homeomorphic_to_disc:
          "simply_connected S \ S = {} \ S homeomorphic ball (0::complex) 1" (is "?disc")
proof -
  interpret SC_Chain
    using assms by (simp add: SC_Chain_def)
  have "?wn0 \ ?ci0 \ ?gp \ ?log \ ?sqrt \ ?bih \ ?disc"
proof -
  have *: "\\ \ \; \ \ \; \ \ \; \ \ \; \ \ \; \ \ \; \ \ \; \ \ \\
        \<Longrightarrow> (\<alpha> \<longleftrightarrow> \<beta>) \<and> (\<alpha> \<longleftrightarrow> \<gamma>) \<and> (\<alpha> \<longleftrightarrow> \<delta>) \<and> (\<alpha> \<longleftrightarrow> \<zeta>) \<and>
            (\<alpha> \<longleftrightarrow> \<eta>) \<and> (\<alpha> \<longleftrightarrow> \<theta>) \<and> (\<alpha> \<longleftrightarrow> \<xi>)" for \<alpha> \<beta> \<gamma> \<delta> \<zeta> \<eta> \<theta> \<xi>
    by blast
  show ?thesis
    apply (rule *)
    using winding_number_zero apply metis
    using contour_integral_zero apply metis
    using global_primitive apply metis
    using holomorphic_log apply metis
    using holomorphic_sqrt apply simp
    using biholomorphic_to_disc apply blast
    using homeomorphic_to_disc apply blast
    using homeomorphic_to_disc_imp_simply_connected apply blast
    done
qed
  then show ?wn0 ?ci0 ?gp ?log ?sqrt ?bih ?disc
    by safe
qed

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

subsection\<open>A further chain of equivalences about components of the complement of a simply connected set\<close>

text\<open>(following 1.35 in Burckel'S book)\<close>

context SC_Chain
begin

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

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

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

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

end

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

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

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

subsection\<open>Further equivalences based on continuous logs and sqrts\<close>

context SC_Chain
begin

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

lemma continuous_sqrt:
  fixes f :: "complex\complex"
  assumes contf: "continuous_on S f" and nz: "\z. z \ S \ f z \ 0"
    and prev: "\f::complex\complex.
                \<lbrakk>continuous_on S f; \<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0\<rbrakk>
                  \<Longrightarrow> \<exists>g. continuous_on S g \<and> (\<forall>z \<in> S. f z = exp(g z))"
  shows "\g. continuous_on S g \ (\z \ S. f z = (g z)\<^sup>2)"
proof -
  obtain g where contg: "continuous_on S g" and geq: "\z. z \ S \ f z = exp(g z)"
    using contf nz prev by metis
  show ?thesis
  proof (intro exI ballI conjI)
    show "continuous_on S (\z. exp(g z/2))"
      by (intro continuous_intros) (auto simp: contg)
    show "\z. z \ S \ f z = (exp (g z/2))\<^sup>2"
      by (metis (no_types, lifting) divide_inverse exp_double geq mult.left_commute mult.right_neutral right_inverse zero_neq_numeral)
  qed
qed

lemma continuous_sqrt_imp_simply_connected:
  assumes "connected S"
    and prev: "\f::complex\complex. \continuous_on S f; \z \ S. f z \ 0\
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.