The Great Picard Theorem
authorpaulson <lp15@cam.ac.uk>
Wed Feb 22 16:21:26 2017 +0000 (2017-02-22)
changeset 650405975839e8d25
parent 65039 87972e6177bc
child 65041 2525e680f94f
The Great Picard Theorem
src/HOL/Analysis/Analysis.thy
src/HOL/Analysis/Great_Picard.thy
     1.1 --- a/src/HOL/Analysis/Analysis.thy	Wed Feb 22 15:04:59 2017 +0000
     1.2 +++ b/src/HOL/Analysis/Analysis.thy	Wed Feb 22 16:21:26 2017 +0000
     1.3 @@ -13,6 +13,7 @@
     1.4    Polytope
     1.5    Jordan_Curve
     1.6    Winding_Numbers
     1.7 +  Great_Picard
     1.8    Poly_Roots
     1.9    Conformal_Mappings
    1.10    Generalised_Binomial_Theorem
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Analysis/Great_Picard.thy	Wed Feb 22 16:21:26 2017 +0000
     2.3 @@ -0,0 +1,1845 @@
     2.4 +section\<open>The Great Picard Theorem and its Applications\<close>
     2.5 +
     2.6 +text\<open>Ported from HOL Light (cauchy.ml) by L C Paulson, 2017\<close>
     2.7 +
     2.8 +theory Great_Picard
     2.9 +  imports Conformal_Mappings Further_Topology
    2.10 +
    2.11 +begin
    2.12 +  
    2.13 +subsection\<open>Schottky's theorem\<close>
    2.14 +
    2.15 +lemma Schottky_lemma0:
    2.16 +  assumes holf: "f holomorphic_on S" and cons: "contractible S" and "a \<in> S"
    2.17 +      and f: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 1 \<and> f z \<noteq> -1"
    2.18 +  obtains g where "g holomorphic_on S"
    2.19 +                  "norm(g a) \<le> 1 + norm(f a) / 3"
    2.20 +                  "\<And>z. z \<in> S \<Longrightarrow> f z = cos(of_real pi * g z)"
    2.21 +proof -
    2.22 +  obtain g where holg: "g holomorphic_on S" and g: "norm(g a) \<le> pi + norm(f a)"
    2.23 +             and f_eq_cos: "\<And>z. z \<in> S \<Longrightarrow> f z = cos(g z)"
    2.24 +    using contractible_imp_holomorphic_arccos_bounded [OF assms]
    2.25 +    by blast
    2.26 +  show ?thesis
    2.27 +  proof
    2.28 +    show "(\<lambda>z. g z / pi) holomorphic_on S"
    2.29 +      by (auto intro: holomorphic_intros holg)
    2.30 +    have "3 \<le> pi"
    2.31 +      using pi_approx by force
    2.32 +    have "3 * norm(g a) \<le> 3 * (pi + norm(f a))"
    2.33 +      using g by auto
    2.34 +    also have "... \<le>  pi * 3 + pi * cmod (f a)"
    2.35 +      using \<open>3 \<le> pi\<close> by (simp add: mult_right_mono algebra_simps)
    2.36 +    finally show "cmod (g a / complex_of_real pi) \<le> 1 + cmod (f a) / 3"
    2.37 +      by (simp add: field_simps norm_divide)
    2.38 +    show "\<And>z. z \<in> S \<Longrightarrow> f z = cos (complex_of_real pi * (g z / complex_of_real pi))"
    2.39 +      by (simp add: f_eq_cos)
    2.40 +  qed
    2.41 +qed
    2.42 +
    2.43 +
    2.44 +lemma Schottky_lemma1:
    2.45 +  fixes n::nat
    2.46 +  assumes "0 < n"
    2.47 +  shows "0 < n + sqrt(real n ^ 2 - 1)"
    2.48 +proof -
    2.49 +  have "(n-1)^2 \<le> n^2 - 1"
    2.50 +    using assms by (simp add: algebra_simps power2_eq_square)
    2.51 +  then have "real (n - 1) \<le> sqrt (real (n\<^sup>2 - 1))"
    2.52 +    by (metis Extended_Nonnegative_Real.of_nat_le_iff of_nat_power real_le_rsqrt)
    2.53 +  then have "n-1 \<le> sqrt(real n ^ 2 - 1)"
    2.54 +    by (simp add: Suc_leI assms of_nat_diff)
    2.55 +  then show ?thesis
    2.56 +    using assms by linarith
    2.57 +qed
    2.58 +
    2.59 +
    2.60 +lemma Schottky_lemma2:
    2.61 +  fixes x::real
    2.62 +  assumes "0 \<le> x"
    2.63 +  obtains n where "0 < n" "\<bar>x - ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi\<bar> < 1/2"
    2.64 +proof -
    2.65 +  obtain n0::nat where "0 < n0" "ln(n0 + sqrt(real n0 ^ 2 - 1)) / pi \<le> x"
    2.66 +  proof
    2.67 +    show "ln(real 1 + sqrt(real 1 ^ 2 - 1))/pi \<le> x"
    2.68 +      by (auto simp: assms)
    2.69 +  qed auto
    2.70 +  moreover
    2.71 +  obtain M::nat where "\<And>n. \<lbrakk>0 < n; ln(n + sqrt(real n ^ 2 - 1)) / pi \<le> x\<rbrakk> \<Longrightarrow> n \<le> M"
    2.72 +  proof
    2.73 +    fix n::nat
    2.74 +    assume "0 < n" "ln (n + sqrt ((real n)\<^sup>2 - 1)) / pi \<le> x"
    2.75 +    then have "ln (n + sqrt ((real n)\<^sup>2 - 1)) \<le> x * pi"
    2.76 +      by (simp add: divide_simps)
    2.77 +    then have *: "exp (ln (n + sqrt ((real n)\<^sup>2 - 1))) \<le> exp (x * pi)"
    2.78 +      by blast
    2.79 +    have 0: "0 \<le> sqrt ((real n)\<^sup>2 - 1)"
    2.80 +      using \<open>0 < n\<close> by auto
    2.81 +    have "n + sqrt ((real n)\<^sup>2 - 1) = exp (ln (n + sqrt ((real n)\<^sup>2 - 1)))"
    2.82 +      by (simp add: Suc_leI \<open>0 < n\<close> add_pos_nonneg real_of_nat_ge_one_iff)
    2.83 +    also have "... \<le> exp (x * pi)"
    2.84 +      using "*" by blast
    2.85 +    finally have "real n \<le> exp (x * pi)"
    2.86 +      using 0 by linarith
    2.87 +    then show "n \<le> nat (ceiling (exp(x * pi)))"
    2.88 +      by linarith
    2.89 +  qed
    2.90 +  ultimately obtain n where
    2.91 +     "0 < n" and le_x: "ln(n + sqrt(real n ^ 2 - 1)) / pi \<le> x"
    2.92 +             and le_n: "\<And>k. \<lbrakk>0 < k; ln(k + sqrt(real k ^ 2 - 1)) / pi \<le> x\<rbrakk> \<Longrightarrow> k \<le> n"
    2.93 +    using bounded_Max_nat [of "\<lambda>n. 0<n \<and> ln (n + sqrt ((real n)\<^sup>2 - 1)) / pi \<le> x"] by metis
    2.94 +  define a where "a \<equiv> ln(n + sqrt(real n ^ 2 - 1)) / pi"
    2.95 +  define b where "b \<equiv> ln (1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / pi"
    2.96 +  have le_xa: "a \<le> x"
    2.97 +   and le_na: "\<And>k. \<lbrakk>0 < k; ln(k + sqrt(real k ^ 2 - 1)) / pi \<le> x\<rbrakk> \<Longrightarrow> k \<le> n"
    2.98 +    using le_x le_n by (auto simp: a_def)
    2.99 +  moreover have "x < b"
   2.100 +    using le_n [of "Suc n"] by (force simp: b_def)
   2.101 +  moreover have "b - a < 1"
   2.102 +  proof -
   2.103 +    have "ln (1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) - ln (real n + sqrt ((real n)\<^sup>2 - 1)) =
   2.104 +         ln ((1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / (real n + sqrt ((real n)\<^sup>2 - 1)))"
   2.105 +      by (simp add: \<open>0 < n\<close> Schottky_lemma1 add_pos_nonneg ln_div [symmetric])
   2.106 +    also have "... \<le> 3"
   2.107 +    proof (cases "n = 1")
   2.108 +      case True
   2.109 +      have "sqrt 3 \<le> 2"
   2.110 +        by (simp add: real_le_lsqrt)
   2.111 +      then have "(2 + sqrt 3) \<le> 4"
   2.112 +        by simp
   2.113 +      also have "... \<le> exp 3"
   2.114 +        using exp_ge_add_one_self [of "3::real"] by simp
   2.115 +      finally have "ln (2 + sqrt 3) \<le> 3"
   2.116 +        by (metis add_nonneg_nonneg add_pos_nonneg dbl_def dbl_inc_def dbl_inc_simps(3)
   2.117 +            dbl_simps(3) exp_gt_zero ln_exp ln_le_cancel_iff real_sqrt_ge_0_iff zero_le_one zero_less_one)
   2.118 +      then show ?thesis
   2.119 +        by (simp add: True)
   2.120 +    next
   2.121 +      case False with \<open>0 < n\<close> have "1 < n" "2 \<le> n"
   2.122 +        by linarith+
   2.123 +      then have 1: "1 \<le> real n * real n"
   2.124 +        by (metis less_imp_le_nat one_le_power power2_eq_square real_of_nat_ge_one_iff)
   2.125 +      have *: "4 + (m+2) * 2 \<le> (m+2) * ((m+2) * 3)" for m::nat
   2.126 +        by simp
   2.127 +      have "4 + n * 2 \<le> n * (n * 3)"
   2.128 +        using * [of "n-2"]  \<open>2 \<le> n\<close>
   2.129 +        by (metis le_add_diff_inverse2)
   2.130 +      then have **: "4 + real n * 2 \<le> real n * (real n * 3)"
   2.131 +        by (metis (mono_tags, hide_lams) of_nat_le_iff of_nat_add of_nat_mult of_nat_numeral)
   2.132 +      have "sqrt ((1 + real n)\<^sup>2 - 1) \<le> 2 * sqrt ((real n)\<^sup>2 - 1)"
   2.133 +        by (auto simp: real_le_lsqrt power2_eq_square algebra_simps 1 **)
   2.134 +      then
   2.135 +      have "((1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / (real n + sqrt ((real n)\<^sup>2 - 1))) \<le> 2"
   2.136 +        using Schottky_lemma1 \<open>0 < n\<close>  by (simp add: divide_simps)
   2.137 +      then have "ln ((1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / (real n + sqrt ((real n)\<^sup>2 - 1))) \<le> ln 2"
   2.138 +        apply (subst ln_le_cancel_iff)
   2.139 +        using Schottky_lemma1 \<open>0 < n\<close> by auto (force simp: divide_simps)
   2.140 +      also have "... \<le> 3"
   2.141 +        using ln_add_one_self_le_self [of 1] by auto
   2.142 +      finally show ?thesis .
   2.143 +    qed
   2.144 +    also have "... < pi"
   2.145 +      using pi_approx by simp
   2.146 +    finally show ?thesis
   2.147 +      by (simp add: a_def b_def divide_simps)
   2.148 +  qed
   2.149 +  ultimately have "\<bar>x - a\<bar> < 1/2 \<or> \<bar>x - b\<bar> < 1/2"
   2.150 +    by (auto simp: abs_if)
   2.151 +  then show thesis
   2.152 +  proof
   2.153 +    assume "\<bar>x - a\<bar> < 1 / 2"
   2.154 +    then show ?thesis
   2.155 +      by (rule_tac n=n in that) (auto simp: a_def \<open>0 < n\<close>)
   2.156 +  next
   2.157 +    assume "\<bar>x - b\<bar> < 1 / 2"
   2.158 +    then show ?thesis
   2.159 +      by (rule_tac n="Suc n" in that) (auto simp: b_def \<open>0 < n\<close>)
   2.160 +  qed
   2.161 +qed
   2.162 +
   2.163 +
   2.164 +lemma Schottky_lemma3:
   2.165 +  fixes z::complex
   2.166 +  assumes "z \<in> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)})
   2.167 +             \<union> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)})"
   2.168 +  shows "cos(pi * cos(pi * z)) = 1 \<or> cos(pi * cos(pi * z)) = -1"
   2.169 +proof -
   2.170 +  have sqrt2 [simp]: "complex_of_real (sqrt x) * complex_of_real (sqrt x) = x" if "x \<ge> 0" for x::real
   2.171 +    by (metis abs_of_nonneg of_real_mult real_sqrt_mult_self that)
   2.172 +  have 1: "\<exists>k. exp (\<i> * (of_int m * complex_of_real pi) -
   2.173 +                 (ln (real n + sqrt ((real n)\<^sup>2 - 1)))) +
   2.174 +            inverse
   2.175 +             (exp (\<i> * (of_int m * complex_of_real pi) -
   2.176 +                    (ln (real n + sqrt ((real n)\<^sup>2 - 1))))) = of_int k * 2"
   2.177 +         if "n > 0" for m n
   2.178 +  proof -
   2.179 +    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
   2.180 +      by (auto simp: field_simps power2_eq_square)
   2.181 +    have [simp]: "1 \<le> real n * real n"
   2.182 +      by (metis One_nat_def add.commute nat_less_real_le of_nat_1 of_nat_Suc one_le_power power2_eq_square that)
   2.183 +    show ?thesis
   2.184 +      apply (simp add: eeq)
   2.185 +      using Schottky_lemma1 [OF that]
   2.186 +      apply (auto simp: eeq exp_diff exp_Euler exp_of_real algebra_simps sin_int_times_real cos_int_times_real)
   2.187 +       apply (rule_tac x="int n" in exI)
   2.188 +       apply (auto simp: power2_eq_square algebra_simps)
   2.189 +       apply (rule_tac x="- int n" in exI)
   2.190 +      apply (auto simp: power2_eq_square algebra_simps)
   2.191 +      done
   2.192 +  qed
   2.193 +  have 2: "\<exists>k. exp (\<i> * (of_int m * complex_of_real pi) +
   2.194 +                 (ln (real n + sqrt ((real n)\<^sup>2 - 1)))) +
   2.195 +            inverse
   2.196 +             (exp (\<i> * (of_int m * complex_of_real pi) +
   2.197 +                    (ln (real n + sqrt ((real n)\<^sup>2 - 1))))) = of_int k * 2"
   2.198 +            if "n > 0" for m n
   2.199 +  proof -
   2.200 +    have eeq: "e \<noteq> 0 \<Longrightarrow> e + inverse e = n*2 \<longleftrightarrow> e^2 - 2 * n*e + 1 = 0" for n e::complex
   2.201 +      by (auto simp: field_simps power2_eq_square)
   2.202 +    have [simp]: "1 \<le> real n * real n"
   2.203 +      by (metis One_nat_def add.commute nat_less_real_le of_nat_1 of_nat_Suc one_le_power power2_eq_square that)
   2.204 +    show ?thesis
   2.205 +      apply (simp add: eeq)
   2.206 +      using Schottky_lemma1 [OF that]
   2.207 +      apply (auto simp: exp_add exp_Euler exp_of_real algebra_simps sin_int_times_real cos_int_times_real)
   2.208 +       apply (rule_tac x="int n" in exI)
   2.209 +       apply (auto simp: power2_eq_square algebra_simps)
   2.210 +       apply (rule_tac x="- int n" in exI)
   2.211 +      apply (auto simp: power2_eq_square algebra_simps)
   2.212 +      done
   2.213 +  qed
   2.214 +  have "\<exists>x. cos (complex_of_real pi * z) = of_int x"
   2.215 +    using assms
   2.216 +    apply safe
   2.217 +      apply (auto simp: Ints_def cos_exp_eq exp_minus)
   2.218 +     apply (auto simp: algebra_simps dest: 1 2)
   2.219 +      done
   2.220 +  then have "sin(pi * cos(pi * z)) ^ 2 = 0"
   2.221 +    by (simp add: Complex_Transcendental.sin_eq_0)
   2.222 +  then have "1 - cos(pi * cos(pi * z)) ^ 2 = 0"
   2.223 +    by (simp add: sin_squared_eq)
   2.224 +  then show ?thesis
   2.225 +    using power2_eq_1_iff by auto
   2.226 +qed
   2.227 +
   2.228 +
   2.229 +theorem Schottky:
   2.230 +  assumes holf: "f holomorphic_on cball 0 1"
   2.231 +      and nof0: "norm(f 0) \<le> r"
   2.232 +      and not01: "\<And>z. z \<in> cball 0 1 \<Longrightarrow> \<not>(f z = 0 \<or> f z = 1)"
   2.233 +      and "0 < t" "t < 1" "norm z \<le> t"
   2.234 +    shows "norm(f z) \<le> exp(pi * exp(pi * (2 + 2 * r + 12 * t / (1 - t))))"
   2.235 +proof -
   2.236 +  obtain h where holf: "h holomorphic_on cball 0 1"
   2.237 +             and nh0: "norm (h 0) \<le> 1 + norm(2 * f 0 - 1) / 3"
   2.238 +             and h:   "\<And>z. z \<in> cball 0 1 \<Longrightarrow> 2 * f z - 1 = cos(of_real pi * h z)"
   2.239 +  proof (rule Schottky_lemma0 [of "\<lambda>z. 2 * f z - 1" "cball 0 1" 0])
   2.240 +    show "(\<lambda>z. 2 * f z - 1) holomorphic_on cball 0 1"
   2.241 +      by (intro holomorphic_intros holf)
   2.242 +    show "contractible (cball (0::complex) 1)"
   2.243 +      by (auto simp: convex_imp_contractible)
   2.244 +    show "\<And>z. z \<in> cball 0 1 \<Longrightarrow> 2 * f z - 1 \<noteq> 1 \<and> 2 * f z - 1 \<noteq> - 1"
   2.245 +      using not01 by force
   2.246 +  qed auto
   2.247 +  obtain g where holg: "g holomorphic_on cball 0 1"
   2.248 +             and ng0:  "norm(g 0) \<le> 1 + norm(h 0) / 3"
   2.249 +             and g:    "\<And>z. z \<in> cball 0 1 \<Longrightarrow> h z = cos(of_real pi * g z)"
   2.250 +  proof (rule Schottky_lemma0 [OF holf convex_imp_contractible, of 0])
   2.251 +    show "\<And>z. z \<in> cball 0 1 \<Longrightarrow> h z \<noteq> 1 \<and> h z \<noteq> - 1"
   2.252 +      using h not01 by fastforce+
   2.253 +  qed auto
   2.254 +  have g0_2_f0: "norm(g 0) \<le> 2 + norm(f 0)"
   2.255 +  proof -
   2.256 +    have "cmod (2 * f 0 - 1) \<le> cmod (2 * f 0) + 1"
   2.257 +      by (metis norm_one norm_triangle_ineq4)
   2.258 +    also have "... \<le> 2 + cmod (f 0) * 3"
   2.259 +      by simp
   2.260 +    finally have "1 + norm(2 * f 0 - 1) / 3 \<le> (2 + norm(f 0) - 1) * 3"
   2.261 +      apply (simp add: divide_simps)
   2.262 +      using norm_ge_zero [of "2 * f 0 - 1"]
   2.263 +      by linarith
   2.264 +    with nh0 have "norm(h 0) \<le> (2 + norm(f 0) - 1) * 3"
   2.265 +      by linarith
   2.266 +    then have "1 + norm(h 0) / 3 \<le> 2 + norm(f 0)"
   2.267 +      by simp
   2.268 +    with ng0 show ?thesis
   2.269 +      by auto
   2.270 +  qed
   2.271 +  have "z \<in> ball 0 1"
   2.272 +    using assms by auto
   2.273 +  have norm_g_12: "norm(g z - g 0) \<le> (12 * t) / (1 - t)"
   2.274 +  proof -
   2.275 +    obtain g' where g': "\<And>x. x \<in> cball 0 1 \<Longrightarrow> (g has_field_derivative g' x) (at x within cball 0 1)"
   2.276 +      using holg [unfolded holomorphic_on_def field_differentiable_def] by metis
   2.277 +    have int_g': "(g' has_contour_integral g z - g 0) (linepath 0 z)"
   2.278 +      using contour_integral_primitive [OF g' valid_path_linepath, of 0 z]
   2.279 +      using \<open>z \<in> ball 0 1\<close> segment_bound1 by fastforce
   2.280 +    have "cmod (g' w) \<le> 12 / (1 - t)" if "w \<in> closed_segment 0 z" for w
   2.281 +    proof -
   2.282 +      have w: "w \<in> ball 0 1"
   2.283 +        using segment_bound [OF that] \<open>z \<in> ball 0 1\<close> by simp
   2.284 +      have ttt: "\<And>z. z \<in> frontier (cball 0 1) \<Longrightarrow> 1 - t \<le> dist w z"
   2.285 +        using \<open>norm z \<le> t\<close> segment_bound1 [OF \<open>w \<in> closed_segment 0 z\<close>]
   2.286 +        apply (simp add: dist_complex_def)
   2.287 +        by (metis diff_left_mono dist_commute dist_complex_def norm_triangle_ineq2 order_trans)
   2.288 +      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
   2.289 +        by force
   2.290 +      have "\<nexists>b. ball b 1 \<subseteq> g ` cball 0 1"
   2.291 +      proof (rule *)
   2.292 +        show "(\<exists>w \<in> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)}) \<union>
   2.293 +                    (\<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
   2.294 +        proof -
   2.295 +          obtain m where m: "m \<in> \<int>" "\<bar>Re b - m\<bar> \<le> 1/2"
   2.296 +            by (metis Ints_of_int abs_minus_commute of_int_round_abs_le)
   2.297 +          show ?thesis
   2.298 +          proof (cases "0::real" "Im b" rule: le_cases)
   2.299 +            case le
   2.300 +            then obtain n where "0 < n" and n: "\<bar>Im b - ln (n + sqrt ((real n)\<^sup>2 - 1)) / pi\<bar> < 1/2"
   2.301 +              using Schottky_lemma2 [of "Im b"] by blast
   2.302 +            have "dist b (Complex m (Im b)) \<le> 1/2"
   2.303 +              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)
   2.304 +            moreover
   2.305 +            have "dist (Complex m (Im b)) (Complex m (ln (n + sqrt ((real n)\<^sup>2 - 1)) / pi)) < 1/2"
   2.306 +              using n by (simp add: complex_norm cmod_eq_Re complex_diff dist_norm del: Complex_eq)
   2.307 +            ultimately have "dist b (Complex m (ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi)) < 1"
   2.308 +              by (simp add: dist_triangle_lt [of b "Complex m (Im b)"] dist_commute)
   2.309 +            with le m \<open>0 < n\<close> show ?thesis
   2.310 +              apply (rule_tac x = "Complex m (ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi)" in bexI)
   2.311 +               apply (simp_all del: Complex_eq greaterThan_0)
   2.312 +              by blast
   2.313 +          next
   2.314 +            case ge
   2.315 +            then obtain n where "0 < n" and n: "\<bar>- Im b - ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi\<bar> < 1/2"
   2.316 +              using Schottky_lemma2 [of "- Im b"] by auto
   2.317 +            have "dist b (Complex m (Im b)) \<le> 1/2"
   2.318 +              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)
   2.319 +            moreover
   2.320 +            have "dist (Complex m (- ln (n + sqrt ((real n)\<^sup>2 - 1)) / pi)) (Complex m (Im b)) < 1/2"
   2.321 +              using n
   2.322 +              apply (simp add: complex_norm cmod_eq_Re complex_diff dist_norm del: Complex_eq)
   2.323 +              by (metis add.commute add_uminus_conv_diff)
   2.324 +            ultimately have "dist b (Complex m (- ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi)) < 1"
   2.325 +              by (simp add: dist_triangle_lt [of b "Complex m (Im b)"] dist_commute)
   2.326 +            with ge m \<open>0 < n\<close> show ?thesis
   2.327 +              apply (rule_tac x = "Complex m (- ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi)" in bexI)
   2.328 +               apply (simp_all del: Complex_eq greaterThan_0)
   2.329 +              by blast
   2.330 +          qed
   2.331 +        qed
   2.332 +        show "g v \<notin> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)}) \<union>
   2.333 +                    (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)})"
   2.334 +             if "v \<in> cball 0 1" for v
   2.335 +          using not01 [OF that]
   2.336 +          by (force simp: g [OF that, symmetric] h [OF that, symmetric] dest!: Schottky_lemma3 [of "g v"])
   2.337 +      qed
   2.338 +      then have 12: "(1 - t) * cmod (deriv g w) / 12 < 1"
   2.339 +        using Bloch_general [OF holg _ ttt, of 1] w by force
   2.340 +      have "g field_differentiable at w within cball 0 1"
   2.341 +        using holg w by (simp add: holomorphic_on_def)
   2.342 +      then have "g field_differentiable at w within ball 0 1"
   2.343 +        using ball_subset_cball field_differentiable_within_subset by blast
   2.344 +      with w have der_gw: "(g has_field_derivative deriv g w) (at w)"
   2.345 +        by (simp add: field_differentiable_within_open [of _ "ball 0 1"] field_differentiable_derivI)
   2.346 +      with DERIV_unique [OF der_gw] g' w have "deriv g w = g' w"
   2.347 +        by (metis Topology_Euclidean_Space.open_ball at_within_open ball_subset_cball has_field_derivative_subset subsetCE)
   2.348 +      then show "cmod (g' w) \<le> 12 / (1 - t)"
   2.349 +        using g' 12 \<open>t < 1\<close> by (simp add: field_simps)
   2.350 +    qed
   2.351 +    then have "cmod (g z - g 0) \<le> 12 / (1 - t) * cmod z"
   2.352 +      using has_contour_integral_bound_linepath [OF int_g', of "12/(1 - t)"] assms
   2.353 +      by simp
   2.354 +    with \<open>cmod z \<le> t\<close> \<open>t < 1\<close> show ?thesis
   2.355 +      by (simp add: divide_simps)
   2.356 +  qed
   2.357 +  have fz: "f z = (1 + cos(of_real pi * h z)) / 2"
   2.358 +    using h \<open>z \<in> ball 0 1\<close> by (auto simp: field_simps)
   2.359 +  have "cmod (f z) \<le> exp (cmod (complex_of_real pi * h z))"
   2.360 +    by (simp add: fz mult.commute norm_cos_plus1_le)
   2.361 +  also have "... \<le> exp (pi * exp (pi * (2 + 2 * r + 12 * t / (1 - t))))"
   2.362 +  proof (simp add: norm_mult)
   2.363 +    have "cmod (g z - g 0) \<le> 12 * t / (1 - t)"
   2.364 +      using norm_g_12 \<open>t < 1\<close> by (simp add: norm_mult)
   2.365 +    then have "cmod (g z) - cmod (g 0) \<le> 12 * t / (1 - t)"
   2.366 +      using norm_triangle_ineq2 order_trans by blast
   2.367 +    then have *: "cmod (g z) \<le> 2 + 2 * r + 12 * t / (1 - t)"
   2.368 +      using g0_2_f0 norm_ge_zero [of "f 0"] nof0
   2.369 +        by linarith
   2.370 +    have "cmod (h z) \<le> exp (cmod (complex_of_real pi * g z))"
   2.371 +      using \<open>z \<in> ball 0 1\<close> by (simp add: g norm_cos_le)
   2.372 +    also have "... \<le> exp (pi * (2 + 2 * r + 12 * t / (1 - t)))"
   2.373 +      using \<open>t < 1\<close> nof0 * by (simp add: norm_mult)
   2.374 +    finally show "cmod (h z) \<le> exp (pi * (2 + 2 * r + 12 * t / (1 - t)))" .
   2.375 +  qed
   2.376 +  finally show ?thesis .
   2.377 +qed
   2.378 +
   2.379 +  
   2.380 +subsection\<open>The Little Picard Theorem\<close>
   2.381 +
   2.382 +lemma Landau_Picard:
   2.383 +  obtains R
   2.384 +    where "\<And>z. 0 < R z"
   2.385 +          "\<And>f. \<lbrakk>f holomorphic_on cball 0 (R(f 0));
   2.386 +                 \<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"
   2.387 +proof -
   2.388 +  define R where "R \<equiv> \<lambda>z. 3 * exp(pi * exp(pi*(2 + 2 * cmod z + 12)))"
   2.389 +  show ?thesis
   2.390 +  proof
   2.391 +    show Rpos: "\<And>z. 0 < R z"
   2.392 +      by (auto simp: R_def)
   2.393 +    show "norm(deriv f 0) < 1"
   2.394 +         if holf: "f holomorphic_on cball 0 (R(f 0))"
   2.395 +         and Rf:  "\<And>z. norm z \<le> R(f 0) \<Longrightarrow> f z \<noteq> 0 \<and> f z \<noteq> 1" for f
   2.396 +    proof -
   2.397 +      let ?r = "R(f 0)"
   2.398 +      define g where "g \<equiv> f \<circ> (\<lambda>z. of_real ?r * z)"
   2.399 +      have "0 < ?r"
   2.400 +        using Rpos by blast
   2.401 +      have holg: "g holomorphic_on cball 0 1"
   2.402 +        unfolding g_def
   2.403 +        apply (intro holomorphic_intros holomorphic_on_compose holomorphic_on_subset [OF holf])
   2.404 +        using Rpos by (auto simp: less_imp_le norm_mult)
   2.405 +      have *: "norm(g z) \<le> exp(pi * exp(pi * (2 + 2 * norm (f 0) + 12 * t / (1 - t))))"
   2.406 +           if "0 < t" "t < 1" "norm z \<le> t" for t z
   2.407 +      proof (rule Schottky [OF holg])
   2.408 +        show "cmod (g 0) \<le> cmod (f 0)"
   2.409 +          by (simp add: g_def)
   2.410 +        show "\<And>z. z \<in> cball 0 1 \<Longrightarrow> \<not> (g z = 0 \<or> g z = 1)"
   2.411 +          using Rpos by (simp add: g_def less_imp_le norm_mult Rf)
   2.412 +      qed (auto simp: that)
   2.413 +      have C1: "g holomorphic_on ball 0 (1 / 2)"
   2.414 +        by (rule holomorphic_on_subset [OF holg]) auto
   2.415 +      have C2: "continuous_on (cball 0 (1 / 2)) g"
   2.416 +        by (meson cball_divide_subset_numeral holg holomorphic_on_imp_continuous_on holomorphic_on_subset)
   2.417 +      have C3: "cmod (g z) \<le> R (f 0) / 3" if "cmod (0 - z) = 1/2" for z
   2.418 +      proof -
   2.419 +        have "norm(g z) \<le> exp(pi * exp(pi * (2 + 2 * norm (f 0) + 12)))"
   2.420 +          using * [of "1/2"] that by simp
   2.421 +        also have "... = ?r / 3"
   2.422 +          by (simp add: R_def)
   2.423 +        finally show ?thesis .
   2.424 +      qed
   2.425 +      then have cmod_g'_le: "cmod (deriv g 0) * 3 \<le> R (f 0) * 2"
   2.426 +        using Cauchy_inequality [OF C1 C2 _ C3, of 1] by simp
   2.427 +      have holf': "f holomorphic_on ball 0 (R(f 0))"
   2.428 +        by (rule holomorphic_on_subset [OF holf]) auto
   2.429 +      then have fd0: "f field_differentiable at 0"
   2.430 +        by (rule holomorphic_on_imp_differentiable_at [OF _ open_ball])
   2.431 +           (auto simp: Rpos [of "f 0"])
   2.432 +      have g_eq: "deriv g 0 = of_real ?r * deriv f 0"
   2.433 +        apply (rule DERIV_imp_deriv)
   2.434 +        apply (simp add: g_def)
   2.435 +        by (metis DERIV_chain DERIV_cmult_Id fd0 field_differentiable_derivI mult.commute mult_zero_right)
   2.436 +      show ?thesis
   2.437 +        using cmod_g'_le Rpos [of "f 0"]  by (simp add: g_eq norm_mult)
   2.438 +    qed
   2.439 +  qed
   2.440 +qed
   2.441 +
   2.442 +lemma little_Picard_01:
   2.443 +  assumes holf: "f holomorphic_on UNIV" and f01: "\<And>z. f z \<noteq> 0 \<and> f z \<noteq> 1"
   2.444 +  obtains c where "f = (\<lambda>x. c)"
   2.445 +proof -
   2.446 +  obtain R
   2.447 +    where Rpos: "\<And>z. 0 < R z"
   2.448 +      and R:    "\<And>h. \<lbrakk>h holomorphic_on cball 0 (R(h 0));
   2.449 +                      \<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"
   2.450 +    using Landau_Picard by metis
   2.451 +  have contf: "continuous_on UNIV f"
   2.452 +    by (simp add: holf holomorphic_on_imp_continuous_on)
   2.453 +  show ?thesis
   2.454 +  proof (cases "\<forall>x. deriv f x = 0")
   2.455 +    case True
   2.456 +    obtain c where "\<And>x. f(x) = c"
   2.457 +      apply (rule DERIV_zero_connected_constant [OF connected_UNIV open_UNIV finite.emptyI contf])
   2.458 +       apply (metis True DiffE holf holomorphic_derivI open_UNIV, auto)
   2.459 +      done
   2.460 +    then show ?thesis
   2.461 +      using that by auto
   2.462 +  next
   2.463 +    case False
   2.464 +    then obtain w where w: "deriv f w \<noteq> 0" by auto
   2.465 +    define fw where "fw \<equiv> (f \<circ> (\<lambda>z. w + z / deriv f w))"
   2.466 +    have norm_let1: "norm(deriv fw 0) < 1"
   2.467 +    proof (rule R)
   2.468 +      show "fw holomorphic_on cball 0 (R (fw 0))"
   2.469 +        unfolding fw_def
   2.470 +        by (intro holomorphic_intros holomorphic_on_compose w holomorphic_on_subset [OF holf] subset_UNIV)
   2.471 +      show "fw z \<noteq> 0 \<and> fw z \<noteq> 1" if "cmod z \<le> R (fw 0)" for z
   2.472 +        using f01 by (simp add: fw_def)
   2.473 +    qed
   2.474 +    have "(fw has_field_derivative deriv f w * inverse (deriv f w)) (at 0)"
   2.475 +      apply (simp add: fw_def)
   2.476 +      apply (rule DERIV_chain)
   2.477 +      using holf holomorphic_derivI apply force
   2.478 +      apply (intro derivative_eq_intros w)
   2.479 +          apply (auto simp: field_simps)
   2.480 +      done
   2.481 +    then show ?thesis
   2.482 +      using norm_let1 w by (simp add: DERIV_imp_deriv)
   2.483 +  qed
   2.484 +qed
   2.485 +
   2.486 +
   2.487 +theorem little_Picard:
   2.488 +  assumes holf: "f holomorphic_on UNIV"
   2.489 +      and "a \<noteq> b" "range f \<inter> {a,b} = {}"
   2.490 +    obtains c where "f = (\<lambda>x. c)"
   2.491 +proof -
   2.492 +  let ?g = "\<lambda>x. 1/(b - a)*(f x - b) + 1"
   2.493 +  obtain c where "?g = (\<lambda>x. c)"
   2.494 +  proof (rule little_Picard_01)
   2.495 +    show "?g holomorphic_on UNIV"
   2.496 +      by (intro holomorphic_intros holf)
   2.497 +    show "\<And>z. ?g z \<noteq> 0 \<and> ?g z \<noteq> 1"
   2.498 +      using assms by (auto simp: field_simps)
   2.499 +  qed auto
   2.500 +  then have "?g x = c" for x
   2.501 +    by meson
   2.502 +  then have "f x = c * (b-a) + a" for x
   2.503 +    using assms by (auto simp: field_simps)
   2.504 +  then show ?thesis
   2.505 +    using that by blast
   2.506 +qed
   2.507 +
   2.508 +
   2.509 +text\<open>A couple of little applications of Little Picard\<close>
   2.510 +
   2.511 +lemma holomorphic_periodic_fixpoint:
   2.512 +  assumes holf: "f holomorphic_on UNIV"
   2.513 +      and "p \<noteq> 0" and per: "\<And>z. f(z + p) = f z"
   2.514 +  obtains x where "f x = x"
   2.515 +proof -
   2.516 +  have False if non: "\<And>x. f x \<noteq> x"
   2.517 +  proof -
   2.518 +    obtain c where "(\<lambda>z. f z - z) = (\<lambda>z. c)"
   2.519 +    proof (rule little_Picard)
   2.520 +      show "(\<lambda>z. f z - z) holomorphic_on UNIV"
   2.521 +        by (simp add: holf holomorphic_on_diff)
   2.522 +      show "range (\<lambda>z. f z - z) \<inter> {p,0} = {}"
   2.523 +          using assms non by auto (metis add.commute diff_eq_eq)
   2.524 +      qed (auto simp: assms)
   2.525 +    with per show False
   2.526 +      by (metis add.commute add_cancel_left_left \<open>p \<noteq> 0\<close> diff_add_cancel)
   2.527 +  qed
   2.528 +  then show ?thesis
   2.529 +    using that by blast
   2.530 +qed
   2.531 +
   2.532 +
   2.533 +lemma holomorphic_involution_point:
   2.534 +  assumes holfU: "f holomorphic_on UNIV" and non: "\<And>a. f \<noteq> (\<lambda>x. a + x)"
   2.535 +  obtains x where "f(f x) = x"
   2.536 +proof -
   2.537 +  { assume non_ff [simp]: "\<And>x. f(f x) \<noteq> x"
   2.538 +    then have non_fp [simp]: "f z \<noteq> z" for z
   2.539 +      by metis
   2.540 +    have holf: "f holomorphic_on X" for X
   2.541 +      using assms holomorphic_on_subset by blast
   2.542 +    obtain c where c: "(\<lambda>x. (f(f x) - x)/(f x - x)) = (\<lambda>x. c)"
   2.543 +    proof (rule little_Picard_01)
   2.544 +      show "(\<lambda>x. (f(f x) - x)/(f x - x)) holomorphic_on UNIV"
   2.545 +        apply (intro holomorphic_intros holf holomorphic_on_compose [unfolded o_def, OF holf])
   2.546 +        using non_fp by auto
   2.547 +    qed auto
   2.548 +    then obtain "c \<noteq> 0" "c \<noteq> 1"
   2.549 +      by (metis (no_types, hide_lams) non_ff diff_zero divide_eq_0_iff right_inverse_eq)
   2.550 +    have eq: "f(f x) - c * f x = x*(1 - c)" for x
   2.551 +      using fun_cong [OF c, of x] by (simp add: field_simps)
   2.552 +    have df_times_dff: "deriv f z * (deriv f (f z) - c) = 1 * (1 - c)" for z
   2.553 +    proof (rule DERIV_unique)
   2.554 +      show "((\<lambda>x. f (f x) - c * f x) has_field_derivative
   2.555 +              deriv f z * (deriv f (f z) - c)) (at z)"
   2.556 +        apply (intro derivative_eq_intros)
   2.557 +            apply (rule DERIV_chain [unfolded o_def, of f])
   2.558 +             apply (auto simp: algebra_simps intro!: holomorphic_derivI [OF holfU])
   2.559 +        done
   2.560 +      show "((\<lambda>x. f (f x) - c * f x) has_field_derivative 1 * (1 - c)) (at z)"
   2.561 +        by (simp add: eq mult_commute_abs)
   2.562 +    qed
   2.563 +    { fix z::complex
   2.564 +      obtain k where k: "deriv f \<circ> f = (\<lambda>x. k)"
   2.565 +      proof (rule little_Picard)
   2.566 +        show "(deriv f \<circ> f) holomorphic_on UNIV"
   2.567 +          by (meson holfU holomorphic_deriv holomorphic_on_compose holomorphic_on_subset open_UNIV subset_UNIV)
   2.568 +        obtain "deriv f (f x) \<noteq> 0" "deriv f (f x) \<noteq> c"  for x
   2.569 +          using df_times_dff \<open>c \<noteq> 1\<close> eq_iff_diff_eq_0
   2.570 +          by (metis lambda_one mult_zero_left mult_zero_right)
   2.571 +        then show "range (deriv f \<circ> f) \<inter> {0,c} = {}"
   2.572 +          by force
   2.573 +      qed (use \<open>c \<noteq> 0\<close> in auto)
   2.574 +      have "\<not> f constant_on UNIV"
   2.575 +        by (meson UNIV_I non_ff constant_on_def)
   2.576 +      with holf open_mapping_thm have "open(range f)"
   2.577 +        by blast
   2.578 +      obtain l where l: "\<And>x. f x - k * x = l"
   2.579 +      proof (rule DERIV_zero_connected_constant [of UNIV "{}" "\<lambda>x. f x - k * x"], simp_all)
   2.580 +        have "deriv f w - k = 0" for w
   2.581 +        proof (rule analytic_continuation [OF _ open_UNIV connected_UNIV subset_UNIV, of "\<lambda>z. deriv f z - k" "f z" "range f" w])
   2.582 +          show "(\<lambda>z. deriv f z - k) holomorphic_on UNIV"
   2.583 +            by (intro holomorphic_intros holf open_UNIV)
   2.584 +          show "f z islimpt range f"
   2.585 +            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)
   2.586 +          show "\<And>z. z \<in> range f \<Longrightarrow> deriv f z - k = 0"
   2.587 +            by (metis comp_def diff_self image_iff k)
   2.588 +        qed auto
   2.589 +        moreover
   2.590 +        have "((\<lambda>x. f x - k * x) has_field_derivative deriv f x - k) (at x)" for x
   2.591 +          by (metis DERIV_cmult_Id Deriv.field_differentiable_diff UNIV_I field_differentiable_derivI holf holomorphic_on_def)
   2.592 +        ultimately
   2.593 +        show "\<forall>x. ((\<lambda>x. f x - k * x) has_field_derivative 0) (at x)"
   2.594 +          by auto
   2.595 +        show "continuous_on UNIV (\<lambda>x. f x - k * x)"
   2.596 +          by (simp add: continuous_on_diff holf holomorphic_on_imp_continuous_on)
   2.597 +      qed (auto simp: connected_UNIV)
   2.598 +      have False
   2.599 +      proof (cases "k=1")
   2.600 +        case True
   2.601 +        then have "\<exists>x. k * x + l \<noteq> a + x" for a
   2.602 +          using l non [of a] ext [of f "op + a"]
   2.603 +          by (metis add.commute diff_eq_eq)
   2.604 +        with True show ?thesis by auto
   2.605 +      next
   2.606 +        case False
   2.607 +        have "\<And>x. (1 - k) * x \<noteq> f 0"
   2.608 +          using l [of 0] apply (simp add: algebra_simps)
   2.609 +          by (metis diff_add_cancel l mult.commute non_fp)
   2.610 +        then show False
   2.611 +          by (metis False eq_iff_diff_eq_0 mult.commute nonzero_mult_div_cancel_right times_divide_eq_right)
   2.612 +      qed
   2.613 +    }
   2.614 +  }
   2.615 +  then show thesis
   2.616 +    using that by blast
   2.617 +qed
   2.618 +
   2.619 +
   2.620 +subsection\<open>The Arzelà–Ascoli theorem\<close>
   2.621 +
   2.622 +lemma subsequence_diagonalization_lemma:
   2.623 +  fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
   2.624 +  assumes sub: "\<And>i r. \<exists>k. subseq k \<and> P i (r \<circ> k)"
   2.625 +      and P_P:  "\<And>i r::nat \<Rightarrow> 'a. \<And>k1 k2 N.
   2.626 +                   \<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)"
   2.627 +   obtains k where "subseq k" "\<And>i. P i (r \<circ> k)"
   2.628 +proof -
   2.629 +  obtain kk where "\<And>i r. subseq (kk i r) \<and> P i (r \<circ> (kk i r))"
   2.630 +    using sub by metis
   2.631 +  then have sub_kk: "\<And>i r. subseq (kk i r)" and P_kk: "\<And>i r. P i (r \<circ> (kk i r))"
   2.632 +    by auto
   2.633 +  define rr where "rr \<equiv> rec_nat (kk 0 r) (\<lambda>n x. x \<circ> kk (Suc n) (r \<circ> x))"
   2.634 +  then have [simp]: "rr 0 = kk 0 r" "\<And>n. rr(Suc n) = rr n \<circ> kk (Suc n) (r \<circ> rr n)"
   2.635 +    by auto
   2.636 +  show thesis
   2.637 +  proof
   2.638 +    have sub_rr: "subseq (rr i)" for i
   2.639 +      using sub_kk  by (induction i) (auto simp: subseq_def o_def)
   2.640 +    have P_rr: "P i (r \<circ> rr i)" for i
   2.641 +      using P_kk  by (induction i) (auto simp: o_def)
   2.642 +    have "i \<le> i+d \<Longrightarrow> rr i n \<le> rr (i+d) n" for d i n
   2.643 +    proof (induction d)
   2.644 +      case 0 then show ?case
   2.645 +        by simp
   2.646 +    next
   2.647 +      case (Suc d) then show ?case
   2.648 +        apply simp
   2.649 +          using seq_suble [OF sub_kk] order_trans subseq_le_mono [OF sub_rr] by blast
   2.650 +    qed
   2.651 +    then have "\<And>i j n. i \<le> j \<Longrightarrow> rr i n \<le> rr j n"
   2.652 +      by (metis le_iff_add)
   2.653 +    show "subseq (\<lambda>n. rr n n)"
   2.654 +      apply (simp add: subseq_Suc_iff)
   2.655 +      by (meson Suc_le_eq seq_suble sub_kk sub_rr subseq_mono)
   2.656 +    have "\<exists>j. i \<le> j \<and> rr (n+d) i = rr n j" for d n i
   2.657 +      apply (induction d arbitrary: i, auto)
   2.658 +      by (meson order_trans seq_suble sub_kk)
   2.659 +    then have "\<And>m n i. n \<le> m \<Longrightarrow> \<exists>j. i \<le> j \<and> rr m i = rr n j"
   2.660 +      by (metis le_iff_add)
   2.661 +    then show "P i (r \<circ> (\<lambda>n. rr n n))" for i
   2.662 +      by (meson P_rr P_P)
   2.663 +  qed
   2.664 +qed
   2.665 +
   2.666 +lemma function_convergent_subsequence:
   2.667 +  fixes f :: "[nat,'a] \<Rightarrow> 'b::{real_normed_vector,heine_borel}"
   2.668 +  assumes "countable S" and M: "\<And>n::nat. \<And>x. x \<in> S \<Longrightarrow> norm(f n x) \<le> M"
   2.669 +   obtains k where "subseq k" "\<And>x. x \<in> S \<Longrightarrow> \<exists>l. (\<lambda>n. f (k n) x) \<longlonglongrightarrow> l"
   2.670 +proof (cases "S = {}")
   2.671 +  case True
   2.672 +  then show ?thesis
   2.673 +    using subseq_id that by fastforce
   2.674 +next
   2.675 +  case False
   2.676 +  with \<open>countable S\<close> obtain \<sigma> :: "nat \<Rightarrow> 'a" where \<sigma>: "S = range \<sigma>"
   2.677 +    using uncountable_def by blast
   2.678 +  obtain k where "subseq k" and k: "\<And>i. \<exists>l. (\<lambda>n. (f \<circ> k) n (\<sigma> i)) \<longlonglongrightarrow> l"
   2.679 +  proof (rule subsequence_diagonalization_lemma
   2.680 +      [of "\<lambda>i r. \<exists>l. ((\<lambda>n. (f \<circ> r) n (\<sigma> i)) \<longlongrightarrow> l) sequentially" id])
   2.681 +    show "\<exists>k. subseq k \<and> (\<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k)) n (\<sigma> i)) \<longlonglongrightarrow> l)" for i r
   2.682 +    proof -
   2.683 +      have "f (r n) (\<sigma> i) \<in> cball 0 M" for n
   2.684 +        by (simp add: \<sigma> M)
   2.685 +      then show ?thesis
   2.686 +        using compact_def [of "cball (0::'b) M"] apply simp
   2.687 +        apply (drule_tac x="(\<lambda>n. f (r n) (\<sigma> i))" in spec)
   2.688 +        apply (force simp: o_def)
   2.689 +        done
   2.690 +    qed
   2.691 +    show "\<And>i r k1 k2 N.
   2.692 +               \<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>
   2.693 +               \<Longrightarrow> \<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k2)) n (\<sigma> i)) \<longlonglongrightarrow> l"
   2.694 +      apply (simp add: lim_sequentially)
   2.695 +      apply (erule ex_forward all_forward imp_forward)+
   2.696 +        apply auto
   2.697 +      by (metis (no_types, hide_lams) le_cases order_trans)
   2.698 +  qed auto
   2.699 +  with \<sigma> that show ?thesis
   2.700 +    by force
   2.701 +qed
   2.702 +
   2.703 +
   2.704 +theorem Arzela_Ascoli:
   2.705 +  fixes \<F> :: "[nat,'a::euclidean_space] \<Rightarrow> 'b::{real_normed_vector,heine_borel}"
   2.706 +  assumes "compact S"
   2.707 +      and M: "\<And>n x. x \<in> S \<Longrightarrow> norm(\<F> n x) \<le> M"
   2.708 +      and equicont:
   2.709 +          "\<And>x e. \<lbrakk>x \<in> S; 0 < e\<rbrakk>
   2.710 +                 \<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)"
   2.711 +  obtains g k where "continuous_on S g" "subseq k"
   2.712 +                    "\<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"
   2.713 +proof -
   2.714 +  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)"
   2.715 +    apply (rule compact_uniformly_equicontinuous [OF \<open>compact S\<close>, of "range \<F>"])
   2.716 +    using equicont by (force simp: dist_commute dist_norm)+
   2.717 +  have "continuous_on S g"
   2.718 +       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"
   2.719 +       for g:: "'a \<Rightarrow> 'b" and r :: "nat \<Rightarrow> nat"
   2.720 +  proof (rule uniform_limit_theorem [of _ "\<F> \<circ> r"])
   2.721 +    show "\<forall>\<^sub>F n in sequentially. continuous_on S ((\<F> \<circ> r) n)"
   2.722 +      apply (simp add: eventually_sequentially)
   2.723 +      apply (rule_tac x=0 in exI)
   2.724 +      using UEQ apply (force simp: continuous_on_iff)
   2.725 +      done
   2.726 +    show "uniform_limit S (\<F> \<circ> r) g sequentially"
   2.727 +      apply (simp add: uniform_limit_iff eventually_sequentially)
   2.728 +        by (metis dist_norm that)
   2.729 +  qed auto
   2.730 +  moreover
   2.731 +  obtain R where "countable R" "R \<subseteq> S" and SR: "S \<subseteq> closure R"
   2.732 +    by (metis separable that)
   2.733 +  obtain k where "subseq k" and k: "\<And>x. x \<in> R \<Longrightarrow> \<exists>l. (\<lambda>n. \<F> (k n) x) \<longlonglongrightarrow> l"
   2.734 +    apply (rule function_convergent_subsequence [OF \<open>countable R\<close> M])
   2.735 +    using \<open>R \<subseteq> S\<close> apply force+
   2.736 +    done
   2.737 +  then have Cauchy: "Cauchy ((\<lambda>n. \<F> (k n) x))" if "x \<in> R" for x
   2.738 +    using convergent_eq_Cauchy that by blast
   2.739 +  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"
   2.740 +    if "0 < e" for e
   2.741 +  proof -
   2.742 +    obtain d where "0 < d"
   2.743 +      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"
   2.744 +      by (metis UEQ \<open>0 < e\<close> divide_pos_pos zero_less_numeral)
   2.745 +    obtain T where "T \<subseteq> R" and "finite T" and T: "S \<subseteq> (\<Union>c\<in>T. ball c d)"
   2.746 +    proof (rule compactE_image [OF  \<open>compact S\<close>, of R "(\<lambda>x. ball x d)"])
   2.747 +      have "closure R \<subseteq> (\<Union>c\<in>R. ball c d)"
   2.748 +        apply clarsimp
   2.749 +        using \<open>0 < d\<close> closure_approachable by blast
   2.750 +      with SR show "S \<subseteq> (\<Union>c\<in>R. ball c d)"
   2.751 +        by auto
   2.752 +    qed auto
   2.753 +    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
   2.754 +      using Cauchy \<open>0 < e\<close> that unfolding Cauchy_def
   2.755 +      by (metis less_divide_eq_numeral1(1) mult_zero_left)
   2.756 +    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"
   2.757 +      using dist_norm by metis
   2.758 +    have "dist ((\<F> \<circ> k) m x) ((\<F> \<circ> k) n x) < e"
   2.759 +         if m: "Max (MF ` T) \<le> m" and n: "Max (MF ` T) \<le> n" "x \<in> S" for m n x
   2.760 +    proof -
   2.761 +      obtain t where "t \<in> T" and t: "x \<in> ball t d"
   2.762 +        using \<open>x \<in> S\<close> T by auto
   2.763 +      have "norm(\<F> (k m) t - \<F> (k m) x) < e / 3"
   2.764 +        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>)
   2.765 +      moreover
   2.766 +      have "norm(\<F> (k n) t - \<F> (k n) x) < e / 3"
   2.767 +        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>)
   2.768 +      moreover
   2.769 +      have "norm(\<F> (k m) t - \<F> (k n) t) < e / 3"
   2.770 +      proof (rule MF)
   2.771 +        show "t \<in> R"
   2.772 +          using \<open>T \<subseteq> R\<close> \<open>t \<in> T\<close> by blast
   2.773 +        show "MF t \<le> m" "MF t \<le> n"
   2.774 +          by (meson Max_ge \<open>finite T\<close> \<open>t \<in> T\<close> finite_imageI imageI le_trans m n)+
   2.775 +      qed
   2.776 +      ultimately
   2.777 +      show ?thesis
   2.778 +        unfolding dist_norm [symmetric] o_def
   2.779 +          by (metis dist_triangle_third dist_commute)
   2.780 +    qed
   2.781 +    then show ?thesis
   2.782 +      by force
   2.783 +  qed
   2.784 +  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"
   2.785 +    using uniformly_convergent_eq_cauchy [of "\<lambda>x. x \<in> S" "\<F> \<circ> k"]
   2.786 +    apply (simp add: o_def dist_norm)
   2.787 +    by meson
   2.788 +  ultimately show thesis
   2.789 +    by (metis that \<open>subseq k\<close>)
   2.790 +qed
   2.791 +
   2.792 +
   2.793 +
   2.794 +subsubsection\<open>Montel's theorem\<close>
   2.795 +
   2.796 +text\<open>a sequence of holomorphic functions uniformly bounded
   2.797 +on compact subsets of an open set S has a subsequence that converges to a
   2.798 +holomorphic function, and converges \emph{uniformly} on compact subsets of S.\<close>
   2.799 +
   2.800 +
   2.801 +theorem Montel:
   2.802 +  fixes \<F> :: "[nat,complex] \<Rightarrow> complex"
   2.803 +  assumes "open S"
   2.804 +      and \<H>: "\<And>h. h \<in> \<H> \<Longrightarrow> h holomorphic_on S"
   2.805 +      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"
   2.806 +      and rng_f: "range \<F> \<subseteq> \<H>"
   2.807 +  obtains g r
   2.808 +    where "g holomorphic_on S" "subseq r"
   2.809 +          "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>n. \<F> (r n) x) \<longlongrightarrow> g x) sequentially"
   2.810 +          "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K (\<F> \<circ> r) g sequentially"        
   2.811 +proof -
   2.812 +  obtain K where comK: "\<And>n. compact(K n)" and KS: "\<And>n::nat. K n \<subseteq> S"
   2.813 +             and subK: "\<And>X. \<lbrakk>compact X; X \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. X \<subseteq> K n"
   2.814 +    using open_Union_compact_subsets [OF \<open>open S\<close>] by metis
   2.815 +  then have "\<And>i. \<exists>B. \<forall>h \<in> \<H>. \<forall> z \<in> K i. norm(h z) \<le> B"
   2.816 +    by (simp add: bounded)
   2.817 +  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"
   2.818 +    by metis
   2.819 +  have *: "\<exists>r g. subseq r \<and> (\<forall>e > 0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> r) n x - g x) < e)"
   2.820 +        if "\<And>n. \<F> n \<in> \<H>" for \<F> i
   2.821 +  proof -
   2.822 +    obtain g k where "continuous_on (K i) g" "subseq k"
   2.823 +                    "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm(\<F>(k n) x - g x) < e"
   2.824 +    proof (rule Arzela_Ascoli [of "K i" "\<F>" "B i"])
   2.825 +      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"
   2.826 +             if z: "z \<in> K i" and "0 < e" for z e
   2.827 +      proof -
   2.828 +        obtain r where "0 < r" and r: "cball z r \<subseteq> S"
   2.829 +          using z KS [of i] \<open>open S\<close> by (force simp: open_contains_cball)
   2.830 +        have "cball z (2 / 3 * r) \<subseteq> cball z r"
   2.831 +          using \<open>0 < r\<close> by (simp add: cball_subset_cball_iff)
   2.832 +        then have z23S: "cball z (2 / 3 * r) \<subseteq> S"
   2.833 +          using r by blast
   2.834 +        obtain M where "0 < M" and M: "\<And>n w. dist z w \<le> 2/3 * r \<Longrightarrow> norm(\<F> n w) \<le> M"
   2.835 +        proof -
   2.836 +          obtain N where N: "\<forall>n\<ge>N. cball z (2/3 * r) \<subseteq> K n"
   2.837 +            using subK compact_cball [of z "(2 / 3 * r)"] z23S by force
   2.838 +          have "cmod (\<F> n w) \<le> \<bar>B N\<bar> + 1" if "dist z w \<le> 2 / 3 * r" for n w
   2.839 +          proof -
   2.840 +            have "w \<in> K N"
   2.841 +              using N mem_cball that by blast
   2.842 +            then have "cmod (\<F> n w) \<le> B N"
   2.843 +              using B \<open>\<And>n. \<F> n \<in> \<H>\<close> by blast
   2.844 +            also have "... \<le> \<bar>B N\<bar> + 1"
   2.845 +              by simp
   2.846 +            finally show ?thesis .
   2.847 +          qed
   2.848 +          then show ?thesis
   2.849 +            by (rule_tac M="\<bar>B N\<bar> + 1" in that) auto
   2.850 +        qed
   2.851 +        have "cmod (\<F> n z - \<F> n y) < e"
   2.852 +              if "y \<in> K i" and y_near_z: "cmod (z - y) < r/3" "cmod (z - y) < e * r / (6 * M)"
   2.853 +              for n y
   2.854 +        proof -
   2.855 +          have "((\<lambda>w. \<F> n w / (w - \<xi>)) has_contour_integral
   2.856 +                    (2 * pi) * \<i> * winding_number (circlepath z (2 / 3 * r)) \<xi> * \<F> n \<xi>)
   2.857 +                (circlepath z (2 / 3 * r))"
   2.858 +             if "dist \<xi> z < (2 / 3 * r)" for \<xi>
   2.859 +          proof (rule Cauchy_integral_formula_convex_simple)
   2.860 +            have "\<F> n holomorphic_on S"
   2.861 +              by (simp add: \<H> \<open>\<And>n. \<F> n \<in> \<H>\<close>)
   2.862 +            with z23S show "\<F> n holomorphic_on cball z (2 / 3 * r)"
   2.863 +              using holomorphic_on_subset by blast
   2.864 +          qed (use that \<open>0 < r\<close> in \<open>auto simp: dist_commute\<close>)
   2.865 +          then have *: "((\<lambda>w. \<F> n w / (w - \<xi>)) has_contour_integral (2 * pi) * \<i> * \<F> n \<xi>)
   2.866 +                     (circlepath z (2 / 3 * r))"
   2.867 +             if "dist \<xi> z < (2 / 3 * r)" for \<xi>
   2.868 +            using that by (simp add: winding_number_circlepath dist_norm)
   2.869 +           have y: "((\<lambda>w. \<F> n w / (w - y)) has_contour_integral (2 * pi) * \<i> * \<F> n y)
   2.870 +                 (circlepath z (2 / 3 * r))"
   2.871 +             apply (rule *)
   2.872 +             using that \<open>0 < r\<close> by (simp only: dist_norm norm_minus_commute)
   2.873 +           have z: "((\<lambda>w. \<F> n w / (w - z)) has_contour_integral (2 * pi) * \<i> * \<F> n z)
   2.874 +                 (circlepath z (2 / 3 * r))"
   2.875 +             apply (rule *)
   2.876 +             using \<open>0 < r\<close> by simp
   2.877 +           have le_er: "cmod (\<F> n x / (x - y) - \<F> n x / (x - z)) \<le> e / r"
   2.878 +                if "cmod (x - z) = r/3 + r/3" for x
   2.879 +           proof -
   2.880 +             have "~ (cmod (x - y) < r/3)"
   2.881 +               using y_near_z(1) that \<open>M > 0\<close> \<open>r > 0\<close>
   2.882 +               by (metis (full_types) norm_diff_triangle_less norm_minus_commute order_less_irrefl)
   2.883 +             then have r4_le_xy: "r/4 \<le> cmod (x - y)"
   2.884 +               using \<open>r > 0\<close> by simp
   2.885 +             then have neq: "x \<noteq> y" "x \<noteq> z"
   2.886 +               using that \<open>r > 0\<close> by (auto simp: divide_simps norm_minus_commute)
   2.887 +             have leM: "cmod (\<F> n x) \<le> M"
   2.888 +               by (simp add: M dist_commute dist_norm that)
   2.889 +             have "cmod (\<F> n x / (x - y) - \<F> n x / (x - z)) = cmod (\<F> n x) * cmod (1 / (x - y) - 1 / (x - z))"
   2.890 +               by (metis (no_types, lifting) divide_inverse mult.left_neutral norm_mult right_diff_distrib')
   2.891 +             also have "... = cmod (\<F> n x) * cmod ((y - z) / ((x - y) * (x - z)))"
   2.892 +               using neq by (simp add: divide_simps)
   2.893 +             also have "... = cmod (\<F> n x) * (cmod (y - z) / (cmod(x - y) * (2/3 * r)))"
   2.894 +               by (simp add: norm_mult norm_divide that)
   2.895 +             also have "... \<le> M * (cmod (y - z) / (cmod(x - y) * (2/3 * r)))"
   2.896 +               apply (rule mult_mono)
   2.897 +                  apply (rule leM)
   2.898 +                 using \<open>r > 0\<close> \<open>M > 0\<close> neq by auto
   2.899 +               also have "... < M * ((e * r / (6 * M)) / (cmod(x - y) * (2/3 * r)))"
   2.900 +                 unfolding mult_less_cancel_left
   2.901 +                 using y_near_z(2) \<open>M > 0\<close> \<open>r > 0\<close> neq
   2.902 +                 apply (simp add: field_simps mult_less_0_iff norm_minus_commute)
   2.903 +                 done
   2.904 +             also have "... \<le> e/r"
   2.905 +               using \<open>e > 0\<close> \<open>r > 0\<close> r4_le_xy by (simp add: divide_simps)
   2.906 +             finally show ?thesis by simp
   2.907 +           qed
   2.908 +           have "(2 * pi) * cmod (\<F> n y - \<F> n z) = cmod ((2 * pi) * \<i> * \<F> n y - (2 * pi) * \<i> * \<F> n z)"
   2.909 +             by (simp add: right_diff_distrib [symmetric] norm_mult)
   2.910 +           also have "cmod ((2 * pi) * \<i> * \<F> n y - (2 * pi) * \<i> * \<F> n z) \<le> e / r * (2 * pi * (2 / 3 * r))"
   2.911 +             apply (rule has_contour_integral_bound_circlepath [OF has_contour_integral_diff [OF y z], of "e/r"])
   2.912 +             using \<open>e > 0\<close> \<open>r > 0\<close> le_er by auto
   2.913 +           also have "... = (2 * pi) * e * ((2 / 3))"
   2.914 +             using \<open>r > 0\<close> by (simp add: divide_simps)
   2.915 +           finally have "cmod (\<F> n y - \<F> n z) \<le> e * (2 / 3)"
   2.916 +             by simp
   2.917 +           also have "... < e"
   2.918 +             using \<open>e > 0\<close> by simp
   2.919 +           finally show ?thesis by (simp add: norm_minus_commute)
   2.920 +        qed
   2.921 +        then show ?thesis
   2.922 +          apply (rule_tac x="min (r/3) ((e * r)/(6 * M))" in exI)
   2.923 +          using \<open>0 < e\<close> \<open>0 < r\<close> \<open>0 < M\<close> by simp
   2.924 +      qed
   2.925 +      show "\<And>n x.  x \<in> K i \<Longrightarrow> cmod (\<F> n x) \<le> B i"
   2.926 +        using B \<open>\<And>n. \<F> n \<in> \<H>\<close> by blast
   2.927 +    qed (use comK in \<open>fastforce+\<close>)
   2.928 +    then show ?thesis
   2.929 +      by fastforce
   2.930 +  qed
   2.931 +  have "\<exists>k g. subseq k \<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)"
   2.932 +         for i r
   2.933 +    apply (rule *)
   2.934 +    using rng_f by auto
   2.935 +  then have **: "\<And>i r. \<exists>k. subseq k \<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)"
   2.936 +    by (force simp: o_assoc)
   2.937 +  obtain k where "subseq k"
   2.938 +             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"
   2.939 +    apply (rule subsequence_diagonalization_lemma [OF **, of id])
   2.940 +     apply (erule ex_forward all_forward imp_forward)+
   2.941 +      apply auto
   2.942 +    apply (rule_tac x="max N Na" in exI, fastforce+)
   2.943 +    done
   2.944 +  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"
   2.945 +    by simp
   2.946 +  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
   2.947 +  proof -
   2.948 +    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"
   2.949 +      using lt_e by metis
   2.950 +    obtain N where "\<And>n. n \<ge> N \<Longrightarrow> z \<in> K n"
   2.951 +      using subK [of "{z}"] that \<open>z \<in> S\<close> by auto
   2.952 +    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"
   2.953 +      using G by auto
   2.954 +    ultimately show ?thesis
   2.955 +      by (metis comp_apply order_refl)
   2.956 +  qed
   2.957 +  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"
   2.958 +    by metis
   2.959 +  show ?thesis
   2.960 +  proof
   2.961 +    show g_lim: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. \<F> (k n) x) \<longlonglongrightarrow> g x"
   2.962 +      by (simp add: lim_sequentially g dist_norm)    
   2.963 +    have dg_le_e: "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>T. cmod (\<F> (k n) x - g x) < e"
   2.964 +      if T: "compact T" "T \<subseteq> S" and "0 < e" for T e
   2.965 +    proof -
   2.966 +      obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> T \<subseteq> K n"
   2.967 +        using subK [OF T] by blast
   2.968 +      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"
   2.969 +        using lt_e by blast
   2.970 +      have geq: "g w = h w" if "w \<in> T" for w
   2.971 +        apply (rule LIMSEQ_unique [of "\<lambda>n. \<F>(k n) w"])
   2.972 +        using \<open>T \<subseteq> S\<close> g_lim that apply blast
   2.973 +        using h N that by (force simp: lim_sequentially dist_norm)
   2.974 +      show ?thesis
   2.975 +        using T h N \<open>0 < e\<close> by (fastforce simp add: geq)
   2.976 +    qed
   2.977 +    then show "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk>
   2.978 +         \<Longrightarrow> uniform_limit K (\<F> \<circ> k) g sequentially"
   2.979 +      by (simp add: uniform_limit_iff dist_norm eventually_sequentially)
   2.980 +    show "g holomorphic_on S"
   2.981 +    proof (rule holomorphic_uniform_sequence [OF \<open>open S\<close> \<H>])
   2.982 +      show "\<And>n. (\<F> \<circ> k) n \<in> \<H>"
   2.983 +        by (simp add: range_subsetD rng_f)
   2.984 +      show "\<exists>d>0. cball z d \<subseteq> S \<and> uniform_limit (cball z d) (\<lambda>n. (\<F> \<circ> k) n) g sequentially"
   2.985 +        if "z \<in> S" for z
   2.986 +      proof -
   2.987 +        obtain d where d: "d>0" "cball z d \<subseteq> S"
   2.988 +          using \<open>open S\<close> \<open>z \<in> S\<close> open_contains_cball by blast
   2.989 +        then have "uniform_limit (cball z d) (\<F> \<circ> k) g sequentially"
   2.990 +          using dg_le_e compact_cball by (auto simp: uniform_limit_iff eventually_sequentially dist_norm)
   2.991 +        with d show ?thesis by blast
   2.992 +      qed
   2.993 +    qed
   2.994 +  qed (auto simp: \<open>subseq k\<close>)
   2.995 +qed
   2.996 +
   2.997 +
   2.998 +
   2.999 +subsection\<open>Some simple but useful cases of Hurwitz's theorem\<close>
  2.1000 +
  2.1001 +proposition Hurwitz_no_zeros:
  2.1002 +  assumes S: "open S" "connected S"
  2.1003 +      and holf: "\<And>n::nat. \<F> n holomorphic_on S"
  2.1004 +      and holg: "g holomorphic_on S"
  2.1005 +      and ul_g: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K \<F> g sequentially"
  2.1006 +      and nonconst: "\<And>c. \<exists>z \<in> S. g z \<noteq> c"
  2.1007 +      and nz: "\<And>n z. z \<in> S \<Longrightarrow> \<F> n z \<noteq> 0"
  2.1008 +      and "z0 \<in> S"
  2.1009 +      shows "g z0 \<noteq> 0"
  2.1010 +proof
  2.1011 +  assume g0: "g z0 = 0"
  2.1012 +  obtain h r m
  2.1013 +    where "0 < m" "0 < r" and subS: "ball z0 r \<subseteq> S"
  2.1014 +      and holh: "h holomorphic_on ball z0 r"
  2.1015 +      and geq:  "\<And>w. w \<in> ball z0 r \<Longrightarrow> g w = (w - z0)^m * h w"
  2.1016 +      and hnz:  "\<And>w. w \<in> ball z0 r \<Longrightarrow> h w \<noteq> 0"
  2.1017 +    by (blast intro: holomorphic_factor_zero_nonconstant [OF holg S \<open>z0 \<in> S\<close> g0 nonconst])
  2.1018 +  then have holf0: "\<F> n holomorphic_on ball z0 r" for n
  2.1019 +    by (meson holf holomorphic_on_subset)
  2.1020 +  have *: "((\<lambda>z. deriv (\<F> n) z / \<F> n z) has_contour_integral 0) (circlepath z0 (r/2))" for n
  2.1021 +  proof (rule Cauchy_theorem_disc_simple [of _ z0 r])
  2.1022 +    show "(\<lambda>z. deriv (\<F> n) z / \<F> n z) holomorphic_on ball z0 r"
  2.1023 +      apply (intro holomorphic_intros holomorphic_deriv holf holf0 open_ball nz)
  2.1024 +      using \<open>ball z0 r \<subseteq> S\<close> by blast
  2.1025 +  qed (use \<open>0 < r\<close> in auto)
  2.1026 +  have hol_dg: "deriv g holomorphic_on S"
  2.1027 +    by (simp add: \<open>open S\<close> holg holomorphic_deriv)
  2.1028 +  have "continuous_on (sphere z0 (r/2)) (deriv g)"
  2.1029 +    apply (intro holomorphic_on_imp_continuous_on holomorphic_on_subset [OF hol_dg])
  2.1030 +    using \<open>0 < r\<close> subS by auto
  2.1031 +  then have "compact (deriv g ` (sphere z0 (r/2)))"
  2.1032 +    by (rule compact_continuous_image [OF _ compact_sphere])
  2.1033 +  then have bo_dg: "bounded (deriv g ` (sphere z0 (r/2)))"
  2.1034 +    using compact_imp_bounded by blast
  2.1035 +  have "continuous_on (sphere z0 (r/2)) (cmod \<circ> g)"
  2.1036 +    apply (intro continuous_intros holomorphic_on_imp_continuous_on holomorphic_on_subset [OF holg])
  2.1037 +    using \<open>0 < r\<close> subS by auto
  2.1038 +  then have "compact ((cmod \<circ> g) ` sphere z0 (r/2))"
  2.1039 +    by (rule compact_continuous_image [OF _ compact_sphere])
  2.1040 +  moreover have "(cmod \<circ> g) ` sphere z0 (r/2) \<noteq> {}"
  2.1041 +    using \<open>0 < r\<close> by auto
  2.1042 +  ultimately obtain b where b: "b \<in> (cmod \<circ> g) ` sphere z0 (r/2)"
  2.1043 +                               "\<And>t. t \<in> (cmod \<circ> g) ` sphere z0 (r/2) \<Longrightarrow> b \<le> t"
  2.1044 +    using compact_attains_inf [of "(norm \<circ> g) ` (sphere z0 (r/2))"] by blast
  2.1045 +  have "(\<lambda>n. contour_integral (circlepath z0 (r/2)) (\<lambda>z. deriv (\<F> n) z / \<F> n z)) \<longlonglongrightarrow>
  2.1046 +        contour_integral (circlepath z0 (r/2)) (\<lambda>z. deriv g z / g z)"
  2.1047 +  proof (rule contour_integral_uniform_limit_circlepath)
  2.1048 +    show "\<forall>\<^sub>F n in sequentially. (\<lambda>z. deriv (\<F> n) z / \<F> n z) contour_integrable_on circlepath z0 (r/2)"
  2.1049 +      using * contour_integrable_on_def eventually_sequentiallyI by meson
  2.1050 +    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"
  2.1051 +    proof (rule uniform_lim_divide [OF _ _ bo_dg])
  2.1052 +      show "uniform_limit (sphere z0 (r/2)) (\<lambda>a. deriv (\<F> a)) (deriv g) sequentially"
  2.1053 +      proof (rule uniform_limitI)
  2.1054 +        fix e::real
  2.1055 +        assume "0 < e"
  2.1056 +        have *: "dist (deriv (\<F> n) w) (deriv g w) < e"
  2.1057 +          if e8: "\<And>x. dist z0 x \<le> 3 * r / 4 \<Longrightarrow> dist (\<F> n x) (g x) * 8 < r * e"
  2.1058 +          and w: "dist w z0 = r/2"  for n w
  2.1059 +        proof -
  2.1060 +          have "ball w (r/4) \<subseteq> ball z0 r"  "cball w (r/4) \<subseteq> ball z0 r"
  2.1061 +            using \<open>0 < r\<close> by (simp_all add: ball_subset_ball_iff cball_subset_ball_iff w)
  2.1062 +          with subS have wr4_sub: "ball w (r/4) \<subseteq> S" "cball w (r/4) \<subseteq> S" by force+
  2.1063 +          moreover
  2.1064 +          have "(\<lambda>z. \<F> n z - g z) holomorphic_on S"
  2.1065 +            by (intro holomorphic_intros holf holg)
  2.1066 +          ultimately have hol: "(\<lambda>z. \<F> n z - g z) holomorphic_on ball w (r/4)"
  2.1067 +            and cont: "continuous_on (cball w (r / 4)) (\<lambda>z. \<F> n z - g z)"
  2.1068 +            using holomorphic_on_subset by (blast intro: holomorphic_on_imp_continuous_on)+
  2.1069 +          have "w \<in> S"
  2.1070 +            using \<open>0 < r\<close> wr4_sub by auto
  2.1071 +          have "\<And>y. dist w y < r / 4 \<Longrightarrow> dist z0 y \<le> 3 * r / 4"
  2.1072 +            apply (rule dist_triangle_le [where z=w])
  2.1073 +            using w by (simp add: dist_commute)
  2.1074 +          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)"
  2.1075 +            by (simp add: dist_norm [symmetric])
  2.1076 +          have "\<F> n field_differentiable at w"
  2.1077 +            by (metis holomorphic_on_imp_differentiable_at \<open>w \<in> S\<close> holf \<open>open S\<close>)
  2.1078 +          moreover
  2.1079 +          have "g field_differentiable at w"
  2.1080 +            using \<open>w \<in> S\<close> \<open>open S\<close> holg holomorphic_on_imp_differentiable_at by auto
  2.1081 +          moreover
  2.1082 +          have "cmod (deriv (\<lambda>w. \<F> n w - g w) w) * 2 \<le> e"
  2.1083 +            apply (rule Cauchy_higher_deriv_bound [OF hol cont in_ball, of 1, simplified])
  2.1084 +            using \<open>r > 0\<close> by auto
  2.1085 +          ultimately have "dist (deriv (\<F> n) w) (deriv g w) \<le> e/2"
  2.1086 +            by (simp add: dist_norm)
  2.1087 +          then show ?thesis
  2.1088 +            using \<open>e > 0\<close> by auto
  2.1089 +        qed
  2.1090 +        have "cball z0 (3 * r / 4) \<subseteq> ball z0 r"
  2.1091 +          by (simp add: cball_subset_ball_iff \<open>0 < r\<close>)
  2.1092 +        with subS have "uniform_limit (cball z0 (3 * r/4)) \<F> g sequentially"
  2.1093 +          by (force intro: ul_g)
  2.1094 +        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"
  2.1095 +          using \<open>0 < e\<close> \<open>0 < r\<close> by (force simp: intro!: uniform_limitD)
  2.1096 +        then show "\<forall>\<^sub>F n in sequentially. \<forall>x \<in> sphere z0 (r/2). dist (deriv (\<F> n) x) (deriv g x) < e"
  2.1097 +          apply (simp add: eventually_sequentially)
  2.1098 +          apply (elim ex_forward all_forward imp_forward asm_rl)
  2.1099 +          using * apply (force simp: dist_commute)
  2.1100 +          done
  2.1101 +      qed
  2.1102 +      show "uniform_limit (sphere z0 (r/2)) \<F> g sequentially"
  2.1103 +      proof (rule uniform_limitI)
  2.1104 +        fix e::real
  2.1105 +        assume "0 < e"
  2.1106 +        have "sphere z0 (r/2) \<subseteq> ball z0 r"
  2.1107 +          using \<open>0 < r\<close> by auto
  2.1108 +        with subS have "uniform_limit (sphere z0 (r/2)) \<F> g sequentially"
  2.1109 +          by (force intro: ul_g)
  2.1110 +        then show "\<forall>\<^sub>F n in sequentially. \<forall>x \<in> sphere z0 (r/2). dist (\<F> n x) (g x) < e"
  2.1111 +          apply (rule uniform_limitD)
  2.1112 +          using \<open>0 < e\<close> by force
  2.1113 +      qed
  2.1114 +      show "b > 0" "\<And>x. x \<in> sphere z0 (r/2) \<Longrightarrow> b \<le> cmod (g x)"
  2.1115 +        using b \<open>0 < r\<close> by (fastforce simp: geq hnz)+
  2.1116 +    qed
  2.1117 +  qed (use \<open>0 < r\<close> in auto)
  2.1118 +  then have "(\<lambda>n. 0) \<longlonglongrightarrow> contour_integral (circlepath z0 (r/2)) (\<lambda>z. deriv g z / g z)"
  2.1119 +    by (simp add: contour_integral_unique [OF *])
  2.1120 +  then have "contour_integral (circlepath z0 (r/2)) (\<lambda>z. deriv g z / g z) = 0"
  2.1121 +    by (simp add: LIMSEQ_const_iff)
  2.1122 +  moreover
  2.1123 +  have "contour_integral (circlepath z0 (r/2)) (\<lambda>z. deriv g z / g z) =
  2.1124 +        contour_integral (circlepath z0 (r/2)) (\<lambda>z. m / (z - z0) + deriv h z / h z)"
  2.1125 +  proof (rule contour_integral_eq, use \<open>0 < r\<close> in simp)
  2.1126 +    fix w
  2.1127 +    assume w: "dist z0 w * 2 = r"
  2.1128 +    then have w_inb: "w \<in> ball z0 r"
  2.1129 +      using \<open>0 < r\<close> by auto
  2.1130 +    have h_der: "(h has_field_derivative deriv h w) (at w)"
  2.1131 +      using holh holomorphic_derivI w_inb by blast
  2.1132 +    have "deriv g w = ((of_nat m * h w + deriv h w * (w - z0)) * (w - z0) ^ m) / (w - z0)"
  2.1133 +         if "r = dist z0 w * 2" "w \<noteq> z0"
  2.1134 +    proof -
  2.1135 +      have "((\<lambda>w. (w - z0) ^ m * h w) has_field_derivative
  2.1136 +            (m * h w + deriv h w * (w - z0)) * (w - z0) ^ m / (w - z0)) (at w)"
  2.1137 +        apply (rule derivative_eq_intros h_der refl)+
  2.1138 +        using that \<open>m > 0\<close> \<open>0 < r\<close> apply (simp add: divide_simps distrib_right)
  2.1139 +        apply (metis Suc_pred mult.commute power_Suc)
  2.1140 +        done
  2.1141 +      then show ?thesis
  2.1142 +        apply (rule DERIV_imp_deriv [OF DERIV_transform_within_open [where s = "ball z0 r"]])
  2.1143 +        using that \<open>m > 0\<close> \<open>0 < r\<close>
  2.1144 +          apply (simp_all add: hnz geq)
  2.1145 +        done
  2.1146 +    qed
  2.1147 +    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"
  2.1148 +      by (auto simp: geq divide_simps hnz)
  2.1149 +  qed
  2.1150 +  moreover
  2.1151 +  have "contour_integral (circlepath z0 (r/2)) (\<lambda>z. m / (z - z0) + deriv h z / h z) =
  2.1152 +        2 * of_real pi * ii * m + 0"
  2.1153 +  proof (rule contour_integral_unique [OF has_contour_integral_add])
  2.1154 +    show "((\<lambda>x. m / (x - z0)) has_contour_integral 2 * of_real pi * \<i> * m) (circlepath z0 (r/2))"
  2.1155 +      by (force simp: \<open>0 < r\<close> intro: Cauchy_integral_circlepath_simple)
  2.1156 +    show "((\<lambda>x. deriv h x / h x) has_contour_integral 0) (circlepath z0 (r/2))"
  2.1157 +      apply (rule Cauchy_theorem_disc_simple [of _ z0 r])
  2.1158 +      using hnz holh holomorphic_deriv holomorphic_on_divide \<open>0 < r\<close>
  2.1159 +         apply force+
  2.1160 +      done
  2.1161 +  qed
  2.1162 +  ultimately show False using \<open>0 < m\<close> by auto
  2.1163 +qed
  2.1164 +
  2.1165 +corollary Hurwitz_injective:
  2.1166 +  assumes S: "open S" "connected S"
  2.1167 +      and holf: "\<And>n::nat. \<F> n holomorphic_on S"
  2.1168 +      and holg: "g holomorphic_on S"
  2.1169 +      and ul_g: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K \<F> g sequentially"
  2.1170 +      and nonconst: "\<And>c. \<exists>z \<in> S. g z \<noteq> c"
  2.1171 +      and inj: "\<And>n. inj_on (\<F> n) S"
  2.1172 +    shows "inj_on g S"
  2.1173 +proof -
  2.1174 +  have False if z12: "z1 \<in> S" "z2 \<in> S" "z1 \<noteq> z2" "g z2 = g z1" for z1 z2
  2.1175 +  proof -
  2.1176 +    obtain z0 where "z0 \<in> S" and z0: "g z0 \<noteq> g z2"
  2.1177 +      using nonconst by blast
  2.1178 +    have "(\<lambda>z. g z - g z1) holomorphic_on S"
  2.1179 +      by (intro holomorphic_intros holg)
  2.1180 +    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"
  2.1181 +      apply (rule isolated_zeros [of "\<lambda>z. g z - g z1" S z2 z0])
  2.1182 +      using S \<open>z0 \<in> S\<close> z0 z12 by auto
  2.1183 +    have "g z2 - g z1 \<noteq> 0"
  2.1184 +    proof (rule Hurwitz_no_zeros [of "S - {z1}" "\<lambda>n z. \<F> n z - \<F> n z1" "\<lambda>z. g z - g z1"])
  2.1185 +      show "open (S - {z1})"
  2.1186 +        by (simp add: S open_delete)
  2.1187 +      show "connected (S - {z1})"
  2.1188 +        by (simp add: connected_open_delete [OF S])
  2.1189 +      show "\<And>n. (\<lambda>z. \<F> n z - \<F> n z1) holomorphic_on S - {z1}"
  2.1190 +        by (intro holomorphic_intros holomorphic_on_subset [OF holf]) blast
  2.1191 +      show "(\<lambda>z. g z - g z1) holomorphic_on S - {z1}"
  2.1192 +        by (intro holomorphic_intros holomorphic_on_subset [OF holg]) blast
  2.1193 +      show "uniform_limit K (\<lambda>n z. \<F> n z - \<F> n z1) (\<lambda>z. g z - g z1) sequentially"
  2.1194 +           if "compact K" "K \<subseteq> S - {z1}" for K
  2.1195 +      proof (rule uniform_limitI)
  2.1196 +        fix e::real
  2.1197 +        assume "e > 0"
  2.1198 +        have "uniform_limit K \<F> g sequentially"
  2.1199 +          using that ul_g by fastforce
  2.1200 +        then have K: "\<forall>\<^sub>F n in sequentially. \<forall>x \<in> K. dist (\<F> n x) (g x) < e/2"
  2.1201 +          using \<open>0 < e\<close> by (force simp: intro!: uniform_limitD)
  2.1202 +        have "uniform_limit {z1} \<F> g sequentially"
  2.1203 +          by (simp add: ul_g z12)
  2.1204 +        then have "\<forall>\<^sub>F n in sequentially. \<forall>x \<in> {z1}. dist (\<F> n x) (g x) < e/2"
  2.1205 +          using \<open>0 < e\<close> by (force simp: intro!: uniform_limitD)
  2.1206 +        then have z1: "\<forall>\<^sub>F n in sequentially. dist (\<F> n z1) (g z1) < e/2"
  2.1207 +          by simp
  2.1208 +        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"
  2.1209 +          apply (rule eventually_mono [OF eventually_conj [OF K z1]])
  2.1210 +          apply (simp add: dist_norm algebra_simps del: divide_const_simps)
  2.1211 +          by (metis add.commute dist_commute dist_norm dist_triangle_add_half)
  2.1212 +        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"
  2.1213 +          using eventually_conj [OF K z1]
  2.1214 +          apply (rule eventually_mono)
  2.1215 +          by (metis (no_types, hide_lams) diff_add_eq diff_diff_eq2 dist_commute dist_norm dist_triangle_add_half real_sum_of_halves)
  2.1216 +        then
  2.1217 +        show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e"
  2.1218 +          by simp
  2.1219 +      qed
  2.1220 +      show "\<And>c. \<exists>z\<in>S - {z1}. g z - g z1 \<noteq> c"
  2.1221 +        by (metis Diff_iff \<open>z0 \<in> S\<close> empty_iff insert_iff right_minus_eq z0 z12)
  2.1222 +      show "\<And>n z. z \<in> S - {z1} \<Longrightarrow> \<F> n z - \<F> n z1 \<noteq> 0"
  2.1223 +        by (metis DiffD1 DiffD2 eq_iff_diff_eq_0 inj inj_onD insertI1 \<open>z1 \<in> S\<close>)
  2.1224 +      show "z2 \<in> S - {z1}"
  2.1225 +        using \<open>z2 \<in> S\<close> \<open>z1 \<noteq> z2\<close> by auto
  2.1226 +    qed
  2.1227 +    with z12 show False by auto
  2.1228 +  qed
  2.1229 +  then show ?thesis by (auto simp: inj_on_def)
  2.1230 +qed
  2.1231 +
  2.1232 +
  2.1233 +
  2.1234 +subsection\<open>The Great Picard theorem\<close>
  2.1235 +
  2.1236 +lemma GPicard1:
  2.1237 +  assumes S: "open S" "connected S" and "w \<in> S" "0 < r" "Y \<subseteq> X"
  2.1238 +      and holX: "\<And>h. h \<in> X \<Longrightarrow> h holomorphic_on S"
  2.1239 +      and X01:  "\<And>h z. \<lbrakk>h \<in> X; z \<in> S\<rbrakk> \<Longrightarrow> h z \<noteq> 0 \<and> h z \<noteq> 1"
  2.1240 +      and r:    "\<And>h. h \<in> Y \<Longrightarrow> norm(h w) \<le> r"
  2.1241 +  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"
  2.1242 +proof -
  2.1243 +  obtain e where "e > 0" and e: "cball w e \<subseteq> S"
  2.1244 +    using assms open_contains_cball_eq by blast
  2.1245 +  show ?thesis
  2.1246 +  proof
  2.1247 +    show "0 < exp(pi * exp(pi * (2 + 2 * r + 12)))"
  2.1248 +      by simp
  2.1249 +    show "ball w (e / 2) \<subseteq> S"
  2.1250 +      using e ball_divide_subset_numeral ball_subset_cball by blast
  2.1251 +    show "cmod (h z) \<le> exp (pi * exp (pi * (2 + 2 * r + 12)))"
  2.1252 +         if "h \<in> Y" "z \<in> ball w (e / 2)" for h z
  2.1253 +    proof -
  2.1254 +      have "h \<in> X"
  2.1255 +        using \<open>Y \<subseteq> X\<close> \<open>h \<in> Y\<close>  by blast
  2.1256 +      with holX have "h holomorphic_on S" 
  2.1257 +        by auto
  2.1258 +      then have "h holomorphic_on cball w e"
  2.1259 +        by (metis e holomorphic_on_subset)
  2.1260 +      then have hol_h_o: "(h \<circ> (\<lambda>z. (w + of_real e * z))) holomorphic_on cball 0 1"
  2.1261 +        apply (intro holomorphic_intros holomorphic_on_compose)
  2.1262 +        apply (erule holomorphic_on_subset)
  2.1263 +        using that \<open>e > 0\<close> by (auto simp: dist_norm norm_mult)
  2.1264 +      have norm_le_r: "cmod ((h \<circ> (\<lambda>z. w + complex_of_real e * z)) 0) \<le> r"
  2.1265 +        by (auto simp: r \<open>h \<in> Y\<close>)
  2.1266 +      have le12: "norm (of_real(inverse e) * (z - w)) \<le> 1/2"
  2.1267 +        using that \<open>e > 0\<close> by (simp add: inverse_eq_divide dist_norm norm_minus_commute norm_divide)
  2.1268 +      have non01: "\<And>z::complex. cmod z \<le> 1 \<Longrightarrow> h (w + e * z) \<noteq> 0 \<and> h (w + e * z) \<noteq> 1"
  2.1269 +        apply (rule X01 [OF \<open>h \<in> X\<close>])
  2.1270 +          apply (rule subsetD [OF e])
  2.1271 +        using \<open>0 < e\<close>  by (auto simp: dist_norm norm_mult)
  2.1272 +      have "cmod (h z) \<le> cmod (h (w + of_real e * (inverse e * (z - w))))"
  2.1273 +        using \<open>0 < e\<close> by (simp add: divide_simps)
  2.1274 +      also have "... \<le> exp (pi * exp (pi * (14 + 2 * r)))"
  2.1275 +        using r [OF \<open>h \<in> Y\<close>] Schottky [OF hol_h_o norm_le_r _ _ _ le12] non01 by auto
  2.1276 +      finally
  2.1277 +      show ?thesis by simp
  2.1278 +    qed
  2.1279 +  qed (use \<open>e > 0\<close> in auto)
  2.1280 +qed 
  2.1281 +
  2.1282 +lemma GPicard2:
  2.1283 +  assumes "S \<subseteq> T" "connected T" "S \<noteq> {}" "open S" "\<And>x. \<lbrakk>x islimpt S; x \<in> T\<rbrakk> \<Longrightarrow> x \<in> S"
  2.1284 +    shows "S = T"
  2.1285 +  by (metis assms open_subset connected_clopen closedin_limpt)
  2.1286 +
  2.1287 +    
  2.1288 +lemma GPicard3:
  2.1289 +  assumes S: "open S" "connected S" "w \<in> S" and "Y \<subseteq> X"
  2.1290 +      and holX: "\<And>h. h \<in> X \<Longrightarrow> h holomorphic_on S"
  2.1291 +      and X01:  "\<And>h z. \<lbrakk>h \<in> X; z \<in> S\<rbrakk> \<Longrightarrow> h z \<noteq> 0 \<and> h z \<noteq> 1"
  2.1292 +      and no_hw_le1: "\<And>h. h \<in> Y \<Longrightarrow> norm(h w) \<le> 1"
  2.1293 +      and "compact K" "K \<subseteq> S"
  2.1294 +  obtains B where "\<And>h z. \<lbrakk>h \<in> Y; z \<in> K\<rbrakk> \<Longrightarrow> norm(h z) \<le> B"
  2.1295 +proof -
  2.1296 +  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>
  2.1297 +                               (\<forall>h z'. h \<in> Y \<and> z' \<in> Z \<longrightarrow> norm(h z') \<le> B)}"
  2.1298 +  then have "U \<subseteq> S" by blast
  2.1299 +  have "U = S"
  2.1300 +  proof (rule GPicard2 [OF \<open>U \<subseteq> S\<close> \<open>connected S\<close>])
  2.1301 +    show "U \<noteq> {}"
  2.1302 +    proof -
  2.1303 +      obtain B Z where "0 < B" "open Z" "w \<in> Z" "Z \<subseteq> S" 
  2.1304 +        and  "\<And>h z. \<lbrakk>h \<in> Y; z \<in> Z\<rbrakk> \<Longrightarrow> norm(h z) \<le> B"
  2.1305 +        apply (rule GPicard1 [OF S zero_less_one \<open>Y \<subseteq> X\<close> holX])
  2.1306 +        using no_hw_le1 X01 by force+
  2.1307 +      then show ?thesis
  2.1308 +        unfolding U_def using \<open>w \<in> S\<close> by blast
  2.1309 +    qed
  2.1310 +    show "open U"
  2.1311 +      unfolding open_subopen [of U] by (auto simp: U_def)
  2.1312 +    fix v
  2.1313 +    assume v: "v islimpt U" "v \<in> S"
  2.1314 +    have "~ (\<forall>r>0. \<exists>h\<in>Y. r < cmod (h v))"
  2.1315 +    proof
  2.1316 +      assume "\<forall>r>0. \<exists>h\<in>Y. r < cmod (h v)"
  2.1317 +      then have "\<forall>n. \<exists>h\<in>Y. Suc n < cmod (h v)"
  2.1318 +        by simp
  2.1319 +      then obtain \<F> where FY: "\<And>n. \<F> n \<in> Y" and ltF: "\<And>n. Suc n < cmod (\<F> n v)"
  2.1320 +        by metis
  2.1321 +      define \<G> where "\<G> \<equiv> \<lambda>n z. inverse(\<F> n z)"
  2.1322 +      have hol\<G>: "\<G> n holomorphic_on S" for n
  2.1323 +        apply (simp add: \<G>_def)
  2.1324 +        using FY X01 \<open>Y \<subseteq> X\<close> holX apply (blast intro: holomorphic_on_inverse)
  2.1325 +        done
  2.1326 +      have \<G>not0: "\<G> n z \<noteq> 0" and \<G>not1: "\<G> n z \<noteq> 1" if "z \<in> S" for n z
  2.1327 +        using FY X01 \<open>Y \<subseteq> X\<close> that by (force simp: \<G>_def)+
  2.1328 +      have \<G>_le1: "cmod (\<G> n v) \<le> 1" for n 
  2.1329 +        using less_le_trans linear ltF 
  2.1330 +        by (fastforce simp add: \<G>_def norm_inverse inverse_le_1_iff)
  2.1331 +      define W where "W \<equiv> {h. h holomorphic_on S \<and> (\<forall>z \<in> S. h z \<noteq> 0 \<and> h z \<noteq> 1)}"
  2.1332 +      obtain B Z where "0 < B" "open Z" "v \<in> Z" "Z \<subseteq> S" 
  2.1333 +                   and B: "\<And>h z. \<lbrakk>h \<in> range \<G>; z \<in> Z\<rbrakk> \<Longrightarrow> norm(h z) \<le> B"
  2.1334 +        apply (rule GPicard1 [OF \<open>open S\<close> \<open>connected S\<close> \<open>v \<in> S\<close> zero_less_one, of "range \<G>" W])
  2.1335 +        using hol\<G> \<G>not0 \<G>not1 \<G>_le1 by (force simp: W_def)+
  2.1336 +      then obtain e where "e > 0" and e: "ball v e \<subseteq> Z"
  2.1337 +        by (meson open_contains_ball)
  2.1338 +      obtain h j where holh: "h holomorphic_on ball v e" and "subseq j"
  2.1339 +                   and lim:  "\<And>x. x \<in> ball v e \<Longrightarrow> (\<lambda>n. \<G> (j n) x) \<longlonglongrightarrow> h x"
  2.1340 +                   and ulim: "\<And>K. \<lbrakk>compact K; K \<subseteq> ball v e\<rbrakk>
  2.1341 +                                  \<Longrightarrow> uniform_limit K (\<G> \<circ> j) h sequentially"
  2.1342 +      proof (rule Montel)
  2.1343 +        show "\<And>h. h \<in> range \<G> \<Longrightarrow> h holomorphic_on ball v e"
  2.1344 +          by (metis \<open>Z \<subseteq> S\<close> e hol\<G> holomorphic_on_subset imageE)
  2.1345 +        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"
  2.1346 +          using B e by blast
  2.1347 +      qed auto
  2.1348 +      have "h v = 0"
  2.1349 +      proof (rule LIMSEQ_unique)
  2.1350 +        show "(\<lambda>n. \<G> (j n) v) \<longlonglongrightarrow> h v"
  2.1351 +          using \<open>e > 0\<close> lim by simp
  2.1352 +        have lt_Fj: "real x \<le> cmod (\<F> (j x) v)" for x
  2.1353 +          by (metis of_nat_Suc ltF \<open>subseq j\<close> add.commute less_eq_real_def less_le_trans nat_le_real_less seq_suble)
  2.1354 +        show "(\<lambda>n. \<G> (j n) v) \<longlonglongrightarrow> 0"
  2.1355 +        proof (rule Lim_null_comparison [OF eventually_sequentiallyI seq_harmonic])
  2.1356 +          show "cmod (\<G> (j x) v) \<le> inverse (real x)" if "1 \<le> x" for x
  2.1357 +            using that by (simp add: \<G>_def norm_inverse_le_norm [OF lt_Fj])
  2.1358 +        qed        
  2.1359 +      qed
  2.1360 +      have "h v \<noteq> 0"
  2.1361 +      proof (rule Hurwitz_no_zeros [of "ball v e" "\<G> \<circ> j" h])
  2.1362 +        show "\<And>n. (\<G> \<circ> j) n holomorphic_on ball v e"
  2.1363 +          using \<open>Z \<subseteq> S\<close> e hol\<G> by force
  2.1364 +        show "\<And>n z. z \<in> ball v e \<Longrightarrow> (\<G> \<circ> j) n z \<noteq> 0"
  2.1365 +          using \<G>not0 \<open>Z \<subseteq> S\<close> e by fastforce
  2.1366 +        show "\<exists>z\<in>ball v e. h z \<noteq> c" for c
  2.1367 +        proof -
  2.1368 +          have False if "\<And>z. dist v z < e \<Longrightarrow> h z = c"  
  2.1369 +          proof -
  2.1370 +            have "h v = c"
  2.1371 +              by (simp add: \<open>0 < e\<close> that)
  2.1372 +            obtain y where "y \<in> U" "y \<noteq> v" and y: "dist y v < e"
  2.1373 +              using v \<open>e > 0\<close> by (auto simp: islimpt_approachable)
  2.1374 +            then obtain C T where "y \<in> S" "C > 0" "open T" "y \<in> T" "T \<subseteq> S"
  2.1375 +              and "\<And>h z'. \<lbrakk>h \<in> Y; z' \<in> T\<rbrakk> \<Longrightarrow> cmod (h z') \<le> C"
  2.1376 +              using \<open>y \<in> U\<close> by (auto simp: U_def)
  2.1377 +            then have le_C: "\<And>n. cmod (\<F> n y) \<le> C"
  2.1378 +              using FY by blast                
  2.1379 +            have "\<forall>\<^sub>F n in sequentially. dist (\<G> (j n) y) (h y) < inverse C"
  2.1380 +              using uniform_limitD [OF ulim [of "{y}"], of "inverse C"] \<open>C > 0\<close> y
  2.1381 +              by (simp add: dist_commute)
  2.1382 +            then obtain n where "dist (\<G> (j n) y) (h y) < inverse C"
  2.1383 +              by (meson eventually_at_top_linorder order_refl)
  2.1384 +            moreover
  2.1385 +            have "h y = h v"
  2.1386 +              by (metis \<open>h v = c\<close> dist_commute that y)
  2.1387 +            ultimately have "norm (\<G> (j n) y) < inverse C"
  2.1388 +              by (simp add: \<open>h v = 0\<close>)
  2.1389 +            then have "C < norm (\<F> (j n) y)"
  2.1390 +              apply (simp add: \<G>_def)
  2.1391 +              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)
  2.1392 +            show False
  2.1393 +              using \<open>C < cmod (\<F> (j n) y)\<close> le_C not_less by blast
  2.1394 +          qed
  2.1395 +          then show ?thesis by force
  2.1396 +        qed
  2.1397 +        show "h holomorphic_on ball v e"
  2.1398 +          by (simp add: holh)
  2.1399 +        show "\<And>K. \<lbrakk>compact K; K \<subseteq> ball v e\<rbrakk> \<Longrightarrow> uniform_limit K (\<G> \<circ> j) h sequentially"
  2.1400 +          by (simp add: ulim)
  2.1401 +      qed (use \<open>e > 0\<close> in auto)
  2.1402 +      with \<open>h v = 0\<close> show False by blast
  2.1403 +    qed
  2.1404 +    then show "v \<in> U"
  2.1405 +      apply (clarsimp simp add: U_def v)
  2.1406 +      apply (rule GPicard1[OF \<open>open S\<close> \<open>connected S\<close> \<open>v \<in> S\<close> _ \<open>Y \<subseteq> X\<close> holX])
  2.1407 +      using X01 no_hw_le1 apply (meson | force simp: not_less)+
  2.1408 +      done
  2.1409 +  qed
  2.1410 +  have "\<And>x. x \<in> K \<longrightarrow> x \<in> U"
  2.1411 +    using \<open>U = S\<close> \<open>K \<subseteq> S\<close> by blast
  2.1412 +  then have "\<And>x. x \<in> K \<longrightarrow> (\<exists>B Z. 0 < B \<and> open Z \<and> x \<in> Z \<and> 
  2.1413 +                               (\<forall>h z'. h \<in> Y \<and> z' \<in> Z \<longrightarrow> norm(h z') \<le> B))"
  2.1414 +    unfolding U_def by blast
  2.1415 +  then obtain F Z where F: "\<And>x. x \<in> K \<Longrightarrow> open (Z x) \<and> x \<in> Z x \<and> 
  2.1416 +                               (\<forall>h z'. h \<in> Y \<and> z' \<in> Z x \<longrightarrow> norm(h z') \<le> F x)"
  2.1417 +    by metis
  2.1418 +  then obtain L where "L \<subseteq> K" "finite L" and L: "K \<subseteq> (\<Union>c \<in> L. Z c)"
  2.1419 +    by (auto intro: compactE_image [OF \<open>compact K\<close>, of K Z])
  2.1420 +  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"
  2.1421 +    using F by blast
  2.1422 +  have "\<exists>B. \<forall>h z. h \<in> Y \<and> z \<in> K \<longrightarrow> norm(h z) \<le> B"
  2.1423 +  proof (cases "L = {}")
  2.1424 +    case True with L show ?thesis by simp
  2.1425 +  next
  2.1426 +    case False
  2.1427 +    with \<open>finite L\<close> show ?thesis 
  2.1428 +      apply (rule_tac x = "Max (F ` L)" in exI)
  2.1429 +      apply (simp add: linorder_class.Max_ge_iff)
  2.1430 +      using * F  by (metis L UN_E subsetD)
  2.1431 +  qed
  2.1432 +  with that show ?thesis by metis
  2.1433 +qed
  2.1434 +    
  2.1435 +  
  2.1436 +lemma GPicard4:
  2.1437 +  assumes "0 < k" and holf: "f holomorphic_on (ball 0 k - {0})" 
  2.1438 +      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)"
  2.1439 +  obtains \<epsilon> where "0 < \<epsilon>" "\<epsilon> < k" "\<And>z. z \<in> ball 0 \<epsilon> - {0} \<Longrightarrow> norm(f z) \<le> B"
  2.1440 +proof -
  2.1441 +  obtain \<epsilon> where "0 < \<epsilon>" "\<epsilon> < k/2" and \<epsilon>: "\<And>z. norm z = \<epsilon> \<Longrightarrow> norm(f z) \<le> B"
  2.1442 +    using AE [of "k/2"] \<open>0 < k\<close> by auto
  2.1443 +  show ?thesis
  2.1444 +  proof
  2.1445 +    show "\<epsilon> < k"
  2.1446 +      using \<open>0 < k\<close> \<open>\<epsilon> < k/2\<close> by auto
  2.1447 +    show "cmod (f \<xi>) \<le> B" if \<xi>: "\<xi> \<in> ball 0 \<epsilon> - {0}" for \<xi>
  2.1448 +    proof -
  2.1449 +      obtain d where "0 < d" "d < norm \<xi>" and d: "\<And>z. norm z = d \<Longrightarrow> norm(f z) \<le> B"
  2.1450 +        using AE [of "norm \<xi>"] \<open>\<epsilon> < k\<close> \<xi> by auto
  2.1451 +      have [simp]: "closure (cball 0 \<epsilon> - ball 0 d) = cball 0 \<epsilon> - ball 0 d"
  2.1452 +        by (blast intro!: closure_closed)
  2.1453 +      have [simp]: "interior (cball 0 \<epsilon> - ball 0 d) = ball 0 \<epsilon> - cball (0::complex) d"
  2.1454 +        using \<open>0 < \<epsilon>\<close> \<open>0 < d\<close> by (simp add: interior_diff)
  2.1455 +      have *: "norm(f w) \<le> B" if "w \<in> cball 0 \<epsilon> - ball 0 d" for w
  2.1456 +      proof (rule maximum_modulus_frontier [of f "cball 0 \<epsilon> - ball 0 d"])
  2.1457 +        show "f holomorphic_on interior (cball 0 \<epsilon> - ball 0 d)"
  2.1458 +          apply (rule holomorphic_on_subset [OF holf])
  2.1459 +          using \<open>\<epsilon> < k\<close> \<open>0 < d\<close> that by auto
  2.1460 +        show "continuous_on (closure (cball 0 \<epsilon> - ball 0 d)) f"
  2.1461 +          apply (rule holomorphic_on_imp_continuous_on)
  2.1462 +          apply (rule holomorphic_on_subset [OF holf])
  2.1463 +          using \<open>0 < d\<close> \<open>\<epsilon> < k\<close> by auto
  2.1464 +        show "\<And>z. z \<in> frontier (cball 0 \<epsilon> - ball 0 d) \<Longrightarrow> cmod (f z) \<le> B"
  2.1465 +          apply (simp add: frontier_def)
  2.1466 +          using \<epsilon> d less_eq_real_def by blast
  2.1467 +      qed (use that in auto)
  2.1468 +      show ?thesis
  2.1469 +        using * \<open>d < cmod \<xi>\<close> that by auto
  2.1470 +    qed
  2.1471 +  qed (use \<open>0 < \<epsilon>\<close> in auto)
  2.1472 +qed
  2.1473 +  
  2.1474 +
  2.1475 +lemma GPicard5:
  2.1476 +  assumes holf: "f holomorphic_on (ball 0 1 - {0})"
  2.1477 +      and f01:  "\<And>z. z \<in> ball 0 1 - {0} \<Longrightarrow> f z \<noteq> 0 \<and> f z \<noteq> 1"
  2.1478 +  obtains e B where "0 < e" "e < 1" "0 < B" 
  2.1479 +                    "(\<forall>z \<in> ball 0 e - {0}. norm(f z) \<le> B) \<or>
  2.1480 +                     (\<forall>z \<in> ball 0 e - {0}. norm(f z) \<ge> B)"
  2.1481 +proof -
  2.1482 +  have [simp]: "1 + of_nat n \<noteq> (0::complex)" for n
  2.1483 +    using of_nat_eq_0_iff by fastforce
  2.1484 +  have [simp]: "cmod (1 + of_nat n) = 1 + of_nat n" for n
  2.1485 +    by (metis norm_of_nat of_nat_Suc)
  2.1486 +  have *: "(\<lambda>x::complex. x / of_nat (Suc n)) ` (ball 0 1 - {0}) \<subseteq> ball 0 1 - {0}" for n
  2.1487 +    by (auto simp: norm_divide divide_simps split: if_split_asm)
  2.1488 +  define h where "h \<equiv> \<lambda>n z::complex. f (z / (Suc n))"
  2.1489 +  have holh: "(h n) holomorphic_on ball 0 1 - {0}" for n
  2.1490 +    unfolding h_def
  2.1491 +  proof (rule holomorphic_on_compose_gen [unfolded o_def, OF _ holf *])
  2.1492 +    show "(\<lambda>x. x / of_nat (Suc n)) holomorphic_on ball 0 1 - {0}"
  2.1493 +      by (intro holomorphic_intros) auto
  2.1494 +  qed
  2.1495 +  have h01: "\<And>n z. z \<in> ball 0 1 - {0} \<Longrightarrow> h n z \<noteq> 0 \<and> h n z \<noteq> 1" 
  2.1496 +    unfolding h_def
  2.1497 +    apply (rule f01)
  2.1498 +    using * by force
  2.1499 +  obtain w where w: "w \<in> ball 0 1 - {0::complex}"
  2.1500 +    by (rule_tac w = "1/2" in that) auto
  2.1501 +  consider "infinite {n. norm(h n w) \<le> 1}" | "infinite {n. 1 \<le> norm(h n w)}"
  2.1502 +    by (metis (mono_tags, lifting) infinite_nat_iff_unbounded_le le_cases mem_Collect_eq)
  2.1503 +  then show ?thesis
  2.1504 +  proof cases
  2.1505 +    case 1
  2.1506 +    with infinite_enumerate obtain r where "subseq r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<le> 1}"
  2.1507 +      by blast
  2.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"
  2.1509 +    proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"])  
  2.1510 +      show "range (h \<circ> r) \<subseteq> 
  2.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)}"
  2.1512 +        apply clarsimp
  2.1513 +        apply (intro conjI holomorphic_intros holomorphic_on_compose holh)
  2.1514 +        using h01 apply auto
  2.1515 +        done
  2.1516 +      show "connected (ball 0 1 - {0::complex})"
  2.1517 +        by (simp add: connected_open_delete)
  2.1518 +    qed (use r in auto)        
  2.1519 +    have normf_le_B: "cmod(f z) \<le> B" if "norm z = 1 / (2 * (1 + of_nat (r n)))" for z n
  2.1520 +    proof -
  2.1521 +      have *: "\<And>w. norm w = 1/2 \<Longrightarrow> cmod((f (w / (1 + of_nat (r n))))) \<le> B"
  2.1522 +        using B by (auto simp: h_def o_def)
  2.1523 +      have half: "norm (z * (1 + of_nat (r n))) = 1/2"
  2.1524 +        by (simp add: norm_mult divide_simps that)
  2.1525 +      show ?thesis
  2.1526 +        using * [OF half] by simp
  2.1527 +    qed
  2.1528 +    obtain \<epsilon> where "0 < \<epsilon>" "\<epsilon> < 1" "\<And>z. z \<in> ball 0 \<epsilon> - {0} \<Longrightarrow> cmod(f z) \<le> B"
  2.1529 +    proof (rule GPicard4 [OF zero_less_one holf, of B])
  2.1530 +      fix e::real
  2.1531 +      assume "0 < e" "e < 1"
  2.1532 +      obtain n where "(1/e - 2) / 2 < real n"
  2.1533 +        using reals_Archimedean2 by blast
  2.1534 +      also have "... \<le> r n"
  2.1535 +        using \<open>subseq r\<close> by (simp add: seq_suble)
  2.1536 +      finally have "(1/e - 2) / 2 < real (r n)" .
  2.1537 +      with \<open>0 < e\<close> have e: "e > 1 / (2 + 2 * real (r n))"
  2.1538 +        by (simp add: field_simps)
  2.1539 +      show "\<exists>d>0. d < e \<and> (\<forall>z\<in>sphere 0 d. cmod (f z) \<le> B)"
  2.1540 +        apply (rule_tac x="1 / (2 * (1 + of_nat (r n)))" in exI)
  2.1541 +        using normf_le_B by (simp add: e)
  2.1542 +    qed blast
  2.1543 +    then have \<epsilon>: "cmod (f z) \<le> \<bar>B\<bar> + 1" if "cmod z < \<epsilon>" "z \<noteq> 0" for z
  2.1544 +      using that by fastforce
  2.1545 +    have "0 < \<bar>B\<bar> + 1"
  2.1546 +      by simp
  2.1547 +    then show ?thesis
  2.1548 +      apply (rule that [OF \<open>0 < \<epsilon>\<close> \<open>\<epsilon> < 1\<close>])
  2.1549 +      using \<epsilon> by auto 
  2.1550 +  next
  2.1551 +    case 2
  2.1552 +    with infinite_enumerate obtain r where "subseq r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<ge> 1}"
  2.1553 +      by blast
  2.1554 +    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"
  2.1555 +    proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"])  
  2.1556 +      show "range (\<lambda>n. inverse \<circ> h (r n)) \<subseteq> 
  2.1557 +            {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)}"
  2.1558 +        apply clarsimp
  2.1559 +        apply (intro conjI holomorphic_intros holomorphic_on_compose_gen [unfolded o_def, OF _ holh] holomorphic_on_compose)
  2.1560 +        using h01 apply auto
  2.1561 +        done
  2.1562 +      show "connected (ball 0 1 - {0::complex})"
  2.1563 +        by (simp add: connected_open_delete)
  2.1564 +      show "\<And>j. j \<in> range (\<lambda>n. inverse \<circ> h (r n)) \<Longrightarrow> cmod (j w) \<le> 1"
  2.1565 +        using r norm_inverse_le_norm by fastforce
  2.1566 +    qed (use r in auto)        
  2.1567 +    have norm_if_le_B: "cmod(inverse (f z)) \<le> B" if "norm z = 1 / (2 * (1 + of_nat (r n)))" for z n
  2.1568 +    proof -
  2.1569 +      have *: "inverse (cmod((f (z / (1 + of_nat (r n)))))) \<le> B" if "norm z = 1/2" for z
  2.1570 +        using B [OF that] by (force simp: norm_inverse h_def)
  2.1571 +      have half: "norm (z * (1 + of_nat (r n))) = 1/2"
  2.1572 +        by (simp add: norm_mult divide_simps that)
  2.1573 +      show ?thesis
  2.1574 +        using * [OF half] by (simp add: norm_inverse)
  2.1575 +    qed
  2.1576 +    have hol_if: "(inverse \<circ> f) holomorphic_on (ball 0 1 - {0})"
  2.1577 +      by (metis (no_types, lifting) holf comp_apply f01 holomorphic_on_inverse holomorphic_transform)
  2.1578 +    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"
  2.1579 +    proof (rule GPicard4 [OF zero_less_one hol_if, of B])
  2.1580 +      fix e::real
  2.1581 +      assume "0 < e" "e < 1"
  2.1582 +      obtain n where "(1/e - 2) / 2 < real n"
  2.1583 +        using reals_Archimedean2 by blast
  2.1584 +      also have "... \<le> r n"
  2.1585 +        using \<open>subseq r\<close> by (simp add: seq_suble)
  2.1586 +      finally have "(1/e - 2) / 2 < real (r n)" .
  2.1587 +      with \<open>0 < e\<close> have e: "e > 1 / (2 + 2 * real (r n))"
  2.1588 +        by (simp add: field_simps)
  2.1589 +      show "\<exists>d>0. d < e \<and> (\<forall>z\<in>sphere 0 d. cmod ((inverse \<circ> f) z) \<le> B)"
  2.1590 +        apply (rule_tac x="1 / (2 * (1 + of_nat (r n)))" in exI)
  2.1591 +        using norm_if_le_B by (simp add: e)
  2.1592 +    qed blast
  2.1593 +    have \<epsilon>: "cmod (f z) \<ge> inverse B" and "B > 0" if "cmod z < \<epsilon>" "z \<noteq> 0" for z
  2.1594 +    proof -
  2.1595 +      have "inverse (cmod (f z)) \<le> B"
  2.1596 +        using leB that by (simp add: norm_inverse)
  2.1597 +      moreover
  2.1598 +      have "f z \<noteq> 0"
  2.1599 +        using \<open>\<epsilon> < 1\<close> f01 that by auto
  2.1600 +      ultimately show "cmod (f z) \<ge> inverse B"
  2.1601 +        by (simp add: norm_inverse inverse_le_imp_le)
  2.1602 +      show "B > 0"
  2.1603 +        using \<open>f z \<noteq> 0\<close> \<open>inverse (cmod (f z)) \<le> B\<close> not_le order.trans by fastforce
  2.1604 +    qed
  2.1605 +    then have "B > 0"
  2.1606 +      by (metis \<open>0 < \<epsilon>\<close> dense leI order.asym vector_choose_size)
  2.1607 +    then have "inverse B > 0"
  2.1608 +      by (simp add: divide_simps)
  2.1609 +    then show ?thesis
  2.1610 +      apply (rule that [OF \<open>0 < \<epsilon>\<close> \<open>\<epsilon> < 1\<close>])
  2.1611 +      using \<epsilon> by auto 
  2.1612 +  qed
  2.1613 +qed
  2.1614 +
  2.1615 +  
  2.1616 +lemma GPicard6:
  2.1617 +  assumes "open M" "z \<in> M" "a \<noteq> 0" and holf: "f holomorphic_on (M - {z})"
  2.1618 +      and f0a: "\<And>w. w \<in> M - {z} \<Longrightarrow> f w \<noteq> 0 \<and> f w \<noteq> a"
  2.1619 +  obtains r where "0 < r" "ball z r \<subseteq> M" 
  2.1620 +                  "bounded(f ` (ball z r - {z})) \<or>
  2.1621 +                   bounded((inverse \<circ> f) ` (ball z r - {z}))"
  2.1622 +proof -
  2.1623 +  obtain r where "0 < r" and r: "ball z r \<subseteq> M"
  2.1624 +    using assms openE by blast 
  2.1625 +  let ?g = "\<lambda>w. f (z + of_real r * w) / a"
  2.1626 +  obtain e B where "0 < e" "e < 1" "0 < B" 
  2.1627 +    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)"
  2.1628 +  proof (rule GPicard5)
  2.1629 +    show "?g holomorphic_on ball 0 1 - {0}"
  2.1630 +      apply (intro holomorphic_intros holomorphic_on_compose_gen [unfolded o_def, OF _ holf])
  2.1631 +      using \<open>0 < r\<close> \<open>a \<noteq> 0\<close> r
  2.1632 +      by (auto simp: dist_norm norm_mult subset_eq)
  2.1633 +    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"
  2.1634 +      apply (simp add: divide_simps \<open>a \<noteq> 0\<close>)
  2.1635 +      apply (rule f0a)
  2.1636 +      using \<open>0 < r\<close> r by (auto simp: dist_norm norm_mult subset_eq)
  2.1637 +  qed
  2.1638 +  show ?thesis
  2.1639 +  proof
  2.1640 +    show "0 < e*r"
  2.1641 +      by (simp add: \<open>0 < e\<close> \<open>0 < r\<close>)
  2.1642 +    have "ball z (e * r) \<subseteq> ball z r"
  2.1643 +      by (simp add: \<open>0 < r\<close> \<open>e < 1\<close> order.strict_implies_order subset_ball)
  2.1644 +    then show "ball z (e * r) \<subseteq> M"
  2.1645 +      using r by blast
  2.1646 +    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"
  2.1647 +      using B by blast
  2.1648 +    then show "bounded (f ` (ball z (e * r) - {z})) \<or>
  2.1649 +          bounded ((inverse \<circ> f) ` (ball z (e * r) - {z}))"
  2.1650 +    proof cases
  2.1651 +      case 1
  2.1652 +      have "\<lbrakk>dist z w < e * r; w \<noteq> z\<rbrakk> \<Longrightarrow> cmod (f w) \<le> B * norm a" for w
  2.1653 +        using \<open>a \<noteq> 0\<close> \<open>0 < r\<close> 1 [of "(w - z) / r"]
  2.1654 +        by (simp add: norm_divide dist_norm divide_simps)
  2.1655 +      then show ?thesis
  2.1656 +        by (force simp: intro!: boundedI)
  2.1657 +    next
  2.1658 +      case 2
  2.1659 +      have "\<lbrakk>dist z w < e * r; w \<noteq> z\<rbrakk> \<Longrightarrow> cmod (f w) \<ge> B * norm a" for w
  2.1660 +        using \<open>a \<noteq> 0\<close> \<open>0 < r\<close> 2 [of "(w - z) / r"]
  2.1661 +        by (simp add: norm_divide dist_norm divide_simps)
  2.1662 +      then have "\<lbrakk>dist z w < e * r; w \<noteq> z\<rbrakk> \<Longrightarrow> inverse (cmod (f w)) \<le> inverse (B * norm a)" for w
  2.1663 +        by (metis \<open>0 < B\<close> \<open>a \<noteq> 0\<close> mult_pos_pos norm_inverse norm_inverse_le_norm zero_less_norm_iff)
  2.1664 +      then show ?thesis 
  2.1665 +        by (force simp: norm_inverse intro!: boundedI)
  2.1666 +    qed
  2.1667 +  qed
  2.1668 +qed
  2.1669 +  
  2.1670 +
  2.1671 +theorem great_Picard:
  2.1672 +  assumes "open M" "z \<in> M" "a \<noteq> b" and holf: "f holomorphic_on (M - {z})"
  2.1673 +      and fab: "\<And>w. w \<in> M - {z} \<Longrightarrow> f w \<noteq> a \<and> f w \<noteq> b"
  2.1674 +  obtains l where "(f \<longlongrightarrow> l) (at z) \<or> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
  2.1675 +proof -
  2.1676 +  obtain r where "0 < r" and zrM: "ball z r \<subseteq> M" 
  2.1677 +             and r: "bounded((\<lambda>z. f z - a) ` (ball z r - {z})) \<or>
  2.1678 +                     bounded((inverse \<circ> (\<lambda>z. f z - a)) ` (ball z r - {z}))"
  2.1679 +  proof (rule GPicard6 [OF \<open>open M\<close> \<open>z \<in> M\<close>])
  2.1680 +    show "b - a \<noteq> 0"
  2.1681 +      using assms by auto
  2.1682 +    show "(\<lambda>z. f z - a) holomorphic_on M - {z}"
  2.1683 +      by (intro holomorphic_intros holf)
  2.1684 +  qed (use fab in auto)
  2.1685 +  have holfb: "f holomorphic_on ball z r - {z}"
  2.1686 +    apply (rule holomorphic_on_subset [OF holf])
  2.1687 +    using zrM by auto
  2.1688 +  have holfb_i: "(\<lambda>z. inverse(f z - a)) holomorphic_on ball z r - {z}"
  2.1689 +    apply (intro holomorphic_intros holfb)
  2.1690 +    using fab zrM by fastforce
  2.1691 +  show ?thesis
  2.1692 +    using r
  2.1693 +  proof              
  2.1694 +    assume "bounded ((\<lambda>z. f z - a) ` (ball z r - {z}))"
  2.1695 +    then obtain B where B: "\<And>w. w \<in> (\<lambda>z. f z - a) ` (ball z r - {z}) \<Longrightarrow> norm w \<le> B"
  2.1696 +      by (force simp: bounded_iff)
  2.1697 +    have "\<forall>\<^sub>F w in at z. cmod (f w - a) \<le> B"
  2.1698 +      apply (simp add: eventually_at)
  2.1699 +      apply (rule_tac x=r in exI)
  2.1700 +      using \<open>0 < r\<close> by (auto simp: dist_commute intro!: B)
  2.1701 +    then have "\<exists>B. \<forall>\<^sub>F w in at z. cmod (f w) \<le> B"
  2.1702 +      apply (rule_tac x="B + norm a" in exI)
  2.1703 +        apply (erule eventually_mono)
  2.1704 +      by (metis add.commute add_le_cancel_right norm_triangle_sub order.trans)
  2.1705 +    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"
  2.1706 +      using \<open>0 < r\<close> holomorphic_on_extend_bounded [OF holfb] by auto
  2.1707 +    then have "g \<midarrow>z\<rightarrow> g z"
  2.1708 +      apply (simp add: continuous_at [symmetric])
  2.1709 +      using \<open>0 < r\<close> centre_in_ball field_differentiable_imp_continuous_at holomorphic_on_imp_differentiable_at by blast
  2.1710 +    then have "(f \<longlongrightarrow> g z) (at z)"
  2.1711 +      apply (rule Lim_transform_within_open [of g "g z" z UNIV "ball z r"])
  2.1712 +      using  \<open>0 < r\<close> by (auto simp: gf)
  2.1713 +    then show ?thesis
  2.1714 +      using that by blast
  2.1715 +  next
  2.1716 +    assume "bounded((inverse \<circ> (\<lambda>z. f z - a)) ` (ball z r - {z}))"
  2.1717 +    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"
  2.1718 +      by (force simp: bounded_iff)
  2.1719 +    have "\<forall>\<^sub>F w in at z. cmod (inverse (f w - a)) \<le> B"
  2.1720 +      apply (simp add: eventually_at)
  2.1721 +      apply (rule_tac x=r in exI)
  2.1722 +      using \<open>0 < r\<close> by (auto simp: dist_commute intro!: B)
  2.1723 +    then have "\<exists>B. \<forall>\<^sub>F z in at z. cmod (inverse (f z - a)) \<le> B"
  2.1724 +      by blast
  2.1725 +    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)"
  2.1726 +      using \<open>0 < r\<close> holomorphic_on_extend_bounded [OF holfb_i] by auto
  2.1727 +    then have gz: "g \<midarrow>z\<rightarrow> g z"
  2.1728 +      apply (simp add: continuous_at [symmetric])
  2.1729 +      using \<open>0 < r\<close> centre_in_ball field_differentiable_imp_continuous_at holomorphic_on_imp_differentiable_at by blast
  2.1730 +    have gnz: "\<And>w. w \<in> ball z r - {z} \<Longrightarrow> g w \<noteq> 0"
  2.1731 +      using gf fab zrM by fastforce
  2.1732 +    show ?thesis
  2.1733 +    proof (cases "g z = 0")
  2.1734 +      case True
  2.1735 +      have *: "\<lbrakk>g \<noteq> 0; inverse g = f - a\<rbrakk> \<Longrightarrow> g / (1 + a * g) = inverse f" for f g::complex
  2.1736 +        by (auto simp: field_simps)
  2.1737 +      have "(inverse \<circ> f) \<midarrow>z\<rightarrow> 0"
  2.1738 +      proof (rule Lim_transform_within_open [of "\<lambda>w. g w / (1 + a * g w)" _ _ UNIV "ball z r"])
  2.1739 +        show "(\<lambda>w. g w / (1 + a * g w)) \<midarrow>z\<rightarrow> 0"
  2.1740 +          using True by (auto simp: intro!: tendsto_eq_intros gz)
  2.1741 +        show "\<And>x. \<lbrakk>x \<in> ball z r; x \<noteq> z\<rbrakk> \<Longrightarrow> g x / (1 + a * g x) = (inverse \<circ> f) x"
  2.1742 +          using * gf gnz by simp
  2.1743 +      qed (use \<open>0 < r\<close> in auto)
  2.1744 +      with that show ?thesis by blast
  2.1745 +    next
  2.1746 +      case False
  2.1747 +      show ?thesis
  2.1748 +      proof (cases "1 + a * g z = 0")
  2.1749 +        case True
  2.1750 +        have "(f \<longlongrightarrow> 0) (at z)"
  2.1751 +        proof (rule Lim_transform_within_open [of "\<lambda>w. (1 + a * g w) / g w" _ _ _ "ball z r"])
  2.1752 +          show "(\<lambda>w. (1 + a * g w) / g w) \<midarrow>z\<rightarrow> 0"
  2.1753 +            apply (rule tendsto_eq_intros refl gz \<open>g z \<noteq> 0\<close>)+
  2.1754 +            by (simp add: True)
  2.1755 +          show "\<And>x. \<lbrakk>x \<in> ball z r; x \<noteq> z\<rbrakk> \<Longrightarrow> (1 + a * g x) / g x = f x"
  2.1756 +            using fab fab zrM by (fastforce simp add: gf divide_simps)
  2.1757 +        qed (use \<open>0 < r\<close> in auto)
  2.1758 +        then show ?thesis
  2.1759 +          using that by blast 
  2.1760 +      next
  2.1761 +        case False
  2.1762 +        have *: "\<lbrakk>g \<noteq> 0; inverse g = f - a\<rbrakk> \<Longrightarrow> g / (1 + a * g) = inverse f" for f g::complex
  2.1763 +          by (auto simp: field_simps)
  2.1764 +        have "(inverse \<circ> f) \<midarrow>z\<rightarrow> g z / (1 + a * g z)"
  2.1765 +        proof (rule Lim_transform_within_open [of "\<lambda>w. g w / (1 + a * g w)" _ _ UNIV "ball z r"])
  2.1766 +          show "(\<lambda>w. g w / (1 + a * g w)) \<midarrow>z\<rightarrow> g z / (1 + a * g z)"
  2.1767 +            using False by (auto simp: False intro!: tendsto_eq_intros gz)
  2.1768 +          show "\<And>x. \<lbrakk>x \<in> ball z r; x \<noteq> z\<rbrakk> \<Longrightarrow> g x / (1 + a * g x) = (inverse \<circ> f) x"
  2.1769 +            using * gf gnz by simp
  2.1770 +        qed (use \<open>0 < r\<close> in auto)
  2.1771 +        with that show ?thesis by blast
  2.1772 +      qed
  2.1773 +    qed 
  2.1774 +  qed
  2.1775 +qed
  2.1776 +
  2.1777 +
  2.1778 +corollary great_Picard_alt:
  2.1779 +  assumes M: "open M" "z \<in> M" and holf: "f holomorphic_on (M - {z})"
  2.1780 +    and non: "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
  2.1781 +  obtains a where "- {a} \<subseteq> f ` (M - {z})"
  2.1782 +  apply (simp add: subset_iff image_iff)
  2.1783 +  by (metis great_Picard [OF M _ holf] non)
  2.1784 +    
  2.1785 +
  2.1786 +corollary great_Picard_infinite:
  2.1787 +  assumes M: "open M" "z \<in> M" and holf: "f holomorphic_on (M - {z})"
  2.1788 +    and non: "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
  2.1789 +  obtains a where "\<And>w. w \<noteq> a \<Longrightarrow> infinite {x. x \<in> M - {z} \<and> f x = w}"
  2.1790 +proof -
  2.1791 +  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
  2.1792 +  proof -
  2.1793 +    have finab: "finite {x. x \<in> M - {z} \<and> f x \<in> {a,b}}"
  2.1794 +      using finite_UnI [OF ab]  unfolding mem_Collect_eq insert_iff empty_iff
  2.1795 +      by (simp add: conj_disj_distribL)
  2.1796 +    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"
  2.1797 +    proof -
  2.1798 +      obtain e where "e > 0" and e: "ball z e \<subseteq> M"
  2.1799 +        using assms openE by blast
  2.1800 +      show ?thesis
  2.1801 +      proof (cases "{x \<in> M - {z}. f x \<in> {a, b}} = {}")
  2.1802 +        case True
  2.1803 +        then show ?thesis
  2.1804 +          apply (rule_tac r=e in that)
  2.1805 +          using e \<open>e > 0\<close> by auto
  2.1806 +      next
  2.1807 +        case False
  2.1808 +        let ?r = "min e (Min (dist z ` {x \<in> M - {z}. f x \<in> {a,b}}))"
  2.1809 +        show ?thesis
  2.1810 +        proof
  2.1811 +          show "0 < ?r"
  2.1812 +            using min_less_iff_conj Min_gr_iff finab False \<open>0 < e\<close> by auto
  2.1813 +          have "ball z ?r \<subseteq> ball z e"
  2.1814 +            by (simp add: subset_ball)
  2.1815 +          with e show "ball z ?r \<subseteq> M" by blast
  2.1816 +          show "\<And>x. \<lbrakk>x \<in> M - {z}; f x \<in> {a, b}\<rbrakk> \<Longrightarrow> x \<notin> ball z ?r"
  2.1817 +            using min_less_iff_conj Min_gr_iff finab False \<open>0 < e\<close> by auto
  2.1818 +        qed
  2.1819 +      qed
  2.1820 +    qed
  2.1821 +    have holfb: "f holomorphic_on (ball z r - {z})"
  2.1822 +      apply (rule holomorphic_on_subset [OF holf])
  2.1823 +       using zrM by auto
  2.1824 +     show ?thesis
  2.1825 +       apply (rule great_Picard [OF open_ball _ \<open>a \<noteq> b\<close> holfb])
  2.1826 +      using non \<open>0 < r\<close> r zrM by auto
  2.1827 +  qed
  2.1828 +  with that show thesis
  2.1829 +    by meson
  2.1830 +qed
  2.1831 +
  2.1832 +
  2.1833 +corollary Casorati_Weierstrass:
  2.1834 +  assumes "open M" "z \<in> M" "f holomorphic_on (M - {z})"
  2.1835 +      and "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
  2.1836 +  shows "closure(f ` (M - {z})) = UNIV"
  2.1837 +proof -
  2.1838 +  obtain a where a: "- {a} \<subseteq> f ` (M - {z})"
  2.1839 +    using great_Picard_alt [OF assms] .
  2.1840 +  have "UNIV = closure(- {a})"
  2.1841 +    by (simp add: closure_interior)
  2.1842 +  also have "... \<subseteq> closure(f ` (M - {z}))"
  2.1843 +    by (simp add: a closure_mono)
  2.1844 +  finally show ?thesis
  2.1845 +    by blast 
  2.1846 +qed
  2.1847 +  
  2.1848 +end