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