|
1 section \<open>The Great Picard Theorem and its Applications\<close> |
|
2 |
|
3 text\<open>Ported from HOL Light (cauchy.ml) by L C Paulson, 2017\<close> |
|
4 |
|
5 theory Great_Picard |
|
6 imports Conformal_Mappings |
|
7 |
|
8 begin |
|
9 |
|
10 subsection\<open>Schottky's theorem\<close> |
|
11 |
|
12 lemma Schottky_lemma0: |
|
13 assumes holf: "f holomorphic_on S" and cons: "contractible S" and "a \<in> S" |
|
14 and f: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 1 \<and> f z \<noteq> -1" |
|
15 obtains g where "g holomorphic_on S" |
|
16 "norm(g a) \<le> 1 + norm(f a) / 3" |
|
17 "\<And>z. z \<in> S \<Longrightarrow> f z = cos(of_real pi * g z)" |
|
18 proof - |
|
19 obtain g where holg: "g holomorphic_on S" and g: "norm(g a) \<le> pi + norm(f a)" |
|
20 and f_eq_cos: "\<And>z. z \<in> S \<Longrightarrow> f z = cos(g z)" |
|
21 using contractible_imp_holomorphic_arccos_bounded [OF assms] |
|
22 by blast |
|
23 show ?thesis |
|
24 proof |
|
25 show "(\<lambda>z. g z / pi) holomorphic_on S" |
|
26 by (auto intro: holomorphic_intros holg) |
|
27 have "3 \<le> pi" |
|
28 using pi_approx by force |
|
29 have "3 * norm(g a) \<le> 3 * (pi + norm(f a))" |
|
30 using g by auto |
|
31 also have "... \<le> pi * 3 + pi * cmod (f a)" |
|
32 using \<open>3 \<le> pi\<close> by (simp add: mult_right_mono algebra_simps) |
|
33 finally show "cmod (g a / complex_of_real pi) \<le> 1 + cmod (f a) / 3" |
|
34 by (simp add: field_simps norm_divide) |
|
35 show "\<And>z. z \<in> S \<Longrightarrow> f z = cos (complex_of_real pi * (g z / complex_of_real pi))" |
|
36 by (simp add: f_eq_cos) |
|
37 qed |
|
38 qed |
|
39 |
|
40 |
|
41 lemma Schottky_lemma1: |
|
42 fixes n::nat |
|
43 assumes "0 < n" |
|
44 shows "0 < n + sqrt(real n ^ 2 - 1)" |
|
45 proof - |
|
46 have "(n-1)^2 \<le> n^2 - 1" |
|
47 using assms by (simp add: algebra_simps power2_eq_square) |
|
48 then have "real (n - 1) \<le> sqrt (real (n\<^sup>2 - 1))" |
|
49 by (metis of_nat_le_iff of_nat_power real_le_rsqrt) |
|
50 then have "n-1 \<le> sqrt(real n ^ 2 - 1)" |
|
51 by (simp add: Suc_leI assms of_nat_diff) |
|
52 then show ?thesis |
|
53 using assms by linarith |
|
54 qed |
|
55 |
|
56 |
|
57 lemma Schottky_lemma2: |
|
58 fixes x::real |
|
59 assumes "0 \<le> x" |
|
60 obtains n where "0 < n" "\<bar>x - ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi\<bar> < 1/2" |
|
61 proof - |
|
62 obtain n0::nat where "0 < n0" "ln(n0 + sqrt(real n0 ^ 2 - 1)) / pi \<le> x" |
|
63 proof |
|
64 show "ln(real 1 + sqrt(real 1 ^ 2 - 1))/pi \<le> x" |
|
65 by (auto simp: assms) |
|
66 qed auto |
|
67 moreover |
|
68 obtain M::nat where "\<And>n. \<lbrakk>0 < n; ln(n + sqrt(real n ^ 2 - 1)) / pi \<le> x\<rbrakk> \<Longrightarrow> n \<le> M" |
|
69 proof |
|
70 fix n::nat |
|
71 assume "0 < n" "ln (n + sqrt ((real n)\<^sup>2 - 1)) / pi \<le> x" |
|
72 then have "ln (n + sqrt ((real n)\<^sup>2 - 1)) \<le> x * pi" |
|
73 by (simp add: field_split_simps) |
|
74 then have *: "exp (ln (n + sqrt ((real n)\<^sup>2 - 1))) \<le> exp (x * pi)" |
|
75 by blast |
|
76 have 0: "0 \<le> sqrt ((real n)\<^sup>2 - 1)" |
|
77 using \<open>0 < n\<close> by auto |
|
78 have "n + sqrt ((real n)\<^sup>2 - 1) = exp (ln (n + sqrt ((real n)\<^sup>2 - 1)))" |
|
79 by (simp add: Suc_leI \<open>0 < n\<close> add_pos_nonneg real_of_nat_ge_one_iff) |
|
80 also have "... \<le> exp (x * pi)" |
|
81 using "*" by blast |
|
82 finally have "real n \<le> exp (x * pi)" |
|
83 using 0 by linarith |
|
84 then show "n \<le> nat (ceiling (exp(x * pi)))" |
|
85 by linarith |
|
86 qed |
|
87 ultimately obtain n where |
|
88 "0 < n" and le_x: "ln(n + sqrt(real n ^ 2 - 1)) / pi \<le> x" |
|
89 and le_n: "\<And>k. \<lbrakk>0 < k; ln(k + sqrt(real k ^ 2 - 1)) / pi \<le> x\<rbrakk> \<Longrightarrow> k \<le> n" |
|
90 using bounded_Max_nat [of "\<lambda>n. 0<n \<and> ln (n + sqrt ((real n)\<^sup>2 - 1)) / pi \<le> x"] by metis |
|
91 define a where "a \<equiv> ln(n + sqrt(real n ^ 2 - 1)) / pi" |
|
92 define b where "b \<equiv> ln (1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / pi" |
|
93 have le_xa: "a \<le> x" |
|
94 and le_na: "\<And>k. \<lbrakk>0 < k; ln(k + sqrt(real k ^ 2 - 1)) / pi \<le> x\<rbrakk> \<Longrightarrow> k \<le> n" |
|
95 using le_x le_n by (auto simp: a_def) |
|
96 moreover have "x < b" |
|
97 using le_n [of "Suc n"] by (force simp: b_def) |
|
98 moreover have "b - a < 1" |
|
99 proof - |
|
100 have "ln (1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) - ln (real n + sqrt ((real n)\<^sup>2 - 1)) = |
|
101 ln ((1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / (real n + sqrt ((real n)\<^sup>2 - 1)))" |
|
102 by (simp add: \<open>0 < n\<close> Schottky_lemma1 add_pos_nonneg ln_div [symmetric]) |
|
103 also have "... \<le> 3" |
|
104 proof (cases "n = 1") |
|
105 case True |
|
106 have "sqrt 3 \<le> 2" |
|
107 by (simp add: real_le_lsqrt) |
|
108 then have "(2 + sqrt 3) \<le> 4" |
|
109 by simp |
|
110 also have "... \<le> exp 3" |
|
111 using exp_ge_add_one_self [of "3::real"] by simp |
|
112 finally have "ln (2 + sqrt 3) \<le> 3" |
|
113 by (metis add_nonneg_nonneg add_pos_nonneg dbl_def dbl_inc_def dbl_inc_simps(3) |
|
114 dbl_simps(3) exp_gt_zero ln_exp ln_le_cancel_iff real_sqrt_ge_0_iff zero_le_one zero_less_one) |
|
115 then show ?thesis |
|
116 by (simp add: True) |
|
117 next |
|
118 case False with \<open>0 < n\<close> have "1 < n" "2 \<le> n" |
|
119 by linarith+ |
|
120 then have 1: "1 \<le> real n * real n" |
|
121 by (metis less_imp_le_nat one_le_power power2_eq_square real_of_nat_ge_one_iff) |
|
122 have *: "4 + (m+2) * 2 \<le> (m+2) * ((m+2) * 3)" for m::nat |
|
123 by simp |
|
124 have "4 + n * 2 \<le> n * (n * 3)" |
|
125 using * [of "n-2"] \<open>2 \<le> n\<close> |
|
126 by (metis le_add_diff_inverse2) |
|
127 then have **: "4 + real n * 2 \<le> real n * (real n * 3)" |
|
128 by (metis (mono_tags, hide_lams) of_nat_le_iff of_nat_add of_nat_mult of_nat_numeral) |
|
129 have "sqrt ((1 + real n)\<^sup>2 - 1) \<le> 2 * sqrt ((real n)\<^sup>2 - 1)" |
|
130 by (auto simp: real_le_lsqrt power2_eq_square algebra_simps 1 **) |
|
131 then |
|
132 have "((1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / (real n + sqrt ((real n)\<^sup>2 - 1))) \<le> 2" |
|
133 using Schottky_lemma1 \<open>0 < n\<close> by (simp add: field_split_simps) |
|
134 then have "ln ((1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / (real n + sqrt ((real n)\<^sup>2 - 1))) \<le> ln 2" |
|
135 apply (subst ln_le_cancel_iff) |
|
136 using Schottky_lemma1 \<open>0 < n\<close> by auto (force simp: field_split_simps) |
|
137 also have "... \<le> 3" |
|
138 using ln_add_one_self_le_self [of 1] by auto |
|
139 finally show ?thesis . |
|
140 qed |
|
141 also have "... < pi" |
|
142 using pi_approx by simp |
|
143 finally show ?thesis |
|
144 by (simp add: a_def b_def field_split_simps) |
|
145 qed |
|
146 ultimately have "\<bar>x - a\<bar> < 1/2 \<or> \<bar>x - b\<bar> < 1/2" |
|
147 by (auto simp: abs_if) |
|
148 then show thesis |
|
149 proof |
|
150 assume "\<bar>x - a\<bar> < 1 / 2" |
|
151 then show ?thesis |
|
152 by (rule_tac n=n in that) (auto simp: a_def \<open>0 < n\<close>) |
|
153 next |
|
154 assume "\<bar>x - b\<bar> < 1 / 2" |
|
155 then show ?thesis |
|
156 by (rule_tac n="Suc n" in that) (auto simp: b_def \<open>0 < n\<close>) |
|
157 qed |
|
158 qed |
|
159 |
|
160 |
|
161 lemma Schottky_lemma3: |
|
162 fixes z::complex |
|
163 assumes "z \<in> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)}) |
|
164 \<union> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)})" |
|
165 shows "cos(pi * cos(pi * z)) = 1 \<or> cos(pi * cos(pi * z)) = -1" |
|
166 proof - |
|
167 have sqrt2 [simp]: "complex_of_real (sqrt x) * complex_of_real (sqrt x) = x" if "x \<ge> 0" for x::real |
|
168 by (metis abs_of_nonneg of_real_mult real_sqrt_mult_self that) |
|
169 have 1: "\<exists>k. exp (\<i> * (of_int m * complex_of_real pi) - |
|
170 (ln (real n + sqrt ((real n)\<^sup>2 - 1)))) + |
|
171 inverse |
|
172 (exp (\<i> * (of_int m * complex_of_real pi) - |
|
173 (ln (real n + sqrt ((real n)\<^sup>2 - 1))))) = of_int k * 2" |
|
174 if "n > 0" for m n |
|
175 proof - |
|
176 have eeq: "e \<noteq> 0 \<Longrightarrow> e + inverse e = n*2 \<longleftrightarrow> inverse e^2 - 2 * n*inverse e + 1 = 0" for n e::complex |
|
177 by (auto simp: field_simps power2_eq_square) |
|
178 have [simp]: "1 \<le> real n * real n" |
|
179 by (metis One_nat_def add.commute nat_less_real_le of_nat_1 of_nat_Suc one_le_power power2_eq_square that) |
|
180 show ?thesis |
|
181 apply (simp add: eeq) |
|
182 using Schottky_lemma1 [OF that] |
|
183 apply (auto simp: eeq exp_diff exp_Euler exp_of_real algebra_simps sin_int_times_real cos_int_times_real) |
|
184 apply (rule_tac x="int n" in exI) |
|
185 apply (auto simp: power2_eq_square algebra_simps) |
|
186 apply (rule_tac x="- int n" in exI) |
|
187 apply (auto simp: power2_eq_square algebra_simps) |
|
188 done |
|
189 qed |
|
190 have 2: "\<exists>k. exp (\<i> * (of_int m * complex_of_real pi) + |
|
191 (ln (real n + sqrt ((real n)\<^sup>2 - 1)))) + |
|
192 inverse |
|
193 (exp (\<i> * (of_int m * complex_of_real pi) + |
|
194 (ln (real n + sqrt ((real n)\<^sup>2 - 1))))) = of_int k * 2" |
|
195 if "n > 0" for m n |
|
196 proof - |
|
197 have eeq: "e \<noteq> 0 \<Longrightarrow> e + inverse e = n*2 \<longleftrightarrow> e^2 - 2 * n*e + 1 = 0" for n e::complex |
|
198 by (auto simp: field_simps power2_eq_square) |
|
199 have [simp]: "1 \<le> real n * real n" |
|
200 by (metis One_nat_def add.commute nat_less_real_le of_nat_1 of_nat_Suc one_le_power power2_eq_square that) |
|
201 show ?thesis |
|
202 apply (simp add: eeq) |
|
203 using Schottky_lemma1 [OF that] |
|
204 apply (auto simp: exp_add exp_Euler exp_of_real algebra_simps sin_int_times_real cos_int_times_real) |
|
205 apply (rule_tac x="int n" in exI) |
|
206 apply (auto simp: power2_eq_square algebra_simps) |
|
207 apply (rule_tac x="- int n" in exI) |
|
208 apply (auto simp: power2_eq_square algebra_simps) |
|
209 done |
|
210 qed |
|
211 have "\<exists>x. cos (complex_of_real pi * z) = of_int x" |
|
212 using assms |
|
213 apply safe |
|
214 apply (auto simp: Ints_def cos_exp_eq exp_minus Complex_eq) |
|
215 apply (auto simp: algebra_simps dest: 1 2) |
|
216 done |
|
217 then have "sin(pi * cos(pi * z)) ^ 2 = 0" |
|
218 by (simp add: Complex_Transcendental.sin_eq_0) |
|
219 then have "1 - cos(pi * cos(pi * z)) ^ 2 = 0" |
|
220 by (simp add: sin_squared_eq) |
|
221 then show ?thesis |
|
222 using power2_eq_1_iff by auto |
|
223 qed |
|
224 |
|
225 |
|
226 theorem Schottky: |
|
227 assumes holf: "f holomorphic_on cball 0 1" |
|
228 and nof0: "norm(f 0) \<le> r" |
|
229 and not01: "\<And>z. z \<in> cball 0 1 \<Longrightarrow> \<not>(f z = 0 \<or> f z = 1)" |
|
230 and "0 < t" "t < 1" "norm z \<le> t" |
|
231 shows "norm(f z) \<le> exp(pi * exp(pi * (2 + 2 * r + 12 * t / (1 - t))))" |
|
232 proof - |
|
233 obtain h where holf: "h holomorphic_on cball 0 1" |
|
234 and nh0: "norm (h 0) \<le> 1 + norm(2 * f 0 - 1) / 3" |
|
235 and h: "\<And>z. z \<in> cball 0 1 \<Longrightarrow> 2 * f z - 1 = cos(of_real pi * h z)" |
|
236 proof (rule Schottky_lemma0 [of "\<lambda>z. 2 * f z - 1" "cball 0 1" 0]) |
|
237 show "(\<lambda>z. 2 * f z - 1) holomorphic_on cball 0 1" |
|
238 by (intro holomorphic_intros holf) |
|
239 show "contractible (cball (0::complex) 1)" |
|
240 by (auto simp: convex_imp_contractible) |
|
241 show "\<And>z. z \<in> cball 0 1 \<Longrightarrow> 2 * f z - 1 \<noteq> 1 \<and> 2 * f z - 1 \<noteq> - 1" |
|
242 using not01 by force |
|
243 qed auto |
|
244 obtain g where holg: "g holomorphic_on cball 0 1" |
|
245 and ng0: "norm(g 0) \<le> 1 + norm(h 0) / 3" |
|
246 and g: "\<And>z. z \<in> cball 0 1 \<Longrightarrow> h z = cos(of_real pi * g z)" |
|
247 proof (rule Schottky_lemma0 [OF holf convex_imp_contractible, of 0]) |
|
248 show "\<And>z. z \<in> cball 0 1 \<Longrightarrow> h z \<noteq> 1 \<and> h z \<noteq> - 1" |
|
249 using h not01 by fastforce+ |
|
250 qed auto |
|
251 have g0_2_f0: "norm(g 0) \<le> 2 + norm(f 0)" |
|
252 proof - |
|
253 have "cmod (2 * f 0 - 1) \<le> cmod (2 * f 0) + 1" |
|
254 by (metis norm_one norm_triangle_ineq4) |
|
255 also have "... \<le> 2 + cmod (f 0) * 3" |
|
256 by simp |
|
257 finally have "1 + norm(2 * f 0 - 1) / 3 \<le> (2 + norm(f 0) - 1) * 3" |
|
258 apply (simp add: field_split_simps) |
|
259 using norm_ge_zero [of "f 0 * 2 - 1"] |
|
260 by linarith |
|
261 with nh0 have "norm(h 0) \<le> (2 + norm(f 0) - 1) * 3" |
|
262 by linarith |
|
263 then have "1 + norm(h 0) / 3 \<le> 2 + norm(f 0)" |
|
264 by simp |
|
265 with ng0 show ?thesis |
|
266 by auto |
|
267 qed |
|
268 have "z \<in> ball 0 1" |
|
269 using assms by auto |
|
270 have norm_g_12: "norm(g z - g 0) \<le> (12 * t) / (1 - t)" |
|
271 proof - |
|
272 obtain g' where g': "\<And>x. x \<in> cball 0 1 \<Longrightarrow> (g has_field_derivative g' x) (at x within cball 0 1)" |
|
273 using holg [unfolded holomorphic_on_def field_differentiable_def] by metis |
|
274 have int_g': "(g' has_contour_integral g z - g 0) (linepath 0 z)" |
|
275 using contour_integral_primitive [OF g' valid_path_linepath, of 0 z] |
|
276 using \<open>z \<in> ball 0 1\<close> segment_bound1 by fastforce |
|
277 have "cmod (g' w) \<le> 12 / (1 - t)" if "w \<in> closed_segment 0 z" for w |
|
278 proof - |
|
279 have w: "w \<in> ball 0 1" |
|
280 using segment_bound [OF that] \<open>z \<in> ball 0 1\<close> by simp |
|
281 have ttt: "\<And>z. z \<in> frontier (cball 0 1) \<Longrightarrow> 1 - t \<le> dist w z" |
|
282 using \<open>norm z \<le> t\<close> segment_bound1 [OF \<open>w \<in> closed_segment 0 z\<close>] |
|
283 apply (simp add: dist_complex_def) |
|
284 by (metis diff_left_mono dist_commute dist_complex_def norm_triangle_ineq2 order_trans) |
|
285 have *: "\<lbrakk>\<And>b. (\<exists>w \<in> T \<union> U. w \<in> ball b 1); \<And>x. x \<in> D \<Longrightarrow> g x \<notin> T \<union> U\<rbrakk> \<Longrightarrow> \<nexists>b. ball b 1 \<subseteq> g ` D" for T U D |
|
286 by force |
|
287 have "\<nexists>b. ball b 1 \<subseteq> g ` cball 0 1" |
|
288 proof (rule *) |
|
289 show "(\<exists>w \<in> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)}) \<union> |
|
290 (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)}). w \<in> ball b 1)" for b |
|
291 proof - |
|
292 obtain m where m: "m \<in> \<int>" "\<bar>Re b - m\<bar> \<le> 1/2" |
|
293 by (metis Ints_of_int abs_minus_commute of_int_round_abs_le) |
|
294 show ?thesis |
|
295 proof (cases "0::real" "Im b" rule: le_cases) |
|
296 case le |
|
297 then obtain n where "0 < n" and n: "\<bar>Im b - ln (n + sqrt ((real n)\<^sup>2 - 1)) / pi\<bar> < 1/2" |
|
298 using Schottky_lemma2 [of "Im b"] by blast |
|
299 have "dist b (Complex m (Im b)) \<le> 1/2" |
|
300 by (metis cancel_comm_monoid_add_class.diff_cancel cmod_eq_Re complex.sel(1) complex.sel(2) dist_norm m(2) minus_complex.code) |
|
301 moreover |
|
302 have "dist (Complex m (Im b)) (Complex m (ln (n + sqrt ((real n)\<^sup>2 - 1)) / pi)) < 1/2" |
|
303 using n by (simp add: complex_norm cmod_eq_Re complex_diff dist_norm del: Complex_eq) |
|
304 ultimately have "dist b (Complex m (ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi)) < 1" |
|
305 by (simp add: dist_triangle_lt [of b "Complex m (Im b)"] dist_commute) |
|
306 with le m \<open>0 < n\<close> show ?thesis |
|
307 apply (rule_tac x = "Complex m (ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi)" in bexI) |
|
308 apply (simp_all del: Complex_eq greaterThan_0) |
|
309 by blast |
|
310 next |
|
311 case ge |
|
312 then obtain n where "0 < n" and n: "\<bar>- Im b - ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi\<bar> < 1/2" |
|
313 using Schottky_lemma2 [of "- Im b"] by auto |
|
314 have "dist b (Complex m (Im b)) \<le> 1/2" |
|
315 by (metis cancel_comm_monoid_add_class.diff_cancel cmod_eq_Re complex.sel(1) complex.sel(2) dist_norm m(2) minus_complex.code) |
|
316 moreover |
|
317 have "dist (Complex m (- ln (n + sqrt ((real n)\<^sup>2 - 1)) / pi)) (Complex m (Im b)) < 1/2" |
|
318 using n |
|
319 apply (simp add: complex_norm cmod_eq_Re complex_diff dist_norm del: Complex_eq) |
|
320 by (metis add.commute add_uminus_conv_diff) |
|
321 ultimately have "dist b (Complex m (- ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi)) < 1" |
|
322 by (simp add: dist_triangle_lt [of b "Complex m (Im b)"] dist_commute) |
|
323 with ge m \<open>0 < n\<close> show ?thesis |
|
324 apply (rule_tac x = "Complex m (- ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi)" in bexI) |
|
325 apply (simp_all del: Complex_eq greaterThan_0) |
|
326 by blast |
|
327 qed |
|
328 qed |
|
329 show "g v \<notin> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)}) \<union> |
|
330 (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)})" |
|
331 if "v \<in> cball 0 1" for v |
|
332 using not01 [OF that] |
|
333 by (force simp: g [OF that, symmetric] h [OF that, symmetric] dest!: Schottky_lemma3 [of "g v"]) |
|
334 qed |
|
335 then have 12: "(1 - t) * cmod (deriv g w) / 12 < 1" |
|
336 using Bloch_general [OF holg _ ttt, of 1] w by force |
|
337 have "g field_differentiable at w within cball 0 1" |
|
338 using holg w by (simp add: holomorphic_on_def) |
|
339 then have "g field_differentiable at w within ball 0 1" |
|
340 using ball_subset_cball field_differentiable_within_subset by blast |
|
341 with w have der_gw: "(g has_field_derivative deriv g w) (at w)" |
|
342 by (simp add: field_differentiable_within_open [of _ "ball 0 1"] field_differentiable_derivI) |
|
343 with DERIV_unique [OF der_gw] g' w have "deriv g w = g' w" |
|
344 by (metis open_ball at_within_open ball_subset_cball has_field_derivative_subset subsetCE) |
|
345 then show "cmod (g' w) \<le> 12 / (1 - t)" |
|
346 using g' 12 \<open>t < 1\<close> by (simp add: field_simps) |
|
347 qed |
|
348 then have "cmod (g z - g 0) \<le> 12 / (1 - t) * cmod z" |
|
349 using has_contour_integral_bound_linepath [OF int_g', of "12/(1 - t)"] assms |
|
350 by simp |
|
351 with \<open>cmod z \<le> t\<close> \<open>t < 1\<close> show ?thesis |
|
352 by (simp add: field_split_simps) |
|
353 qed |
|
354 have fz: "f z = (1 + cos(of_real pi * h z)) / 2" |
|
355 using h \<open>z \<in> ball 0 1\<close> by (auto simp: field_simps) |
|
356 have "cmod (f z) \<le> exp (cmod (complex_of_real pi * h z))" |
|
357 by (simp add: fz mult.commute norm_cos_plus1_le) |
|
358 also have "... \<le> exp (pi * exp (pi * (2 + 2 * r + 12 * t / (1 - t))))" |
|
359 proof (simp add: norm_mult) |
|
360 have "cmod (g z - g 0) \<le> 12 * t / (1 - t)" |
|
361 using norm_g_12 \<open>t < 1\<close> by (simp add: norm_mult) |
|
362 then have "cmod (g z) - cmod (g 0) \<le> 12 * t / (1 - t)" |
|
363 using norm_triangle_ineq2 order_trans by blast |
|
364 then have *: "cmod (g z) \<le> 2 + 2 * r + 12 * t / (1 - t)" |
|
365 using g0_2_f0 norm_ge_zero [of "f 0"] nof0 |
|
366 by linarith |
|
367 have "cmod (h z) \<le> exp (cmod (complex_of_real pi * g z))" |
|
368 using \<open>z \<in> ball 0 1\<close> by (simp add: g norm_cos_le) |
|
369 also have "... \<le> exp (pi * (2 + 2 * r + 12 * t / (1 - t)))" |
|
370 using \<open>t < 1\<close> nof0 * by (simp add: norm_mult) |
|
371 finally show "cmod (h z) \<le> exp (pi * (2 + 2 * r + 12 * t / (1 - t)))" . |
|
372 qed |
|
373 finally show ?thesis . |
|
374 qed |
|
375 |
|
376 |
|
377 subsection\<open>The Little Picard Theorem\<close> |
|
378 |
|
379 theorem Landau_Picard: |
|
380 obtains R |
|
381 where "\<And>z. 0 < R z" |
|
382 "\<And>f. \<lbrakk>f holomorphic_on cball 0 (R(f 0)); |
|
383 \<And>z. norm z \<le> R(f 0) \<Longrightarrow> f z \<noteq> 0 \<and> f z \<noteq> 1\<rbrakk> \<Longrightarrow> norm(deriv f 0) < 1" |
|
384 proof - |
|
385 define R where "R \<equiv> \<lambda>z. 3 * exp(pi * exp(pi*(2 + 2 * cmod z + 12)))" |
|
386 show ?thesis |
|
387 proof |
|
388 show Rpos: "\<And>z. 0 < R z" |
|
389 by (auto simp: R_def) |
|
390 show "norm(deriv f 0) < 1" |
|
391 if holf: "f holomorphic_on cball 0 (R(f 0))" |
|
392 and Rf: "\<And>z. norm z \<le> R(f 0) \<Longrightarrow> f z \<noteq> 0 \<and> f z \<noteq> 1" for f |
|
393 proof - |
|
394 let ?r = "R(f 0)" |
|
395 define g where "g \<equiv> f \<circ> (\<lambda>z. of_real ?r * z)" |
|
396 have "0 < ?r" |
|
397 using Rpos by blast |
|
398 have holg: "g holomorphic_on cball 0 1" |
|
399 unfolding g_def |
|
400 apply (intro holomorphic_intros holomorphic_on_compose holomorphic_on_subset [OF holf]) |
|
401 using Rpos by (auto simp: less_imp_le norm_mult) |
|
402 have *: "norm(g z) \<le> exp(pi * exp(pi * (2 + 2 * norm (f 0) + 12 * t / (1 - t))))" |
|
403 if "0 < t" "t < 1" "norm z \<le> t" for t z |
|
404 proof (rule Schottky [OF holg]) |
|
405 show "cmod (g 0) \<le> cmod (f 0)" |
|
406 by (simp add: g_def) |
|
407 show "\<And>z. z \<in> cball 0 1 \<Longrightarrow> \<not> (g z = 0 \<or> g z = 1)" |
|
408 using Rpos by (simp add: g_def less_imp_le norm_mult Rf) |
|
409 qed (auto simp: that) |
|
410 have C1: "g holomorphic_on ball 0 (1 / 2)" |
|
411 by (rule holomorphic_on_subset [OF holg]) auto |
|
412 have C2: "continuous_on (cball 0 (1 / 2)) g" |
|
413 by (meson cball_divide_subset_numeral holg holomorphic_on_imp_continuous_on holomorphic_on_subset) |
|
414 have C3: "cmod (g z) \<le> R (f 0) / 3" if "cmod (0 - z) = 1/2" for z |
|
415 proof - |
|
416 have "norm(g z) \<le> exp(pi * exp(pi * (2 + 2 * norm (f 0) + 12)))" |
|
417 using * [of "1/2"] that by simp |
|
418 also have "... = ?r / 3" |
|
419 by (simp add: R_def) |
|
420 finally show ?thesis . |
|
421 qed |
|
422 then have cmod_g'_le: "cmod (deriv g 0) * 3 \<le> R (f 0) * 2" |
|
423 using Cauchy_inequality [OF C1 C2 _ C3, of 1] by simp |
|
424 have holf': "f holomorphic_on ball 0 (R(f 0))" |
|
425 by (rule holomorphic_on_subset [OF holf]) auto |
|
426 then have fd0: "f field_differentiable at 0" |
|
427 by (rule holomorphic_on_imp_differentiable_at [OF _ open_ball]) |
|
428 (auto simp: Rpos [of "f 0"]) |
|
429 have g_eq: "deriv g 0 = of_real ?r * deriv f 0" |
|
430 apply (rule DERIV_imp_deriv) |
|
431 apply (simp add: g_def) |
|
432 by (metis DERIV_chain DERIV_cmult_Id fd0 field_differentiable_derivI mult.commute mult_zero_right) |
|
433 show ?thesis |
|
434 using cmod_g'_le Rpos [of "f 0"] by (simp add: g_eq norm_mult) |
|
435 qed |
|
436 qed |
|
437 qed |
|
438 |
|
439 lemma little_Picard_01: |
|
440 assumes holf: "f holomorphic_on UNIV" and f01: "\<And>z. f z \<noteq> 0 \<and> f z \<noteq> 1" |
|
441 obtains c where "f = (\<lambda>x. c)" |
|
442 proof - |
|
443 obtain R |
|
444 where Rpos: "\<And>z. 0 < R z" |
|
445 and R: "\<And>h. \<lbrakk>h holomorphic_on cball 0 (R(h 0)); |
|
446 \<And>z. norm z \<le> R(h 0) \<Longrightarrow> h z \<noteq> 0 \<and> h z \<noteq> 1\<rbrakk> \<Longrightarrow> norm(deriv h 0) < 1" |
|
447 using Landau_Picard by metis |
|
448 have contf: "continuous_on UNIV f" |
|
449 by (simp add: holf holomorphic_on_imp_continuous_on) |
|
450 show ?thesis |
|
451 proof (cases "\<forall>x. deriv f x = 0") |
|
452 case True |
|
453 obtain c where "\<And>x. f(x) = c" |
|
454 apply (rule DERIV_zero_connected_constant [OF connected_UNIV open_UNIV finite.emptyI contf]) |
|
455 apply (metis True DiffE holf holomorphic_derivI open_UNIV, auto) |
|
456 done |
|
457 then show ?thesis |
|
458 using that by auto |
|
459 next |
|
460 case False |
|
461 then obtain w where w: "deriv f w \<noteq> 0" by auto |
|
462 define fw where "fw \<equiv> (f \<circ> (\<lambda>z. w + z / deriv f w))" |
|
463 have norm_let1: "norm(deriv fw 0) < 1" |
|
464 proof (rule R) |
|
465 show "fw holomorphic_on cball 0 (R (fw 0))" |
|
466 unfolding fw_def |
|
467 by (intro holomorphic_intros holomorphic_on_compose w holomorphic_on_subset [OF holf] subset_UNIV) |
|
468 show "fw z \<noteq> 0 \<and> fw z \<noteq> 1" if "cmod z \<le> R (fw 0)" for z |
|
469 using f01 by (simp add: fw_def) |
|
470 qed |
|
471 have "(fw has_field_derivative deriv f w * inverse (deriv f w)) (at 0)" |
|
472 apply (simp add: fw_def) |
|
473 apply (rule DERIV_chain) |
|
474 using holf holomorphic_derivI apply force |
|
475 apply (intro derivative_eq_intros w) |
|
476 apply (auto simp: field_simps) |
|
477 done |
|
478 then show ?thesis |
|
479 using norm_let1 w by (simp add: DERIV_imp_deriv) |
|
480 qed |
|
481 qed |
|
482 |
|
483 |
|
484 theorem little_Picard: |
|
485 assumes holf: "f holomorphic_on UNIV" |
|
486 and "a \<noteq> b" "range f \<inter> {a,b} = {}" |
|
487 obtains c where "f = (\<lambda>x. c)" |
|
488 proof - |
|
489 let ?g = "\<lambda>x. 1/(b - a)*(f x - b) + 1" |
|
490 obtain c where "?g = (\<lambda>x. c)" |
|
491 proof (rule little_Picard_01) |
|
492 show "?g holomorphic_on UNIV" |
|
493 by (intro holomorphic_intros holf) |
|
494 show "\<And>z. ?g z \<noteq> 0 \<and> ?g z \<noteq> 1" |
|
495 using assms by (auto simp: field_simps) |
|
496 qed auto |
|
497 then have "?g x = c" for x |
|
498 by meson |
|
499 then have "f x = c * (b-a) + a" for x |
|
500 using assms by (auto simp: field_simps) |
|
501 then show ?thesis |
|
502 using that by blast |
|
503 qed |
|
504 |
|
505 |
|
506 text\<open>A couple of little applications of Little Picard\<close> |
|
507 |
|
508 lemma holomorphic_periodic_fixpoint: |
|
509 assumes holf: "f holomorphic_on UNIV" |
|
510 and "p \<noteq> 0" and per: "\<And>z. f(z + p) = f z" |
|
511 obtains x where "f x = x" |
|
512 proof - |
|
513 have False if non: "\<And>x. f x \<noteq> x" |
|
514 proof - |
|
515 obtain c where "(\<lambda>z. f z - z) = (\<lambda>z. c)" |
|
516 proof (rule little_Picard) |
|
517 show "(\<lambda>z. f z - z) holomorphic_on UNIV" |
|
518 by (simp add: holf holomorphic_on_diff) |
|
519 show "range (\<lambda>z. f z - z) \<inter> {p,0} = {}" |
|
520 using assms non by auto (metis add.commute diff_eq_eq) |
|
521 qed (auto simp: assms) |
|
522 with per show False |
|
523 by (metis add.commute add_cancel_left_left \<open>p \<noteq> 0\<close> diff_add_cancel) |
|
524 qed |
|
525 then show ?thesis |
|
526 using that by blast |
|
527 qed |
|
528 |
|
529 |
|
530 lemma holomorphic_involution_point: |
|
531 assumes holfU: "f holomorphic_on UNIV" and non: "\<And>a. f \<noteq> (\<lambda>x. a + x)" |
|
532 obtains x where "f(f x) = x" |
|
533 proof - |
|
534 { assume non_ff [simp]: "\<And>x. f(f x) \<noteq> x" |
|
535 then have non_fp [simp]: "f z \<noteq> z" for z |
|
536 by metis |
|
537 have holf: "f holomorphic_on X" for X |
|
538 using assms holomorphic_on_subset by blast |
|
539 obtain c where c: "(\<lambda>x. (f(f x) - x)/(f x - x)) = (\<lambda>x. c)" |
|
540 proof (rule little_Picard_01) |
|
541 show "(\<lambda>x. (f(f x) - x)/(f x - x)) holomorphic_on UNIV" |
|
542 apply (intro holomorphic_intros holf holomorphic_on_compose [unfolded o_def, OF holf]) |
|
543 using non_fp by auto |
|
544 qed auto |
|
545 then obtain "c \<noteq> 0" "c \<noteq> 1" |
|
546 by (metis (no_types, hide_lams) non_ff diff_zero divide_eq_0_iff right_inverse_eq) |
|
547 have eq: "f(f x) - c * f x = x*(1 - c)" for x |
|
548 using fun_cong [OF c, of x] by (simp add: field_simps) |
|
549 have df_times_dff: "deriv f z * (deriv f (f z) - c) = 1 * (1 - c)" for z |
|
550 proof (rule DERIV_unique) |
|
551 show "((\<lambda>x. f (f x) - c * f x) has_field_derivative |
|
552 deriv f z * (deriv f (f z) - c)) (at z)" |
|
553 apply (intro derivative_eq_intros) |
|
554 apply (rule DERIV_chain [unfolded o_def, of f]) |
|
555 apply (auto simp: algebra_simps intro!: holomorphic_derivI [OF holfU]) |
|
556 done |
|
557 show "((\<lambda>x. f (f x) - c * f x) has_field_derivative 1 * (1 - c)) (at z)" |
|
558 by (simp add: eq mult_commute_abs) |
|
559 qed |
|
560 { fix z::complex |
|
561 obtain k where k: "deriv f \<circ> f = (\<lambda>x. k)" |
|
562 proof (rule little_Picard) |
|
563 show "(deriv f \<circ> f) holomorphic_on UNIV" |
|
564 by (meson holfU holomorphic_deriv holomorphic_on_compose holomorphic_on_subset open_UNIV subset_UNIV) |
|
565 obtain "deriv f (f x) \<noteq> 0" "deriv f (f x) \<noteq> c" for x |
|
566 using df_times_dff \<open>c \<noteq> 1\<close> eq_iff_diff_eq_0 |
|
567 by (metis lambda_one mult_zero_left mult_zero_right) |
|
568 then show "range (deriv f \<circ> f) \<inter> {0,c} = {}" |
|
569 by force |
|
570 qed (use \<open>c \<noteq> 0\<close> in auto) |
|
571 have "\<not> f constant_on UNIV" |
|
572 by (meson UNIV_I non_ff constant_on_def) |
|
573 with holf open_mapping_thm have "open(range f)" |
|
574 by blast |
|
575 obtain l where l: "\<And>x. f x - k * x = l" |
|
576 proof (rule DERIV_zero_connected_constant [of UNIV "{}" "\<lambda>x. f x - k * x"], simp_all) |
|
577 have "deriv f w - k = 0" for w |
|
578 proof (rule analytic_continuation [OF _ open_UNIV connected_UNIV subset_UNIV, of "\<lambda>z. deriv f z - k" "f z" "range f" w]) |
|
579 show "(\<lambda>z. deriv f z - k) holomorphic_on UNIV" |
|
580 by (intro holomorphic_intros holf open_UNIV) |
|
581 show "f z islimpt range f" |
|
582 by (metis (no_types, lifting) IntI UNIV_I \<open>open (range f)\<close> image_eqI inf.absorb_iff2 inf_aci(1) islimpt_UNIV islimpt_eq_acc_point open_Int top_greatest) |
|
583 show "\<And>z. z \<in> range f \<Longrightarrow> deriv f z - k = 0" |
|
584 by (metis comp_def diff_self image_iff k) |
|
585 qed auto |
|
586 moreover |
|
587 have "((\<lambda>x. f x - k * x) has_field_derivative deriv f x - k) (at x)" for x |
|
588 by (metis DERIV_cmult_Id Deriv.field_differentiable_diff UNIV_I field_differentiable_derivI holf holomorphic_on_def) |
|
589 ultimately |
|
590 show "\<forall>x. ((\<lambda>x. f x - k * x) has_field_derivative 0) (at x)" |
|
591 by auto |
|
592 show "continuous_on UNIV (\<lambda>x. f x - k * x)" |
|
593 by (simp add: continuous_on_diff holf holomorphic_on_imp_continuous_on) |
|
594 qed (auto simp: connected_UNIV) |
|
595 have False |
|
596 proof (cases "k=1") |
|
597 case True |
|
598 then have "\<exists>x. k * x + l \<noteq> a + x" for a |
|
599 using l non [of a] ext [of f "(+) a"] |
|
600 by (metis add.commute diff_eq_eq) |
|
601 with True show ?thesis by auto |
|
602 next |
|
603 case False |
|
604 have "\<And>x. (1 - k) * x \<noteq> f 0" |
|
605 using l [of 0] apply (simp add: algebra_simps) |
|
606 by (metis diff_add_cancel l mult.commute non_fp) |
|
607 then show False |
|
608 by (metis False eq_iff_diff_eq_0 mult.commute nonzero_mult_div_cancel_right times_divide_eq_right) |
|
609 qed |
|
610 } |
|
611 } |
|
612 then show thesis |
|
613 using that by blast |
|
614 qed |
|
615 |
|
616 |
|
617 subsection\<open>The Arzelà --Ascoli theorem\<close> |
|
618 |
|
619 lemma subsequence_diagonalization_lemma: |
|
620 fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool" |
|
621 assumes sub: "\<And>i r. \<exists>k. strict_mono (k :: nat \<Rightarrow> nat) \<and> P i (r \<circ> k)" |
|
622 and P_P: "\<And>i r::nat \<Rightarrow> 'a. \<And>k1 k2 N. |
|
623 \<lbrakk>P i (r \<circ> k1); \<And>j. N \<le> j \<Longrightarrow> \<exists>j'. j \<le> j' \<and> k2 j = k1 j'\<rbrakk> \<Longrightarrow> P i (r \<circ> k2)" |
|
624 obtains k where "strict_mono (k :: nat \<Rightarrow> nat)" "\<And>i. P i (r \<circ> k)" |
|
625 proof - |
|
626 obtain kk where "\<And>i r. strict_mono (kk i r :: nat \<Rightarrow> nat) \<and> P i (r \<circ> (kk i r))" |
|
627 using sub by metis |
|
628 then have sub_kk: "\<And>i r. strict_mono (kk i r)" and P_kk: "\<And>i r. P i (r \<circ> (kk i r))" |
|
629 by auto |
|
630 define rr where "rr \<equiv> rec_nat (kk 0 r) (\<lambda>n x. x \<circ> kk (Suc n) (r \<circ> x))" |
|
631 then have [simp]: "rr 0 = kk 0 r" "\<And>n. rr(Suc n) = rr n \<circ> kk (Suc n) (r \<circ> rr n)" |
|
632 by auto |
|
633 show thesis |
|
634 proof |
|
635 have sub_rr: "strict_mono (rr i)" for i |
|
636 using sub_kk by (induction i) (auto simp: strict_mono_def o_def) |
|
637 have P_rr: "P i (r \<circ> rr i)" for i |
|
638 using P_kk by (induction i) (auto simp: o_def) |
|
639 have "i \<le> i+d \<Longrightarrow> rr i n \<le> rr (i+d) n" for d i n |
|
640 proof (induction d) |
|
641 case 0 then show ?case |
|
642 by simp |
|
643 next |
|
644 case (Suc d) then show ?case |
|
645 apply simp |
|
646 using seq_suble [OF sub_kk] order_trans strict_mono_less_eq [OF sub_rr] by blast |
|
647 qed |
|
648 then have "\<And>i j n. i \<le> j \<Longrightarrow> rr i n \<le> rr j n" |
|
649 by (metis le_iff_add) |
|
650 show "strict_mono (\<lambda>n. rr n n)" |
|
651 apply (simp add: strict_mono_Suc_iff) |
|
652 by (meson lessI less_le_trans seq_suble strict_monoD sub_kk sub_rr) |
|
653 have "\<exists>j. i \<le> j \<and> rr (n+d) i = rr n j" for d n i |
|
654 apply (induction d arbitrary: i, auto) |
|
655 by (meson order_trans seq_suble sub_kk) |
|
656 then have "\<And>m n i. n \<le> m \<Longrightarrow> \<exists>j. i \<le> j \<and> rr m i = rr n j" |
|
657 by (metis le_iff_add) |
|
658 then show "P i (r \<circ> (\<lambda>n. rr n n))" for i |
|
659 by (meson P_rr P_P) |
|
660 qed |
|
661 qed |
|
662 |
|
663 lemma function_convergent_subsequence: |
|
664 fixes f :: "[nat,'a] \<Rightarrow> 'b::{real_normed_vector,heine_borel}" |
|
665 assumes "countable S" and M: "\<And>n::nat. \<And>x. x \<in> S \<Longrightarrow> norm(f n x) \<le> M" |
|
666 obtains k where "strict_mono (k::nat\<Rightarrow>nat)" "\<And>x. x \<in> S \<Longrightarrow> \<exists>l. (\<lambda>n. f (k n) x) \<longlonglongrightarrow> l" |
|
667 proof (cases "S = {}") |
|
668 case True |
|
669 then show ?thesis |
|
670 using strict_mono_id that by fastforce |
|
671 next |
|
672 case False |
|
673 with \<open>countable S\<close> obtain \<sigma> :: "nat \<Rightarrow> 'a" where \<sigma>: "S = range \<sigma>" |
|
674 using uncountable_def by blast |
|
675 obtain k where "strict_mono k" and k: "\<And>i. \<exists>l. (\<lambda>n. (f \<circ> k) n (\<sigma> i)) \<longlonglongrightarrow> l" |
|
676 proof (rule subsequence_diagonalization_lemma |
|
677 [of "\<lambda>i r. \<exists>l. ((\<lambda>n. (f \<circ> r) n (\<sigma> i)) \<longlongrightarrow> l) sequentially" id]) |
|
678 show "\<exists>k::nat\<Rightarrow>nat. strict_mono k \<and> (\<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k)) n (\<sigma> i)) \<longlonglongrightarrow> l)" for i r |
|
679 proof - |
|
680 have "f (r n) (\<sigma> i) \<in> cball 0 M" for n |
|
681 by (simp add: \<sigma> M) |
|
682 then show ?thesis |
|
683 using compact_def [of "cball (0::'b) M"] apply simp |
|
684 apply (drule_tac x="(\<lambda>n. f (r n) (\<sigma> i))" in spec) |
|
685 apply (force simp: o_def) |
|
686 done |
|
687 qed |
|
688 show "\<And>i r k1 k2 N. |
|
689 \<lbrakk>\<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k1)) n (\<sigma> i)) \<longlonglongrightarrow> l; \<And>j. N \<le> j \<Longrightarrow> \<exists>j'\<ge>j. k2 j = k1 j'\<rbrakk> |
|
690 \<Longrightarrow> \<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k2)) n (\<sigma> i)) \<longlonglongrightarrow> l" |
|
691 apply (simp add: lim_sequentially) |
|
692 apply (erule ex_forward all_forward imp_forward)+ |
|
693 apply auto |
|
694 by (metis (no_types, hide_lams) le_cases order_trans) |
|
695 qed auto |
|
696 with \<sigma> that show ?thesis |
|
697 by force |
|
698 qed |
|
699 |
|
700 |
|
701 theorem Arzela_Ascoli: |
|
702 fixes \<F> :: "[nat,'a::euclidean_space] \<Rightarrow> 'b::{real_normed_vector,heine_borel}" |
|
703 assumes "compact S" |
|
704 and M: "\<And>n x. x \<in> S \<Longrightarrow> norm(\<F> n x) \<le> M" |
|
705 and equicont: |
|
706 "\<And>x e. \<lbrakk>x \<in> S; 0 < e\<rbrakk> |
|
707 \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>n y. y \<in> S \<and> norm(x - y) < d \<longrightarrow> norm(\<F> n x - \<F> n y) < e)" |
|
708 obtains g k where "continuous_on S g" "strict_mono (k :: nat \<Rightarrow> nat)" |
|
709 "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<and> x \<in> S \<longrightarrow> norm(\<F>(k n) x - g x) < e" |
|
710 proof - |
|
711 have UEQ: "\<And>e. 0 < e \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>n. \<forall>x \<in> S. \<forall>x' \<in> S. dist x' x < d \<longrightarrow> dist (\<F> n x') (\<F> n x) < e)" |
|
712 apply (rule compact_uniformly_equicontinuous [OF \<open>compact S\<close>, of "range \<F>"]) |
|
713 using equicont by (force simp: dist_commute dist_norm)+ |
|
714 have "continuous_on S g" |
|
715 if "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<and> x \<in> S \<longrightarrow> norm(\<F>(r n) x - g x) < e" |
|
716 for g:: "'a \<Rightarrow> 'b" and r :: "nat \<Rightarrow> nat" |
|
717 proof (rule uniform_limit_theorem [of _ "\<F> \<circ> r"]) |
|
718 show "\<forall>\<^sub>F n in sequentially. continuous_on S ((\<F> \<circ> r) n)" |
|
719 apply (simp add: eventually_sequentially) |
|
720 apply (rule_tac x=0 in exI) |
|
721 using UEQ apply (force simp: continuous_on_iff) |
|
722 done |
|
723 show "uniform_limit S (\<F> \<circ> r) g sequentially" |
|
724 apply (simp add: uniform_limit_iff eventually_sequentially) |
|
725 by (metis dist_norm that) |
|
726 qed auto |
|
727 moreover |
|
728 obtain R where "countable R" "R \<subseteq> S" and SR: "S \<subseteq> closure R" |
|
729 by (metis separable that) |
|
730 obtain k where "strict_mono k" and k: "\<And>x. x \<in> R \<Longrightarrow> \<exists>l. (\<lambda>n. \<F> (k n) x) \<longlonglongrightarrow> l" |
|
731 apply (rule function_convergent_subsequence [OF \<open>countable R\<close> M]) |
|
732 using \<open>R \<subseteq> S\<close> apply force+ |
|
733 done |
|
734 then have Cauchy: "Cauchy ((\<lambda>n. \<F> (k n) x))" if "x \<in> R" for x |
|
735 using convergent_eq_Cauchy that by blast |
|
736 have "\<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> x \<in> S \<longrightarrow> dist ((\<F> \<circ> k) m x) ((\<F> \<circ> k) n x) < e" |
|
737 if "0 < e" for e |
|
738 proof - |
|
739 obtain d where "0 < d" |
|
740 and d: "\<And>n. \<forall>x \<in> S. \<forall>x' \<in> S. dist x' x < d \<longrightarrow> dist (\<F> n x') (\<F> n x) < e/3" |
|
741 by (metis UEQ \<open>0 < e\<close> divide_pos_pos zero_less_numeral) |
|
742 obtain T where "T \<subseteq> R" and "finite T" and T: "S \<subseteq> (\<Union>c\<in>T. ball c d)" |
|
743 proof (rule compactE_image [OF \<open>compact S\<close>, of R "(\<lambda>x. ball x d)"]) |
|
744 have "closure R \<subseteq> (\<Union>c\<in>R. ball c d)" |
|
745 apply clarsimp |
|
746 using \<open>0 < d\<close> closure_approachable by blast |
|
747 with SR show "S \<subseteq> (\<Union>c\<in>R. ball c d)" |
|
748 by auto |
|
749 qed auto |
|
750 have "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (\<F> (k m) x) (\<F> (k n) x) < e/3" if "x \<in> R" for x |
|
751 using Cauchy \<open>0 < e\<close> that unfolding Cauchy_def |
|
752 by (metis less_divide_eq_numeral1(1) mult_zero_left) |
|
753 then obtain MF where MF: "\<And>x m n. \<lbrakk>x \<in> R; m \<ge> MF x; n \<ge> MF x\<rbrakk> \<Longrightarrow> norm (\<F> (k m) x - \<F> (k n) x) < e/3" |
|
754 using dist_norm by metis |
|
755 have "dist ((\<F> \<circ> k) m x) ((\<F> \<circ> k) n x) < e" |
|
756 if m: "Max (MF ` T) \<le> m" and n: "Max (MF ` T) \<le> n" "x \<in> S" for m n x |
|
757 proof - |
|
758 obtain t where "t \<in> T" and t: "x \<in> ball t d" |
|
759 using \<open>x \<in> S\<close> T by auto |
|
760 have "norm(\<F> (k m) t - \<F> (k m) x) < e / 3" |
|
761 by (metis \<open>R \<subseteq> S\<close> \<open>T \<subseteq> R\<close> \<open>t \<in> T\<close> d dist_norm mem_ball subset_iff t \<open>x \<in> S\<close>) |
|
762 moreover |
|
763 have "norm(\<F> (k n) t - \<F> (k n) x) < e / 3" |
|
764 by (metis \<open>R \<subseteq> S\<close> \<open>T \<subseteq> R\<close> \<open>t \<in> T\<close> subsetD d dist_norm mem_ball t \<open>x \<in> S\<close>) |
|
765 moreover |
|
766 have "norm(\<F> (k m) t - \<F> (k n) t) < e / 3" |
|
767 proof (rule MF) |
|
768 show "t \<in> R" |
|
769 using \<open>T \<subseteq> R\<close> \<open>t \<in> T\<close> by blast |
|
770 show "MF t \<le> m" "MF t \<le> n" |
|
771 by (meson Max_ge \<open>finite T\<close> \<open>t \<in> T\<close> finite_imageI imageI le_trans m n)+ |
|
772 qed |
|
773 ultimately |
|
774 show ?thesis |
|
775 unfolding dist_norm [symmetric] o_def |
|
776 by (metis dist_triangle_third dist_commute) |
|
777 qed |
|
778 then show ?thesis |
|
779 by force |
|
780 qed |
|
781 then have "\<exists>g. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> S. norm(\<F>(k n) x - g x) < e" |
|
782 using uniformly_convergent_eq_cauchy [of "\<lambda>x. x \<in> S" "\<F> \<circ> k"] |
|
783 apply (simp add: o_def dist_norm) |
|
784 by meson |
|
785 ultimately show thesis |
|
786 by (metis that \<open>strict_mono k\<close>) |
|
787 qed |
|
788 |
|
789 |
|
790 |
|
791 subsubsection\<^marker>\<open>tag important\<close>\<open>Montel's theorem\<close> |
|
792 |
|
793 text\<open>a sequence of holomorphic functions uniformly bounded |
|
794 on compact subsets of an open set S has a subsequence that converges to a |
|
795 holomorphic function, and converges \emph{uniformly} on compact subsets of S.\<close> |
|
796 |
|
797 |
|
798 theorem Montel: |
|
799 fixes \<F> :: "[nat,complex] \<Rightarrow> complex" |
|
800 assumes "open S" |
|
801 and \<H>: "\<And>h. h \<in> \<H> \<Longrightarrow> h holomorphic_on S" |
|
802 and bounded: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>B. \<forall>h \<in> \<H>. \<forall> z \<in> K. norm(h z) \<le> B" |
|
803 and rng_f: "range \<F> \<subseteq> \<H>" |
|
804 obtains g r |
|
805 where "g holomorphic_on S" "strict_mono (r :: nat \<Rightarrow> nat)" |
|
806 "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>n. \<F> (r n) x) \<longlongrightarrow> g x) sequentially" |
|
807 "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K (\<F> \<circ> r) g sequentially" |
|
808 proof - |
|
809 obtain K where comK: "\<And>n. compact(K n)" and KS: "\<And>n::nat. K n \<subseteq> S" |
|
810 and subK: "\<And>X. \<lbrakk>compact X; X \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. X \<subseteq> K n" |
|
811 using open_Union_compact_subsets [OF \<open>open S\<close>] by metis |
|
812 then have "\<And>i. \<exists>B. \<forall>h \<in> \<H>. \<forall> z \<in> K i. norm(h z) \<le> B" |
|
813 by (simp add: bounded) |
|
814 then obtain B where B: "\<And>i h z. \<lbrakk>h \<in> \<H>; z \<in> K i\<rbrakk> \<Longrightarrow> norm(h z) \<le> B i" |
|
815 by metis |
|
816 have *: "\<exists>r g. strict_mono (r::nat\<Rightarrow>nat) \<and> (\<forall>e > 0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> r) n x - g x) < e)" |
|
817 if "\<And>n. \<F> n \<in> \<H>" for \<F> i |
|
818 proof - |
|
819 obtain g k where "continuous_on (K i) g" "strict_mono (k::nat\<Rightarrow>nat)" |
|
820 "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm(\<F>(k n) x - g x) < e" |
|
821 proof (rule Arzela_Ascoli [of "K i" "\<F>" "B i"]) |
|
822 show "\<exists>d>0. \<forall>n y. y \<in> K i \<and> cmod (z - y) < d \<longrightarrow> cmod (\<F> n z - \<F> n y) < e" |
|
823 if z: "z \<in> K i" and "0 < e" for z e |
|
824 proof - |
|
825 obtain r where "0 < r" and r: "cball z r \<subseteq> S" |
|
826 using z KS [of i] \<open>open S\<close> by (force simp: open_contains_cball) |
|
827 have "cball z (2 / 3 * r) \<subseteq> cball z r" |
|
828 using \<open>0 < r\<close> by (simp add: cball_subset_cball_iff) |
|
829 then have z23S: "cball z (2 / 3 * r) \<subseteq> S" |
|
830 using r by blast |
|
831 obtain M where "0 < M" and M: "\<And>n w. dist z w \<le> 2/3 * r \<Longrightarrow> norm(\<F> n w) \<le> M" |
|
832 proof - |
|
833 obtain N where N: "\<forall>n\<ge>N. cball z (2/3 * r) \<subseteq> K n" |
|
834 using subK compact_cball [of z "(2 / 3 * r)"] z23S by force |
|
835 have "cmod (\<F> n w) \<le> \<bar>B N\<bar> + 1" if "dist z w \<le> 2 / 3 * r" for n w |
|
836 proof - |
|
837 have "w \<in> K N" |
|
838 using N mem_cball that by blast |
|
839 then have "cmod (\<F> n w) \<le> B N" |
|
840 using B \<open>\<And>n. \<F> n \<in> \<H>\<close> by blast |
|
841 also have "... \<le> \<bar>B N\<bar> + 1" |
|
842 by simp |
|
843 finally show ?thesis . |
|
844 qed |
|
845 then show ?thesis |
|
846 by (rule_tac M="\<bar>B N\<bar> + 1" in that) auto |
|
847 qed |
|
848 have "cmod (\<F> n z - \<F> n y) < e" |
|
849 if "y \<in> K i" and y_near_z: "cmod (z - y) < r/3" "cmod (z - y) < e * r / (6 * M)" |
|
850 for n y |
|
851 proof - |
|
852 have "((\<lambda>w. \<F> n w / (w - \<xi>)) has_contour_integral |
|
853 (2 * pi) * \<i> * winding_number (circlepath z (2 / 3 * r)) \<xi> * \<F> n \<xi>) |
|
854 (circlepath z (2 / 3 * r))" |
|
855 if "dist \<xi> z < (2 / 3 * r)" for \<xi> |
|
856 proof (rule Cauchy_integral_formula_convex_simple) |
|
857 have "\<F> n holomorphic_on S" |
|
858 by (simp add: \<H> \<open>\<And>n. \<F> n \<in> \<H>\<close>) |
|
859 with z23S show "\<F> n holomorphic_on cball z (2 / 3 * r)" |
|
860 using holomorphic_on_subset by blast |
|
861 qed (use that \<open>0 < r\<close> in \<open>auto simp: dist_commute\<close>) |
|
862 then have *: "((\<lambda>w. \<F> n w / (w - \<xi>)) has_contour_integral (2 * pi) * \<i> * \<F> n \<xi>) |
|
863 (circlepath z (2 / 3 * r))" |
|
864 if "dist \<xi> z < (2 / 3 * r)" for \<xi> |
|
865 using that by (simp add: winding_number_circlepath dist_norm) |
|
866 have y: "((\<lambda>w. \<F> n w / (w - y)) has_contour_integral (2 * pi) * \<i> * \<F> n y) |
|
867 (circlepath z (2 / 3 * r))" |
|
868 apply (rule *) |
|
869 using that \<open>0 < r\<close> by (simp only: dist_norm norm_minus_commute) |
|
870 have z: "((\<lambda>w. \<F> n w / (w - z)) has_contour_integral (2 * pi) * \<i> * \<F> n z) |
|
871 (circlepath z (2 / 3 * r))" |
|
872 apply (rule *) |
|
873 using \<open>0 < r\<close> by simp |
|
874 have le_er: "cmod (\<F> n x / (x - y) - \<F> n x / (x - z)) \<le> e / r" |
|
875 if "cmod (x - z) = r/3 + r/3" for x |
|
876 proof - |
|
877 have "\<not> (cmod (x - y) < r/3)" |
|
878 using y_near_z(1) that \<open>M > 0\<close> \<open>r > 0\<close> |
|
879 by (metis (full_types) norm_diff_triangle_less norm_minus_commute order_less_irrefl) |
|
880 then have r4_le_xy: "r/4 \<le> cmod (x - y)" |
|
881 using \<open>r > 0\<close> by simp |
|
882 then have neq: "x \<noteq> y" "x \<noteq> z" |
|
883 using that \<open>r > 0\<close> by (auto simp: field_split_simps norm_minus_commute) |
|
884 have leM: "cmod (\<F> n x) \<le> M" |
|
885 by (simp add: M dist_commute dist_norm that) |
|
886 have "cmod (\<F> n x / (x - y) - \<F> n x / (x - z)) = cmod (\<F> n x) * cmod (1 / (x - y) - 1 / (x - z))" |
|
887 by (metis (no_types, lifting) divide_inverse mult.left_neutral norm_mult right_diff_distrib') |
|
888 also have "... = cmod (\<F> n x) * cmod ((y - z) / ((x - y) * (x - z)))" |
|
889 using neq by (simp add: field_split_simps) |
|
890 also have "... = cmod (\<F> n x) * (cmod (y - z) / (cmod(x - y) * (2/3 * r)))" |
|
891 by (simp add: norm_mult norm_divide that) |
|
892 also have "... \<le> M * (cmod (y - z) / (cmod(x - y) * (2/3 * r)))" |
|
893 apply (rule mult_mono) |
|
894 apply (rule leM) |
|
895 using \<open>r > 0\<close> \<open>M > 0\<close> neq by auto |
|
896 also have "... < M * ((e * r / (6 * M)) / (cmod(x - y) * (2/3 * r)))" |
|
897 unfolding mult_less_cancel_left |
|
898 using y_near_z(2) \<open>M > 0\<close> \<open>r > 0\<close> neq |
|
899 apply (simp add: field_simps mult_less_0_iff norm_minus_commute) |
|
900 done |
|
901 also have "... \<le> e/r" |
|
902 using \<open>e > 0\<close> \<open>r > 0\<close> r4_le_xy by (simp add: field_split_simps) |
|
903 finally show ?thesis by simp |
|
904 qed |
|
905 have "(2 * pi) * cmod (\<F> n y - \<F> n z) = cmod ((2 * pi) * \<i> * \<F> n y - (2 * pi) * \<i> * \<F> n z)" |
|
906 by (simp add: right_diff_distrib [symmetric] norm_mult) |
|
907 also have "cmod ((2 * pi) * \<i> * \<F> n y - (2 * pi) * \<i> * \<F> n z) \<le> e / r * (2 * pi * (2 / 3 * r))" |
|
908 apply (rule has_contour_integral_bound_circlepath [OF has_contour_integral_diff [OF y z], of "e/r"]) |
|
909 using \<open>e > 0\<close> \<open>r > 0\<close> le_er by auto |
|
910 also have "... = (2 * pi) * e * ((2 / 3))" |
|
911 using \<open>r > 0\<close> by (simp add: field_split_simps) |
|
912 finally have "cmod (\<F> n y - \<F> n z) \<le> e * (2 / 3)" |
|
913 by simp |
|
914 also have "... < e" |
|
915 using \<open>e > 0\<close> by simp |
|
916 finally show ?thesis by (simp add: norm_minus_commute) |
|
917 qed |
|
918 then show ?thesis |
|
919 apply (rule_tac x="min (r/3) ((e * r)/(6 * M))" in exI) |
|
920 using \<open>0 < e\<close> \<open>0 < r\<close> \<open>0 < M\<close> by simp |
|
921 qed |
|
922 show "\<And>n x. x \<in> K i \<Longrightarrow> cmod (\<F> n x) \<le> B i" |
|
923 using B \<open>\<And>n. \<F> n \<in> \<H>\<close> by blast |
|
924 next |
|
925 fix g :: "complex \<Rightarrow> complex" and k :: "nat \<Rightarrow> nat" |
|
926 assume *: "\<And>(g::complex\<Rightarrow>complex) (k::nat\<Rightarrow>nat). continuous_on (K i) g \<Longrightarrow> |
|
927 strict_mono k \<Longrightarrow> |
|
928 (\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>K i. cmod (\<F> (k n) x - g x) < e) \<Longrightarrow> thesis" |
|
929 "continuous_on (K i) g" |
|
930 "strict_mono k" |
|
931 "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. N \<le> n \<and> x \<in> K i \<longrightarrow> cmod (\<F> (k n) x - g x) < e" |
|
932 show ?thesis |
|
933 by (rule *(1)[OF *(2,3)], drule *(4)) auto |
|
934 qed (use comK in simp_all) |
|
935 then show ?thesis |
|
936 by auto |
|
937 qed |
|
938 have "\<exists>k g. strict_mono (k::nat\<Rightarrow>nat) \<and> (\<forall>e > 0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> r \<circ> k) n x - g x) < e)" |
|
939 for i r |
|
940 apply (rule *) |
|
941 using rng_f by auto |
|
942 then have **: "\<And>i r. \<exists>k. strict_mono (k::nat\<Rightarrow>nat) \<and> (\<exists>g. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> (r \<circ> k)) n x - g x) < e)" |
|
943 by (force simp: o_assoc) |
|
944 obtain k :: "nat \<Rightarrow> nat" where "strict_mono k" |
|
945 and "\<And>i. \<exists>g. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>K i. cmod ((\<F> \<circ> (id \<circ> k)) n x - g x) < e" |
|
946 (* TODO: clean up this mess *) |
|
947 apply (rule subsequence_diagonalization_lemma [OF **, of id id]) |
|
948 apply (erule ex_forward all_forward imp_forward)+ |
|
949 apply force |
|
950 apply (erule exE) |
|
951 apply (rename_tac i r k1 k2 N g e Na) |
|
952 apply (rule_tac x="max N Na" in exI) |
|
953 apply fastforce+ |
|
954 done |
|
955 then have lt_e: "\<And>i. \<exists>g. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>K i. cmod ((\<F> \<circ> k) n x - g x) < e" |
|
956 by simp |
|
957 have "\<exists>l. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. norm(\<F> (k n) z - l) < e" if "z \<in> S" for z |
|
958 proof - |
|
959 obtain G where G: "\<And>i e. e > 0 \<Longrightarrow> \<exists>M. \<forall>n\<ge>M. \<forall>x\<in>K i. cmod ((\<F> \<circ> k) n x - G i x) < e" |
|
960 using lt_e by metis |
|
961 obtain N where "\<And>n. n \<ge> N \<Longrightarrow> z \<in> K n" |
|
962 using subK [of "{z}"] that \<open>z \<in> S\<close> by auto |
|
963 moreover have "\<And>e. e > 0 \<Longrightarrow> \<exists>M. \<forall>n\<ge>M. \<forall>x\<in>K N. cmod ((\<F> \<circ> k) n x - G N x) < e" |
|
964 using G by auto |
|
965 ultimately show ?thesis |
|
966 by (metis comp_apply order_refl) |
|
967 qed |
|
968 then obtain g where g: "\<And>z e. \<lbrakk>z \<in> S; e > 0\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. norm(\<F> (k n) z - g z) < e" |
|
969 by metis |
|
970 show ?thesis |
|
971 proof |
|
972 show g_lim: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. \<F> (k n) x) \<longlonglongrightarrow> g x" |
|
973 by (simp add: lim_sequentially g dist_norm) |
|
974 have dg_le_e: "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>T. cmod (\<F> (k n) x - g x) < e" |
|
975 if T: "compact T" "T \<subseteq> S" and "0 < e" for T e |
|
976 proof - |
|
977 obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> T \<subseteq> K n" |
|
978 using subK [OF T] by blast |
|
979 obtain h where h: "\<And>e. e>0 \<Longrightarrow> \<exists>M. \<forall>n\<ge>M. \<forall>x\<in>K N. cmod ((\<F> \<circ> k) n x - h x) < e" |
|
980 using lt_e by blast |
|
981 have geq: "g w = h w" if "w \<in> T" for w |
|
982 apply (rule LIMSEQ_unique [of "\<lambda>n. \<F>(k n) w"]) |
|
983 using \<open>T \<subseteq> S\<close> g_lim that apply blast |
|
984 using h N that by (force simp: lim_sequentially dist_norm) |
|
985 show ?thesis |
|
986 using T h N \<open>0 < e\<close> by (fastforce simp add: geq) |
|
987 qed |
|
988 then show "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> |
|
989 \<Longrightarrow> uniform_limit K (\<F> \<circ> k) g sequentially" |
|
990 by (simp add: uniform_limit_iff dist_norm eventually_sequentially) |
|
991 show "g holomorphic_on S" |
|
992 proof (rule holomorphic_uniform_sequence [OF \<open>open S\<close> \<H>]) |
|
993 show "\<And>n. (\<F> \<circ> k) n \<in> \<H>" |
|
994 by (simp add: range_subsetD rng_f) |
|
995 show "\<exists>d>0. cball z d \<subseteq> S \<and> uniform_limit (cball z d) (\<lambda>n. (\<F> \<circ> k) n) g sequentially" |
|
996 if "z \<in> S" for z |
|
997 proof - |
|
998 obtain d where d: "d>0" "cball z d \<subseteq> S" |
|
999 using \<open>open S\<close> \<open>z \<in> S\<close> open_contains_cball by blast |
|
1000 then have "uniform_limit (cball z d) (\<F> \<circ> k) g sequentially" |
|
1001 using dg_le_e compact_cball by (auto simp: uniform_limit_iff eventually_sequentially dist_norm) |
|
1002 with d show ?thesis by blast |
|
1003 qed |
|
1004 qed |
|
1005 qed (auto simp: \<open>strict_mono k\<close>) |
|
1006 qed |
|
1007 |
|
1008 |
|
1009 |
|
1010 subsection\<open>Some simple but useful cases of Hurwitz's theorem\<close> |
|
1011 |
|
1012 proposition Hurwitz_no_zeros: |
|
1013 assumes S: "open S" "connected S" |
|
1014 and holf: "\<And>n::nat. \<F> n holomorphic_on S" |
|
1015 and holg: "g holomorphic_on S" |
|
1016 and ul_g: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K \<F> g sequentially" |
|
1017 and nonconst: "\<not> g constant_on S" |
|
1018 and nz: "\<And>n z. z \<in> S \<Longrightarrow> \<F> n z \<noteq> 0" |
|
1019 and "z0 \<in> S" |
|
1020 shows "g z0 \<noteq> 0" |
|
1021 proof |
|
1022 assume g0: "g z0 = 0" |
|
1023 obtain h r m |
|
1024 where "0 < m" "0 < r" and subS: "ball z0 r \<subseteq> S" |
|
1025 and holh: "h holomorphic_on ball z0 r" |
|
1026 and geq: "\<And>w. w \<in> ball z0 r \<Longrightarrow> g w = (w - z0)^m * h w" |
|
1027 and hnz: "\<And>w. w \<in> ball z0 r \<Longrightarrow> h w \<noteq> 0" |
|
1028 by (blast intro: holomorphic_factor_zero_nonconstant [OF holg S \<open>z0 \<in> S\<close> g0 nonconst]) |
|
1029 then have holf0: "\<F> n holomorphic_on ball z0 r" for n |
|
1030 by (meson holf holomorphic_on_subset) |
|
1031 have *: "((\<lambda>z. deriv (\<F> n) z / \<F> n z) has_contour_integral 0) (circlepath z0 (r/2))" for n |
|
1032 proof (rule Cauchy_theorem_disc_simple [of _ z0 r]) |
|
1033 show "(\<lambda>z. deriv (\<F> n) z / \<F> n z) holomorphic_on ball z0 r" |
|
1034 apply (intro holomorphic_intros holomorphic_deriv holf holf0 open_ball nz) |
|
1035 using \<open>ball z0 r \<subseteq> S\<close> by blast |
|
1036 qed (use \<open>0 < r\<close> in auto) |
|
1037 have hol_dg: "deriv g holomorphic_on S" |
|
1038 by (simp add: \<open>open S\<close> holg holomorphic_deriv) |
|
1039 have "continuous_on (sphere z0 (r/2)) (deriv g)" |
|
1040 apply (intro holomorphic_on_imp_continuous_on holomorphic_on_subset [OF hol_dg]) |
|
1041 using \<open>0 < r\<close> subS by auto |
|
1042 then have "compact (deriv g ` (sphere z0 (r/2)))" |
|
1043 by (rule compact_continuous_image [OF _ compact_sphere]) |
|
1044 then have bo_dg: "bounded (deriv g ` (sphere z0 (r/2)))" |
|
1045 using compact_imp_bounded by blast |
|
1046 have "continuous_on (sphere z0 (r/2)) (cmod \<circ> g)" |
|
1047 apply (intro continuous_intros holomorphic_on_imp_continuous_on holomorphic_on_subset [OF holg]) |
|
1048 using \<open>0 < r\<close> subS by auto |
|
1049 then have "compact ((cmod \<circ> g) ` sphere z0 (r/2))" |
|
1050 by (rule compact_continuous_image [OF _ compact_sphere]) |
|
1051 moreover have "(cmod \<circ> g) ` sphere z0 (r/2) \<noteq> {}" |
|
1052 using \<open>0 < r\<close> by auto |
|
1053 ultimately obtain b where b: "b \<in> (cmod \<circ> g) ` sphere z0 (r/2)" |
|
1054 "\<And>t. t \<in> (cmod \<circ> g) ` sphere z0 (r/2) \<Longrightarrow> b \<le> t" |
|
1055 using compact_attains_inf [of "(norm \<circ> g) ` (sphere z0 (r/2))"] by blast |
|
1056 have "(\<lambda>n. contour_integral (circlepath z0 (r/2)) (\<lambda>z. deriv (\<F> n) z / \<F> n z)) \<longlonglongrightarrow> |
|
1057 contour_integral (circlepath z0 (r/2)) (\<lambda>z. deriv g z / g z)" |
|
1058 proof (rule contour_integral_uniform_limit_circlepath) |
|
1059 show "\<forall>\<^sub>F n in sequentially. (\<lambda>z. deriv (\<F> n) z / \<F> n z) contour_integrable_on circlepath z0 (r/2)" |
|
1060 using * contour_integrable_on_def eventually_sequentiallyI by meson |
|
1061 show "uniform_limit (sphere z0 (r/2)) (\<lambda>n z. deriv (\<F> n) z / \<F> n z) (\<lambda>z. deriv g z / g z) sequentially" |
|
1062 proof (rule uniform_lim_divide [OF _ _ bo_dg]) |
|
1063 show "uniform_limit (sphere z0 (r/2)) (\<lambda>a. deriv (\<F> a)) (deriv g) sequentially" |
|
1064 proof (rule uniform_limitI) |
|
1065 fix e::real |
|
1066 assume "0 < e" |
|
1067 have *: "dist (deriv (\<F> n) w) (deriv g w) < e" |
|
1068 if e8: "\<And>x. dist z0 x \<le> 3 * r / 4 \<Longrightarrow> dist (\<F> n x) (g x) * 8 < r * e" |
|
1069 and w: "dist w z0 = r/2" for n w |
|
1070 proof - |
|
1071 have "ball w (r/4) \<subseteq> ball z0 r" "cball w (r/4) \<subseteq> ball z0 r" |
|
1072 using \<open>0 < r\<close> by (simp_all add: ball_subset_ball_iff cball_subset_ball_iff w) |
|
1073 with subS have wr4_sub: "ball w (r/4) \<subseteq> S" "cball w (r/4) \<subseteq> S" by force+ |
|
1074 moreover |
|
1075 have "(\<lambda>z. \<F> n z - g z) holomorphic_on S" |
|
1076 by (intro holomorphic_intros holf holg) |
|
1077 ultimately have hol: "(\<lambda>z. \<F> n z - g z) holomorphic_on ball w (r/4)" |
|
1078 and cont: "continuous_on (cball w (r / 4)) (\<lambda>z. \<F> n z - g z)" |
|
1079 using holomorphic_on_subset by (blast intro: holomorphic_on_imp_continuous_on)+ |
|
1080 have "w \<in> S" |
|
1081 using \<open>0 < r\<close> wr4_sub by auto |
|
1082 have "\<And>y. dist w y < r / 4 \<Longrightarrow> dist z0 y \<le> 3 * r / 4" |
|
1083 apply (rule dist_triangle_le [where z=w]) |
|
1084 using w by (simp add: dist_commute) |
|
1085 with e8 have in_ball: "\<And>y. y \<in> ball w (r/4) \<Longrightarrow> \<F> n y - g y \<in> ball 0 (r/4 * e/2)" |
|
1086 by (simp add: dist_norm [symmetric]) |
|
1087 have "\<F> n field_differentiable at w" |
|
1088 by (metis holomorphic_on_imp_differentiable_at \<open>w \<in> S\<close> holf \<open>open S\<close>) |
|
1089 moreover |
|
1090 have "g field_differentiable at w" |
|
1091 using \<open>w \<in> S\<close> \<open>open S\<close> holg holomorphic_on_imp_differentiable_at by auto |
|
1092 moreover |
|
1093 have "cmod (deriv (\<lambda>w. \<F> n w - g w) w) * 2 \<le> e" |
|
1094 apply (rule Cauchy_higher_deriv_bound [OF hol cont in_ball, of 1, simplified]) |
|
1095 using \<open>r > 0\<close> by auto |
|
1096 ultimately have "dist (deriv (\<F> n) w) (deriv g w) \<le> e/2" |
|
1097 by (simp add: dist_norm) |
|
1098 then show ?thesis |
|
1099 using \<open>e > 0\<close> by auto |
|
1100 qed |
|
1101 have "cball z0 (3 * r / 4) \<subseteq> ball z0 r" |
|
1102 by (simp add: cball_subset_ball_iff \<open>0 < r\<close>) |
|
1103 with subS have "uniform_limit (cball z0 (3 * r/4)) \<F> g sequentially" |
|
1104 by (force intro: ul_g) |
|
1105 then have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>cball z0 (3 * r / 4). dist (\<F> n x) (g x) < r / 4 * e / 2" |
|
1106 using \<open>0 < e\<close> \<open>0 < r\<close> by (force simp: intro!: uniform_limitD) |
|
1107 then show "\<forall>\<^sub>F n in sequentially. \<forall>x \<in> sphere z0 (r/2). dist (deriv (\<F> n) x) (deriv g x) < e" |
|
1108 apply (simp add: eventually_sequentially) |
|
1109 apply (elim ex_forward all_forward imp_forward asm_rl) |
|
1110 using * apply (force simp: dist_commute) |
|
1111 done |
|
1112 qed |
|
1113 show "uniform_limit (sphere z0 (r/2)) \<F> g sequentially" |
|
1114 proof (rule uniform_limitI) |
|
1115 fix e::real |
|
1116 assume "0 < e" |
|
1117 have "sphere z0 (r/2) \<subseteq> ball z0 r" |
|
1118 using \<open>0 < r\<close> by auto |
|
1119 with subS have "uniform_limit (sphere z0 (r/2)) \<F> g sequentially" |
|
1120 by (force intro: ul_g) |
|
1121 then show "\<forall>\<^sub>F n in sequentially. \<forall>x \<in> sphere z0 (r/2). dist (\<F> n x) (g x) < e" |
|
1122 apply (rule uniform_limitD) |
|
1123 using \<open>0 < e\<close> by force |
|
1124 qed |
|
1125 show "b > 0" "\<And>x. x \<in> sphere z0 (r/2) \<Longrightarrow> b \<le> cmod (g x)" |
|
1126 using b \<open>0 < r\<close> by (fastforce simp: geq hnz)+ |
|
1127 qed |
|
1128 qed (use \<open>0 < r\<close> in auto) |
|
1129 then have "(\<lambda>n. 0) \<longlonglongrightarrow> contour_integral (circlepath z0 (r/2)) (\<lambda>z. deriv g z / g z)" |
|
1130 by (simp add: contour_integral_unique [OF *]) |
|
1131 then have "contour_integral (circlepath z0 (r/2)) (\<lambda>z. deriv g z / g z) = 0" |
|
1132 by (simp add: LIMSEQ_const_iff) |
|
1133 moreover |
|
1134 have "contour_integral (circlepath z0 (r/2)) (\<lambda>z. deriv g z / g z) = |
|
1135 contour_integral (circlepath z0 (r/2)) (\<lambda>z. m / (z - z0) + deriv h z / h z)" |
|
1136 proof (rule contour_integral_eq, use \<open>0 < r\<close> in simp) |
|
1137 fix w |
|
1138 assume w: "dist z0 w * 2 = r" |
|
1139 then have w_inb: "w \<in> ball z0 r" |
|
1140 using \<open>0 < r\<close> by auto |
|
1141 have h_der: "(h has_field_derivative deriv h w) (at w)" |
|
1142 using holh holomorphic_derivI w_inb by blast |
|
1143 have "deriv g w = ((of_nat m * h w + deriv h w * (w - z0)) * (w - z0) ^ m) / (w - z0)" |
|
1144 if "r = dist z0 w * 2" "w \<noteq> z0" |
|
1145 proof - |
|
1146 have "((\<lambda>w. (w - z0) ^ m * h w) has_field_derivative |
|
1147 (m * h w + deriv h w * (w - z0)) * (w - z0) ^ m / (w - z0)) (at w)" |
|
1148 apply (rule derivative_eq_intros h_der refl)+ |
|
1149 using that \<open>m > 0\<close> \<open>0 < r\<close> apply (simp add: divide_simps distrib_right) |
|
1150 apply (metis Suc_pred mult.commute power_Suc) |
|
1151 done |
|
1152 then show ?thesis |
|
1153 apply (rule DERIV_imp_deriv [OF has_field_derivative_transform_within_open [where S = "ball z0 r"]]) |
|
1154 using that \<open>m > 0\<close> \<open>0 < r\<close> |
|
1155 apply (simp_all add: hnz geq) |
|
1156 done |
|
1157 qed |
|
1158 with \<open>0 < r\<close> \<open>0 < m\<close> w w_inb show "deriv g w / g w = of_nat m / (w - z0) + deriv h w / h w" |
|
1159 by (auto simp: geq field_split_simps hnz) |
|
1160 qed |
|
1161 moreover |
|
1162 have "contour_integral (circlepath z0 (r/2)) (\<lambda>z. m / (z - z0) + deriv h z / h z) = |
|
1163 2 * of_real pi * \<i> * m + 0" |
|
1164 proof (rule contour_integral_unique [OF has_contour_integral_add]) |
|
1165 show "((\<lambda>x. m / (x - z0)) has_contour_integral 2 * of_real pi * \<i> * m) (circlepath z0 (r/2))" |
|
1166 by (force simp: \<open>0 < r\<close> intro: Cauchy_integral_circlepath_simple) |
|
1167 show "((\<lambda>x. deriv h x / h x) has_contour_integral 0) (circlepath z0 (r/2))" |
|
1168 apply (rule Cauchy_theorem_disc_simple [of _ z0 r]) |
|
1169 using hnz holh holomorphic_deriv holomorphic_on_divide \<open>0 < r\<close> |
|
1170 apply force+ |
|
1171 done |
|
1172 qed |
|
1173 ultimately show False using \<open>0 < m\<close> by auto |
|
1174 qed |
|
1175 |
|
1176 corollary Hurwitz_injective: |
|
1177 assumes S: "open S" "connected S" |
|
1178 and holf: "\<And>n::nat. \<F> n holomorphic_on S" |
|
1179 and holg: "g holomorphic_on S" |
|
1180 and ul_g: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K \<F> g sequentially" |
|
1181 and nonconst: "\<not> g constant_on S" |
|
1182 and inj: "\<And>n. inj_on (\<F> n) S" |
|
1183 shows "inj_on g S" |
|
1184 proof - |
|
1185 have False if z12: "z1 \<in> S" "z2 \<in> S" "z1 \<noteq> z2" "g z2 = g z1" for z1 z2 |
|
1186 proof - |
|
1187 obtain z0 where "z0 \<in> S" and z0: "g z0 \<noteq> g z2" |
|
1188 using constant_on_def nonconst by blast |
|
1189 have "(\<lambda>z. g z - g z1) holomorphic_on S" |
|
1190 by (intro holomorphic_intros holg) |
|
1191 then obtain r where "0 < r" "ball z2 r \<subseteq> S" "\<And>z. dist z2 z < r \<and> z \<noteq> z2 \<Longrightarrow> g z \<noteq> g z1" |
|
1192 apply (rule isolated_zeros [of "\<lambda>z. g z - g z1" S z2 z0]) |
|
1193 using S \<open>z0 \<in> S\<close> z0 z12 by auto |
|
1194 have "g z2 - g z1 \<noteq> 0" |
|
1195 proof (rule Hurwitz_no_zeros [of "S - {z1}" "\<lambda>n z. \<F> n z - \<F> n z1" "\<lambda>z. g z - g z1"]) |
|
1196 show "open (S - {z1})" |
|
1197 by (simp add: S open_delete) |
|
1198 show "connected (S - {z1})" |
|
1199 by (simp add: connected_open_delete [OF S]) |
|
1200 show "\<And>n. (\<lambda>z. \<F> n z - \<F> n z1) holomorphic_on S - {z1}" |
|
1201 by (intro holomorphic_intros holomorphic_on_subset [OF holf]) blast |
|
1202 show "(\<lambda>z. g z - g z1) holomorphic_on S - {z1}" |
|
1203 by (intro holomorphic_intros holomorphic_on_subset [OF holg]) blast |
|
1204 show "uniform_limit K (\<lambda>n z. \<F> n z - \<F> n z1) (\<lambda>z. g z - g z1) sequentially" |
|
1205 if "compact K" "K \<subseteq> S - {z1}" for K |
|
1206 proof (rule uniform_limitI) |
|
1207 fix e::real |
|
1208 assume "e > 0" |
|
1209 have "uniform_limit K \<F> g sequentially" |
|
1210 using that ul_g by fastforce |
|
1211 then have K: "\<forall>\<^sub>F n in sequentially. \<forall>x \<in> K. dist (\<F> n x) (g x) < e/2" |
|
1212 using \<open>0 < e\<close> by (force simp: intro!: uniform_limitD) |
|
1213 have "uniform_limit {z1} \<F> g sequentially" |
|
1214 by (simp add: ul_g z12) |
|
1215 then have "\<forall>\<^sub>F n in sequentially. \<forall>x \<in> {z1}. dist (\<F> n x) (g x) < e/2" |
|
1216 using \<open>0 < e\<close> by (force simp: intro!: uniform_limitD) |
|
1217 then have z1: "\<forall>\<^sub>F n in sequentially. dist (\<F> n z1) (g z1) < e/2" |
|
1218 by simp |
|
1219 have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e/2 + e/2" |
|
1220 apply (rule eventually_mono [OF eventually_conj [OF K z1]]) |
|
1221 apply (simp add: dist_norm algebra_simps del: divide_const_simps) |
|
1222 by (metis add.commute dist_commute dist_norm dist_triangle_add_half) |
|
1223 have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e/2 + e/2" |
|
1224 using eventually_conj [OF K z1] |
|
1225 apply (rule eventually_mono) |
|
1226 by (metis (no_types, hide_lams) diff_add_eq diff_diff_eq2 dist_commute dist_norm dist_triangle_add_half field_sum_of_halves) |
|
1227 then |
|
1228 show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e" |
|
1229 by simp |
|
1230 qed |
|
1231 show "\<not> (\<lambda>z. g z - g z1) constant_on S - {z1}" |
|
1232 unfolding constant_on_def |
|
1233 by (metis Diff_iff \<open>z0 \<in> S\<close> empty_iff insert_iff right_minus_eq z0 z12) |
|
1234 show "\<And>n z. z \<in> S - {z1} \<Longrightarrow> \<F> n z - \<F> n z1 \<noteq> 0" |
|
1235 by (metis DiffD1 DiffD2 eq_iff_diff_eq_0 inj inj_onD insertI1 \<open>z1 \<in> S\<close>) |
|
1236 show "z2 \<in> S - {z1}" |
|
1237 using \<open>z2 \<in> S\<close> \<open>z1 \<noteq> z2\<close> by auto |
|
1238 qed |
|
1239 with z12 show False by auto |
|
1240 qed |
|
1241 then show ?thesis by (auto simp: inj_on_def) |
|
1242 qed |
|
1243 |
|
1244 |
|
1245 |
|
1246 subsection\<open>The Great Picard theorem\<close> |
|
1247 |
|
1248 lemma GPicard1: |
|
1249 assumes S: "open S" "connected S" and "w \<in> S" "0 < r" "Y \<subseteq> X" |
|
1250 and holX: "\<And>h. h \<in> X \<Longrightarrow> h holomorphic_on S" |
|
1251 and X01: "\<And>h z. \<lbrakk>h \<in> X; z \<in> S\<rbrakk> \<Longrightarrow> h z \<noteq> 0 \<and> h z \<noteq> 1" |
|
1252 and r: "\<And>h. h \<in> Y \<Longrightarrow> norm(h w) \<le> r" |
|
1253 obtains B Z where "0 < B" "open Z" "w \<in> Z" "Z \<subseteq> S" "\<And>h z. \<lbrakk>h \<in> Y; z \<in> Z\<rbrakk> \<Longrightarrow> norm(h z) \<le> B" |
|
1254 proof - |
|
1255 obtain e where "e > 0" and e: "cball w e \<subseteq> S" |
|
1256 using assms open_contains_cball_eq by blast |
|
1257 show ?thesis |
|
1258 proof |
|
1259 show "0 < exp(pi * exp(pi * (2 + 2 * r + 12)))" |
|
1260 by simp |
|
1261 show "ball w (e / 2) \<subseteq> S" |
|
1262 using e ball_divide_subset_numeral ball_subset_cball by blast |
|
1263 show "cmod (h z) \<le> exp (pi * exp (pi * (2 + 2 * r + 12)))" |
|
1264 if "h \<in> Y" "z \<in> ball w (e / 2)" for h z |
|
1265 proof - |
|
1266 have "h \<in> X" |
|
1267 using \<open>Y \<subseteq> X\<close> \<open>h \<in> Y\<close> by blast |
|
1268 with holX have "h holomorphic_on S" |
|
1269 by auto |
|
1270 then have "h holomorphic_on cball w e" |
|
1271 by (metis e holomorphic_on_subset) |
|
1272 then have hol_h_o: "(h \<circ> (\<lambda>z. (w + of_real e * z))) holomorphic_on cball 0 1" |
|
1273 apply (intro holomorphic_intros holomorphic_on_compose) |
|
1274 apply (erule holomorphic_on_subset) |
|
1275 using that \<open>e > 0\<close> by (auto simp: dist_norm norm_mult) |
|
1276 have norm_le_r: "cmod ((h \<circ> (\<lambda>z. w + complex_of_real e * z)) 0) \<le> r" |
|
1277 by (auto simp: r \<open>h \<in> Y\<close>) |
|
1278 have le12: "norm (of_real(inverse e) * (z - w)) \<le> 1/2" |
|
1279 using that \<open>e > 0\<close> by (simp add: inverse_eq_divide dist_norm norm_minus_commute norm_divide) |
|
1280 have non01: "\<And>z::complex. cmod z \<le> 1 \<Longrightarrow> h (w + e * z) \<noteq> 0 \<and> h (w + e * z) \<noteq> 1" |
|
1281 apply (rule X01 [OF \<open>h \<in> X\<close>]) |
|
1282 apply (rule subsetD [OF e]) |
|
1283 using \<open>0 < e\<close> by (auto simp: dist_norm norm_mult) |
|
1284 have "cmod (h z) \<le> cmod (h (w + of_real e * (inverse e * (z - w))))" |
|
1285 using \<open>0 < e\<close> by (simp add: field_split_simps) |
|
1286 also have "... \<le> exp (pi * exp (pi * (14 + 2 * r)))" |
|
1287 using r [OF \<open>h \<in> Y\<close>] Schottky [OF hol_h_o norm_le_r _ _ _ le12] non01 by auto |
|
1288 finally |
|
1289 show ?thesis by simp |
|
1290 qed |
|
1291 qed (use \<open>e > 0\<close> in auto) |
|
1292 qed |
|
1293 |
|
1294 lemma GPicard2: |
|
1295 assumes "S \<subseteq> T" "connected T" "S \<noteq> {}" "open S" "\<And>x. \<lbrakk>x islimpt S; x \<in> T\<rbrakk> \<Longrightarrow> x \<in> S" |
|
1296 shows "S = T" |
|
1297 by (metis assms open_subset connected_clopen closedin_limpt) |
|
1298 |
|
1299 |
|
1300 lemma GPicard3: |
|
1301 assumes S: "open S" "connected S" "w \<in> S" and "Y \<subseteq> X" |
|
1302 and holX: "\<And>h. h \<in> X \<Longrightarrow> h holomorphic_on S" |
|
1303 and X01: "\<And>h z. \<lbrakk>h \<in> X; z \<in> S\<rbrakk> \<Longrightarrow> h z \<noteq> 0 \<and> h z \<noteq> 1" |
|
1304 and no_hw_le1: "\<And>h. h \<in> Y \<Longrightarrow> norm(h w) \<le> 1" |
|
1305 and "compact K" "K \<subseteq> S" |
|
1306 obtains B where "\<And>h z. \<lbrakk>h \<in> Y; z \<in> K\<rbrakk> \<Longrightarrow> norm(h z) \<le> B" |
|
1307 proof - |
|
1308 define U where "U \<equiv> {z \<in> S. \<exists>B Z. 0 < B \<and> open Z \<and> z \<in> Z \<and> Z \<subseteq> S \<and> |
|
1309 (\<forall>h z'. h \<in> Y \<and> z' \<in> Z \<longrightarrow> norm(h z') \<le> B)}" |
|
1310 then have "U \<subseteq> S" by blast |
|
1311 have "U = S" |
|
1312 proof (rule GPicard2 [OF \<open>U \<subseteq> S\<close> \<open>connected S\<close>]) |
|
1313 show "U \<noteq> {}" |
|
1314 proof - |
|
1315 obtain B Z where "0 < B" "open Z" "w \<in> Z" "Z \<subseteq> S" |
|
1316 and "\<And>h z. \<lbrakk>h \<in> Y; z \<in> Z\<rbrakk> \<Longrightarrow> norm(h z) \<le> B" |
|
1317 apply (rule GPicard1 [OF S zero_less_one \<open>Y \<subseteq> X\<close> holX]) |
|
1318 using no_hw_le1 X01 by force+ |
|
1319 then show ?thesis |
|
1320 unfolding U_def using \<open>w \<in> S\<close> by blast |
|
1321 qed |
|
1322 show "open U" |
|
1323 unfolding open_subopen [of U] by (auto simp: U_def) |
|
1324 fix v |
|
1325 assume v: "v islimpt U" "v \<in> S" |
|
1326 have "\<not> (\<forall>r>0. \<exists>h\<in>Y. r < cmod (h v))" |
|
1327 proof |
|
1328 assume "\<forall>r>0. \<exists>h\<in>Y. r < cmod (h v)" |
|
1329 then have "\<forall>n. \<exists>h\<in>Y. Suc n < cmod (h v)" |
|
1330 by simp |
|
1331 then obtain \<F> where FY: "\<And>n. \<F> n \<in> Y" and ltF: "\<And>n. Suc n < cmod (\<F> n v)" |
|
1332 by metis |
|
1333 define \<G> where "\<G> \<equiv> \<lambda>n z. inverse(\<F> n z)" |
|
1334 have hol\<G>: "\<G> n holomorphic_on S" for n |
|
1335 apply (simp add: \<G>_def) |
|
1336 using FY X01 \<open>Y \<subseteq> X\<close> holX apply (blast intro: holomorphic_on_inverse) |
|
1337 done |
|
1338 have \<G>not0: "\<G> n z \<noteq> 0" and \<G>not1: "\<G> n z \<noteq> 1" if "z \<in> S" for n z |
|
1339 using FY X01 \<open>Y \<subseteq> X\<close> that by (force simp: \<G>_def)+ |
|
1340 have \<G>_le1: "cmod (\<G> n v) \<le> 1" for n |
|
1341 using less_le_trans linear ltF |
|
1342 by (fastforce simp add: \<G>_def norm_inverse inverse_le_1_iff) |
|
1343 define W where "W \<equiv> {h. h holomorphic_on S \<and> (\<forall>z \<in> S. h z \<noteq> 0 \<and> h z \<noteq> 1)}" |
|
1344 obtain B Z where "0 < B" "open Z" "v \<in> Z" "Z \<subseteq> S" |
|
1345 and B: "\<And>h z. \<lbrakk>h \<in> range \<G>; z \<in> Z\<rbrakk> \<Longrightarrow> norm(h z) \<le> B" |
|
1346 apply (rule GPicard1 [OF \<open>open S\<close> \<open>connected S\<close> \<open>v \<in> S\<close> zero_less_one, of "range \<G>" W]) |
|
1347 using hol\<G> \<G>not0 \<G>not1 \<G>_le1 by (force simp: W_def)+ |
|
1348 then obtain e where "e > 0" and e: "ball v e \<subseteq> Z" |
|
1349 by (meson open_contains_ball) |
|
1350 obtain h j where holh: "h holomorphic_on ball v e" and "strict_mono j" |
|
1351 and lim: "\<And>x. x \<in> ball v e \<Longrightarrow> (\<lambda>n. \<G> (j n) x) \<longlonglongrightarrow> h x" |
|
1352 and ulim: "\<And>K. \<lbrakk>compact K; K \<subseteq> ball v e\<rbrakk> |
|
1353 \<Longrightarrow> uniform_limit K (\<G> \<circ> j) h sequentially" |
|
1354 proof (rule Montel) |
|
1355 show "\<And>h. h \<in> range \<G> \<Longrightarrow> h holomorphic_on ball v e" |
|
1356 by (metis \<open>Z \<subseteq> S\<close> e hol\<G> holomorphic_on_subset imageE) |
|
1357 show "\<And>K. \<lbrakk>compact K; K \<subseteq> ball v e\<rbrakk> \<Longrightarrow> \<exists>B. \<forall>h\<in>range \<G>. \<forall>z\<in>K. cmod (h z) \<le> B" |
|
1358 using B e by blast |
|
1359 qed auto |
|
1360 have "h v = 0" |
|
1361 proof (rule LIMSEQ_unique) |
|
1362 show "(\<lambda>n. \<G> (j n) v) \<longlonglongrightarrow> h v" |
|
1363 using \<open>e > 0\<close> lim by simp |
|
1364 have lt_Fj: "real x \<le> cmod (\<F> (j x) v)" for x |
|
1365 by (metis of_nat_Suc ltF \<open>strict_mono j\<close> add.commute less_eq_real_def less_le_trans nat_le_real_less seq_suble) |
|
1366 show "(\<lambda>n. \<G> (j n) v) \<longlonglongrightarrow> 0" |
|
1367 proof (rule Lim_null_comparison [OF eventually_sequentiallyI lim_inverse_n]) |
|
1368 show "cmod (\<G> (j x) v) \<le> inverse (real x)" if "1 \<le> x" for x |
|
1369 using that by (simp add: \<G>_def norm_inverse_le_norm [OF lt_Fj]) |
|
1370 qed |
|
1371 qed |
|
1372 have "h v \<noteq> 0" |
|
1373 proof (rule Hurwitz_no_zeros [of "ball v e" "\<G> \<circ> j" h]) |
|
1374 show "\<And>n. (\<G> \<circ> j) n holomorphic_on ball v e" |
|
1375 using \<open>Z \<subseteq> S\<close> e hol\<G> by force |
|
1376 show "\<And>n z. z \<in> ball v e \<Longrightarrow> (\<G> \<circ> j) n z \<noteq> 0" |
|
1377 using \<G>not0 \<open>Z \<subseteq> S\<close> e by fastforce |
|
1378 show "\<not> h constant_on ball v e" |
|
1379 proof (clarsimp simp: constant_on_def) |
|
1380 fix c |
|
1381 have False if "\<And>z. dist v z < e \<Longrightarrow> h z = c" |
|
1382 proof - |
|
1383 have "h v = c" |
|
1384 by (simp add: \<open>0 < e\<close> that) |
|
1385 obtain y where "y \<in> U" "y \<noteq> v" and y: "dist y v < e" |
|
1386 using v \<open>e > 0\<close> by (auto simp: islimpt_approachable) |
|
1387 then obtain C T where "y \<in> S" "C > 0" "open T" "y \<in> T" "T \<subseteq> S" |
|
1388 and "\<And>h z'. \<lbrakk>h \<in> Y; z' \<in> T\<rbrakk> \<Longrightarrow> cmod (h z') \<le> C" |
|
1389 using \<open>y \<in> U\<close> by (auto simp: U_def) |
|
1390 then have le_C: "\<And>n. cmod (\<F> n y) \<le> C" |
|
1391 using FY by blast |
|
1392 have "\<forall>\<^sub>F n in sequentially. dist (\<G> (j n) y) (h y) < inverse C" |
|
1393 using uniform_limitD [OF ulim [of "{y}"], of "inverse C"] \<open>C > 0\<close> y |
|
1394 by (simp add: dist_commute) |
|
1395 then obtain n where "dist (\<G> (j n) y) (h y) < inverse C" |
|
1396 by (meson eventually_at_top_linorder order_refl) |
|
1397 moreover |
|
1398 have "h y = h v" |
|
1399 by (metis \<open>h v = c\<close> dist_commute that y) |
|
1400 ultimately have "norm (\<G> (j n) y) < inverse C" |
|
1401 by (simp add: \<open>h v = 0\<close>) |
|
1402 then have "C < norm (\<F> (j n) y)" |
|
1403 apply (simp add: \<G>_def) |
|
1404 by (metis FY X01 \<open>0 < C\<close> \<open>y \<in> S\<close> \<open>Y \<subseteq> X\<close> inverse_less_iff_less norm_inverse subsetD zero_less_norm_iff) |
|
1405 show False |
|
1406 using \<open>C < cmod (\<F> (j n) y)\<close> le_C not_less by blast |
|
1407 qed |
|
1408 then show "\<exists>x\<in>ball v e. h x \<noteq> c" by force |
|
1409 qed |
|
1410 show "h holomorphic_on ball v e" |
|
1411 by (simp add: holh) |
|
1412 show "\<And>K. \<lbrakk>compact K; K \<subseteq> ball v e\<rbrakk> \<Longrightarrow> uniform_limit K (\<G> \<circ> j) h sequentially" |
|
1413 by (simp add: ulim) |
|
1414 qed (use \<open>e > 0\<close> in auto) |
|
1415 with \<open>h v = 0\<close> show False by blast |
|
1416 qed |
|
1417 then show "v \<in> U" |
|
1418 apply (clarsimp simp add: U_def v) |
|
1419 apply (rule GPicard1[OF \<open>open S\<close> \<open>connected S\<close> \<open>v \<in> S\<close> _ \<open>Y \<subseteq> X\<close> holX]) |
|
1420 using X01 no_hw_le1 apply (meson | force simp: not_less)+ |
|
1421 done |
|
1422 qed |
|
1423 have "\<And>x. x \<in> K \<longrightarrow> x \<in> U" |
|
1424 using \<open>U = S\<close> \<open>K \<subseteq> S\<close> by blast |
|
1425 then have "\<And>x. x \<in> K \<longrightarrow> (\<exists>B Z. 0 < B \<and> open Z \<and> x \<in> Z \<and> |
|
1426 (\<forall>h z'. h \<in> Y \<and> z' \<in> Z \<longrightarrow> norm(h z') \<le> B))" |
|
1427 unfolding U_def by blast |
|
1428 then obtain F Z where F: "\<And>x. x \<in> K \<Longrightarrow> open (Z x) \<and> x \<in> Z x \<and> |
|
1429 (\<forall>h z'. h \<in> Y \<and> z' \<in> Z x \<longrightarrow> norm(h z') \<le> F x)" |
|
1430 by metis |
|
1431 then obtain L where "L \<subseteq> K" "finite L" and L: "K \<subseteq> (\<Union>c \<in> L. Z c)" |
|
1432 by (auto intro: compactE_image [OF \<open>compact K\<close>, of K Z]) |
|
1433 then have *: "\<And>x h z'. \<lbrakk>x \<in> L; h \<in> Y \<and> z' \<in> Z x\<rbrakk> \<Longrightarrow> cmod (h z') \<le> F x" |
|
1434 using F by blast |
|
1435 have "\<exists>B. \<forall>h z. h \<in> Y \<and> z \<in> K \<longrightarrow> norm(h z) \<le> B" |
|
1436 proof (cases "L = {}") |
|
1437 case True with L show ?thesis by simp |
|
1438 next |
|
1439 case False |
|
1440 with \<open>finite L\<close> show ?thesis |
|
1441 apply (rule_tac x = "Max (F ` L)" in exI) |
|
1442 apply (simp add: linorder_class.Max_ge_iff) |
|
1443 using * F by (metis L UN_E subsetD) |
|
1444 qed |
|
1445 with that show ?thesis by metis |
|
1446 qed |
|
1447 |
|
1448 |
|
1449 lemma GPicard4: |
|
1450 assumes "0 < k" and holf: "f holomorphic_on (ball 0 k - {0})" |
|
1451 and AE: "\<And>e. \<lbrakk>0 < e; e < k\<rbrakk> \<Longrightarrow> \<exists>d. 0 < d \<and> d < e \<and> (\<forall>z \<in> sphere 0 d. norm(f z) \<le> B)" |
|
1452 obtains \<epsilon> where "0 < \<epsilon>" "\<epsilon> < k" "\<And>z. z \<in> ball 0 \<epsilon> - {0} \<Longrightarrow> norm(f z) \<le> B" |
|
1453 proof - |
|
1454 obtain \<epsilon> where "0 < \<epsilon>" "\<epsilon> < k/2" and \<epsilon>: "\<And>z. norm z = \<epsilon> \<Longrightarrow> norm(f z) \<le> B" |
|
1455 using AE [of "k/2"] \<open>0 < k\<close> by auto |
|
1456 show ?thesis |
|
1457 proof |
|
1458 show "\<epsilon> < k" |
|
1459 using \<open>0 < k\<close> \<open>\<epsilon> < k/2\<close> by auto |
|
1460 show "cmod (f \<xi>) \<le> B" if \<xi>: "\<xi> \<in> ball 0 \<epsilon> - {0}" for \<xi> |
|
1461 proof - |
|
1462 obtain d where "0 < d" "d < norm \<xi>" and d: "\<And>z. norm z = d \<Longrightarrow> norm(f z) \<le> B" |
|
1463 using AE [of "norm \<xi>"] \<open>\<epsilon> < k\<close> \<xi> by auto |
|
1464 have [simp]: "closure (cball 0 \<epsilon> - ball 0 d) = cball 0 \<epsilon> - ball 0 d" |
|
1465 by (blast intro!: closure_closed) |
|
1466 have [simp]: "interior (cball 0 \<epsilon> - ball 0 d) = ball 0 \<epsilon> - cball (0::complex) d" |
|
1467 using \<open>0 < \<epsilon>\<close> \<open>0 < d\<close> by (simp add: interior_diff) |
|
1468 have *: "norm(f w) \<le> B" if "w \<in> cball 0 \<epsilon> - ball 0 d" for w |
|
1469 proof (rule maximum_modulus_frontier [of f "cball 0 \<epsilon> - ball 0 d"]) |
|
1470 show "f holomorphic_on interior (cball 0 \<epsilon> - ball 0 d)" |
|
1471 apply (rule holomorphic_on_subset [OF holf]) |
|
1472 using \<open>\<epsilon> < k\<close> \<open>0 < d\<close> that by auto |
|
1473 show "continuous_on (closure (cball 0 \<epsilon> - ball 0 d)) f" |
|
1474 apply (rule holomorphic_on_imp_continuous_on) |
|
1475 apply (rule holomorphic_on_subset [OF holf]) |
|
1476 using \<open>0 < d\<close> \<open>\<epsilon> < k\<close> by auto |
|
1477 show "\<And>z. z \<in> frontier (cball 0 \<epsilon> - ball 0 d) \<Longrightarrow> cmod (f z) \<le> B" |
|
1478 apply (simp add: frontier_def) |
|
1479 using \<epsilon> d less_eq_real_def by blast |
|
1480 qed (use that in auto) |
|
1481 show ?thesis |
|
1482 using * \<open>d < cmod \<xi>\<close> that by auto |
|
1483 qed |
|
1484 qed (use \<open>0 < \<epsilon>\<close> in auto) |
|
1485 qed |
|
1486 |
|
1487 |
|
1488 lemma GPicard5: |
|
1489 assumes holf: "f holomorphic_on (ball 0 1 - {0})" |
|
1490 and f01: "\<And>z. z \<in> ball 0 1 - {0} \<Longrightarrow> f z \<noteq> 0 \<and> f z \<noteq> 1" |
|
1491 obtains e B where "0 < e" "e < 1" "0 < B" |
|
1492 "(\<forall>z \<in> ball 0 e - {0}. norm(f z) \<le> B) \<or> |
|
1493 (\<forall>z \<in> ball 0 e - {0}. norm(f z) \<ge> B)" |
|
1494 proof - |
|
1495 have [simp]: "1 + of_nat n \<noteq> (0::complex)" for n |
|
1496 using of_nat_eq_0_iff by fastforce |
|
1497 have [simp]: "cmod (1 + of_nat n) = 1 + of_nat n" for n |
|
1498 by (metis norm_of_nat of_nat_Suc) |
|
1499 have *: "(\<lambda>x::complex. x / of_nat (Suc n)) ` (ball 0 1 - {0}) \<subseteq> ball 0 1 - {0}" for n |
|
1500 by (auto simp: norm_divide field_split_simps split: if_split_asm) |
|
1501 define h where "h \<equiv> \<lambda>n z::complex. f (z / (Suc n))" |
|
1502 have holh: "(h n) holomorphic_on ball 0 1 - {0}" for n |
|
1503 unfolding h_def |
|
1504 proof (rule holomorphic_on_compose_gen [unfolded o_def, OF _ holf *]) |
|
1505 show "(\<lambda>x. x / of_nat (Suc n)) holomorphic_on ball 0 1 - {0}" |
|
1506 by (intro holomorphic_intros) auto |
|
1507 qed |
|
1508 have h01: "\<And>n z. z \<in> ball 0 1 - {0} \<Longrightarrow> h n z \<noteq> 0 \<and> h n z \<noteq> 1" |
|
1509 unfolding h_def |
|
1510 apply (rule f01) |
|
1511 using * by force |
|
1512 obtain w where w: "w \<in> ball 0 1 - {0::complex}" |
|
1513 by (rule_tac w = "1/2" in that) auto |
|
1514 consider "infinite {n. norm(h n w) \<le> 1}" | "infinite {n. 1 \<le> norm(h n w)}" |
|
1515 by (metis (mono_tags, lifting) infinite_nat_iff_unbounded_le le_cases mem_Collect_eq) |
|
1516 then show ?thesis |
|
1517 proof cases |
|
1518 case 1 |
|
1519 with infinite_enumerate obtain r :: "nat \<Rightarrow> nat" |
|
1520 where "strict_mono r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<le> 1}" |
|
1521 by blast |
|
1522 obtain B where B: "\<And>j z. \<lbrakk>norm z = 1/2; j \<in> range (h \<circ> r)\<rbrakk> \<Longrightarrow> norm(j z) \<le> B" |
|
1523 proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"]) |
|
1524 show "range (h \<circ> r) \<subseteq> |
|
1525 {g. g holomorphic_on ball 0 1 - {0} \<and> (\<forall>z\<in>ball 0 1 - {0}. g z \<noteq> 0 \<and> g z \<noteq> 1)}" |
|
1526 apply clarsimp |
|
1527 apply (intro conjI holomorphic_intros holomorphic_on_compose holh) |
|
1528 using h01 apply auto |
|
1529 done |
|
1530 show "connected (ball 0 1 - {0::complex})" |
|
1531 by (simp add: connected_open_delete) |
|
1532 qed (use r in auto) |
|
1533 have normf_le_B: "cmod(f z) \<le> B" if "norm z = 1 / (2 * (1 + of_nat (r n)))" for z n |
|
1534 proof - |
|
1535 have *: "\<And>w. norm w = 1/2 \<Longrightarrow> cmod((f (w / (1 + of_nat (r n))))) \<le> B" |
|
1536 using B by (auto simp: h_def o_def) |
|
1537 have half: "norm (z * (1 + of_nat (r n))) = 1/2" |
|
1538 by (simp add: norm_mult divide_simps that) |
|
1539 show ?thesis |
|
1540 using * [OF half] by simp |
|
1541 qed |
|
1542 obtain \<epsilon> where "0 < \<epsilon>" "\<epsilon> < 1" "\<And>z. z \<in> ball 0 \<epsilon> - {0} \<Longrightarrow> cmod(f z) \<le> B" |
|
1543 proof (rule GPicard4 [OF zero_less_one holf, of B]) |
|
1544 fix e::real |
|
1545 assume "0 < e" "e < 1" |
|
1546 obtain n where "(1/e - 2) / 2 < real n" |
|
1547 using reals_Archimedean2 by blast |
|
1548 also have "... \<le> r n" |
|
1549 using \<open>strict_mono r\<close> by (simp add: seq_suble) |
|
1550 finally have "(1/e - 2) / 2 < real (r n)" . |
|
1551 with \<open>0 < e\<close> have e: "e > 1 / (2 + 2 * real (r n))" |
|
1552 by (simp add: field_simps) |
|
1553 show "\<exists>d>0. d < e \<and> (\<forall>z\<in>sphere 0 d. cmod (f z) \<le> B)" |
|
1554 apply (rule_tac x="1 / (2 * (1 + of_nat (r n)))" in exI) |
|
1555 using normf_le_B by (simp add: e) |
|
1556 qed blast |
|
1557 then have \<epsilon>: "cmod (f z) \<le> \<bar>B\<bar> + 1" if "cmod z < \<epsilon>" "z \<noteq> 0" for z |
|
1558 using that by fastforce |
|
1559 have "0 < \<bar>B\<bar> + 1" |
|
1560 by simp |
|
1561 then show ?thesis |
|
1562 apply (rule that [OF \<open>0 < \<epsilon>\<close> \<open>\<epsilon> < 1\<close>]) |
|
1563 using \<epsilon> by auto |
|
1564 next |
|
1565 case 2 |
|
1566 with infinite_enumerate obtain r :: "nat \<Rightarrow> nat" |
|
1567 where "strict_mono r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<ge> 1}" |
|
1568 by blast |
|
1569 obtain B where B: "\<And>j z. \<lbrakk>norm z = 1/2; j \<in> range (\<lambda>n. inverse \<circ> h (r n))\<rbrakk> \<Longrightarrow> norm(j z) \<le> B" |
|
1570 proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"]) |
|
1571 show "range (\<lambda>n. inverse \<circ> h (r n)) \<subseteq> |
|
1572 {g. g holomorphic_on ball 0 1 - {0} \<and> (\<forall>z\<in>ball 0 1 - {0}. g z \<noteq> 0 \<and> g z \<noteq> 1)}" |
|
1573 apply clarsimp |
|
1574 apply (intro conjI holomorphic_intros holomorphic_on_compose_gen [unfolded o_def, OF _ holh] holomorphic_on_compose) |
|
1575 using h01 apply auto |
|
1576 done |
|
1577 show "connected (ball 0 1 - {0::complex})" |
|
1578 by (simp add: connected_open_delete) |
|
1579 show "\<And>j. j \<in> range (\<lambda>n. inverse \<circ> h (r n)) \<Longrightarrow> cmod (j w) \<le> 1" |
|
1580 using r norm_inverse_le_norm by fastforce |
|
1581 qed (use r in auto) |
|
1582 have norm_if_le_B: "cmod(inverse (f z)) \<le> B" if "norm z = 1 / (2 * (1 + of_nat (r n)))" for z n |
|
1583 proof - |
|
1584 have *: "inverse (cmod((f (z / (1 + of_nat (r n)))))) \<le> B" if "norm z = 1/2" for z |
|
1585 using B [OF that] by (force simp: norm_inverse h_def) |
|
1586 have half: "norm (z * (1 + of_nat (r n))) = 1/2" |
|
1587 by (simp add: norm_mult divide_simps that) |
|
1588 show ?thesis |
|
1589 using * [OF half] by (simp add: norm_inverse) |
|
1590 qed |
|
1591 have hol_if: "(inverse \<circ> f) holomorphic_on (ball 0 1 - {0})" |
|
1592 by (metis (no_types, lifting) holf comp_apply f01 holomorphic_on_inverse holomorphic_transform) |
|
1593 obtain \<epsilon> where "0 < \<epsilon>" "\<epsilon> < 1" and leB: "\<And>z. z \<in> ball 0 \<epsilon> - {0} \<Longrightarrow> cmod((inverse \<circ> f) z) \<le> B" |
|
1594 proof (rule GPicard4 [OF zero_less_one hol_if, of B]) |
|
1595 fix e::real |
|
1596 assume "0 < e" "e < 1" |
|
1597 obtain n where "(1/e - 2) / 2 < real n" |
|
1598 using reals_Archimedean2 by blast |
|
1599 also have "... \<le> r n" |
|
1600 using \<open>strict_mono r\<close> by (simp add: seq_suble) |
|
1601 finally have "(1/e - 2) / 2 < real (r n)" . |
|
1602 with \<open>0 < e\<close> have e: "e > 1 / (2 + 2 * real (r n))" |
|
1603 by (simp add: field_simps) |
|
1604 show "\<exists>d>0. d < e \<and> (\<forall>z\<in>sphere 0 d. cmod ((inverse \<circ> f) z) \<le> B)" |
|
1605 apply (rule_tac x="1 / (2 * (1 + of_nat (r n)))" in exI) |
|
1606 using norm_if_le_B by (simp add: e) |
|
1607 qed blast |
|
1608 have \<epsilon>: "cmod (f z) \<ge> inverse B" and "B > 0" if "cmod z < \<epsilon>" "z \<noteq> 0" for z |
|
1609 proof - |
|
1610 have "inverse (cmod (f z)) \<le> B" |
|
1611 using leB that by (simp add: norm_inverse) |
|
1612 moreover |
|
1613 have "f z \<noteq> 0" |
|
1614 using \<open>\<epsilon> < 1\<close> f01 that by auto |
|
1615 ultimately show "cmod (f z) \<ge> inverse B" |
|
1616 by (simp add: norm_inverse inverse_le_imp_le) |
|
1617 show "B > 0" |
|
1618 using \<open>f z \<noteq> 0\<close> \<open>inverse (cmod (f z)) \<le> B\<close> not_le order.trans by fastforce |
|
1619 qed |
|
1620 then have "B > 0" |
|
1621 by (metis \<open>0 < \<epsilon>\<close> dense leI order.asym vector_choose_size) |
|
1622 then have "inverse B > 0" |
|
1623 by (simp add: field_split_simps) |
|
1624 then show ?thesis |
|
1625 apply (rule that [OF \<open>0 < \<epsilon>\<close> \<open>\<epsilon> < 1\<close>]) |
|
1626 using \<epsilon> by auto |
|
1627 qed |
|
1628 qed |
|
1629 |
|
1630 |
|
1631 lemma GPicard6: |
|
1632 assumes "open M" "z \<in> M" "a \<noteq> 0" and holf: "f holomorphic_on (M - {z})" |
|
1633 and f0a: "\<And>w. w \<in> M - {z} \<Longrightarrow> f w \<noteq> 0 \<and> f w \<noteq> a" |
|
1634 obtains r where "0 < r" "ball z r \<subseteq> M" |
|
1635 "bounded(f ` (ball z r - {z})) \<or> |
|
1636 bounded((inverse \<circ> f) ` (ball z r - {z}))" |
|
1637 proof - |
|
1638 obtain r where "0 < r" and r: "ball z r \<subseteq> M" |
|
1639 using assms openE by blast |
|
1640 let ?g = "\<lambda>w. f (z + of_real r * w) / a" |
|
1641 obtain e B where "0 < e" "e < 1" "0 < B" |
|
1642 and B: "(\<forall>z \<in> ball 0 e - {0}. norm(?g z) \<le> B) \<or> (\<forall>z \<in> ball 0 e - {0}. norm(?g z) \<ge> B)" |
|
1643 proof (rule GPicard5) |
|
1644 show "?g holomorphic_on ball 0 1 - {0}" |
|
1645 apply (intro holomorphic_intros holomorphic_on_compose_gen [unfolded o_def, OF _ holf]) |
|
1646 using \<open>0 < r\<close> \<open>a \<noteq> 0\<close> r |
|
1647 by (auto simp: dist_norm norm_mult subset_eq) |
|
1648 show "\<And>w. w \<in> ball 0 1 - {0} \<Longrightarrow> f (z + of_real r * w) / a \<noteq> 0 \<and> f (z + of_real r * w) / a \<noteq> 1" |
|
1649 apply (simp add: field_split_simps \<open>a \<noteq> 0\<close>) |
|
1650 apply (rule f0a) |
|
1651 using \<open>0 < r\<close> r by (auto simp: dist_norm norm_mult subset_eq) |
|
1652 qed |
|
1653 show ?thesis |
|
1654 proof |
|
1655 show "0 < e*r" |
|
1656 by (simp add: \<open>0 < e\<close> \<open>0 < r\<close>) |
|
1657 have "ball z (e * r) \<subseteq> ball z r" |
|
1658 by (simp add: \<open>0 < r\<close> \<open>e < 1\<close> order.strict_implies_order subset_ball) |
|
1659 then show "ball z (e * r) \<subseteq> M" |
|
1660 using r by blast |
|
1661 consider "\<And>z. z \<in> ball 0 e - {0} \<Longrightarrow> norm(?g z) \<le> B" | "\<And>z. z \<in> ball 0 e - {0} \<Longrightarrow> norm(?g z) \<ge> B" |
|
1662 using B by blast |
|
1663 then show "bounded (f ` (ball z (e * r) - {z})) \<or> |
|
1664 bounded ((inverse \<circ> f) ` (ball z (e * r) - {z}))" |
|
1665 proof cases |
|
1666 case 1 |
|
1667 have "\<lbrakk>dist z w < e * r; w \<noteq> z\<rbrakk> \<Longrightarrow> cmod (f w) \<le> B * norm a" for w |
|
1668 using \<open>a \<noteq> 0\<close> \<open>0 < r\<close> 1 [of "(w - z) / r"] |
|
1669 by (simp add: norm_divide dist_norm field_split_simps) |
|
1670 then show ?thesis |
|
1671 by (force simp: intro!: boundedI) |
|
1672 next |
|
1673 case 2 |
|
1674 have "\<lbrakk>dist z w < e * r; w \<noteq> z\<rbrakk> \<Longrightarrow> cmod (f w) \<ge> B * norm a" for w |
|
1675 using \<open>a \<noteq> 0\<close> \<open>0 < r\<close> 2 [of "(w - z) / r"] |
|
1676 by (simp add: norm_divide dist_norm field_split_simps) |
|
1677 then have "\<lbrakk>dist z w < e * r; w \<noteq> z\<rbrakk> \<Longrightarrow> inverse (cmod (f w)) \<le> inverse (B * norm a)" for w |
|
1678 by (metis \<open>0 < B\<close> \<open>a \<noteq> 0\<close> mult_pos_pos norm_inverse norm_inverse_le_norm zero_less_norm_iff) |
|
1679 then show ?thesis |
|
1680 by (force simp: norm_inverse intro!: boundedI) |
|
1681 qed |
|
1682 qed |
|
1683 qed |
|
1684 |
|
1685 |
|
1686 theorem great_Picard: |
|
1687 assumes "open M" "z \<in> M" "a \<noteq> b" and holf: "f holomorphic_on (M - {z})" |
|
1688 and fab: "\<And>w. w \<in> M - {z} \<Longrightarrow> f w \<noteq> a \<and> f w \<noteq> b" |
|
1689 obtains l where "(f \<longlongrightarrow> l) (at z) \<or> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)" |
|
1690 proof - |
|
1691 obtain r where "0 < r" and zrM: "ball z r \<subseteq> M" |
|
1692 and r: "bounded((\<lambda>z. f z - a) ` (ball z r - {z})) \<or> |
|
1693 bounded((inverse \<circ> (\<lambda>z. f z - a)) ` (ball z r - {z}))" |
|
1694 proof (rule GPicard6 [OF \<open>open M\<close> \<open>z \<in> M\<close>]) |
|
1695 show "b - a \<noteq> 0" |
|
1696 using assms by auto |
|
1697 show "(\<lambda>z. f z - a) holomorphic_on M - {z}" |
|
1698 by (intro holomorphic_intros holf) |
|
1699 qed (use fab in auto) |
|
1700 have holfb: "f holomorphic_on ball z r - {z}" |
|
1701 apply (rule holomorphic_on_subset [OF holf]) |
|
1702 using zrM by auto |
|
1703 have holfb_i: "(\<lambda>z. inverse(f z - a)) holomorphic_on ball z r - {z}" |
|
1704 apply (intro holomorphic_intros holfb) |
|
1705 using fab zrM by fastforce |
|
1706 show ?thesis |
|
1707 using r |
|
1708 proof |
|
1709 assume "bounded ((\<lambda>z. f z - a) ` (ball z r - {z}))" |
|
1710 then obtain B where B: "\<And>w. w \<in> (\<lambda>z. f z - a) ` (ball z r - {z}) \<Longrightarrow> norm w \<le> B" |
|
1711 by (force simp: bounded_iff) |
|
1712 have "\<forall>\<^sub>F w in at z. cmod (f w - a) \<le> B" |
|
1713 apply (simp add: eventually_at) |
|
1714 apply (rule_tac x=r in exI) |
|
1715 using \<open>0 < r\<close> by (auto simp: dist_commute intro!: B) |
|
1716 then have "\<exists>B. \<forall>\<^sub>F w in at z. cmod (f w) \<le> B" |
|
1717 apply (rule_tac x="B + norm a" in exI) |
|
1718 apply (erule eventually_mono) |
|
1719 by (metis add.commute add_le_cancel_right norm_triangle_sub order.trans) |
|
1720 then obtain g where holg: "g holomorphic_on ball z r" and gf: "\<And>w. w \<in> ball z r - {z} \<Longrightarrow> g w = f w" |
|
1721 using \<open>0 < r\<close> holomorphic_on_extend_bounded [OF holfb] by auto |
|
1722 then have "g \<midarrow>z\<rightarrow> g z" |
|
1723 apply (simp add: continuous_at [symmetric]) |
|
1724 using \<open>0 < r\<close> centre_in_ball field_differentiable_imp_continuous_at holomorphic_on_imp_differentiable_at by blast |
|
1725 then have "(f \<longlongrightarrow> g z) (at z)" |
|
1726 apply (rule Lim_transform_within_open [of g "g z" z UNIV "ball z r"]) |
|
1727 using \<open>0 < r\<close> by (auto simp: gf) |
|
1728 then show ?thesis |
|
1729 using that by blast |
|
1730 next |
|
1731 assume "bounded((inverse \<circ> (\<lambda>z. f z - a)) ` (ball z r - {z}))" |
|
1732 then obtain B where B: "\<And>w. w \<in> (inverse \<circ> (\<lambda>z. f z - a)) ` (ball z r - {z}) \<Longrightarrow> norm w \<le> B" |
|
1733 by (force simp: bounded_iff) |
|
1734 have "\<forall>\<^sub>F w in at z. cmod (inverse (f w - a)) \<le> B" |
|
1735 apply (simp add: eventually_at) |
|
1736 apply (rule_tac x=r in exI) |
|
1737 using \<open>0 < r\<close> by (auto simp: dist_commute intro!: B) |
|
1738 then have "\<exists>B. \<forall>\<^sub>F z in at z. cmod (inverse (f z - a)) \<le> B" |
|
1739 by blast |
|
1740 then obtain g where holg: "g holomorphic_on ball z r" and gf: "\<And>w. w \<in> ball z r - {z} \<Longrightarrow> g w = inverse (f w - a)" |
|
1741 using \<open>0 < r\<close> holomorphic_on_extend_bounded [OF holfb_i] by auto |
|
1742 then have gz: "g \<midarrow>z\<rightarrow> g z" |
|
1743 apply (simp add: continuous_at [symmetric]) |
|
1744 using \<open>0 < r\<close> centre_in_ball field_differentiable_imp_continuous_at holomorphic_on_imp_differentiable_at by blast |
|
1745 have gnz: "\<And>w. w \<in> ball z r - {z} \<Longrightarrow> g w \<noteq> 0" |
|
1746 using gf fab zrM by fastforce |
|
1747 show ?thesis |
|
1748 proof (cases "g z = 0") |
|
1749 case True |
|
1750 have *: "\<lbrakk>g \<noteq> 0; inverse g = f - a\<rbrakk> \<Longrightarrow> g / (1 + a * g) = inverse f" for f g::complex |
|
1751 by (auto simp: field_simps) |
|
1752 have "(inverse \<circ> f) \<midarrow>z\<rightarrow> 0" |
|
1753 proof (rule Lim_transform_within_open [of "\<lambda>w. g w / (1 + a * g w)" _ _ UNIV "ball z r"]) |
|
1754 show "(\<lambda>w. g w / (1 + a * g w)) \<midarrow>z\<rightarrow> 0" |
|
1755 using True by (auto simp: intro!: tendsto_eq_intros gz) |
|
1756 show "\<And>x. \<lbrakk>x \<in> ball z r; x \<noteq> z\<rbrakk> \<Longrightarrow> g x / (1 + a * g x) = (inverse \<circ> f) x" |
|
1757 using * gf gnz by simp |
|
1758 qed (use \<open>0 < r\<close> in auto) |
|
1759 with that show ?thesis by blast |
|
1760 next |
|
1761 case False |
|
1762 show ?thesis |
|
1763 proof (cases "1 + a * g z = 0") |
|
1764 case True |
|
1765 have "(f \<longlongrightarrow> 0) (at z)" |
|
1766 proof (rule Lim_transform_within_open [of "\<lambda>w. (1 + a * g w) / g w" _ _ _ "ball z r"]) |
|
1767 show "(\<lambda>w. (1 + a * g w) / g w) \<midarrow>z\<rightarrow> 0" |
|
1768 apply (rule tendsto_eq_intros refl gz \<open>g z \<noteq> 0\<close>)+ |
|
1769 by (simp add: True) |
|
1770 show "\<And>x. \<lbrakk>x \<in> ball z r; x \<noteq> z\<rbrakk> \<Longrightarrow> (1 + a * g x) / g x = f x" |
|
1771 using fab fab zrM by (fastforce simp add: gf field_split_simps) |
|
1772 qed (use \<open>0 < r\<close> in auto) |
|
1773 then show ?thesis |
|
1774 using that by blast |
|
1775 next |
|
1776 case False |
|
1777 have *: "\<lbrakk>g \<noteq> 0; inverse g = f - a\<rbrakk> \<Longrightarrow> g / (1 + a * g) = inverse f" for f g::complex |
|
1778 by (auto simp: field_simps) |
|
1779 have "(inverse \<circ> f) \<midarrow>z\<rightarrow> g z / (1 + a * g z)" |
|
1780 proof (rule Lim_transform_within_open [of "\<lambda>w. g w / (1 + a * g w)" _ _ UNIV "ball z r"]) |
|
1781 show "(\<lambda>w. g w / (1 + a * g w)) \<midarrow>z\<rightarrow> g z / (1 + a * g z)" |
|
1782 using False by (auto simp: False intro!: tendsto_eq_intros gz) |
|
1783 show "\<And>x. \<lbrakk>x \<in> ball z r; x \<noteq> z\<rbrakk> \<Longrightarrow> g x / (1 + a * g x) = (inverse \<circ> f) x" |
|
1784 using * gf gnz by simp |
|
1785 qed (use \<open>0 < r\<close> in auto) |
|
1786 with that show ?thesis by blast |
|
1787 qed |
|
1788 qed |
|
1789 qed |
|
1790 qed |
|
1791 |
|
1792 |
|
1793 corollary great_Picard_alt: |
|
1794 assumes M: "open M" "z \<in> M" and holf: "f holomorphic_on (M - {z})" |
|
1795 and non: "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)" |
|
1796 obtains a where "- {a} \<subseteq> f ` (M - {z})" |
|
1797 apply (simp add: subset_iff image_iff) |
|
1798 by (metis great_Picard [OF M _ holf] non) |
|
1799 |
|
1800 |
|
1801 corollary great_Picard_infinite: |
|
1802 assumes M: "open M" "z \<in> M" and holf: "f holomorphic_on (M - {z})" |
|
1803 and non: "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)" |
|
1804 obtains a where "\<And>w. w \<noteq> a \<Longrightarrow> infinite {x. x \<in> M - {z} \<and> f x = w}" |
|
1805 proof - |
|
1806 have False if "a \<noteq> b" and ab: "finite {x. x \<in> M - {z} \<and> f x = a}" "finite {x. x \<in> M - {z} \<and> f x = b}" for a b |
|
1807 proof - |
|
1808 have finab: "finite {x. x \<in> M - {z} \<and> f x \<in> {a,b}}" |
|
1809 using finite_UnI [OF ab] unfolding mem_Collect_eq insert_iff empty_iff |
|
1810 by (simp add: conj_disj_distribL) |
|
1811 obtain r where "0 < r" and zrM: "ball z r \<subseteq> M" and r: "\<And>x. \<lbrakk>x \<in> M - {z}; f x \<in> {a,b}\<rbrakk> \<Longrightarrow> x \<notin> ball z r" |
|
1812 proof - |
|
1813 obtain e where "e > 0" and e: "ball z e \<subseteq> M" |
|
1814 using assms openE by blast |
|
1815 show ?thesis |
|
1816 proof (cases "{x \<in> M - {z}. f x \<in> {a, b}} = {}") |
|
1817 case True |
|
1818 then show ?thesis |
|
1819 apply (rule_tac r=e in that) |
|
1820 using e \<open>e > 0\<close> by auto |
|
1821 next |
|
1822 case False |
|
1823 let ?r = "min e (Min (dist z ` {x \<in> M - {z}. f x \<in> {a,b}}))" |
|
1824 show ?thesis |
|
1825 proof |
|
1826 show "0 < ?r" |
|
1827 using min_less_iff_conj Min_gr_iff finab False \<open>0 < e\<close> by auto |
|
1828 have "ball z ?r \<subseteq> ball z e" |
|
1829 by (simp add: subset_ball) |
|
1830 with e show "ball z ?r \<subseteq> M" by blast |
|
1831 show "\<And>x. \<lbrakk>x \<in> M - {z}; f x \<in> {a, b}\<rbrakk> \<Longrightarrow> x \<notin> ball z ?r" |
|
1832 using min_less_iff_conj Min_gr_iff finab False \<open>0 < e\<close> by auto |
|
1833 qed |
|
1834 qed |
|
1835 qed |
|
1836 have holfb: "f holomorphic_on (ball z r - {z})" |
|
1837 apply (rule holomorphic_on_subset [OF holf]) |
|
1838 using zrM by auto |
|
1839 show ?thesis |
|
1840 apply (rule great_Picard [OF open_ball _ \<open>a \<noteq> b\<close> holfb]) |
|
1841 using non \<open>0 < r\<close> r zrM by auto |
|
1842 qed |
|
1843 with that show thesis |
|
1844 by meson |
|
1845 qed |
|
1846 |
|
1847 theorem Casorati_Weierstrass: |
|
1848 assumes "open M" "z \<in> M" "f holomorphic_on (M - {z})" |
|
1849 and "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)" |
|
1850 shows "closure(f ` (M - {z})) = UNIV" |
|
1851 proof - |
|
1852 obtain a where a: "- {a} \<subseteq> f ` (M - {z})" |
|
1853 using great_Picard_alt [OF assms] . |
|
1854 have "UNIV = closure(- {a})" |
|
1855 by (simp add: closure_interior) |
|
1856 also have "... \<subseteq> closure(f ` (M - {z}))" |
|
1857 by (simp add: a closure_mono) |
|
1858 finally show ?thesis |
|
1859 by blast |
|
1860 qed |
|
1861 |
|
1862 end |