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