src/HOL/Analysis/Riemann_Mapping.thy
 author paulson Mon Oct 30 17:20:56 2017 +0000 (21 months ago) changeset 66941 c67bb79a0ceb parent 66827 c94531b5007d child 67399 eab6ce8368fa permissions -rw-r--r--
More topological results overlooked last time
 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 \Moebius functions, Equivalents of Simply Connected Sets, Riemann Mapping Theorem\ ``` lp15@66826 ` 6` lp15@66826 ` 7` ```theory Riemann_Mapping ``` lp15@66826 ` 8` ```imports Great_Picard ``` lp15@66826 ` 9` ```begin ``` lp15@66826 ` 10` lp15@66826 ` 11` ```subsection\Moebius functions are biholomorphisms of the unit disc.\ ``` lp15@66826 ` 12` lp15@66826 ` 13` ```definition Moebius_function :: "[real,complex,complex] \ complex" where ``` lp15@66826 ` 14` ``` "Moebius_function \ \t w z. exp(\ * 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(\ * 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 \ 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 \ 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 \1 - cnj w * z \ 0\ 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 \ 0" if "norm z < 1" for z ``` lp15@66826 ` 59` ``` proof - ``` lp15@66826 ` 60` ``` have "norm (1::complex) \ 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) \cmod w2 < 1\ 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 \ 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 \ ball 0 1" ``` lp15@66826 ` 97` ``` "g holomorphic_on ball 0 1" "g ` ball 0 1 \ ball 0 1" ``` lp15@66826 ` 98` ``` "\z. z \ ball 0 1 \ f (g z) = z" ``` lp15@66826 ` 99` ``` "\z. z \ ball 0 1 \ 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 \ ball 0 1" ``` lp15@66826 ` 106` ``` "Moebius_function 0 (- a) ` ball 0 1 \ 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 \ 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\A big chain of equivalents of simple connectedness for an open set\ ``` lp15@66826 ` 115` lp15@66826 ` 116` ```lemma biholomorphic_to_disc_aux: ``` lp15@66826 ` 117` ``` assumes "open S" "connected S" "0 \ S" and S01: "S \ ball 0 1" ``` lp15@66826 ` 118` ``` and prev: "\f. \f holomorphic_on S; \z. z \ S \ f z \ 0; inj_on f S\ ``` lp15@66826 ` 119` ``` \ \g. g holomorphic_on S \ (\z \ S. f z = (g z)\<^sup>2)" ``` lp15@66826 ` 120` ``` shows "\f g. f holomorphic_on S \ g holomorphic_on ball 0 1 \ ``` lp15@66826 ` 121` ``` (\z \ S. f z \ ball 0 1 \ g(f z) = z) \ ``` lp15@66826 ` 122` ``` (\z \ ball 0 1. g z \ S \ f(g z) = z)" ``` lp15@66826 ` 123` ```proof - ``` lp15@66826 ` 124` ``` define F where "F \ {h. h holomorphic_on S \ h ` S \ ball 0 1 \ h 0 = 0 \ inj_on h S}" ``` lp15@66826 ` 125` ``` have idF: "id \ F" ``` lp15@66826 ` 126` ``` using S01 by (auto simp: F_def) ``` lp15@66826 ` 127` ``` then have "F \ {}" ``` lp15@66826 ` 128` ``` by blast ``` lp15@66826 ` 129` ``` have imF_ne: "((\h. norm(deriv h 0)) ` F) \ {}" ``` lp15@66826 ` 130` ``` using idF by auto ``` lp15@66826 ` 131` ``` have holF: "\h. h \ F \ h holomorphic_on S" ``` lp15@66826 ` 132` ``` by (auto simp: F_def) ``` lp15@66826 ` 133` ``` obtain f where "f \ F" and normf: "\h. h \ F \ norm(deriv h 0) \ norm(deriv f 0)" ``` lp15@66826 ` 134` ``` proof - ``` lp15@66826 ` 135` ``` obtain r where "r > 0" and r: "ball 0 r \ S" ``` lp15@66826 ` 136` ``` using \open S\ \0 \ S\ openE by auto ``` lp15@66826 ` 137` ``` have bdd: "bdd_above ((\h. norm(deriv h 0)) ` F)" ``` lp15@66826 ` 138` ``` proof (intro bdd_aboveI exI ballI, clarify) ``` lp15@66826 ` 139` ``` show "norm (deriv f 0) \ 1 / r" if "f \ F" for f ``` lp15@66826 ` 140` ``` proof - ``` lp15@66826 ` 141` ``` have r01: "op * (complex_of_real r) ` ball 0 1 \ S" ``` lp15@66826 ` 142` ``` using that \r > 0\ by (auto simp: norm_mult r [THEN subsetD]) ``` lp15@66826 ` 143` ``` then have "f holomorphic_on op * (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 \ (\z. (r * z)) holomorphic_on (ball 0 1)" ``` lp15@66826 ` 146` ``` by (intro holomorphic_intros holomorphic_on_compose) ``` lp15@66826 ` 147` ``` have f0: "(f \ op * (complex_of_real r)) 0 = 0" ``` lp15@66826 ` 148` ``` using F_def that by auto ``` lp15@66826 ` 149` ``` have "f ` S \ ball 0 1" ``` lp15@66826 ` 150` ``` using F_def that by blast ``` lp15@66826 ` 151` ``` with r01 have fr1: "\z. norm z < 1 \ norm ((f \ op*(of_real r))z) < 1" ``` lp15@66826 ` 152` ``` by force ``` lp15@66826 ` 153` ``` have *: "((\w. f (r * w)) has_field_derivative deriv f (r * z) * r) (at z)" ``` lp15@66826 ` 154` ``` if "z \ 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 S\]) ``` lp15@66826 ` 158` ``` apply (rule \f \ F\) ``` lp15@66826 ` 159` ``` by (meson imageI r01 subset_iff that) ``` lp15@66826 ` 160` ``` qed simp ``` lp15@66826 ` 161` ``` have df0: "((\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 (\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 ``` lp15@66826 ` 165` ``` have "norm (deriv (f \ op * (complex_of_real r)) 0) \ 1" ``` lp15@66826 ` 166` ``` by (auto intro: Schwarz_Lemma [OF holf f0 fr1, of 0]) ``` lp15@66826 ` 167` ``` with \r > 0\ 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 \ SUP h:F. norm (deriv h 0)" ``` lp15@66826 ` 172` ``` have eql: "norm (deriv f 0) = l" if le: "l \ norm (deriv f 0)" and "f \ F" for f ``` lp15@66826 ` 173` ``` apply (rule order_antisym [OF _ le]) ``` lp15@66826 ` 174` ``` using \f \ F\ bdd cSUP_upper by (fastforce simp: l_def) ``` lp15@66826 ` 175` ``` obtain \ where \in: "\n. \ n \ F" and \lim: "(\n. norm (deriv (\ n) 0)) \ l" ``` lp15@66826 ` 176` ``` proof - ``` lp15@66826 ` 177` ``` have "\f. f \ F \ \norm (deriv f 0) - l\ < 1 / (Suc n)" for n ``` lp15@66826 ` 178` ``` proof - ``` lp15@66826 ` 179` ``` obtain f where "f \ 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 "\norm (deriv f 0) - l\ < 1 / (Suc n)" ``` lp15@66826 ` 182` ``` by (fastforce simp add: abs_if not_less eql) ``` lp15@66826 ` 183` ``` with \f \ F\ show ?thesis ``` lp15@66826 ` 184` ``` by blast ``` lp15@66826 ` 185` ``` qed ``` lp15@66826 ` 186` ``` then obtain \ where fF: "\n. (\ n) \ F" ``` lp15@66826 ` 187` ``` and fless: "\n. \norm (deriv (\ n) 0) - l\ < 1 / (Suc n)" ``` lp15@66826 ` 188` ``` by metis ``` lp15@66826 ` 189` ``` have "(\n. norm (deriv (\ n) 0)) \ 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 "\N. \n\N. dist (norm (deriv (\ n) 0)) l < e" ``` lp15@66826 ` 196` ``` proof (intro exI allI impI) ``` lp15@66826 ` 197` ``` fix n assume "N \ n" ``` lp15@66826 ` 198` ``` have "dist (norm (deriv (\ 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 \N \ n\ inverse_of_nat_le le_less_trans by blast ``` lp15@66826 ` 202` ``` finally show "dist (norm (deriv (\ 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 "\K. \compact K; K \ S\ \ \B. \h\F. \z\K. norm (h z) \ B" ``` lp15@66826 ` 209` ``` by (rule_tac x=1 in exI) (force simp: F_def) ``` lp15@66826 ` 210` ``` moreover have "range \ \ F" ``` lp15@66826 ` 211` ``` using \\n. \ n \ F\ by blast ``` lp15@66826 ` 212` ``` ultimately obtain f and r :: "nat \ nat" ``` lp15@66826 ` 213` ``` where holf: "f holomorphic_on S" and r: "strict_mono r" ``` lp15@66826 ` 214` ``` and limf: "\x. x \ S \ (\n. \ (r n) x) \ f x" ``` lp15@66826 ` 215` ``` and ulimf: "\K. \compact K; K \ S\ \ uniform_limit K (\ \ r) f sequentially" ``` lp15@66826 ` 216` ``` using Montel [of S F \, OF \open S\ holF] by auto+ ``` lp15@66826 ` 217` ``` have der: "\n x. x \ S \ ((\ \ r) n has_field_derivative ((\n. deriv (\ n)) \ r) n x) (at x)" ``` lp15@66826 ` 218` ``` using \\n. \ n \ F\ \open S\ holF holomorphic_derivI by fastforce ``` lp15@66826 ` 219` ``` have ulim: "\x. x \ S \ \d>0. cball x d \ S \ uniform_limit (cball x d) (\ \ r) f sequentially" ``` lp15@66826 ` 220` ``` by (meson ulimf \open S\ compact_cball open_contains_cball) ``` lp15@66826 ` 221` ``` obtain f' :: "complex\complex" where f': "(f has_field_derivative f' 0) (at 0)" ``` lp15@66826 ` 222` ``` and tof'0: "(\n. ((\n. deriv (\ n)) \ r) n 0) \ f' 0" ``` lp15@66826 ` 223` ``` using has_complex_derivative_uniform_sequence [OF \open S\ der ulim] \0 \ S\ 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 "(\x. (norm (deriv (\ (r x)) 0))) \ 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 \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: "\ f constant_on S" ``` lp15@66826 ` 233` ``` proof - ``` lp15@66826 ` 234` ``` have False if "\x. x \ S \ f x = c" for c ``` lp15@66826 ` 235` ``` proof - ``` lp15@66826 ` 236` ``` have "deriv f 0 = 0" ``` lp15@66826 ` 237` ``` by (metis that \open S\ \0 \ S\ 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 \ F" ``` lp15@66826 ` 248` ``` unfolding F_def ``` lp15@66826 ` 249` ``` proof (intro CollectI conjI holf) ``` lp15@66826 ` 250` ``` have "norm(f z) \ 1" if "z \ 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 "\ (r n) \ F" ``` lp15@66826 ` 254` ``` by (simp add: \in) ``` lp15@66826 ` 255` ``` then show "norm (\ (r n) z) \ 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 \ S" for z ``` lp15@66826 ` 259` ``` using maximum_modulus_principle [OF holf \open S\ \connected S\ \open S\] nonconstf that ``` lp15@66826 ` 260` ``` by fastforce ``` lp15@66826 ` 261` ``` then show "f ` S \ ball 0 1" ``` lp15@66826 ` 262` ``` by auto ``` lp15@66826 ` 263` ``` have "(\n. \ (r n) 0) \ 0" ``` lp15@66826 ` 264` ``` using \in by (auto simp: F_def) ``` lp15@66826 ` 265` ``` then show "f 0 = 0" ``` lp15@66826 ` 266` ``` using tendsto_unique [OF _ limf ] \0 \ S\ trivial_limit_sequentially by blast ``` lp15@66826 ` 267` ``` show "inj_on f S" ``` lp15@66826 ` 268` ``` proof (rule Hurwitz_injective [OF \open S\ \connected S\ _ holf]) ``` lp15@66826 ` 269` ``` show "\n. (\ \ r) n holomorphic_on S" ``` lp15@66826 ` 270` ``` by (simp add: \in holF) ``` lp15@66826 ` 271` ``` show "\K. \compact K; K \ S\ \ uniform_limit K(\ \ r) f sequentially" ``` lp15@66826 ` 272` ``` by (metis ulimf) ``` lp15@66826 ` 273` ``` show "\ f constant_on S" ``` lp15@66826 ` 274` ``` using nonconstf by auto ``` lp15@66826 ` 275` ``` show "\n. inj_on ((\ \ r) n) S" ``` lp15@66826 ` 276` ``` using \in by (auto simp: F_def) ``` lp15@66826 ` 277` ``` qed ``` lp15@66826 ` 278` ``` qed ``` lp15@66826 ` 279` ``` show "\h. h \ F \ norm (deriv h 0) \ 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 \ ball 0 1" ``` lp15@66826 ` 284` ``` using \f \ F\ by (auto simp: F_def) ``` lp15@66826 ` 285` ``` obtain g where holg: "g holomorphic_on (f ` S)" ``` lp15@66826 ` 286` ``` and derg: "\z. z \ S \ deriv f z * deriv g (f z) = 1" ``` lp15@66826 ` 287` ``` and gf: "\z. z \ S \ g(f z) = z" ``` lp15@66826 ` 288` ``` using holomorphic_has_inverse [OF holf \open S\ injf] by metis ``` lp15@66826 ` 289` ``` have "ball 0 1 \ f ` S" ``` lp15@66826 ` 290` ``` proof ``` lp15@66826 ` 291` ``` fix a::complex ``` lp15@66826 ` 292` ``` assume a: "a \ ball 0 1" ``` lp15@66826 ` 293` ``` have False if "\x. x \ S \ f x \ 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 \ ball 0 1" ``` lp15@66826 ` 297` ``` and holk: "k holomorphic_on ball 0 1" and k01: "k ` ball 0 1 \ ball 0 1" ``` lp15@66826 ` 298` ``` and hk: "\z. z \ ball 0 1 \ h (k z) = z" ``` lp15@66826 ` 299` ``` and kh: "\z. z \ ball 0 1 \ k (h z) = z" ``` lp15@66826 ` 300` ``` using ball_biholomorphism_exists [OF a] by blast ``` lp15@66826 ` 301` ``` have nf1: "\z. z \ S \ norm(f z) < 1" ``` lp15@66826 ` 302` ``` using \f \ F\ by (auto simp: F_def) ``` lp15@66826 ` 303` ``` have 1: "h \ f holomorphic_on S" ``` lp15@66826 ` 304` ``` using F_def \f \ F\ holh holomorphic_on_compose holomorphic_on_subset by blast ``` lp15@66826 ` 305` ``` have 2: "\z. z \ S \ (h \ f) z \ 0" ``` lp15@66826 ` 306` ``` by (metis \h a = 0\ a comp_eq_dest_lhs nf1 kh mem_ball_0 that) ``` lp15@66826 ` 307` ``` have 3: "inj_on (h \ f) S" ``` lp15@66826 ` 308` ``` by (metis (no_types, lifting) F_def \f \ F\ comp_inj_on inj_on_inverseI injf kh mem_Collect_eq subset_inj_on) ``` lp15@66826 ` 309` ``` obtain \ where hol\: "\ holomorphic_on ((h \ f) ` S)" ``` lp15@66826 ` 310` ``` and \2: "\z. z \ S \ \(h (f z)) ^ 2 = h(f z)" ``` lp15@66826 ` 311` ``` proof (rule exE [OF prev [OF 1 2 3]], safe) ``` lp15@66826 ` 312` ``` fix \ ``` lp15@66826 ` 313` ``` assume hol\: "\ holomorphic_on S" and \2: "(\z\S. (h \ f) z = (\ z)\<^sup>2)" ``` lp15@66826 ` 314` ``` show thesis ``` lp15@66826 ` 315` ``` proof ``` lp15@66826 ` 316` ``` show "(\ \ g \ k) holomorphic_on (h \ f) ` S" ``` lp15@66826 ` 317` ``` proof (intro holomorphic_on_compose) ``` lp15@66826 ` 318` ``` show "k holomorphic_on (h \ 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 \ f) ` S" ``` lp15@66826 ` 322` ``` apply (rule holomorphic_on_subset [OF holg]) ``` lp15@66826 ` 323` ``` by (auto simp: kh nf1) ``` lp15@66826 ` 324` ``` show "\ holomorphic_on g ` k ` (h \ f) ` S" ``` lp15@66826 ` 325` ``` apply (rule holomorphic_on_subset [OF hol\]) ``` lp15@66826 ` 326` ``` by (auto simp: gf kh nf1) ``` lp15@66826 ` 327` ``` qed ``` lp15@66826 ` 328` ``` show "((\ \ g \ k) (h (f z)))\<^sup>2 = h (f z)" if "z \ S" for z ``` lp15@66826 ` 329` ``` proof - ``` lp15@66826 ` 330` ``` have "f z \ ball 0 1" ``` lp15@66826 ` 331` ``` by (simp add: nf1 that) ``` lp15@66826 ` 332` ``` then have "(\ (g (k (h (f z)))))\<^sup>2 = (\ (g (f z)))\<^sup>2" ``` lp15@66826 ` 333` ``` by (metis kh) ``` lp15@66826 ` 334` ``` also have "... = h (f z)" ``` lp15@66826 ` 335` ``` using \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\1: "norm(\ (h (f z))) < 1" if "z \ S" for z ``` lp15@66826 ` 342` ``` proof - ``` lp15@66826 ` 343` ``` have "norm (\ (h (f z)) ^ 2) < 1" ``` lp15@66826 ` 344` ``` by (metis (no_types) that DIM_complex \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 \01: "\ (h (f 0)) \ ball 0 1" ``` lp15@66826 ` 349` ``` by (simp add: \0 \ S\) ``` lp15@66826 ` 350` ``` obtain p q where p0: "p (\ (h (f 0))) = 0" ``` lp15@66826 ` 351` ``` and holp: "p holomorphic_on ball 0 1" and p01: "p ` ball 0 1 \ ball 0 1" ``` lp15@66826 ` 352` ``` and holq: "q holomorphic_on ball 0 1" and q01: "q ` ball 0 1 \ ball 0 1" ``` lp15@66826 ` 353` ``` and pq: "\z. z \ ball 0 1 \ p (q z) = z" ``` lp15@66826 ` 354` ``` and qp: "\z. z \ ball 0 1 \ q (p z) = z" ``` lp15@66826 ` 355` ``` using ball_biholomorphism_exists [OF \01] by metis ``` lp15@66826 ` 356` ``` have "p \ \ \ h \ f \ F" ``` lp15@66826 ` 357` ``` unfolding F_def ``` lp15@66826 ` 358` ``` proof (intro CollectI conjI holf) ``` lp15@66826 ` 359` ``` show "p \ \ \ h \ 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 "\ holomorphic_on h ` f ` S" ``` lp15@66826 ` 365` ``` apply (rule holomorphic_on_subset [OF hol\]) ``` lp15@66826 ` 366` ``` by auto ``` lp15@66826 ` 367` ``` show "p holomorphic_on \ ` h ` f ` S" ``` lp15@66826 ` 368` ``` apply (rule holomorphic_on_subset [OF holp]) ``` lp15@66826 ` 369` ``` by (auto simp: norm\1) ``` lp15@66826 ` 370` ``` qed ``` lp15@66826 ` 371` ``` show "(p \ \ \ h \ f) ` S \ ball 0 1" ``` lp15@66826 ` 372` ``` apply clarsimp ``` lp15@66826 ` 373` ``` by (meson norm\1 p01 image_subset_iff mem_ball_0) ``` lp15@66826 ` 374` ``` show "(p \ \ \ h \ f) 0 = 0" ``` lp15@66826 ` 375` ``` by (simp add: \p (\ (h (f 0))) = 0\) ``` lp15@66826 ` 376` ``` show "inj_on (p \ \ \ h \ f) S" ``` lp15@66826 ` 377` ``` unfolding inj_on_def o_def ``` lp15@66826 ` 378` ``` by (metis \2 dist_0_norm gf kh mem_ball nf1 norm\1 qp) ``` lp15@66826 ` 379` ``` qed ``` lp15@66826 ` 380` ``` then have le_norm_df0: "norm (deriv (p \ \ \ h \ f) 0) \ norm (deriv f 0)" ``` lp15@66826 ` 381` ``` by (rule normf) ``` lp15@66826 ` 382` ``` have 1: "k \ power2 \ 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 \ power2 \ q) 0 = 0" ``` lp15@66826 ` 392` ``` using p0 F_def \f \ F\ \01 \2 \0 \ S\ kh qp by force ``` lp15@66826 ` 393` ``` have 3: "norm ((k \ power2 \ q) z) < 1" if "norm z < 1" for z ``` lp15@66826 ` 394` ``` proof - ``` lp15@66826 ` 395` ``` have "norm ((power2 \ 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: "\z. norm z < 1 \ (k \ power2 \ q) z = c * z" and "norm c = 1" for c ``` lp15@66826 ` 401` ``` proof - ``` lp15@66826 ` 402` ``` have "c \ 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 \ power2 \ q) (p(1/2)) = c * p(1/2)" "(k \ power2 \ 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: \c \ 0\ 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 \ power2 \ q) 0) \ 1" "norm (deriv (k \ power2 \ q) 0) \ 1" ``` lp15@66826 ` 418` ``` and le: "\\. norm \ < 1 \ norm ((k \ power2 \ q) \) \ norm \" ``` lp15@66826 ` 419` ``` proof - ``` lp15@66826 ` 420` ``` have "norm (deriv (k \ power2 \ q) 0) < 1" ``` lp15@66826 ` 421` ``` using that by simp ``` lp15@66826 ` 422` ``` moreover have eq: "deriv f 0 = deriv (k \ (\z. z ^ 2) \ q) 0 * deriv (p \ \ \ h \ f) 0" ``` lp15@66826 ` 423` ``` proof (intro DERIV_imp_deriv DERIV_transform_within_open [OF DERIV_chain]) ``` lp15@66826 ` 424` ``` show "(k \ power2 \ q has_field_derivative deriv (k \ power2 \ q) 0) (at ((p \ \ \ h \ f) 0))" ``` lp15@66826 ` 425` ``` using "1" holomorphic_derivI p0 by auto ``` lp15@66826 ` 426` ``` show "(p \ \ \ h \ f has_field_derivative deriv (p \ \ \ h \ f) 0) (at 0)" ``` lp15@66826 ` 427` ``` using \p \ \ \ h \ f \ F\ \open S\ \0 \ S\ holF holomorphic_derivI by blast ``` lp15@66826 ` 428` ``` show "\x. x \ S \ (k \ power2 \ q \ (p \ \ \ h \ f)) x = f x" ``` lp15@66826 ` 429` ``` using \2 f01 kh norm\1 qp by auto ``` lp15@66826 ` 430` ``` qed (use assms in simp_all) ``` lp15@66826 ` 431` ``` ultimately have "cmod (deriv (p \ \ \ h \ f) 0) \ 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 \ 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 \ 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 \f \ F\ 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 \ ``` lp15@66826 ` 462` ``` (\\ z. path \ \ path_image \ \ S \ ``` lp15@66826 ` 463` ``` pathfinish \ = pathstart \ \ z \ S \ winding_number \ 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 \ S" "pathfinish g = pathstart g" "f holomorphic_on S" ``` lp15@66826 ` 469` ``` "\\ z. \path \; path_image \ \ S; pathfinish \ = pathstart \; z \ S\ \ winding_number \ 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: "\\ f. \valid_path \; path_image \ \ S; pathfinish \ = pathstart \; f holomorphic_on S\ \ (f has_contour_integral 0) \" ``` lp15@66826 ` 476` ``` shows "\h. \z \ 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 \ 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 \ S" ``` lp15@66826 ` 487` ``` then obtain d where "d > 0" and d: "cball x d \ S" ``` lp15@66826 ` 488` ``` using openS open_contains_cball_eq by blast ``` lp15@66826 ` 489` ``` let ?g = "\z. (SOME g. polynomial_function g \ path_image g \ S \ pathstart g = a \ pathfinish g = z)" ``` lp15@66826 ` 490` ``` show "((\z. contour_integral (?g z) f) has_field_derivative f x) ``` lp15@66826 ` 491` ``` (at x)" ``` lp15@66826 ` 492` ``` proof (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right, rule Lim_transform) ``` lp15@66826 ` 493` ``` show "(\y. inverse(norm(y - x)) *\<^sub>R (contour_integral(linepath x y) f - f x * (y - x))) \x\ 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 \x \ S\ 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: "\x'. dist x' x < d1 \ 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 \ S" ``` lp15@66826 ` 503` ``` using openS \x \ S\ 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 \ 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 \ 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 \ 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: "((\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)) \ (e/2) * norm (y - x)" ``` lp15@66826 ` 521` ``` proof (rule has_contour_integral_bound_linepath) ``` lp15@66826 ` 522` ``` show "((\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 "\w. w \ closed_segment x y \ norm (f w - f x) \ 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 \e > 0\ in auto) ``` lp15@66826 ` 527` ``` with \e > 0\ have "inverse (norm (y - x)) * norm (z - f x * (y - x)) \ e/2" ``` lp15@66826 ` 528` ``` by (simp add: divide_simps) ``` lp15@66826 ` 529` ``` also have "... < e" ``` lp15@66826 ` 530` ``` using \e > 0\ 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 \d1 > 0\ \d2 > 0\ ``` lp15@66826 ` 535` ``` show "\d>0. \z. z \ x \ dist z x < d \ ``` 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 \ x" and yx: "dist y x < d" for y ``` lp15@66826 ` 544` ``` proof - ``` lp15@66826 ` 545` ``` have "y \ 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) \ path_image (?g x) \ S \ pathstart (?g x) = a \ pathfinish (?g x) = x" ``` lp15@66826 ` 548` ``` "polynomial_function (?g y) \ path_image (?g y) \ S \ pathstart (?g y) = a \ pathfinish (?g y) = y" ``` lp15@66826 ` 549` ``` using someI_ex [OF connected_open_polynomial_connected [OF openS \connected S\ \a \ S\]] \x \ S\ \y \ S\ ``` 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 \ 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 \ S" ``` lp15@66826 ` 560` ``` using d by blast ``` lp15@66826 ` 561` ``` then show "path_image ((?g x) +++ linepath x y +++ reversepath (?g y)) \ 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 "(\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` ``` \x\ 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 \d > 0\ * 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: "\z. z \ S \ f z \ 0" ``` lp15@66826 ` 589` ``` and prev: "\f. f holomorphic_on S \ \h. \z \ S. (h has_field_derivative f z) (at z)" ``` lp15@66826 ` 590` ``` shows "\g. g holomorphic_on S \ (\z \ S. f z = exp(g z))" ``` lp15@66826 ` 591` ```proof - ``` lp15@66826 ` 592` ``` have "(\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: "\z. z \ S \ (g has_field_derivative deriv f z / f z) (at z)" ``` lp15@66826 ` 595` ``` using prev [of "\z. deriv f z / f z"] by metis ``` lp15@66826 ` 596` ``` have hfd: "\x. x \ S \ ((\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: "\x. x \ S \ exp (g x) / f x = c" ``` lp15@66826 ` 602` ``` proof (rule DERIV_zero_connected_constant[OF \connected S\ openS finite.emptyI]) ``` lp15@66826 ` 603` ``` show "continuous_on S (\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 "\x\S - {}. ((\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 \connected S\ openS finite.emptyI, of "\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 "(\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 \ 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 \ 0" ``` lp15@66826 ` 618` ``` using \z \ S\ 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: "\z. z \ S \ f z \ 0" ``` lp15@66826 ` 626` ``` and prev: "\f. \f holomorphic_on S; \z \ S. f z \ 0\ \ \g. g holomorphic_on S \ (\z \ S. f z = exp(g z))" ``` lp15@66826 ` 627` ``` shows "\g. g holomorphic_on S \ (\z \ S. f z = (g z)\<^sup>2)" ``` lp15@66826 ` 628` ```proof - ``` lp15@66826 ` 629` ``` obtain g where holg: "g holomorphic_on S" and g: "\z. z \ S \ 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 "(\z. exp(g z/2)) holomorphic_on S" ``` lp15@66826 ` 634` ``` by (intro holomorphic_intros) (auto simp: holg) ``` lp15@66826 ` 635` ``` show "\z. z \ S \ 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 \ {}" "S \ UNIV" ``` lp15@66826 ` 642` ``` 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)" ``` lp15@66826 ` 643` ``` shows "\f g. f holomorphic_on S \ g holomorphic_on ball 0 1 \ ``` lp15@66826 ` 644` ``` (\z \ S. f z \ ball 0 1 \ g(f z) = z) \ ``` lp15@66826 ` 645` ``` (\z \ ball 0 1. g z \ S \ f(g z) = z)" ``` lp15@66826 ` 646` ```proof - ``` lp15@66826 ` 647` ``` obtain a b where "a \ S" "b \ S" ``` lp15@66826 ` 648` ``` using S by blast ``` lp15@66826 ` 649` ``` then obtain \ where "\ > 0" and \: "ball a \ \ S" ``` lp15@66826 ` 650` ``` using openS openE by blast ``` lp15@66826 ` 651` ``` obtain g where holg: "g holomorphic_on S" and eqg: "\z. z \ S \ z - b = (g z)\<^sup>2" ``` lp15@66826 ` 652` ``` proof (rule exE [OF prev [of "\z. z - b"]]) ``` lp15@66826 ` 653` ``` show "(\z. z - b) holomorphic_on S" ``` lp15@66826 ` 654` ``` by (intro holomorphic_intros) ``` lp15@66826 ` 655` ``` qed (use \b \ S\ in auto) ``` lp15@66826 ` 656` ``` have "\ g constant_on S" ``` lp15@66826 ` 657` ``` proof - ``` lp15@66826 ` 658` ``` have "(a + \/2) \ ball a \" "a + (\/2) \ a" ``` lp15@66826 ` 659` ``` using \\ > 0\ 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 + \/2"] \a \ S\ \ ``` lp15@66826 ` 663` ``` by (metis diff_add_cancel subset_eq) ``` lp15@66826 ` 664` ``` qed ``` lp15@66826 ` 665` ``` then have "open (g ` ball a \)" ``` lp15@66826 ` 666` ``` using open_mapping_thm [of g S "ball a \", OF holg openS \connected S\] \ by blast ``` lp15@66826 ` 667` ``` then obtain r where "r > 0" and r: "ball (g a) r \ (g ` ball a \)" ``` lp15@66826 ` 668` ``` by (metis \0 < \\ centre_in_ball imageI openE) ``` lp15@66826 ` 669` ``` have g_not_r: "g z \ ball (-(g a)) r" if "z \ S" for z ``` lp15@66826 ` 670` ``` proof ``` lp15@66826 ` 671` ``` assume "g z \ ball (-(g a)) r" ``` lp15@66826 ` 672` ``` then have "- g z \ ball (g a) r" ``` lp15@66826 ` 673` ``` by (metis add.inverse_inverse dist_minus mem_ball) ``` lp15@66826 ` 674` ``` with r have "- g z \ (g ` ball a \)" ``` lp15@66826 ` 675` ``` by blast ``` lp15@66826 ` 676` ``` then obtain w where w: "- g z = g w" "dist a w < \" ``` lp15@66826 ` 677` ``` by auto ``` lp15@66826 ` 678` ``` then have "w \ ball a \" ``` lp15@66826 ` 679` ``` by simp ``` lp15@66826 ` 680` ``` then have "w \ S" ``` lp15@66826 ` 681` ``` using \ 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 \- g z = g w\ by auto ``` lp15@66826 ` 686` ``` with eqg [OF that] have "z = b" ``` lp15@66826 ` 687` ``` by auto ``` lp15@66826 ` 688` ``` with that \b \ S\ show False ``` lp15@66826 ` 689` ``` by simp ``` lp15@66826 ` 690` ``` qed ``` lp15@66826 ` 691` ``` then have nz: "\z. z \ S \ g z + g a \ 0" ``` lp15@66826 ` 692` ``` by (metis \0 < r\ add.commute add_diff_cancel_left' centre_in_ball diff_0) ``` lp15@66826 ` 693` ``` let ?f = "\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 \ 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: "\norm x \ 1/3; norm y \ 1/3\ \ 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 \ S" for z ``` lp15@66826 ` 701` ``` apply (rule 3) ``` lp15@66826 ` 702` ``` unfolding norm_divide ``` lp15@66826 ` 703` ``` using \r > 0\ g_not_r [OF \z \ S\] g_not_r [OF \a \ S\] ``` lp15@66826 ` 704` ``` by (simp_all add: divide_simps dist_commute dist_norm) ``` lp15@66826 ` 705` ``` then show "?f ` S \ ball 0 1" ``` lp15@66826 ` 706` ``` by auto ``` lp15@66826 ` 707` ``` show "inj_on ?f S" ``` lp15@66826 ` 708` ``` using \r > 0\ 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: "\z. z \ S \ deriv h z * deriv k (h z) = 1" ``` lp15@66826 ` 713` ``` and kh: "\z. z \ S \ k(h z) = z" ``` lp15@66826 ` 714` ``` using holomorphic_has_inverse [OF holh openS \inj_on h S\] by metis ``` lp15@66826 ` 715` lp15@66826 ` 716` ``` have 1: "open (h ` S)" ``` lp15@66826 ` 717` ``` by (simp add: \inj_on h S\ holh openS open_mapping_thm3) ``` lp15@66826 ` 718` ``` have 2: "connected (h ` S)" ``` lp15@66826 ` 719` ``` by (simp add: connected_continuous_image \connected S\ holh holomorphic_on_imp_continuous_on) ``` lp15@66826 ` 720` ``` have 3: "0 \ h ` S" ``` lp15@66826 ` 721` ``` using \a \ S\ \h a = 0\ by auto ``` lp15@66826 ` 722` ``` have 4: "\g. g holomorphic_on h ` S \ (\z\h ` S. f z = (g z)\<^sup>2)" ``` lp15@66826 ` 723` ``` if holf: "f holomorphic_on h ` S" and nz: "\z. z \ h ` S \ f z \ 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: "\z. z \ S \ (f \ h) z = (g z)\<^sup>2" ``` lp15@66826 ` 726` ``` proof - ``` lp15@66826 ` 727` ``` have "f \ h holomorphic_on S" ``` lp15@66826 ` 728` ``` by (simp add: holh holomorphic_on_compose holf) ``` lp15@66826 ` 729` ``` moreover have "\z\S. (f \ h) z \ 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 \ k holomorphic_on h ` S" ``` lp15@66826 ` 737` ``` proof - ``` lp15@66826 ` 738` ``` have "k ` h ` S \ S" ``` lp15@66826 ` 739` ``` by (simp add: \\z. z \ S \ k (h z) = z\ 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 "\z\h ` S. f z = ((g \ 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: "\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" ``` 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 \ h holomorphic_on S" ``` lp15@66826 ` 753` ``` by (simp add: f holh holomorphic_on_compose) ``` lp15@66826 ` 754` ``` show "k \ 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 \ {}" ``` lp15@66826 ` 761` ``` and prev: "S = UNIV \ ``` lp15@66826 ` 762` ``` (\f g. f holomorphic_on S \ g holomorphic_on ball 0 1 \ ``` lp15@66826 ` 763` ``` (\z \ S. f z \ ball 0 1 \ g(f z) = z) \ ``` lp15@66826 ` 764` ``` (\z \ ball 0 1. g z \ S \ f(g z) = z))" (is "_ \ ?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 = {} \ 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 \ ``` lp15@66826 ` 789` ``` connected S \ ``` lp15@66826 ` 790` ``` (\g z. path g \ path_image g \ S \ ``` lp15@66826 ` 791` ``` pathfinish g = pathstart g \ (z \ S) ``` lp15@66826 ` 792` ``` \ winding_number g z = 0)" (is "?wn0") ``` lp15@66826 ` 793` ``` and simply_connected_eq_contour_integral_zero: ``` lp15@66826 ` 794` ``` "simply_connected S \ ``` lp15@66826 ` 795` ``` connected S \ ``` lp15@66826 ` 796` ``` (\g f. valid_path g \ path_image g \ S \ ``` lp15@66826 ` 797` ``` pathfinish g = pathstart g \ f holomorphic_on S ``` lp15@66826 ` 798` ``` \ (f has_contour_integral 0) g)" (is "?ci0") ``` lp15@66826 ` 799` ``` and simply_connected_eq_global_primitive: ``` lp15@66826 ` 800` ``` "simply_connected S \ ``` lp15@66826 ` 801` ``` connected S \ ``` lp15@66826 ` 802` ``` (\f. f holomorphic_on S \ ``` lp15@66826 ` 803` ``` (\h. \z. z \ S \ (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 \ ``` lp15@66826 ` 806` ``` connected S \ ``` lp15@66826 ` 807` ``` (\f. f holomorphic_on S \ (\z \ S. f z \ 0) ``` lp15@66826 ` 808` ``` \ (\g. g holomorphic_on S \ (\z \ S. f z = exp(g z))))" (is "?log") ``` lp15@66826 ` 809` ``` and simply_connected_eq_holomorphic_sqrt: ``` lp15@66826 ` 810` ``` "simply_connected S \ ``` lp15@66826 ` 811` ``` connected S \ ``` lp15@66826 ` 812` ``` (\f. f holomorphic_on S \ (\z \ S. f z \ 0) ``` lp15@66826 ` 813` ``` \ (\g. g holomorphic_on S \ (\z \ 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 \ ``` lp15@66826 ` 816` ``` S = {} \ S = UNIV \ ``` lp15@66826 ` 817` ``` (\f g. f holomorphic_on S \ g holomorphic_on ball 0 1 \ ``` lp15@66826 ` 818` ``` (\z \ S. f z \ ball 0 1 \ g(f z) = z) \ ``` lp15@66826 ` 819` ``` (\z \ ball 0 1. g z \ S \ f(g z) = z))" (is "?bih") ``` lp15@66826 ` 820` ``` and simply_connected_eq_homeomorphic_to_disc: ``` lp15@66826 ` 821` ``` "simply_connected S \ S = {} \ 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 \ ?ci0 \ ?gp \ ?log \ ?sqrt \ ?bih \ ?disc" ``` lp15@66826 ` 826` ```proof - ``` lp15@66826 ` 827` ``` have *: "\\ \ \; \ \ \; \ \ \; \ \ \; \ \ \; \ \ \; \ \ \; \ \ \\ ``` lp15@66826 ` 828` ``` \ (\ \ \) \ (\ \ \) \ (\ \ \) \ (\ \ \) \ ``` lp15@66826 ` 829` ``` (\ \ \) \ (\ \ \) \ (\ \ \)" for \ \ \ \ \ \ \ \ ``` 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 \ (contractible S \ 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` lp15@66826 ` 856` ```subsection\A further chain of equivalences about components of the complement of a simply connected set.\ ``` lp15@66826 ` 857` lp15@66826 ` 858` ```text\(following 1.35 in Burckel'S book)\ ``` 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 \C \ components(frontier S). ~bounded C" ``` lp15@66826 ` 867` ```proof - ``` lp15@66826 ` 868` ``` have "S = {} \ 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 \S = {}\ 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: "\x. x \ S \ f(g x) = x" ``` lp15@66826 ` 881` ``` and fim: "f ` ball 0 1 = S" and gf: "\y. cmod y < 1 \ 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 \ \n. ball (0::complex) (1 - 1/(of_nat n + 2))" ``` lp15@66826 ` 885` ``` define A where "A \ \n. {z::complex. 1 - 1/(of_nat n + 2) < norm z \ norm z < 1}" ``` lp15@66826 ` 886` ``` define X where "X \ \n::nat. closure(f ` A n)" ``` lp15@66826 ` 887` ``` have D01: "D n \ ball 0 1" for n ``` lp15@66826 ` 888` ``` by (simp add: D_def ball_subset_ball_iff) ``` lp15@66826 ` 889` ``` have A01: "A n \ 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 \ 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 \ X m" if "m \ n" for m n ``` lp15@66826 ` 902` ``` proof - ``` lp15@66826 ` 903` ``` have "1 - 1 / (real m + 2) \ 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 \ (\n. X n)" ``` lp15@66826 ` 909` ``` proof ``` lp15@66826 ` 910` ``` fix x ``` lp15@66826 ` 911` ``` assume "x \ closure S - S" ``` lp15@66826 ` 912` ``` then have "x \ closure S" "x \ S" by auto ``` lp15@66826 ` 913` ``` show "x \ (\n. X n)" ``` lp15@66826 ` 914` ``` proof ``` lp15@66826 ` 915` ``` fix n ``` lp15@66826 ` 916` ``` have "ball 0 1 = closure (D n) \ 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)) \ 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))) \ S" ``` lp15@66826 ` 927` ``` by (force simp: D_def Seq) ``` lp15@66826 ` 928` ``` show "x \ X n" ``` lp15@66826 ` 929` ``` using \x \ closure S\ unfolding X_def Seq ``` lp15@66826 ` 930` ``` using \x \ S\ * D_def clo_fim by auto ``` lp15@66826 ` 931` ``` qed ``` lp15@66826 ` 932` ``` qed ``` lp15@66826 ` 933` ``` moreover have "(\n. X n) \ closure S - S" ``` lp15@66826 ` 934` ``` proof - ``` lp15@66826 ` 935` ``` have "(\n. X n) \ closure S" ``` lp15@66826 ` 936` ``` proof - ``` lp15@66826 ` 937` ``` have "(\n. X n) \ X 0" ``` lp15@66826 ` 938` ``` by blast ``` lp15@66826 ` 939` ``` also have "... \ 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 "(\n. X n) \ closure S" . ``` lp15@66826 ` 944` ``` qed ``` lp15@66826 ` 945` ``` moreover have "(\n. X n) \ S \ {}" ``` lp15@66826 ` 946` ``` proof (clarify, clarsimp simp: X_def fim [symmetric]) ``` lp15@66826 ` 947` ``` fix x assume x [rule_format]: "\n. f x \ 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 \cmod x < 1\ 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 \ f ` (D n)" ``` lp15@66826 ` 953` ``` using n \cmod x < 1\ by (auto simp: divide_simps algebra_simps D_def) ``` lp15@66826 ` 954` ``` moreover have " f ` D n \ 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 \ A n \ ball 0 1" ``` lp15@66826 ` 968` ``` using D01 A01 by simp ``` lp15@66826 ` 969` ``` moreover have "D n \ A n = {}" ``` lp15@66826 ` 970` ``` by (auto simp: D_def A_def) ``` lp15@66826 ` 971` ``` ultimately have "f ` D n \ 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 "(\n. X n) \ 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 = (\n. X n)" by blast ``` lp15@66826 ` 984` ``` then have frontierS: "frontier S = (\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 (\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 \frontier S = (\n. X n)\) ``` lp15@66826 ` 1001` ``` next ``` lp15@66826 ` 1002` ``` case False ``` lp15@66826 ` 1003` ``` have unboundedX: "\ 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)) \ 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(\(range X))" ``` lp15@66826 ` 1022` ``` by (metis cloX closed_INT) ``` lp15@66826 ` 1023` ``` then have lcX: "locally compact (\(range X))" ``` lp15@66826 ` 1024` ``` by (metis closed_imp_locally_compact) ``` lp15@66826 ` 1025` ``` have False if C: "C \ 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 \ components (\(range X))" ``` lp15@66826 ` 1032` ``` by (metis frontierS C) ``` lp15@66826 ` 1033` ``` obtain K where "C \ K" "compact K" ``` lp15@66826 ` 1034` ``` and Ksub: "K \ \(range X)" and clo: "closed(\(range X) - K)" ``` lp15@66826 ` 1035` ``` proof (cases "{k. C \ k \ compact k \ openin (subtopology euclidean (\(range X))) k} = {}") ``` lp15@66826 ` 1036` ``` case True ``` lp15@66826 ` 1037` ``` then show ?thesis ``` lp15@66826 ` 1038` ``` using Sura_Bura [OF lcX Cco \compact C\] 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 \ L" and K: "openin (subtopology euclidean (\x. X x)) L" ``` lp15@66826 ` 1043` ``` by blast ``` lp15@66826 ` 1044` ``` show ?thesis ``` lp15@66826 ` 1045` ``` proof ``` lp15@66826 ` 1046` ``` show "L \ \(range X)" ``` lp15@66826 ` 1047` ``` by (metis K openin_imp_subset) ``` lp15@66826 ` 1048` ``` show "closed (\(range X) - L)" ``` lp15@66826 ` 1049` ``` by (metis closedin_diff closedin_self closedin_closed_trans [OF _ clo_INTX] K) ``` lp15@66826 ` 1050` ``` qed (use \compact L\ \C \ L\ in auto) ``` lp15@66826 ` 1051` ``` qed ``` lp15@66826 ` 1052` ``` obtain U V where "open U" and "compact (closure U)" and "open V" "K \ U" ``` lp15@66826 ` 1053` ``` and V: "\(range X) - K \ V" and "U \ V = {}" ``` lp15@66826 ` 1054` ``` using separation_normal_compact [OF \compact K\ clo] by blast ``` lp15@66826 ` 1055` ``` then have "U \ (\ (range X) - K) = {}" ``` lp15@66826 ` 1056` ``` by blast ``` lp15@66826 ` 1057` ``` have "(closure U - U) \ (\n. X n \ closure U) \ {}" ``` lp15@66826 ` 1058` ``` proof (rule compact_imp_fip) ``` lp15@66826 ` 1059` ``` show "compact (closure U - U)" ``` lp15@66826 ` 1060` ``` by (metis \compact (closure U)\ \open U\ compact_diff) ``` lp15@66826 ` 1061` ``` show "\T. T \ range (\n. X n \ closure U) \ closed T" ``` lp15@66826 ` 1062` ``` by clarify (metis cloX closed_Int closed_closure) ``` lp15@66826 ` 1063` ``` show "(closure U - U) \ \\ \ {}" ``` lp15@66826 ` 1064` ``` if "finite \" and \: "\ \ range (\n. X n \ closure U)" for \ ``` lp15@66826 ` 1065` ``` proof ``` lp15@66826 ` 1066` ``` assume empty: "(closure U - U) \ \\ = {}" ``` lp15@66826 ` 1067` ``` obtain J where "finite J" and J: "\ = (\n. X n \ closure U) ` J" ``` lp15@66826 ` 1068` ``` using finite_subset_image [OF \finite \\ \] 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 \ {}" ``` lp15@66826 ` 1075` ``` using C in_components_nonempty by blast ``` lp15@66826 ` 1076` ``` then have "U \ {}" ``` lp15@66826 ` 1077` ``` using \K \ U\ \C \ K\ by blast ``` lp15@66826 ` 1078` ``` moreover have "U \ UNIV" ``` lp15@66826 ` 1079` ``` using \compact (closure U)\ by auto ``` lp15@66826 ` 1080` ``` ultimately show False ``` lp15@66826 ` 1081` ``` using \open U\ \closed U\ clopen by blast ``` lp15@66826 ` 1082` ``` next ``` lp15@66826 ` 1083` ``` case False ``` lp15@66826 ` 1084` ``` define j where "j \ Max J" ``` lp15@66826 ` 1085` ``` have "j \ J" ``` lp15@66826 ` 1086` ``` by (simp add: False \finite J\ j_def) ``` lp15@66826 ` 1087` ``` have jmax: "\m. m \ J \ m \ j" ``` lp15@66826 ` 1088` ``` by (simp add: j_def \finite J\) ``` lp15@66826 ` 1089` ``` have "\ ((\n. X n \ closure U) ` J) = X j \ closure U" ``` lp15@66826 ` 1090` ``` using False jmax nestX \j \ J\ by auto ``` lp15@66826 ` 1091` ``` then have "X j \ closure U = X j \ 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 \ closure U)" ``` lp15@66826 ` 1096` ``` by (simp add: openin_open_Int \open U\) ``` lp15@66826 ` 1097` ``` moreover have "closedin (subtopology euclidean (X j)) (X j \ closure U)" ``` lp15@66826 ` 1098` ``` by (simp add: closedin_closed_Int) ``` lp15@66826 ` 1099` ``` moreover have "X j \ closure U \ X j" ``` lp15@66826 ` 1100` ``` by (metis unboundedX \compact (closure U)\ bounded_subset compact_eq_bounded_closed inf.order_iff) ``` lp15@66826 ` 1101` ``` moreover have "X j \ closure U \ {}" ``` lp15@66826 ` 1102` ``` proof - ``` lp15@66826 ` 1103` ``` have "C \ {}" ``` lp15@66826 ` 1104` ``` using C in_components_nonempty by blast ``` lp15@66826 ` 1105` ``` moreover have "C \ X j \ closure U" ``` lp15@66826 ` 1106` ``` using \C \ K\ \K \ U\ 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 "(\n. X n \ closure U) = (\n. X n) \ closure U" ``` lp15@66826 ` 1115` ``` by blast ``` lp15@66826 ` 1116` ``` moreover have "x \ U" if "\n. x \ X n" "x \ closure U" for x ``` lp15@66826 ` 1117` ``` proof - ``` lp15@66826 ` 1118` ``` have "x \ V" ``` lp15@66826 ` 1119` ``` using \U \ V = {}\ \open V\ 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 \K \ U\ 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 V\, 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 \ components (- S)" and S: "connected S" ``` lp15@66826 ` 1135` ``` and prev: "if bounded S then connected(frontier S) ``` lp15@66826 ` 1136` ``` else \C \ components(frontier S). \ bounded C" ``` lp15@66826 ` 1137` ``` shows "\ bounded C" ``` lp15@66826 ` 1138` ```proof (cases "bounded S") ``` lp15@66826 ` 1139` ``` case True ``` lp15@66826 ` 1140` ``` with prev have "S \ 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 \ 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 \ {}" ``` lp15@66826 ` 1153` ``` using outside_bounded_nonempty by metis ``` lp15@66826 ` 1154` ``` then obtain z where z: "\ bounded (connected_component_set (- C) z)" and "z \ 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 \ - S" ``` lp15@66826 ` 1161` ``` using openS by (auto simp: frontier_def interior_open) ``` lp15@66826 ` 1162` ``` have False if "connected_component_set (- S) w \ frontier (- S) = {}" ``` lp15@66826 ` 1163` ``` proof - ``` lp15@66826 ` 1164` ``` have "C \ 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 \w \ S\ 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 \ frontier S \ {}" ``` lp15@66826 ` 1170` ``` by auto ``` lp15@66826 ` 1171` ``` have *: "\frontier C \ C; frontier C \ F; frontier C \ {}\ \ C \ F \ {}" for C F::"complex set" ``` lp15@66826 ` 1172` ``` by blast ``` lp15@66826 ` 1173` ``` have "connected_component_set (- S) z \ frontier (- S) \ {}" ``` lp15@66826 ` 1174` ``` proof (rule *) ``` lp15@66826 ` 1175` ``` show "frontier (connected_component_set (- S) z) \ 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) \ frontier (- S)" ``` lp15@66826 ` 1178` ``` using frontier_of_connected_component_subset by fastforce ``` lp15@66826 ` 1179` ``` have "\ bounded (-S)" ``` lp15@66826 ` 1180` ``` by (simp add: True cobounded_imp_unbounded) ``` lp15@66826 ` 1181` ``` then have "connected_component_set (- S) z \ {}" ``` lp15@66826 ` 1182` ``` apply (simp only: connected_component_eq_empty) ``` lp15@66826 ` 1183` ``` using confr openS \bounded C\ \w \ S\ ``` 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) \ {}" ``` 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 \ frontier S \ {}" ``` lp15@66826 ` 1193` ``` by auto ``` lp15@66826 ` 1194` ``` qed ``` lp15@66826 ` 1195` ``` then show False ``` lp15@66826 ` 1196` ``` by (metis C_ccsw Compl_iff \w \ S\ \z \ C\ 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 \ S" ``` lp15@66826 ` 1202` ``` using C by (auto simp: components_def) ``` lp15@66826 ` 1203` ``` have "frontier (connected_component_set (- S) w) \ 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) \ 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) \ {}" ``` 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 \ frontier S" and z: "z \ connected_component_set (- S) w" ``` lp15@66826 ` 1210` ``` by blast ``` lp15@66826 ` 1211` ``` have *: "connected_component_set (frontier S) z \ components(frontier S)" ``` lp15@66826 ` 1212` ``` by (simp add: \z \ frontier S\ componentsI) ``` lp15@66826 ` 1213` ``` with prev False have "\ 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" "\C. C \ components (- S) \ ~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` ``` "\connected S; inside S = {}\ \ 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 \ ``` lp15@66826 ` 1238` ``` connected S \ ``` lp15@66826 ` 1239` ``` (if bounded S then connected(frontier S) ``` lp15@66826 ` 1240` ``` else (\C \ components(frontier S). \bounded C))" (is "?fp") ``` lp15@66826 ` 1241` ``` and simply_connected_eq_unbounded_complement_components: ``` lp15@66826 ` 1242` ``` "simply_connected S \ ``` lp15@66826 ` 1243` ``` connected S \ (\C \ components(- S). \bounded C)" (is "?ucc") ``` lp15@66826 ` 1244` ``` and simply_connected_eq_empty_inside: ``` lp15@66826 ` 1245` ``` "simply_connected S \ ``` lp15@66826 ` 1246` ``` connected S \ 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 \ ?ucc \ ?ei" ``` lp15@66826 ` 1251` ```proof - ``` lp15@66826 ` 1252` ``` have *: "\\ \ \; \ \ \; \ \ \; \ \ \\ ``` lp15@66826 ` 1253` ``` \ (\ \ \) \ (\ \ \) \ (\ \ \)" for \ \ \ \ ``` 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 \ connected S \ 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\Further equivalences based on continuous logs and sqrts\ ``` 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\complex" ``` lp15@66826 ` 1284` ``` assumes S: "simply_connected S" ``` lp15@66826 ` 1285` ``` and contf: "continuous_on S f" and nz: "\z. z \ S \ f z \ 0" ``` lp15@66826 ` 1286` ``` shows "\g. continuous_on S g \ (\z \ 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\complex" ``` lp15@66826 ` 1297` ``` where kh: "\x. x \ S \ 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: "\y. y \ ball 0 1 \ 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: "\z. z \ ball 0 1 \ (f \ k) z = exp (g z)" ``` lp15@66826 ` 1304` ``` proof (rule continuous_logarithm_on_ball) ``` lp15@66826 ` 1305` ``` show "continuous_on (ball 0 1) (f \ 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 "\z. z \ ball 0 1 \ (f \ k) z \ 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\complex" ``` lp15@66826 ` 1319` ``` assumes contf: "continuous_on S f" and nz: "\z. z \ S \ f z \ 0" ``` lp15@66826 ` 1320` ``` and prev: "\f::complex\complex. ``` lp15@66826 ` 1321` ``` \continuous_on S f; \z. z \ S \ f z \ 0\ ``` lp15@66826 ` 1322` ``` \ \g. continuous_on S g \ (\z \ S. f z = exp(g z))" ``` lp15@66826 ` 1323` ``` shows "\g. continuous_on S g \ (\z \ S. f z = (g z)\<^sup>2)" ``` lp15@66826 ` 1324` ```proof - ``` lp15@66826 ` 1325` ``` obtain g where contg: "continuous_on S g" and geq: "\z. z \ S \ 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 (\z. exp(g z/2))" ``` lp15@66826 ` 1330` ``` by (intro continuous_intros) (auto simp: contg) ``` lp15@66826 ` 1331` ``` show "\z. z \ S \ 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: "\f::complex\complex. \continuous_on S f; \z \ S. f z \ 0\ ``` lp15@66826 ` 1340` ``` \ \g. continuous_on S g \ (\z \ 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] \connected S\) ``` lp15@66826 ` 1343` ``` fix f ``` lp15@66826 ` 1344` ``` assume "f holomorphic_on S" and nz: "\z\S. f z \ 0" ``` lp15@66826 ` 1345` ``` then obtain g where contg: "continuous_on S g" and geq: "\z. z \ S \ f z = (g z)\<^sup>2" ``` lp15@66826 ` 1346` ``` by (metis holomorphic_on_imp_continuous_on prev) ``` lp15@66826 ` 1347` ``` show "\g. g holomorphic_on S \ (\z\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 \ S" ``` lp15@66826 ` 1353` ``` with nz geq have "g z \ 0" ``` lp15@66826 ` 1354` ``` by auto ``` lp15@66826 ` 1355` ``` obtain \ where "0 < \" "\w. \w \ S; dist w z < \\ \ dist (g w) (g z) < cmod (g z)" ``` lp15@66826 ` 1356` ``` using contg [unfolded continuous_on_iff] by (metis \g z \ 0\ \z \ S\ zero_less_norm_iff) ``` lp15@66826 ` 1357` ``` then have \: "\w. \w \ S; w \ ball z \\ \ g w + g z \ 0" ``` lp15@66826 ` 1358` ``` apply (clarsimp simp: dist_norm) ``` lp15@66826 ` 1359` ``` by (metis \g z \ 0\ 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 *: "(\x. (f x - f z) / (x - z) / (g x + g z)) \z\ deriv f z / (g z + g z)" ``` lp15@66826 ` 1361` ``` apply (intro tendsto_intros) ``` lp15@66826 ` 1362` ``` using SC_Chain.openS SC_Chain_axioms \f holomorphic_on S\ \z \ S\ has_field_derivativeD holomorphic_derivI apply fastforce ``` lp15@66826 ` 1363` ``` using \z \ S\ contg continuous_on_eq_continuous_at isCont_def openS apply blast ``` lp15@66826 ` 1364` ``` by (simp add: \g z \ 0\) ``` 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 \ \ S)" ``` lp15@66826 ` 1369` ``` by (simp add: openS open_Int) ``` lp15@66826 ` 1370` ``` show "z \ ball z \ \ S" ``` lp15@66826 ` 1371` ``` using \z \ S\ \0 < \\ by simp ``` lp15@66826 ` 1372` ``` show "\x. \x \ ball z \ \ S; x \ z\ ``` lp15@66826 ` 1373` ``` \ (f x - f z) / (x - z) / (g x + g z) = (g x - g z) / (x - z)" ``` lp15@66826 ` 1374` ``` using \ ``` lp15@66826 ` 1375` ``` apply (simp add: geq \z \ S\ 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 "\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 \ ``` lp15@66826 ` 1391` ``` connected S \ ``` lp15@66826 ` 1392` ``` (\f::complex\complex. continuous_on S f \ (\z \ S. f z \ 0) ``` lp15@66826 ` 1393` ``` \ (\g. continuous_on S g \ (\z \ S. f z = exp (g z))))" (is "?log") ``` lp15@66826 ` 1394` ``` and simply_connected_eq_continuous_sqrt: ``` lp15@66826 ` 1395` ``` "simply_connected S \ ``` lp15@66826 ` 1396` ``` connected S \ ``` lp15@66826 ` 1397` ``` (\f::complex\complex. continuous_on S f \ (\z \ S. f z \ 0) ``` lp15@66826 ` 1398` ``` \ (\g. continuous_on S g \ (\z \ 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 \ ?sqrt" ``` lp15@66826 ` 1403` ```proof - ``` lp15@66826 ` 1404` ``` have *: "\\ \ \; \ \ \; \ \ \\ ``` lp15@66826 ` 1405` ``` \ (\ \ \) \ (\ \ \)" for \ \ \ ``` 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\More Borsukian results\ ``` 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 \ compact S" ``` lp15@66941 ` 1424` ``` shows "Borsukian S \ (\C \ 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 \ compact S" "\C. C \ components S \ 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 \ (simply_connected S \ connected S \ 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 \ Borsukian S \ (\C \ 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 \ closed S" and "bounded S" ``` lp15@66941 ` 1453` ``` shows "Borsukian S \ 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 S\] ``` lp15@66941 ` 1459` ``` by (meson \open S\ \bounded S\ 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 \bounded S\ 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\Finally, the Riemann Mapping Theorem\ ``` lp15@66941 ` 1468` lp15@66826 ` 1469` ```theorem Riemann_mapping_theorem: ``` lp15@66826 ` 1470` ``` "open S \ simply_connected S \ ``` lp15@66826 ` 1471` ``` S = {} \ S = UNIV \ ``` lp15@66826 ` 1472` ``` (\f g. f holomorphic_on S \ g holomorphic_on ball 0 1 \ ``` lp15@66826 ` 1473` ``` (\z \ S. f z \ ball 0 1 \ g(f z) = z) \ ``` lp15@66826 ` 1474` ``` (\z \ ball 0 1. g z \ S \ f(g z) = z))" ``` lp15@66826 ` 1475` ``` (is "_ = ?rhs") ``` lp15@66826 ` 1476` ```proof - ``` lp15@66826 ` 1477` ``` have "simply_connected S \ ?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" "\z\ball 0 1. g z \ S \ f (g z) = z" ``` lp15@66826 ` 1483` ``` and "\z\S. cmod (f z) < 1 \ 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 ```