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