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