Theory HOL-Complex_Analysis.Great_Picard

section ‹The Great Picard Theorem and its Applications›

text‹Ported from HOL Light (cauchy.ml) by L C Paulson, 2017›

theory Great_Picard
  imports Conformal_Mappings
begin
  
subsection‹Schottky's theorem›

lemma Schottky_lemma0:
  assumes holf: "f holomorphic_on S" and cons: "contractible S" and "a  S"
      and f: "z. z  S  f z  1  f z  -1"
  obtains g where "g holomorphic_on S"
                  "norm(g a)  1 + norm(f a) / 3"
                  "z. z  S  f z = cos(of_real pi * g z)"
proof -
  obtain g where holg: "g holomorphic_on S" and g: "norm(g a)  pi + norm(f a)"
             and f_eq_cos: "z. z  S  f z = cos(g z)"
    using contractible_imp_holomorphic_arccos_bounded [OF assms]
    by blast
  show ?thesis
  proof
    show "(λz. g z / pi) holomorphic_on S"
      by (auto intro: holomorphic_intros holg)
    have "3  pi"
      using pi_approx by force
    have "3 * norm(g a)  3 * (pi + norm(f a))"
      using g by auto
    also have "...   pi * 3 + pi * cmod (f a)"
      using 3  pi by (simp add: mult_right_mono algebra_simps)
    finally show "cmod (g a / complex_of_real pi)  1 + cmod (f a) / 3"
      by (simp add: field_simps norm_divide)
    show "z. z  S  f z = cos (complex_of_real pi * (g z / complex_of_real pi))"
      by (simp add: f_eq_cos)
  qed
qed


lemma Schottky_lemma1:
  fixes n::nat
  assumes "0 < n"
  shows "0 < n + sqrt(real n ^ 2 - 1)"
proof -
  have "0 < n * n"
    by (simp add: assms)
  then show ?thesis
    by (metis add.commute add.right_neutral add_pos_nonneg assms diff_ge_0_iff_ge nat_less_real_le of_nat_0 of_nat_0_less_iff of_nat_power power2_eq_square real_sqrt_ge_0_iff)
qed


lemma Schottky_lemma2:
  fixes x::real
  assumes "0  x"
  obtains n where "0 < n" "¦x - ln (real n + sqrt ((real n)2 - 1)) / pi¦ < 1/2"
proof -
  obtain n0::nat where "0 < n0" "ln(n0 + sqrt(real n0 ^ 2 - 1)) / pi  x"
  proof
    show "ln(real 1 + sqrt(real 1 ^ 2 - 1))/pi  x"
      by (auto simp: assms)
  qed auto
  moreover
  obtain M::nat where "n. 0 < n; ln(n + sqrt(real n ^ 2 - 1)) / pi  x  n  M"
  proof
    fix n::nat
    assume "0 < n" "ln (n + sqrt ((real n)2 - 1)) / pi  x"
    then have "ln (n + sqrt ((real n)2 - 1))  x * pi"
      by (simp add: field_split_simps)
    then have *: "exp (ln (n + sqrt ((real n)2 - 1)))  exp (x * pi)"
      by blast
    have 0: "0  sqrt ((real n)2 - 1)"
      using 0 < n by auto
    have "n + sqrt ((real n)2 - 1) = exp (ln (n + sqrt ((real n)2 - 1)))"
      by (simp add: Suc_leI 0 < n add_pos_nonneg real_of_nat_ge_one_iff)
    also have "...  exp (x * pi)"
      using "*" by blast
    finally have "real n  exp (x * pi)"
      using 0 by linarith
    then show "n  nat (ceiling (exp(x * pi)))"
      by linarith
  qed
  ultimately obtain n where
     "0 < n" and le_x: "ln(n + sqrt(real n ^ 2 - 1)) / pi  x"
             and le_n: "k. 0 < k; ln(k + sqrt(real k ^ 2 - 1)) / pi  x  k  n"
    using bounded_Max_nat [of "λn. 0<n  ln (n + sqrt ((real n)2 - 1)) / pi  x"] by metis
  define a where "a  ln(n + sqrt(real n ^ 2 - 1)) / pi"
  define b where "b  ln (1 + real n + sqrt ((1 + real n)2 - 1)) / pi"
  have le_xa: "a  x"
   and le_na: "k. 0 < k; ln(k + sqrt(real k ^ 2 - 1)) / pi  x  k  n"
    using le_x le_n by (auto simp: a_def)
  moreover have "x < b"
    using le_n [of "Suc n"] by (force simp: b_def)
  moreover have "b - a < 1"
  proof -
    have "ln (1 + real n + sqrt ((1 + real n)2 - 1)) - ln (real n + sqrt ((real n)2 - 1)) =
         ln ((1 + real n + sqrt ((1 + real n)2 - 1)) / (real n + sqrt ((real n)2 - 1)))"
      by (simp add: 0 < n Schottky_lemma1 add_pos_nonneg ln_div [symmetric])
    also have "...  3"
    proof (cases "n = 1")
      case True
      have "sqrt 3  2"
        by (simp add: real_le_lsqrt)
      then have "(2 + sqrt 3)  4"
        by simp
      also have "...  exp 3"
        using exp_ge_add_one_self [of "3::real"] by simp
      finally have "ln (2 + sqrt 3)  3"
        by (metis add_nonneg_nonneg add_pos_nonneg dbl_def dbl_inc_def dbl_inc_simps(3)
            dbl_simps(3) exp_gt_zero ln_exp ln_le_cancel_iff real_sqrt_ge_0_iff zero_le_one zero_less_one)
      then show ?thesis
        by (simp add: True)
    next
      case False with 0 < n have "1 < n" "2  n"
        by linarith+
      then have 1: "1  real n * real n"
        by (metis less_imp_le_nat one_le_power power2_eq_square real_of_nat_ge_one_iff)
      have *: "4 + (m+2) * 2  (m+2) * ((m+2) * 3)" for m::nat
        by simp
      have "4 + n * 2  n * (n * 3)"
        using * [of "n-2"]  2  n
        by (metis le_add_diff_inverse2)
      then have **: "4 + real n * 2  real n * (real n * 3)"
        by (metis (mono_tags, opaque_lifting) of_nat_le_iff of_nat_add of_nat_mult of_nat_numeral)
      have "sqrt ((1 + real n)2 - 1)  2 * sqrt ((real n)2 - 1)"
        by (auto simp: real_le_lsqrt power2_eq_square algebra_simps 1 **)
      then
      have "((1 + real n + sqrt ((1 + real n)2 - 1)) / (real n + sqrt ((real n)2 - 1)))  2"
        using Schottky_lemma1 0 < n  by (simp add: field_split_simps)
      then have "ln ((1 + real n + sqrt ((1 + real n)2 - 1)) / (real n + sqrt ((real n)2 - 1)))  ln 2"
        using Schottky_lemma1 [of n] 0 < n 
        by (simp add: field_split_simps add_pos_nonneg)
      also have "...  3"
        using ln_add_one_self_le_self [of 1] by auto
      finally show ?thesis .
    qed
    also have "... < pi"
      using pi_approx by simp
    finally show ?thesis
      by (simp add: a_def b_def field_split_simps)
  qed
  ultimately have "¦x - a¦ < 1/2  ¦x - b¦ < 1/2"
    by (auto simp: abs_if)
  then show thesis
  proof
    assume "¦x - a¦ < 1/2"
    then show ?thesis
      by (rule_tac n=n in that) (auto simp: a_def 0 < n)
  next
    assume "¦x - b¦ < 1/2"
    then show ?thesis
      by (rule_tac n="Suc n" in that) (auto simp: b_def 0 < n)
  qed
qed


lemma Schottky_lemma3:
  fixes z::complex
  assumes "z  (m  Ints. n  {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)})
              (m  Ints. n  {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)})"
  shows "cos(pi * cos(pi * z)) = 1  cos(pi * cos(pi * z)) = -1"
proof -
  have sqrt2 [simp]: "complex_of_real (sqrt x) * complex_of_real (sqrt x) = x" if "x  0" for x::real
    by (metis abs_of_nonneg of_real_mult real_sqrt_mult_self that)
  define plusi where "plusi (e::complex)  e + inverse e" for e
  have 1: "k. plusi (exp (𝗂 * (of_int m * complex_of_real pi) - ln (real n + sqrt ((real n)2 - 1)))) = of_int k * 2" 
           (is "k.  k")
         if "n > 0" for m n
  proof -
    have eeq: "e  0  plusi e = n  (inverse e) ^ 2 = n/e - 1" for n e::complex
      by (auto simp: plusi_def field_simps power2_eq_square)
    have [simp]: "1  real n * real n"
      using nat_0_less_mult_iff nat_less_real_le that by force
    consider "odd m" | "even m"
      by blast
    then have "k.  k"
    proof cases
      case 1
      then have " (- n)"
        using Schottky_lemma1 [OF that]
        by (simp add: eeq) (simp add: power2_eq_square exp_diff exp_Euler exp_of_real algebra_simps sin_int_times_real cos_int_times_real)
      then show ?thesis ..
    next
      case 2
      then have " n"
        using Schottky_lemma1 [OF that]
        by (simp add: eeq) (simp add: power2_eq_square exp_diff exp_Euler exp_of_real algebra_simps)
      then show ?thesis ..
    qed
    then show ?thesis by blast
  qed
  have 2: "k. plusi (exp (𝗂 * (of_int m * complex_of_real pi) +
                      (ln (real n + sqrt ((real n)2 - 1))))) = of_int k * 2"
           (is "k.  k")
            if "n > 0" for m n
  proof -
    have eeq: "e  0  plusi e = n  e^2 - n*e + 1 = 0" for n e::complex
      by (auto simp: plusi_def field_simps power2_eq_square)
    have [simp]: "1  real n * real n"
      by (metis One_nat_def add.commute nat_less_real_le of_nat_1 of_nat_Suc one_le_power power2_eq_square that)
    consider "odd m" | "even m"
      by blast
    then have "k.  k"
    proof cases
      case 1
      then have " (- n)"
        using Schottky_lemma1 [OF that]
        by (simp add: eeq) (simp add: power2_eq_square exp_add exp_Euler exp_of_real algebra_simps sin_int_times_real cos_int_times_real)
      then show ?thesis ..
    next
      case 2
      then have " n"
        using Schottky_lemma1 [OF that]
        by (simp add: eeq) (simp add: power2_eq_square exp_add exp_Euler exp_of_real algebra_simps)
      then show ?thesis ..
    qed
    then show ?thesis by blast
  qed
  have "x. cos (complex_of_real pi * z) = of_int x"
    using assms
    apply (auto simp: Ints_def cos_exp_eq exp_minus Complex_eq simp flip: plusi_def)
     apply (auto simp: algebra_simps dest: 1 2)
    done
  then have "sin(pi * cos(pi * z)) ^ 2 = 0"
    by (simp add: Complex_Transcendental.sin_eq_0)
  then have "1 - cos(pi * cos(pi * z)) ^ 2 = 0"
    by (simp add: sin_squared_eq)
  then show ?thesis
    using power2_eq_1_iff by auto
qed


theorem Schottky:
  assumes holf: "f holomorphic_on cball 0 1"
      and nof0: "norm(f 0)  r"
      and not01: "z. z  cball 0 1  ¬(f z = 0  f z = 1)"
      and "0 < t" "t < 1" "norm z  t"
    shows "norm(f z)  exp(pi * exp(pi * (2 + 2 * r + 12 * t / (1 - t))))"
proof -
  obtain h where holf: "h holomorphic_on cball 0 1"
             and nh0: "norm (h 0)  1 + norm(2 * f 0 - 1) / 3"
             and h:   "z. z  cball 0 1  2 * f z - 1 = cos(of_real pi * h z)"
  proof (rule Schottky_lemma0 [of "λz. 2 * f z - 1" "cball 0 1" 0])
    show "(λz. 2 * f z - 1) holomorphic_on cball 0 1"
      by (intro holomorphic_intros holf)
    show "contractible (cball (0::complex) 1)"
      by (auto simp: convex_imp_contractible)
    show "z. z  cball 0 1  2 * f z - 1  1  2 * f z - 1  - 1"
      using not01 by force
  qed auto
  obtain g where holg: "g holomorphic_on cball 0 1"
             and ng0:  "norm(g 0)  1 + norm(h 0) / 3"
             and g:    "z. z  cball 0 1  h z = cos(of_real pi * g z)"
  proof (rule Schottky_lemma0 [OF holf convex_imp_contractible, of 0])
    show "z. z  cball 0 1  h z  1  h z  - 1"
      using h not01 by fastforce+
  qed auto
  have g0_2_f0: "norm(g 0)  2 + norm(f 0)"
  proof -
    have "cmod (2 * f 0 - 1)  cmod (2 * f 0) + 1"
      by (metis norm_one norm_triangle_ineq4)
    also have "...  6 + 9 * cmod (f 0)"
      by auto
    finally have "1 + norm(2 * f 0 - 1) / 3  (2 + norm(f 0) - 1) * 3"
      by (simp add: divide_simps)
    with nh0 have "norm(h 0)  (2 + norm(f 0) - 1) * 3"
      by linarith
    then have "1 + norm(h 0) / 3  2 + norm(f 0)"
      by simp
    with ng0 show ?thesis
      by auto
  qed
  have "z  ball 0 1"
    using assms by auto
  have norm_g_12: "norm(g z - g 0)  (12 * t) / (1 - t)"
  proof -
    obtain g' where g': "x. x  cball 0 1  (g has_field_derivative g' x) (at x within cball 0 1)"
      using holg [unfolded holomorphic_on_def field_differentiable_def] by metis
    have int_g': "(g' has_contour_integral g z - g 0) (linepath 0 z)"
      using contour_integral_primitive [OF g' valid_path_linepath, of 0 z]
      using z  ball 0 1 segment_bound1 by fastforce
    have "cmod (g' w)  12 / (1 - t)" if "w  closed_segment 0 z" for w
    proof -
      have w: "w  ball 0 1"
        using segment_bound [OF that] z  ball 0 1 by simp
      have *: "b. (w  T  U. w  ball b 1); x. x  D  g x  T  U  b. ball b 1  g ` D" for T U D
        by force
      have ttt: "1 - t  dist w u" if "cmod u = 1" for u
        using norm z  t segment_bound1 [OF w  closed_segment 0 z] norm_triangle_ineq2 [of u w] that
        by (simp add: dist_norm norm_minus_commute)
      have "b. ball b 1  g ` cball 0 1"
      proof (rule *)
        show "(w  (m  Ints. n  {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)}) 
                    (m  Ints. n  {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)}). w  ball b 1)" for b
        proof -
          obtain m where m: "m  " "¦Re b - m¦  1/2"
            by (metis Ints_of_int abs_minus_commute of_int_round_abs_le)
          show ?thesis
          proof (cases "0::real" "Im b" rule: le_cases)
            case le
            then obtain n where "0 < n" and n: "¦Im b - ln (n + sqrt ((real n)2 - 1)) / pi¦ < 1/2"
              using Schottky_lemma2 [of "Im b"] by blast
            have "dist b (Complex m (Im b))  1/2"
              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)
            moreover
            have "dist (Complex m (Im b)) (Complex m (ln (n + sqrt ((real n)2 - 1)) / pi)) < 1/2"
              using n by (simp add: complex_norm cmod_eq_Re complex_diff dist_norm del: Complex_eq)
            ultimately have "dist b (Complex m (ln (real n + sqrt ((real n)2 - 1)) / pi)) < 1"
              by (simp add: dist_triangle_lt [of b "Complex m (Im b)"] dist_commute)
            with le m 0 < n show ?thesis
              apply (rule_tac x = "Complex m (ln (real n + sqrt ((real n)2 - 1)) / pi)" in bexI)
               by (force simp del: Complex_eq greaterThan_0)+
          next
            case ge
            then obtain n where "0 < n" and n: "¦- Im b - ln (real n + sqrt ((real n)2 - 1)) / pi¦ < 1/2"
              using Schottky_lemma2 [of "- Im b"] by auto
            have "dist b (Complex m (Im b))  1/2"
              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)
            moreover
            have "dist (Complex m (- ln (n + sqrt ((real n)2 - 1)) / pi)) (Complex m (Im b)) 
                = ¦ - Im b - ln (real n + sqrt ((real n)2 - 1)) / pi¦"
              by (simp add: complex_norm dist_norm cmod_eq_Re complex_diff)
            ultimately have "dist b (Complex m (- ln (real n + sqrt ((real n)2 - 1)) / pi)) < 1"
              using n by (simp add: dist_triangle_lt [of b "Complex m (Im b)"] dist_commute)
            with ge m 0 < n show ?thesis
              by (rule_tac x = "Complex m (- ln (real n + sqrt ((real n)2 - 1)) / pi)" in bexI) auto
          qed
        qed
        show "g v  (m  Ints. n  {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)}) 
                    (m  Ints. n  {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)})"
             if "v  cball 0 1" for v
          using not01 [OF that]
          by (force simp: g [OF that, symmetric] h [OF that, symmetric] dest!: Schottky_lemma3 [of "g v"])
      qed
      then have 12: "(1 - t) * cmod (deriv g w) / 12 < 1"
        using Bloch_general [OF holg _ ttt, of 1] w by force
      have "g field_differentiable at w within cball 0 1"
        using holg w by (simp add: holomorphic_on_def)
      then have "g field_differentiable at w within ball 0 1"
        using ball_subset_cball field_differentiable_within_subset by blast
      with w have der_gw: "(g has_field_derivative deriv g w) (at w)"
        by (simp add: field_differentiable_within_open [of _ "ball 0 1"] field_differentiable_derivI)
      with DERIV_unique [OF der_gw] g' w have "deriv g w = g' w"
        by (metis open_ball at_within_open ball_subset_cball has_field_derivative_subset subsetCE)
      then show "cmod (g' w)  12 / (1 - t)"
        using g' 12 t < 1 by (simp add: field_simps)
    qed
    then have "cmod (g z - g 0)  12 / (1 - t) * cmod z"
      using has_contour_integral_bound_linepath [OF int_g', of "12/(1 - t)"] assms
      by simp
    with cmod z  t t < 1 show ?thesis
      by (simp add: field_split_simps)
  qed
  have fz: "f z = (1 + cos(of_real pi * h z)) / 2"
    using h z  ball 0 1 by (auto simp: field_simps)
  have "cmod (f z)  exp (cmod (complex_of_real pi * h z))"
    by (simp add: fz mult.commute norm_cos_plus1_le)
  also have "...  exp (pi * exp (pi * (2 + 2 * r + 12 * t / (1 - t))))"
  proof (simp add: norm_mult)
    have "cmod (g z - g 0)  12 * t / (1 - t)"
      using norm_g_12 t < 1 by (simp add: norm_mult)
    then have "cmod (g z) - cmod (g 0)  12 * t / (1 - t)"
      using norm_triangle_ineq2 order_trans by blast
    then have *: "cmod (g z)  2 + 2 * r + 12 * t / (1 - t)"
      using g0_2_f0 norm_ge_zero [of "f 0"] nof0
        by linarith
    have "cmod (h z)  exp (cmod (complex_of_real pi * g z))"
      using z  ball 0 1 by (simp add: g norm_cos_le)
    also have "...  exp (pi * (2 + 2 * r + 12 * t / (1 - t)))"
      using t < 1 nof0 * by (simp add: norm_mult)
    finally show "cmod (h z)  exp (pi * (2 + 2 * r + 12 * t / (1 - t)))" .
  qed
  finally show ?thesis .
qed

  
subsection‹The Little Picard Theorem›

theorem Landau_Picard:
  obtains R
    where "z. 0 < R z"
          "f. f holomorphic_on cball 0 (R(f 0));
                 z. norm z  R(f 0)  f z  0  f z  1  norm(deriv f 0) < 1"
proof -
  define R where "R  λz. 3 * exp(pi * exp(pi*(2 + 2 * cmod z + 12)))"
  show ?thesis
  proof
    show Rpos: "z. 0 < R z"
      by (auto simp: R_def)
    show "norm(deriv f 0) < 1"
         if holf: "f holomorphic_on cball 0 (R(f 0))"
         and Rf:  "z. norm z  R(f 0)  f z  0  f z  1" for f
    proof -
      let ?r = "R(f 0)"
      define g where "g  f  (λz. of_real ?r * z)"
      have "0 < ?r"
        using Rpos by blast
      have holg: "g holomorphic_on cball 0 1"
        unfolding g_def
      proof (intro holomorphic_intros holomorphic_on_compose holomorphic_on_subset [OF holf])
        show "(*) (complex_of_real (R (f 0))) ` cball 0 1  cball 0 (R (f 0))"
          using Rpos by (auto simp: less_imp_le norm_mult)
      qed
      have *: "norm(g z)  exp(pi * exp(pi * (2 + 2 * norm (f 0) + 12 * t / (1 - t))))"
           if "0 < t" "t < 1" "norm z  t" for t z
      proof (rule Schottky [OF holg])
        show "cmod (g 0)  cmod (f 0)"
          by (simp add: g_def)
        show "z. z  cball 0 1  ¬ (g z = 0  g z = 1)"
          using Rpos by (simp add: g_def less_imp_le norm_mult Rf)
      qed (auto simp: that)
      have C1: "g holomorphic_on ball 0 (1/2)"
        by (rule holomorphic_on_subset [OF holg]) auto
      have C2: "continuous_on (cball 0 (1/2)) g"
        by (meson cball_divide_subset_numeral holg holomorphic_on_imp_continuous_on holomorphic_on_subset)
      have C3: "cmod (g z)  R (f 0) / 3" if "cmod (0 - z) = 1/2" for z
      proof -
        have "norm(g z)  exp(pi * exp(pi * (2 + 2 * norm (f 0) + 12)))"
          using * [of "1/2"] that by simp
        also have "... = ?r / 3"
          by (simp add: R_def)
        finally show ?thesis .
      qed
      then have cmod_g'_le: "cmod (deriv g 0) * 3  R (f 0) * 2"
        using Cauchy_inequality [OF C1 C2 _ C3, of 1] by simp
      have holf': "f holomorphic_on ball 0 (R(f 0))"
        by (rule holomorphic_on_subset [OF holf]) auto
      then have fd0: "f field_differentiable at 0"
        by (rule holomorphic_on_imp_differentiable_at [OF _ open_ball])
           (auto simp: Rpos [of "f 0"])
      have g_eq: "deriv g 0 = of_real ?r * deriv f 0"
        unfolding g_def
        by (metis DERIV_imp_deriv DERIV_chain DERIV_cmult_Id fd0 field_differentiable_derivI mult.commute mult_zero_right)
      show ?thesis
        using cmod_g'_le Rpos [of "f 0"]  by (simp add: g_eq norm_mult)
    qed
  qed
qed

lemma little_Picard_01:
  assumes holf: "f holomorphic_on UNIV" and f01: "z. f z  0  f z  1"
  obtains c where "f = (λx. c)"
proof -
  obtain R
    where Rpos: "z. 0 < R z"
      and R:    "h. h holomorphic_on cball 0 (R(h 0));
                      z. norm z  R(h 0)  h z  0  h z  1  norm(deriv h 0) < 1"
    using Landau_Picard by metis
  have contf: "continuous_on UNIV f"
    by (simp add: holf holomorphic_on_imp_continuous_on)
  show ?thesis
  proof (cases "x. deriv f x = 0")
    case True
    have "(f has_field_derivative 0) (at x)" for x
      by (metis True UNIV_I holf holomorphic_derivI open_UNIV)
    then obtain c where "x. f(x) = c"
      by (meson UNIV_I DERIV_zero_connected_constant [OF connected_UNIV open_UNIV finite.emptyI contf])
    then show ?thesis
      using that by auto
  next
    case False
    then obtain w where w: "deriv f w  0" by auto
    define fw where "fw  (f  (λz. w + z / deriv f w))"
    have norm_let1: "norm(deriv fw 0) < 1"
    proof (rule R)
      show "fw holomorphic_on cball 0 (R (fw 0))"
        unfolding fw_def
        by (intro holomorphic_intros holomorphic_on_compose w holomorphic_on_subset [OF holf] subset_UNIV)
      show "fw z  0  fw z  1" if "cmod z  R (fw 0)" for z
        using f01 by (simp add: fw_def)
    qed
    have "(fw has_field_derivative deriv f w * inverse (deriv f w)) (at 0)"
      unfolding fw_def
      apply (intro DERIV_chain derivative_eq_intros w)+
      using holf holomorphic_derivI by (force simp: field_simps)+
    then show ?thesis
      using norm_let1 w by (simp add: DERIV_imp_deriv)
  qed
qed


theorem little_Picard:
  assumes holf: "f holomorphic_on UNIV"
      and "a  b" "range f  {a,b} = {}"
    obtains c where "f = (λx. c)"
proof -
  let ?g = "λx. 1/(b - a)*(f x - b) + 1"
  obtain c where "?g = (λx. c)"
  proof (rule little_Picard_01)
    show "?g holomorphic_on UNIV"
      by (intro holomorphic_intros holf)
    show "z. ?g z  0  ?g z  1"
      using assms by (auto simp: field_simps)
  qed auto
  then have "?g x = c" for x
    by meson
  then have "f x = c * (b-a) + a" for x
    using assms by (auto simp: field_simps)
  then show ?thesis
    using that by blast
qed


text‹A couple of little applications of Little Picard›

lemma holomorphic_periodic_fixpoint:
  assumes holf: "f holomorphic_on UNIV"
      and "p  0" and per: "z. f(z + p) = f z"
  obtains x where "f x = x"
proof -
  have False if non: "x. f x  x"
  proof -
    obtain c where "(λz. f z - z) = (λz. c)"
    proof (rule little_Picard)
      show "(λz. f z - z) holomorphic_on UNIV"
        by (simp add: holf holomorphic_on_diff)
      show "range (λz. f z - z)  {p,0} = {}"
          using assms non by auto (metis add.commute diff_eq_eq)
      qed (auto simp: assms)
    with per show False
      by (metis add.commute add_cancel_left_left p  0 diff_add_cancel)
  qed
  then show ?thesis
    using that by blast
qed


lemma holomorphic_involution_point:
  assumes holfU: "f holomorphic_on UNIV" and non: "a. f  (λx. a + x)"
  obtains x where "f(f x) = x"
proof -
  { assume non_ff [simp]: "x. f(f x)  x"
    then have non_fp [simp]: "f z  z" for z
      by metis
    have holf: "f holomorphic_on X" for X
      using assms holomorphic_on_subset by blast
    obtain c where c: "(λx. (f(f x) - x)/(f x - x)) = (λx. c)"
    proof (rule little_Picard_01)
      show "(λx. (f(f x) - x)/(f x - x)) holomorphic_on UNIV"
        using non_fp
        by (intro holomorphic_intros holf holomorphic_on_compose [unfolded o_def, OF holf]) auto
    qed auto
    then obtain "c  0" "c  1"
      by (metis (no_types, opaque_lifting) non_ff diff_zero divide_eq_0_iff right_inverse_eq)
    have eq: "f(f x) - c * f x = x*(1 - c)" for x
      using fun_cong [OF c, of x] by (simp add: field_simps)
    have df_times_dff: "deriv f z * (deriv f (f z) - c) = 1 * (1 - c)" for z
    proof (rule DERIV_unique)
      show "((λx. f (f x) - c * f x) has_field_derivative
              deriv f z * (deriv f (f z) - c)) (at z)"
        by (rule derivative_eq_intros holomorphic_derivI [OF holfU] 
                    DERIV_chain [unfolded o_def, where f=f and g=f] | simp add: algebra_simps)+
      show "((λx. f (f x) - c * f x) has_field_derivative 1 * (1 - c)) (at z)"
        by (simp add: eq mult_commute_abs)
    qed
    { fix z::complex
      obtain k where k: "deriv f  f = (λx. k)"
      proof (rule little_Picard)
        show "(deriv f  f) holomorphic_on UNIV"
          by (meson holfU holomorphic_deriv holomorphic_on_compose holomorphic_on_subset open_UNIV subset_UNIV)
        obtain "deriv f (f x)  0" "deriv f (f x)  c"  for x
          using df_times_dff c  1 eq_iff_diff_eq_0
          by (metis lambda_one mult_zero_left mult_zero_right)
        then show "range (deriv f  f)  {0,c} = {}"
          by force
      qed (use c  0 in auto)
      have "¬ f constant_on UNIV"
        by (meson UNIV_I non_ff constant_on_def)
      with holf open_mapping_thm have "open(range f)"
        by blast
      obtain l where l: "x. f x - k * x = l"
      proof (rule DERIV_zero_connected_constant [of UNIV "{}" "λx. f x - k * x"], simp_all)
        have "deriv f w - k = 0" for w
        proof (rule analytic_continuation [OF _ open_UNIV connected_UNIV subset_UNIV, of "λz. deriv f z - k" "f z" "range f" w])
          show "(λz. deriv f z - k) holomorphic_on UNIV"
            by (intro holomorphic_intros holf open_UNIV)
          show "f z islimpt range f"
            by (metis (no_types, lifting) IntI UNIV_I open (range f) image_eqI inf.absorb_iff2 inf_aci(1) islimpt_UNIV islimpt_eq_acc_point open_Int top_greatest)
          show "z. z  range f  deriv f z - k = 0"
            by (metis comp_def diff_self image_iff k)
        qed auto
        moreover
        have "((λx. f x - k * x) has_field_derivative deriv f x - k) (at x)" for x
          by (metis DERIV_cmult_Id Deriv.field_differentiable_diff UNIV_I field_differentiable_derivI holf holomorphic_on_def)
        ultimately
        show "x. ((λx. f x - k * x) has_field_derivative 0) (at x)"
          by auto
        show "continuous_on UNIV (λx. f x - k * x)"
          by (simp add: continuous_on_diff holf holomorphic_on_imp_continuous_on)
      qed (auto simp: connected_UNIV)
      have False
      proof (cases "k=1")
        case True
        then have "x. k * x + l  a + x" for a
          using l non [of a] ext [of f "(+) a"]
          by (metis add.commute diff_eq_eq)
        with True show ?thesis by auto
      next
        case False
        have "x. (1 - k) * x  f 0"
          using l [of 0]
          by (simp add: algebra_simps) (metis diff_add_cancel l mult.commute non_fp)
        then show False
          by (metis False eq_iff_diff_eq_0 mult.commute nonzero_mult_div_cancel_right times_divide_eq_right)
      qed
    }
  }
  then show thesis
    using that by blast
qed


subsection‹The Arzelà--Ascoli theorem›

lemma subsequence_diagonalization_lemma:
  fixes P :: "nat  (nat  'a)  bool"
  assumes sub: "i r. k. strict_mono (k :: nat  nat)  P i (r  k)"
      and P_P:  "i r::nat  'a. k1 k2 N.
                   P i (r  k1); j. N  j  j'. j  j'  k2 j = k1 j'  P i (r  k2)"
   obtains k where "strict_mono (k :: nat  nat)" "i. P i (r  k)"
proof -
  obtain kk where "i r. strict_mono (kk i r :: nat  nat)  P i (r  (kk i r))"
    using sub by metis
  then have sub_kk: "i r. strict_mono (kk i r)" and P_kk: "i r. P i (r  (kk i r))"
    by auto
  define rr where "rr  rec_nat (kk 0 r) (λn x. x  kk (Suc n) (r  x))"
  then have [simp]: "rr 0 = kk 0 r" "n. rr(Suc n) = rr n  kk (Suc n) (r  rr n)"
    by auto
  show thesis
  proof
    have sub_rr: "strict_mono (rr i)" for i
      using sub_kk  by (induction i) (auto simp: strict_mono_def o_def)
    have P_rr: "P i (r  rr i)" for i
      using P_kk  by (induction i) (auto simp: o_def)
    have "i  i+d  rr i n  rr (i+d) n" for d i n
    proof (induction d)
      case 0 then show ?case
        by simp
    next
      case (Suc d) then show ?case
        using seq_suble [OF sub_kk] strict_mono_less_eq [OF sub_rr]
        by (simp add: order_subst1)
    qed
    then have "i j n. i  j  rr i n  rr j n"
      by (metis le_iff_add)
    show "strict_mono (λn. rr n n)"
      unfolding strict_mono_Suc_iff
      by (simp add: Suc_le_lessD strict_monoD strict_mono_imp_increasing sub_kk sub_rr)
    have "j. i  j  rr (n+d) i = rr n j" for d n i
    proof (induction d arbitrary: i)
      case (Suc d)
      then show ?case
        using seq_suble [OF sub_kk] by simp (meson order_trans)
    qed auto
    then have "m n i. n  m  j. i  j  rr m i = rr n j"
      by (metis le_iff_add)
    then show "P i (r  (λn. rr n n))" for i
      by (meson P_rr P_P)
  qed
qed

lemma function_convergent_subsequence:
  fixes f :: "[nat,'a]  'b::{real_normed_vector,heine_borel}"
  assumes "countable S" and M: "n::nat. x. x  S  norm(f n x)  M"
   obtains k where "strict_mono (k::natnat)" "x. x  S  l. (λn. f (k n) x)  l"
proof (cases "S = {}")
  case True
  then show ?thesis
    using strict_mono_id that by fastforce
next
  case False
  with countable S obtain σ :: "nat  'a" where σ: "S = range σ"
    using uncountable_def by blast
  obtain k where "strict_mono k" and k: "i. l. (λn. (f  k) n (σ i))  l"
  proof (rule subsequence_diagonalization_lemma
      [of "λi r. l. ((λn. (f  r) n (σ i))  l) sequentially" id])
    show "k::natnat. strict_mono k  (l. (λn. (f  (r  k)) n (σ i))  l)" for i r
    proof -
      have "f (r n) (σ i)  cball 0 M" for n
        by (simp add: σ M)
      then show ?thesis
        using compact_def [of "cball (0::'b) M"] by (force simp: o_def)
    qed
    show "l. (λn. (f  (r  k2)) n (σ i))  l" 
      if "l. (λn. (f  (r  k1)) n (σ i))  l" "j. N  j  j'j. k2 j = k1 j'"
      for i N and r k1 k2 :: "natnat"
      using that
      by (simp add: lim_sequentially) (metis (no_types, opaque_lifting) le_cases order_trans)
  qed auto
  with σ that show ?thesis
    by force
qed


theorem Arzela_Ascoli:
  fixes  :: "[nat,'a::euclidean_space]  'b::{real_normed_vector,heine_borel}"
  assumes "compact S"
      and M: "n x. x  S  norm( n x)  M"
      and equicont:
          "x e. x  S; 0 < e
                  d. 0 < d  (n y. y  S  norm(x - y) < d  norm( n x -  n y) < e)"
  obtains g k where "continuous_on S g" "strict_mono (k :: nat  nat)"
                    "e. 0 < e  N. n x. n  N  x  S  norm((k n) x - g x) < e"
proof -
  have UEQ: "e. 0 < e  d. 0 < d  (n. x  S. x'  S. dist x' x < d  dist ( n x') ( n x) < e)"
    apply (rule compact_uniformly_equicontinuous [OF compact S, of "range "])
    using equicont by (force simp: dist_commute dist_norm)+
  have "continuous_on S g"
       if "e. 0 < e  N. n x. n  N  x  S  norm((r n) x - g x) < e"
       for g:: "'a  'b" and r :: "nat  nat"
  proof (rule uniform_limit_theorem [of _ "  r"])
    have "continuous_on S ( (r n))" for n
      using UEQ by (force simp: continuous_on_iff)
    then show "F n in sequentially. continuous_on S ((  r) n)"
      by (simp add: eventually_sequentially)
    show "uniform_limit S (  r) g sequentially"
      using that by (metis (mono_tags, opaque_lifting) comp_apply dist_norm uniform_limit_sequentially_iff)
  qed auto
  moreover
  obtain R where "countable R" "R  S" and SR: "S  closure R"
    by (metis separable that)
  obtain k where "strict_mono k" and k: "x. x  R  l. (λn.  (k n) x)  l"
    using R  S by (force intro: function_convergent_subsequence [OF countable R M])
  then have Cauchy: "Cauchy ((λn.  (k n) x))" if "x  R" for x
    using convergent_eq_Cauchy that by blast
  have "N. m n x. N  m  N  n  x  S  dist ((  k) m x) ((  k) n x) < e"
    if "0 < e" for e
  proof -
    obtain d where "0 < d"
      and d: "n. x  S. x'  S. dist x' x < d  dist ( n x') ( n x) < e/3"
      by (metis UEQ 0 < e divide_pos_pos zero_less_numeral)
    obtain T where "T  R" and "finite T" and T: "S  (cT. ball c d)"
    proof (rule compactE_image [OF  compact S, of R "(λx. ball x d)"])
      have "closure R  (cR. ball c d)"
        using 0 < d by (auto simp: closure_approachable)
      with SR show "S  (cR. ball c d)"
        by auto
    qed auto
    have "M. mM. nM. dist ( (k m) x) ( (k n) x) < e/3" if "x  R" for x
      using Cauchy 0 < e that unfolding Cauchy_def
      by (metis less_divide_eq_numeral1(1) mult_zero_left)
    then obtain MF where MF: "x m n. x  R; m  MF x; n  MF x  norm ( (k m) x -  (k n) x) < e/3"
      using dist_norm by metis
    have "dist ((  k) m x) ((  k) n x) < e"
         if m: "Max (MF ` T)  m" and n: "Max (MF ` T)  n" "x  S" for m n x
    proof -
      obtain t where "t  T" and t: "x  ball t d"
        using x  S T by auto
      have "norm( (k m) t -  (k m) x) < e / 3"
        by (metis R  S T  R t  T d dist_norm mem_ball subset_iff t x  S)
      moreover
      have "norm( (k n) t -  (k n) x) < e / 3"
        by (metis R  S T  R t  T subsetD d dist_norm mem_ball t x  S)
      moreover
      have "norm( (k m) t -  (k n) t) < e / 3"
      proof (rule MF)
        show "t  R"
          using T  R t  T by blast
        show "MF t  m" "MF t  n"
          by (meson Max_ge finite T t  T finite_imageI imageI le_trans m n)+
      qed
      ultimately
      show ?thesis
        unfolding dist_norm [symmetric] o_def
          by (metis dist_triangle_third dist_commute)
    qed
    then show ?thesis
      by force
  qed
  then obtain g where "e>0. N. n x. N  n  x  S  norm ((  k) n x - g x) < e"
    using uniformly_convergent_eq_cauchy [of "λx. x  S" "  k"] by (auto simp add: dist_norm)
  ultimately show thesis
    by (metis strict_mono k comp_apply that)
qed



subsubsectiontag important›‹Montel's theorem›

text‹a sequence of holomorphic functions uniformly bounded
on compact subsets of an open set S has a subsequence that converges to a
holomorphic function, and converges \emph{uniformly} on compact subsets of S.›


theorem Montel:
  fixes  :: "[nat,complex]  complex"
  assumes "open S"
      and : "h. h    h holomorphic_on S"
      and bounded: "K. compact K; K  S  B. h  .  z  K. norm(h z)  B"
      and rng_f: "range   "
  obtains g r
    where "g holomorphic_on S" "strict_mono (r :: nat  nat)"
          "x. x  S  ((λn.  (r n) x)  g x) sequentially"
          "K. compact K; K  S  uniform_limit K (  r) g sequentially"        
proof -
  obtain K where comK: "n. compact(K n)" and KS: "n::nat. K n  S"
             and subK: "X. compact X; X  S  N. nN. X  K n"
    using open_Union_compact_subsets [OF open S] by metis
  then have "i. B. h  .  z  K i. norm(h z)  B"
    by (simp add: bounded)
  then obtain B where B: "i h z. h  ; z  K i  norm(h z)  B i"
    by metis
  have *: "r g. strict_mono (r::natnat)  (e > 0. N. nN. x  K i. norm((  r) n x - g x) < e)"
        if "n.  n  " for  i
  proof -
    obtain g k where "continuous_on (K i) g" "strict_mono (k::natnat)"
                    "e. 0 < e  N. nN. x  K i. norm((k n) x - g x) < e"
    proof (rule Arzela_Ascoli [of "K i" "" "B i"])
      show "d>0. n y. y  K i  cmod (z - y) < d  cmod ( n z -  n y) < e"
             if z: "z  K i" and "0 < e" for z e
      proof -
        obtain r where "0 < r" and r: "cball z r  S"
          using z KS [of i] open S by (force simp: open_contains_cball)
        have "cball z (2/3 * r)  cball z r"
          using 0 < r by (simp add: cball_subset_cball_iff)
        then have z23S: "cball z (2/3 * r)  S"
          using r by blast
        obtain M where "0 < M" and M: "n w. dist z w  2/3 * r  norm( n w)  M"
        proof -
          obtain N where N: "nN. cball z (2/3 * r)  K n"
            using subK compact_cball [of z "(2/3 * r)"] z23S by force
          have "cmod ( n w)  ¦B N¦ + 1" if "dist z w  2/3 * r" for n w
          proof -
            have "w  K N"
              using N mem_cball that by blast
            then have "cmod ( n w)  B N"
              using B n.  n   by blast
            also have "...  ¦B N¦ + 1"
              by simp
            finally show ?thesis .
          qed
          then show ?thesis
            by (rule_tac M="¦B N¦ + 1" in that) auto
        qed
        have "cmod ( n z -  n y) < e"
              if "y  K i" and y_near_z: "cmod (z - y) < r/3" "cmod (z - y) < e * r / (6 * M)"
              for n y
        proof -
          have "((λw.  n w / (w - ξ)) has_contour_integral
                    (2 * pi) * 𝗂 * winding_number (circlepath z (2/3 * r)) ξ *  n ξ)
                (circlepath z (2/3 * r))"
             if "dist ξ z < (2/3 * r)" for ξ
          proof (rule Cauchy_integral_formula_convex_simple)
            have " n holomorphic_on S"
              by (simp add:  n.  n  )
            with z23S show " n holomorphic_on cball z (2/3 * r)"
              using holomorphic_on_subset by blast
          qed (use that 0 < r in auto simp: dist_commute)
          then have *: "((λw.  n w / (w - ξ)) has_contour_integral (2 * pi) * 𝗂 *  n ξ)
                     (circlepath z (2/3 * r))"
             if "dist ξ z < (2/3 * r)" for ξ
            using that by (simp add: winding_number_circlepath dist_norm)
           have y: "((λw.  n w / (w - y)) has_contour_integral (2 * pi) * 𝗂 *  n y)
                    (circlepath z (2/3 * r))"
           proof (rule *)
             show "dist y z < 2/3 * r"
               using that 0 < r by (simp only: dist_norm norm_minus_commute)
           qed
           have z: "((λw.  n w / (w - z)) has_contour_integral (2 * pi) * 𝗂 *  n z)
                 (circlepath z (2/3 * r))"
             using 0 < r by (force intro!: *)
           have le_er: "cmod ( n x / (x - y) -  n x / (x - z))  e / r"
                if "cmod (x - z) = r/3 + r/3" for x
           proof -
             have "¬ (cmod (x - y) < r/3)"
               using y_near_z(1) that M > 0 r > 0
               by (metis (full_types) norm_diff_triangle_less norm_minus_commute order_less_irrefl)
             then have r4_le_xy: "r/4  cmod (x - y)"
               using r > 0 by simp
             then have neq: "x  y" "x  z"
               using that r > 0 by (auto simp: field_split_simps norm_minus_commute)
             have leM: "cmod ( n x)  M"
               by (simp add: M dist_commute dist_norm that)
             have "cmod ( n x / (x - y) -  n x / (x - z)) = cmod ( n x) * cmod (1 / (x - y) - 1 / (x - z))"
               by (metis (no_types, lifting) divide_inverse mult.left_neutral norm_mult right_diff_distrib')
             also have "... = cmod ( n x) * cmod ((y - z) / ((x - y) * (x - z)))"
               using neq by (simp add: field_split_simps)
             also have "... = cmod ( n x) * (cmod (y - z) / (cmod(x - y) * (2/3 * r)))"
               by (simp add: norm_mult norm_divide that)
             also have "...  M * (cmod (y - z) / (cmod(x - y) * (2/3 * r)))"
               using r > 0 M > 0 by (intro mult_mono [OF leM]) auto
             also have "... < M * ((e * r / (6 * M)) / (cmod(x - y) * (2/3 * r)))"
               unfolding mult_less_cancel_left
               using y_near_z(2) M > 0 r > 0 neq
               by (simp add: field_simps mult_less_0_iff norm_minus_commute)
             also have "...  e/r"
               using e > 0 r > 0 r4_le_xy by (simp add: field_split_simps)
             finally show ?thesis by simp
           qed
           have "(2 * pi) * cmod ( n y -  n z) = cmod ((2 * pi) * 𝗂 *  n y - (2 * pi) * 𝗂 *  n z)"
             by (simp add: right_diff_distrib [symmetric] norm_mult)
           also have "cmod ((2 * pi) * 𝗂 *  n y - (2 * pi) * 𝗂 *  n z)  e / r * (2 * pi * (2/3 * r))"

           proof (rule has_contour_integral_bound_circlepath [OF has_contour_integral_diff [OF y z]])
             show "x. cmod (x - z) = 2/3 * r  cmod ( n x / (x - y) -  n x / (x - z))  e / r"
               using le_er by auto
           qed (use e > 0 r > 0 in auto)
           also have "... = (2 * pi) * e * ((2/3))"
             using r > 0 by (simp add: field_split_simps)
           finally have "cmod ( n y -  n z)  e * (2/3)"
             by simp
           also have "... < e"
             using e > 0 by simp
           finally show ?thesis by (simp add: norm_minus_commute)
        qed
        then show ?thesis
          apply (rule_tac x="min (r/3) ((e * r)/(6 * M))" in exI)
          using 0 < e 0 < r 0 < M by simp
      qed
      show "n x.  x  K i  cmod ( n x)  B i"
        using B n.  n   by blast
    next
      fix g :: "complex  complex" and k :: "nat  nat"
      assume *: "(g::complexcomplex) (k::natnat). continuous_on (K i) g 
                  strict_mono k 
                  (e. 0 < e  N. nN. xK i. cmod ( (k n) x - g x) < e)  thesis"
           "continuous_on (K i) g"
           "strict_mono k"
           "e. 0 < e  N. n x. N  n  x  K i  cmod ( (k n) x - g x) < e"
      show ?thesis
        by (rule *(1)[OF *(2,3)], drule *(4)) auto
    qed (use comK in simp_all)
    then show ?thesis
      by auto
  qed
  define Φ where "Φ  λg i r. λk::natnat. e>0. N. nN. xK i. cmod ((  (r  k)) n x - g x) < e"
  obtain k :: "nat  nat" where "strict_mono k" and k: "i. g. Φ g i id k"
  proof (rule subsequence_diagonalization_lemma [where r=id])
    show "g. Φ g i id (r  k2)" 
      if ex: "g. Φ g i id (r  k1)" and "j. N  j  j'j. k2 j = k1 j'" 
      for i k1 k2 N and r::"natnat"
    proof -
      obtain g where "Φ g i id (r  k1)"
        using ex by blast
      then have "Φ g i id (r  k2)"
        using that
        by (simp add: Φ_def) (metis (no_types, opaque_lifting) le_trans linear)
      then show ?thesis
        by metis
    qed
    have "k g. strict_mono (k::natnat)  Φ g i id (r  k)" for i r
      unfolding Φ_def o_assoc using rng_f by (force intro!: *)
    then show "i r. k. strict_mono (k::natnat)  (g. Φ g i id (r  k))"
      by force
  qed fastforce
  have "l. e>0. N. nN. norm( (k n) z - l) < e" if "z  S" for z
  proof -
    obtain G where G: "i e. e > 0  M. nM. xK i. cmod ((  k) n x - G i x) < e"
      using k unfolding Φ_def by (metis id_comp)
    obtain N where "n. n  N  z  K n"
      using subK [of "{z}"] that z  S by auto
    moreover have "e. e > 0  M. nM. xK N. cmod ((  k) n x - G N x) < e"
      using G by auto
    ultimately show ?thesis
      by (metis comp_apply order_refl)
  qed
  then obtain g where g: "z e. z  S; e > 0  N. nN. norm( (k n) z - g z) < e"
    by metis
  show ?thesis
  proof
    show g_lim: "x. x  S  (λn.  (k n) x)  g x"
      by (simp add: lim_sequentially g dist_norm)    
    have dg_le_e: "N. nN. xT. cmod ( (k n) x - g x) < e"
      if T: "compact T" "T  S" and "0 < e" for T e
    proof -
      obtain N where N: "n. n  N  T  K n"
        using subK [OF T] by blast
      obtain h where h: "e. e>0  M. nM. xK N. cmod ((  k) n x - h x) < e"
        using k unfolding Φ_def by (metis id_comp)
      have geq: "g w = h w" if "w  T" for w
      proof (rule LIMSEQ_unique)
        show "(λn.  (k n) w)  g w"
          using T  S g_lim that by blast
        show "(λn.  (k n) w)  h w"
          using h N that by (force simp: lim_sequentially dist_norm)
      qed
      show ?thesis
        using T h N 0 < e by (fastforce simp add: geq)
    qed
    then show "K. compact K; K  S
          uniform_limit K (  k) g sequentially"
      by (simp add: uniform_limit_iff dist_norm eventually_sequentially)
    show "g holomorphic_on S"
    proof (rule holomorphic_uniform_sequence [OF open S ])
      show "n. (  k) n  "
        by (simp add: range_subsetD rng_f)
      show "d>0. cball z d  S  uniform_limit (cball z d) (λn. (  k) n) g sequentially"
        if "z  S" for z
      proof -
        obtain d where d: "d>0" "cball z d  S"
          using open S z  S open_contains_cball by blast
        then have "uniform_limit (cball z d) (  k) g sequentially"
          using dg_le_e compact_cball by (auto simp: uniform_limit_iff eventually_sequentially dist_norm)
        with d show ?thesis by blast
      qed
    qed
  qed (auto simp: strict_mono k)
qed



subsection‹Some simple but useful cases of Hurwitz's theorem›

proposition Hurwitz_no_zeros:
  assumes S: "open S" "connected S"
      and holf: "n::nat.  n holomorphic_on S"
      and holg: "g holomorphic_on S"
      and ul_g: "K. compact K; K  S  uniform_limit K  g sequentially"
      and nonconst: "¬ g constant_on S"
      and nz: "n z. z  S   n z  0"
      and "z0  S"
      shows "g z0  0"
proof
  assume g0: "g z0 = 0"
  obtain h r m
    where "0 < m" "0 < r" and subS: "ball z0 r  S"
      and holh: "h holomorphic_on ball z0 r"
      and geq:  "w. w  ball z0 r  g w = (w - z0)^m * h w"
      and hnz:  "w. w  ball z0 r  h w  0"
    by (blast intro: holomorphic_factor_zero_nonconstant [OF holg S z0  S g0 nonconst])
  then have holf0: " n holomorphic_on ball z0 r" for n
    by (meson holf holomorphic_on_subset)
  have *: "((λz. deriv ( n) z /  n z) has_contour_integral 0) (circlepath z0 (r/2))" for n
  proof (rule Cauchy_theorem_disc_simple)
    show "(λz. deriv ( n) z /  n z) holomorphic_on ball z0 r"
      by (metis (no_types) open S holf holomorphic_deriv holomorphic_on_divide holomorphic_on_subset nz subS)
  qed (use 0 < r in auto)
  have hol_dg: "deriv g holomorphic_on S"
    by (simp add: open S holg holomorphic_deriv)
  have "continuous_on (sphere z0 (r/2)) (deriv g)"
    using 0 < r subS 
    by (intro holomorphic_on_imp_continuous_on holomorphic_on_subset [OF hol_dg]) auto
  then have "compact (deriv g ` (sphere z0 (r/2)))"
    by (rule compact_continuous_image [OF _ compact_sphere])
  then have bo_dg: "bounded (deriv g ` (sphere z0 (r/2)))"
    using compact_imp_bounded by blast
  have "continuous_on (sphere z0 (r/2)) (cmod  g)"
    using 0 < r subS 
    by (intro continuous_intros holomorphic_on_imp_continuous_on holomorphic_on_subset [OF holg]) auto
  then have "compact ((cmod  g) ` sphere z0 (r/2))"
    by (rule compact_continuous_image [OF _ compact_sphere])
  moreover have "(cmod  g) ` sphere z0 (r/2)  {}"
    using 0 < r by auto
  ultimately obtain b where b: "b  (cmod  g) ` sphere z0 (r/2)"
                               "t. t  (cmod  g) ` sphere z0 (r/2)  b  t"
    using compact_attains_inf [of "(norm  g) ` (sphere z0 (r/2))"] by blast
  have "(λn. contour_integral (circlepath z0 (r/2)) (λz. deriv ( n) z /  n z)) 
        contour_integral (circlepath z0 (r/2)) (λz. deriv g z / g z)"
  proof (rule contour_integral_uniform_limit_circlepath)
    show "F n in sequentially. (λz. deriv ( n) z /  n z) contour_integrable_on circlepath z0 (r/2)"
      using * contour_integrable_on_def eventually_sequentiallyI by meson
    show "uniform_limit (sphere z0 (r/2)) (λn z. deriv ( n) z /  n z) (λz. deriv g z / g z) sequentially"
    proof (rule uniform_lim_divide [OF _ _ bo_dg])
      show "uniform_limit (sphere z0 (r/2)) (λa. deriv ( a)) (deriv g) sequentially"
      proof (rule uniform_limitI)
        fix e::real
        assume "0 < e"

        show "F n in sequentially. x  sphere z0 (r/2). dist (deriv ( n) x) (deriv g x) < e"
        proof -
          have "dist (deriv ( n) w) (deriv g w) < e"
            if e8: "x. dist z0 x  3 * r / 4  dist ( n x) (g x) * 8 < r * e"
              and w: "w  sphere z0 (r/2)"  for n w
          proof -
            have "ball w (r/4)  ball z0 r"  "cball w (r/4)  ball z0 r"
              using 0 < r w by (simp_all add: ball_subset_ball_iff cball_subset_ball_iff dist_commute)
            with subS have wr4_sub: "ball w (r/4)  S" "cball w (r/4)  S" by force+
            moreover
            have "(λz.  n z - g z) holomorphic_on S"
              by (intro holomorphic_intros holf holg)
            ultimately have hol: "(λz.  n z - g z) holomorphic_on ball w (r/4)"
              and cont: "continuous_on (cball w (r / 4)) (λz.  n z - g z)"
              using holomorphic_on_subset by (blast intro: holomorphic_on_imp_continuous_on)+
            have "w  S"
              using 0 < r wr4_sub by auto
            have "dist z0 y  3 * r / 4" if "dist w y < r/4" for y
            proof (rule dist_triangle_le [where z=w])
              show "dist z0 w + dist y w  3 * r / 4"
                using w that by (simp add: dist_commute)
            qed
            with e8 have in_ball: "y. y  ball w (r/4)   n y - g y  ball 0 (r/4 * e/2)"
              by (simp add: dist_norm [symmetric])
            have " n field_differentiable at w"
              by (metis holomorphic_on_imp_differentiable_at w  S holf open S)
            moreover
            have "g field_differentiable at w"
              using w  S open S holg holomorphic_on_imp_differentiable_at by auto
            moreover
            have "cmod (deriv (λw.  n w - g w) w) * 2  e"
              using Cauchy_higher_deriv_bound [OF hol cont in_ball, of 1] r > 0 by auto
            ultimately have "dist (deriv ( n) w) (deriv g w)  e/2"
              by (simp add: dist_norm)
            then show ?thesis
              using e > 0 by auto
          qed
          moreover
          have "cball z0 (3 * r / 4)  ball z0 r"
            by (simp add: cball_subset_ball_iff 0 < r)
          with subS have "uniform_limit (cball z0 (3 * r/4))  g sequentially"
            by (force intro: ul_g)
          then have "F n in sequentially. xcball z0 (3 * r / 4). dist ( n x) (g x) < r / 4 * e / 2"
            using 0 < e 0 < r by (force simp: intro!: uniform_limitD)
          ultimately show ?thesis
            by (force simp add: eventually_sequentially)
        qed
      qed
      show "uniform_limit (sphere z0 (r/2))  g sequentially"
      proof (rule uniform_limitI)
        fix e::real
        assume "0 < e"
        have "sphere z0 (r/2)  ball z0 r"
          using 0 < r by auto
        with subS have "uniform_limit (sphere z0 (r/2))  g sequentially"
          by (force intro: ul_g)
        then show "F n in sequentially. x  sphere z0 (r/2). dist ( n x) (g x) < e"
          using 0 < e uniform_limit_iff by blast
      qed
      show "b > 0" "x. x  sphere z0 (r/2)  b  cmod (g x)"
        using b 0 < r by (fastforce simp: geq hnz)+
    qed
  qed (use 0 < r in auto)
  then have "(λn. 0)  contour_integral (circlepath z0 (r/2)) (λz. deriv g z / g z)"
    by (simp add: contour_integral_unique [OF *])
  then have "contour_integral (circlepath z0 (r/2)) (λz. deriv g z / g z) = 0"
    by (simp add: LIMSEQ_const_iff)
  moreover
  have "contour_integral (circlepath z0 (r/2)) (λz. deriv g z / g z) =
        contour_integral (circlepath z0 (r/2)) (λz. m / (z - z0) + deriv h z / h z)"
  proof (rule contour_integral_eq, use 0 < r in simp)
    fix w
    assume w: "dist z0 w * 2 = r"
    then have w_inb: "w  ball z0 r"
      using 0 < r by auto
    have h_der: "(h has_field_derivative deriv h w) (at w)"
      using holh holomorphic_derivI w_inb by blast
    have "deriv g w = ((of_nat m * h w + deriv h w * (w - z0)) * (w - z0) ^ m) / (w - z0)"
      if "r = dist z0 w * 2" "w  z0"
    proof -
      have "((λw. (w - z0) ^ m * h w) has_field_derivative
            (m * h w + deriv h w * (w - z0)) * (w - z0) ^ m / (w - z0)) (at w)"
        apply (rule derivative_eq_intros h_der refl)+
        using that m > 0 0 < r apply (simp add: divide_simps distrib_right)
        by (metis Suc_pred mult.commute power_Suc)
      then show ?thesis
      proof (rule DERIV_imp_deriv [OF has_field_derivative_transform_within_open])
        show "x. x  ball z0 r  (x - z0) ^ m * h x = g x"
          by (simp add: hnz geq)
      qed (use that m > 0 0 < r in auto)
    qed
    with 0 < r 0 < m w w_inb show "deriv g w / g w = of_nat m / (w - z0) + deriv h w / h w"
      by (auto simp: geq field_split_simps hnz)
  qed
  moreover
  have "contour_integral (circlepath z0 (r/2)) (λz. m / (z - z0) + deriv h z / h z) =
        2 * of_real pi * 𝗂 * m + 0"
  proof (rule contour_integral_unique [OF has_contour_integral_add])
    show "((λx. m / (x - z0)) has_contour_integral 2 * of_real pi * 𝗂 * m) (circlepath z0 (r/2))"
      by (force simp: 0 < r intro: Cauchy_integral_circlepath_simple)
    show "((λx. deriv h x / h x) has_contour_integral 0) (circlepath z0 (r/2))"
      using hnz holh holomorphic_deriv holomorphic_on_divide 0 < r
      by (fastforce intro!: Cauchy_theorem_disc_simple [of _ z0 r])
  qed
  ultimately show False using 0 < m by auto
qed

corollary Hurwitz_injective:
  assumes S: "open S" "connected S"
      and holf: "n::nat.  n holomorphic_on S"
      and holg: "g holomorphic_on S"
      and ul_g: "K. compact K; K  S  uniform_limit K  g sequentially"
      and nonconst: "¬ g constant_on S"
      and inj: "n. inj_on ( n) S"
    shows "inj_on g S"
proof -
  have False if z12: "z1  S" "z2  S" "z1  z2" "g z2 = g z1" for z1 z2
  proof -
    obtain z0 where "z0  S" and z0: "g z0  g z2"
      using constant_on_def nonconst by blast
    have "(λz. g z - g z1) holomorphic_on S"
      by (intro holomorphic_intros holg)
    then obtain r where "0 < r" "ball z2 r  S" "z. dist z2 z < r  z  z2  g z  g z1"
      apply (rule isolated_zeros [of "λz. g z - g z1" S z2 z0])
      using S z0  S z0 z12 by auto
    have "g z2 - g z1  0"
    proof (rule Hurwitz_no_zeros [of "S - {z1}" "λn z.  n z -  n z1" "λz. g z - g z1"])
      show "open (S - {z1})"
        by (simp add: S open_delete)
      show "connected (S - {z1})"
        by (simp add: connected_open_delete [OF S])
      show "n. (λz.  n z -  n z1) holomorphic_on S - {z1}"
        by (intro holomorphic_intros holomorphic_on_subset [OF holf]) blast
      show "(λz. g z - g z1) holomorphic_on S - {z1}"
        by (intro holomorphic_intros holomorphic_on_subset [OF holg]) blast
      show "uniform_limit K (λn z.  n z -  n z1) (λz. g z - g z1) sequentially"
           if "compact K" "K  S - {z1}" for K
      proof (rule uniform_limitI)
        fix e::real
        assume "e > 0"
        have "uniform_limit K  g sequentially"
          using that ul_g by fastforce
        then have K: "F n in sequentially. x  K. dist ( n x) (g x) < e/2"
          using 0 < e by (force simp: intro!: uniform_limitD)
        have "uniform_limit {z1}  g sequentially"
          by (simp add: ul_g z12)
        then have "F n in sequentially. x  {z1}. dist ( n x) (g x) < e/2"
          using 0 < e by (force simp: intro!: uniform_limitD)
        then have z1: "F n in sequentially. dist ( n z1) (g z1) < e/2"
          by simp
        show "F n in sequentially. xK. dist ( n x -  n z1) (g x - g z1) < e" 
          apply (rule eventually_mono [OF  eventually_conj [OF K z1]])
          by (metis (no_types, opaque_lifting) diff_add_eq diff_diff_eq2 dist_commute dist_norm dist_triangle_add_half)
      qed
      show "¬ (λz. g z - g z1) constant_on S - {z1}"
        unfolding constant_on_def
        by (metis Diff_iff z0  S empty_iff insert_iff right_minus_eq z0 z12)
      show "n z. z  S - {z1}   n z -  n z1  0"
        by (metis DiffD1 DiffD2 eq_iff_diff_eq_0 inj inj_onD insertI1 z1  S)
      show "z2  S - {z1}"
        using z2  S z1  z2 by auto
    qed
    with z12 show False by auto
  qed
  then show ?thesis by (auto simp: inj_on_def)
qed



subsection‹The Great Picard theorem›

lemma GPicard1:
  assumes S: "open S" "connected S" and "w  S" "0 < r" "Y  X"
      and holX: "h. h  X  h holomorphic_on S"
      and X01:  "h z. h  X; z  S  h z  0  h z  1"
      and r:    "h. h  Y  norm(h w)  r"
  obtains B Z where "0 < B" "open Z" "w  Z" "Z  S" "h z. h  Y; z  Z  norm(h z)  B"
proof -
  obtain e where "e > 0" and e: "cball w e  S"
    using assms open_contains_cball_eq by blast
  show ?thesis
  proof
    show "0 < exp(pi * exp(pi * (2 + 2 * r + 12)))"
      by simp
    show "ball w (e / 2)  S"
      using e ball_divide_subset_numeral ball_subset_cball by blast
    show "cmod (h z)  exp (pi * exp (pi * (2 + 2 * r + 12)))"
         if "h  Y" "z  ball w (e / 2)" for h z
    proof -
      have "h  X"
        using Y  X h  Y  by blast
      have hol_h_o: "(h  (λz. (w + of_real e * z))) holomorphic_on cball 0 1"
      proof (intro holomorphic_intros holomorphic_on_compose)
        have "h holomorphic_on S" 
          using holX h  X by auto
        then have "h holomorphic_on cball w e"
          by (metis e holomorphic_on_subset)
        moreover have "(λz. w + complex_of_real e * z) ` cball 0 1  cball w e"
          using that e > 0 by (auto simp: dist_norm norm_mult)
        ultimately show "h holomorphic_on (λz. w + complex_of_real e * z) ` cball 0 1"
          by (rule holomorphic_on_subset)
      qed
      have norm_le_r: "cmod ((h  (λz. w + complex_of_real e * z)) 0)  r"
        by (auto simp: r h  Y)
      have le12: "norm (of_real(inverse e) * (z - w))  1/2"
        using that e > 0 by (simp add: inverse_eq_divide dist_norm norm_minus_commute norm_divide)
      have non01: "h (w + e * z)  0  h (w + e * z)  1" if "z  cball 0 1" for z::complex
      proof (rule X01 [OF h  X])
        have "w + complex_of_real e * z  cball w e"
          using 0 < e that by (auto simp: dist_norm norm_mult)
        then show "w + complex_of_real e * z  S"
          by (rule subsetD [OF e])
      qed
      have "cmod (h z)  cmod (h (w + of_real e * (inverse e * (z - w))))"
        using 0 < e by (simp add: field_split_simps)
      also have "...  exp (pi * exp (pi * (14 + 2 * r)))"
        using r [OF h  Y] Schottky [OF hol_h_o norm_le_r _ _ _ le12] non01 by auto
      finally
      show ?thesis by simp
    qed
  qed (use e > 0 in auto)
qed 

lemma GPicard2:
  assumes "S  T" "connected T" "S  {}" "open S" "x. x islimpt S; x  T  x  S"
    shows "S = T"
  by (metis assms open_subset connected_clopen closedin_limpt)

    
lemma GPicard3:
  assumes S: "open S" "connected S" "w  S" and "Y  X"
      and holX: "h. h  X  h holomorphic_on S"
      and X01:  "h z. h  X; z  S  h z  0  h z  1"
      and no_hw_le1: "h. h  Y  norm(h w)  1"
      and "compact K" "K  S"
  obtains B where "h z. h  Y; z  K  norm(h z)  B"
proof -
  define U where "U  {z  S. B Z. 0 < B  open Z  z  Z  Z  S 
                               (h z'. h  Y  z'  Z  norm(h z')  B)}"
  then have "U  S" by blast
  have "U = S"
  proof (rule GPicard2 [OF U  S connected S])
    show "U  {}"
    proof -
      obtain B Z where "0 < B" "open Z" "w  Z" "Z  S" 
        and  "h z. h  Y; z  Z  norm(h z)  B"
        using GPicard1 [OF S zero_less_one Y  X holX] X01 no_hw_le1 by blast
      then show ?thesis
        unfolding U_def using w  S by blast
    qed
    show "open U"
      unfolding open_subopen [of U] by (auto simp: U_def)
    fix v
    assume v: "v islimpt U" "v  S"
    have "¬ (r>0. hY. r < cmod (h v))"
    proof
      assume "r>0. hY. r < cmod (h v)"
      then have "n. hY. Suc n < cmod (h v)"
        by simp
      then obtain  where FY: "n.  n  Y" and ltF: "n. Suc n < cmod ( n v)"
        by metis
      define 𝒢 where "𝒢  λn z. inverse( n z)"
      have hol𝒢: "𝒢 n holomorphic_on S" for n
      proof (simp add: 𝒢_def)
        show "(λz. inverse ( n z)) holomorphic_on S"
          using FY X01 Y  X holX by (blast intro: holomorphic_on_inverse)
      qed
      have 𝒢not0: "𝒢 n z  0" and 𝒢not1: "𝒢 n z  1" if "z  S" for n z
        using FY X01 Y  X that by (force simp: 𝒢_def)+
      have 𝒢_le1: "cmod (𝒢 n v)  1" for n 
        using less_le_trans linear ltF 
        by (fastforce simp add: 𝒢_def norm_inverse inverse_le_1_iff)
      define W where "W  {h. h holomorphic_on S  (z  S. h z  0  h z  1)}"
      obtain B Z where "0 < B" "open Z" "v  Z" "Z  S" 
                   and B: "h z. h  range 𝒢; z  Z  norm(h z)  B"
        apply (rule GPicard1 [OF open S connected S v  S zero_less_one, of "range 𝒢" W])
        using hol𝒢 𝒢not0 𝒢not1 𝒢_le1 by (force simp: W_def)+
      then obtain e where "e > 0" and e: "ball v e  Z"
        by (meson open_contains_ball)
      obtain h j where holh: "h holomorphic_on ball v e" and "strict_mono j"
                   and lim:  "x. x  ball v e  (λn. 𝒢 (j n) x)  h x"
                   and ulim: "K. compact K; K  ball v e
                                   uniform_limit K (𝒢  j) h sequentially"
      proof (rule Montel)
        show "h. h  range 𝒢  h holomorphic_on ball v e"
          by (metis Z  S e hol𝒢 holomorphic_on_subset imageE)
        show "K. compact K; K  ball v e  B. hrange 𝒢. zK. cmod (h z)  B"
          using B e by blast
      qed auto
      have "h v = 0"
      proof (rule LIMSEQ_unique)
        show "(λn. 𝒢 (j n) v)  h v"
          using e > 0 lim by simp
        have lt_Fj: "real x  cmod ( (j x) v)" for x
          by (metis of_nat_Suc ltF strict_mono j add.commute less_eq_real_def less_le_trans nat_le_real_less seq_suble)
        show "(λn. 𝒢 (j n) v)  0"
        proof (rule Lim_null_comparison [OF eventually_sequentiallyI lim_inverse_n])
          show "cmod (𝒢 (j x) v)  inverse (real x)" if "1  x" for x
            using that by (simp add: 𝒢_def norm_inverse_le_norm [OF lt_Fj])
        qed        
      qed
      have "h v  0"
      proof (rule Hurwitz_no_zeros [of "ball v e" "𝒢  j" h])
        show "n. (𝒢  j) n holomorphic_on ball v e"
          using Z  S e hol𝒢 by force
        show "n z. z  ball v e  (𝒢  j) n z  0"
          using 𝒢not0 Z  S e by fastforce
        show "¬ h constant_on ball v e"
        proof (clarsimp simp: constant_on_def)
          fix c
          have False if "z. dist v z < e  h z = c"  
          proof -
            have "h v = c"
              by (simp add: 0 < e that)
            obtain y where "y  U" "y  v" and y: "dist y v < e"
              using v e > 0 by (auto simp: islimpt_approachable)
            then obtain C T where "y  S" "C > 0" "open T" "y  T" "T  S"
              and "h z'. h  Y; z'  T  cmod (h z')  C"
              using y  U by (auto simp: U_def)
            then have le_C: "n. cmod ( n y)  C"
              using FY by blast

            have "F n in sequentially. dist (𝒢 (j n) y) (h y) < inverse C"
              using uniform_limitD [OF ulim [of "{y}"], of "inverse C"] C > 0 y
              by (simp add: dist_commute)
            then obtain n where "dist (𝒢 (j n) y) (h y) < inverse C"
              by (meson eventually_at_top_linorder order_refl)
            moreover
            have "h y = h v"
              by (metis h v = c dist_commute that y)
            ultimately have "cmod (inverse ( (j n) y)) < inverse C"
              by (simp add: h v = 0 𝒢_def)
            then have "C < norm ( (j n) y)"
              by (metis 𝒢_def 𝒢not0 y  S inverse_less_imp_less inverse_zero norm_inverse zero_less_norm_iff)
            show False
              using C < cmod ( (j n) y) le_C not_less by blast
          qed
          then show "xball v e. h x  c" by force
        qed
        show "h holomorphic_on ball v e"
          by (simp add: holh)
        show "K. compact K; K  ball v e  uniform_limit K (𝒢  j) h sequentially"
          by (simp add: ulim)
      qed (use e > 0 in auto)
      with h v = 0 show False by blast
    qed
    then obtain r where "0 < r" and r: "h. h  Y  cmod (h v)  r"
      by (metis not_le)
    moreover     
    obtain B Z where "0 < B" "open Z" "v  Z" "Z  S" "h z. h  Y; z  Z  norm(h z)  B"
      using X01 
      by (auto simp: r intro: GPicard1[OF open S connected S v  S r>0 Y  X holX] X01)
    ultimately show "v  U"
      using v by (simp add: U_def) meson
  qed
  have "x. x  K  x  U"
    using U = S K  S by blast
  then have "x. x  K  (B Z. 0 < B  open Z  x  Z  
                               (h z'. h  Y  z'  Z  norm(h z')  B))"
    unfolding U_def by blast
  then obtain F Z where F: "x. x  K  open (Z x)  x  Z x  
                               (h z'. h  Y  z'  Z x  norm(h z')  F x)"
    by metis
  then obtain L where "L  K" "finite L" and L: "K  (c  L. Z c)"
    by (auto intro: compactE_image [OF compact K, of K Z])
  then have *: "x h z'. x  L; h  Y  z'  Z x  cmod (h z')  F x"
    using F by blast
  have "B. h z. h  Y  z  K  norm(h z)  B"
  proof (cases "L = {}")
    case True with L show ?thesis by simp
  next
    case False
    then have "h z. h  Y  z  K  (xL. cmod (h z)  F x)"
      by (metis "*" L UN_E subset_iff)
    with False finite L show ?thesis 
      by (rule_tac x = "Max (F ` L)" in exI) (simp add: linorder_class.Max_ge_iff)
  qed
  with that show ?thesis by metis
qed


lemma GPicard4:
  assumes "0 < k" and holf: "f holomorphic_on (ball 0 k - {0})" 
      and AE: "e. 0 < e; e < k  d. 0 < d  d < e  (z  sphere 0 d. norm(f z)  B)"
  obtains ε where "0 < ε" "ε < k" "z. z  ball 0 ε - {0}  norm(f z)  B"
proof -
  obtain ε where "0 < ε" "ε < k/2" and ε: "z. norm z = ε  norm(f z)  B"
    using AE [of "k/2"] 0 < k by auto
  show ?thesis
  proof
    show "ε < k"
      using 0 < k ε < k/2 by auto
    show "cmod (f ξ)  B" if ξ: "ξ  ball 0 ε - {0}" for ξ
    proof -
      obtain d where "0 < d" "d < norm ξ" and d: "z. norm z = d  norm(f z)  B"
        using AE [of "norm ξ"] ε < k ξ by auto
      have [simp]: "closure (cball 0 ε - ball 0 d) = cball 0 ε - ball 0 d"
        by (blast intro!: closure_closed)
      have [simp]: "interior (cball 0 ε - ball 0 d) = ball 0 ε - cball (0::complex) d"
        using 0 < ε 0 < d by (simp add: interior_diff)
      have *: "norm(f w)  B" if "w  cball 0 ε - ball 0 d" for w
      proof (rule maximum_modulus_frontier [of f "cball 0 ε - ball 0 d"])
        show "f holomorphic_on interior (cball 0 ε - ball 0 d)"
          using ε < k 0 < d that by (auto intro:  holomorphic_on_subset [OF holf])
        show "continuous_on (closure (cball 0 ε - ball 0 d)) f"
        proof (intro holomorphic_on_imp_continuous_on holomorphic_on_subset [OF holf])
          show "closure (cball 0 ε - ball 0 d)  ball 0 k - {0}"
            using 0 < d ε < k by auto
        qed
        show "z. z  frontier (cball 0 ε - ball 0 d)  cmod (f z)  B"
          unfolding frontier_def
          using ε d less_eq_real_def by force
      qed (use that in auto)
      show ?thesis
        using * d < cmod ξ that by auto
    qed
  qed (use 0 < ε in auto)
qed
  

lemma GPicard5:
  assumes holf: "f holomorphic_on (ball 0 1 - {0})"
      and f01:  "z. z  ball 0 1 - {0}  f z  0  f z  1"
  obtains e B where "0 < e" "e < 1" "0 < B" 
                    "(z  ball 0 e - {0}. norm(f z)  B) 
                     (z  ball 0 e - {0}. norm(f z)  B)"
proof -
  have [simp]: "1 + of_nat n  (0::complex)" for n
    using of_nat_eq_0_iff by fastforce
  have [simp]: "cmod (1 + of_nat n) = 1 + of_nat n" for n
    by (metis norm_of_nat of_nat_Suc)
  have *: "(λx::complex. x / of_nat (Suc n)) ` (ball 0 1 - {0})  ball 0 1 - {0}" for n
    by (auto simp: norm_divide field_split_simps split: if_split_asm)
  define h where "h  λn z::complex. f (z / (Suc n))"
  have holh: "(h n) holomorphic_on ball 0 1 - {0}" for n
    unfolding h_def
  proof (rule holomorphic_on_compose_gen [unfolded o_def, OF _ holf *])
    show "(λx. x / of_nat (Suc n)) holomorphic_on ball 0 1 - {0}"
      by (intro holomorphic_intros) auto
  qed
  have h01: "n z. z  ball 0 1 - {0}  h n z  0  h n z  1" 
    unfolding h_def 
    using * by (force intro!: f01)
  obtain w where w: "w  ball 0 1 - {0::complex}"
    by (rule_tac w = "1/2" in that) auto
  consider "infinite {n. norm(h n w)  1}" | "infinite {n. 1  norm(h n w)}"
    by (metis (mono_tags, lifting) infinite_nat_iff_unbounded_le le_cases mem_Collect_eq)
  then show ?thesis
  proof cases
    case 1
    with infinite_enumerate obtain r :: "nat  nat" 
      where "strict_mono r" and r: "n. r n  {n. norm(h n w)  1}"
      by blast
    obtain B where B: "j z. norm z = 1/2; j  range (h  r)  norm(j z)  B"
    proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"])  
      show "range (h  r)  
            {g. g holomorphic_on ball 0 1 - {0}  (z  ball 0 1 - {0}. g z  0  g z  1)}"
        using h01 by (auto intro: holomorphic_intros holomorphic_on_compose holh)
      show "connected (ball 0 1 - {0::complex})"
        by (simp add: connected_open_delete)
    qed (use r in auto)        
    have normf_le_B: "cmod(f z)  B" if "norm z = 1 / (2 * (1 + of_nat (r n)))" for z n
    proof -
      have *: "w. norm w = 1/2  cmod((f (w / (1 + of_nat (r n)))))  B"
        using B by (auto simp: h_def o_def)
      have half: "norm (z * (1 + of_nat (r n))) = 1/2"
        by (simp add: norm_mult divide_simps that)
      show ?thesis
        using * [OF half] by simp
    qed
    obtain ε where "0 < ε" "ε < 1" "z. z  ball 0 ε - {0}  cmod(f z)  B"
    proof (rule GPicard4 [OF zero_less_one holf, of B])
      fix e::real
      assume "0 < e" "e < 1"
      obtain n where "(1/e - 2) / 2 < real n"
        using reals_Archimedean2 by blast
      also have "...  r n"
        using strict_mono r by (simp add: seq_suble)
      finally have "(1/e - 2) / 2 < real (r n)" .
      with 0 < e have e: "e > 1 / (2 + 2 * real (r n))"
        by (simp add: field_simps)
      show "d>0. d < e  (zsphere 0 d. cmod (f z)  B)"
        apply (rule_tac x="1 / (2 * (1 + of_nat (r n)))" in exI)
        using normf_le_B by (simp add: e)
    qed blast
    then have ε: "cmod (f z)  ¦B¦ + 1" if "cmod z < ε" "z  0" for z
      using that by fastforce
    have "0 < ¦B¦ + 1"
      by simp
    then show ?thesis
      using ε by (force intro!: that [OF 0 < ε ε < 1])
  next
    case 2
    with infinite_enumerate obtain r :: "nat  nat" 
      where "strict_mono r" and r: "n. r n  {n. norm(h n w)  1}"
      by blast
    obtain B where B: "j z. norm z = 1/2; j  range (λn. inverse  h (r n))  norm(j z)  B"
    proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"])  
      show "range (λn. inverse  h (r n))  
            {g. g holomorphic_on ball 0 1 - {0}  (zball 0 1 - {0}. g z  0  g z  1)}"
        using h01 by (auto intro!: holomorphic_intros holomorphic_on_compose_gen [unfolded o_def, OF _ holh] holomorphic_on_compose)
      show "connected (ball 0 1 - {0::complex})"
        by (simp add: connected_open_delete)
      show "j. j  range (λn. inverse  h (r n))  cmod (j w)  1"
        using r norm_inverse_le_norm by fastforce
    qed (use r in auto)        
    have norm_if_le_B: "cmod(inverse (f z))  B" if "norm z = 1 / (2 * (1 + of_nat (r n)))" for z n
    proof -
      have *: "inverse (cmod((f (z / (1 + of_nat (r n))))))  B" if "norm z = 1/2" for z
        using B [OF that] by (force simp: norm_inverse h_def)
      have half: "norm (z * (1 + of_nat (r n))) = 1/2"
        by (simp add: norm_mult divide_simps that)
      show ?thesis
        using * [OF half] by (simp add: norm_inverse)
    qed
    have hol_if: "(inverse  f) holomorphic_on (ball 0 1 - {0})"
      by (metis (no_types, lifting) holf comp_apply f01 holomorphic_on_inverse holomorphic_transform)
    obtain ε where "0 < ε" "ε < 1" and leB: "z. z  ball 0 ε - {0}  cmod((inverse  f) z)  B"
    proof (rule GPicard4 [OF zero_less_one hol_if, of B])
      fix e::real
      assume "0 < e" "e < 1"
      obtain n where "(1/e - 2) / 2 < real n"
        using reals_Archimedean2 by blast
      also have "...  r n"
        using strict_mono r by (simp add: seq_suble)
      finally have "(1/e - 2) / 2 < real (r n)" .
      with 0 < e have e: "e > 1 / (2 + 2 * real (r n))"
        by (simp add: field_simps)
      show "d>0. d < e  (zsphere 0 d. cmod ((inverse  f) z)  B)"
        apply (rule_tac x="1 / (2 * (1 + of_nat (r n)))" in exI)
        using norm_if_le_B by (simp add: e)
    qed blast
    have ε: "cmod (f z)  inverse B" and "B > 0" if "cmod z < ε" "z  0" for z
    proof -
      have "inverse (cmod (f z))  B"
        using leB that by (simp add: norm_inverse)
      moreover
      have "f z  0"
        using ε < 1 f01 that by auto
      ultimately show "cmod (f z)  inverse B"
        by (simp add: norm_inverse inverse_le_imp_le)
      show "B > 0"
        using f z  0 inverse (cmod (f z))  B not_le order.trans by fastforce
    qed
    then have "B > 0"
      by (metis 0 < ε dense leI order.asym vector_choose_size)
    then have "inverse B > 0"
      by (simp add: field_split_simps)
    then show ?thesis
      using ε that [OF 0 < ε ε < 1]
      by (metis Diff_iff dist_0_norm insert_iff mem_ball)
  qed
qed

  
lemma GPicard6:
  assumes "open M" "z  M" "a  0" and holf: "f holomorphic_on (M - {z})"
      and f0a: "w. w  M - {z}  f w  0  f w  a"
  obtains r where "0 < r" "ball z r  M" 
                  "bounded(f ` (ball z r - {z})) 
                   bounded((inverse  f) ` (ball z r - {z}))"
proof -
  obtain r where "0 < r" and r: "ball z r  M"
    using assms openE by blast 
  let ?g = "λw. f (z + of_real r * w) / a"
  obtain e B where "0 < e" "e < 1" "0 < B" 
    and B: "(z  ball 0 e - {0}. norm(?g z)  B)  (z  ball 0 e - {0}. norm(?g z)  B)"
  proof (rule GPicard5)
    show "?g holomorphic_on ball 0 1 - {0}"
    proof (intro holomorphic_intros holomorphic_on_compose_gen [unfolded o_def, OF _ holf])
      show "(λx. z + complex_of_real r * x) ` (ball 0 1 - {0})  M - {z}"
        using 0 < r r
        by (auto simp: dist_norm norm_mult subset_eq)
    qed (use a  0 in auto)
    show "w. w  ball 0 1 - {0}  f (z + of_real r * w) / a  0  f (z + of_real r * w) / a  1"
      using f0a 0 < r a  0 r
      by (auto simp: field_split_simps dist_norm norm_mult subset_eq)
  qed
  show ?thesis
  proof
    show "0 < e*r"
      by (simp add: 0 < e 0 < r)
    have "ball z (e * r)  ball z r"
      by (simp add: 0 < r e < 1 order.strict_implies_order subset_ball)
    then show "ball z (e * r)  M"
      using r by blast
    consider "z. z  ball 0 e - {0}  norm(?g z)  B" | "z. z  ball 0 e - {0}  norm(?g z)  B"
      using B by blast
    then show "bounded (f ` (ball z (e * r) - {z})) 
          bounded ((inverse  f) ` (ball z (e * r) - {z}))"
    proof cases
      case 1
      have "dist z w < e * r; w  z  cmod (f w)  B * norm a" for w
        using a  0 0 < r 1 [of "(w - z) / r"]
        by (simp add: norm_divide dist_norm field_split_simps)
      then show ?thesis
        by (force simp: intro!: boundedI)
    next
      case 2
      have "dist z w < e * r; w  z  cmod (f w)  B * norm a" for w
        using a  0 0 < r 2 [of "(w - z) / r"]
        by (simp add: norm_divide dist_norm field_split_simps)
      then have "dist z w < e * r; w  z  inverse (cmod (f w))  inverse (B * norm a)" for w
        by (metis 0 < B a  0 mult_pos_pos norm_inverse norm_inverse_le_norm zero_less_norm_iff)
      then show ?thesis 
        by (force simp: norm_inverse intro!: boundedI)
    qed
  qed
qed
  

theorem great_Picard:
  assumes "open M" "z  M" "a  b" and holf: "f holomorphic_on (M - {z})"
      and fab: "w. w  M - {z}  f w  a  f w  b"
  obtains l where "(f  l) (at z)  ((inverse  f)  l) (at z)"
proof -
  obtain r where "0 < r" and zrM: "ball z r  M" 
             and r: "bounded((λz. f z - a) ` (ball z r - {z})) 
                     bounded((inverse  (λz. f z - a)) ` (ball z r - {z}))"
  proof (rule GPicard6 [OF open M z  M])
    show "b - a  0"
      using assms by auto
    show "(λz. f z - a) holomorphic_on M - {z}"
      by (intro holomorphic_intros holf)
  qed (use fab in auto)
  have holfb: "f holomorphic_on ball z r - {z}"
    using zrM by (auto intro: holomorphic_on_subset [OF holf])
  have holfb_i: "(λz. inverse(f z - a)) holomorphic_on ball z r - {z}"
    using fab zrM by (fastforce intro!: holomorphic_intros holfb)
  show ?thesis
    using r
  proof              
    assume "bounded ((λz. f z - a) ` (ball z r - {z}))"
    then obtain B where B: "w. w  (λz. f z - a) ` (ball z r - {z})  norm w  B"
      by (force simp: bounded_iff)
    then have "x. x  z  dist x z < r  cmod (f x - a)  B"
      by (simp add: dist_commute)
    with 0 < r have "F w in at z. cmod (f w - a)  B"
      by (force simp add: eventually_at)
    moreover have "x. cmod (f x - a)  B  cmod (f x)  B + cmod a"
      by (metis add.commute add_le_cancel_right norm_triangle_sub order.trans)
    ultimately have "B. F w in at z. cmod (f w)  B"
      by (metis (mono_tags, lifting) eventually_at)
    then obtain g where holg: "g holomorphic_on ball z r" and gf: "w. w  ball z r - {z}  g w = f w"
      using 0 < r holomorphic_on_extend_bounded [OF holfb] by auto
    then have "g z g z"
      unfolding continuous_at [symmetric]
      using 0 < r centre_in_ball field_differentiable_imp_continuous_at 
            holomorphic_on_imp_differentiable_at by blast
    then have "(f  g z) (at z)"
      using Lim_transform_within_open [of g "g z" z]
      using 0 < r centre_in_ball gf by blast
    then show ?thesis
      using that by blast
  next
    assume "bounded((inverse  (λz. f z - a)) ` (ball z r - {z}))"
    then obtain B where B: "w. w  (inverse  (λz. f z - a)) ` (ball z r - {z})  norm w  B"
      by (force simp: bounded_iff)
    then have "x. x  z  dist x z < r  cmod (inverse (f x - a))  B"
      by (simp add: dist_commute)
    with 0 < r have "F w in at z. cmod (inverse (f w - a))  B"
      by (auto simp add: eventually_at)
    then have "B. F z in at z. cmod (inverse (f z - a))  B"
      by blast
    then obtain g where holg: "g holomorphic_on ball z r" and gf: "w. w  ball z r - {z}  g w = inverse (f w - a)"
      using 0 < r holomorphic_on_extend_bounded [OF holfb_i] by auto
    then have gz: "g z g z"
      unfolding continuous_at [symmetric]
      using 0 < r centre_in_ball field_differentiable_imp_continuous_at 
            holomorphic_on_imp_differentiable_at by blast
    have gnz: "w. w  ball z r - {z}  g w  0"
      using gf fab zrM by fastforce
    show ?thesis
    proof (cases "g z = 0")
      case True
      have *: "g  0; inverse g = f - a  g / (1 + a * g) = inverse f" for f g::complex
        by (auto simp: field_simps)
      have "(inverse  f) z 0"
      proof (rule Lim_transform_within_open [of "λw. g w / (1 + a * g w)" _ _ UNIV "ball z r"])
        show "(λw. g w / (1 + a * g w)) z 0"
          using True by (auto simp: intro!: tendsto_eq_intros gz)
        show "x. x  ball z r; x  z  g x / (1 + a * g x) = (inverse  f) x"
          using * gf gnz by simp
      qed (use 0 < r in auto)
      with that show ?thesis by blast
    next
      case False
      show ?thesis
      proof (cases "1 + a * g z = 0")
        case True
        have "(f  0) (at z)"
        proof (rule Lim_transform_within_open [of "λw. (1 + a * g w) / g w" _ _ _ "ball z r"])
          show "(λw. (1 + a * g w) / g w) z 0"
            by (rule tendsto_eq_intros refl gz g z  0 | simp add: True)+
          show "x. x  ball z r; x  z  (1 + a * g x) / g x = f x"
            using fab fab zrM by (fastforce simp add: gf field_split_simps)
        qed (use 0 < r in auto)
        then show ?thesis
          using that by blast 
      next
        case False
        have *: "g  0; inverse g = f - a  g / (1 + a * g) = inverse f" for f g::complex
          by (auto simp: field_simps)
        have "(inverse  f) z g z / (1 + a * g z)"
        proof (rule Lim_transform_within_open [of "λw. g w / (1 + a * g w)" _ _ UNIV "ball z r"])
          show "(λw. g w / (1 + a * g w)) z g z / (1 + a * g z)"
            using False by (auto simp: False intro!: tendsto_eq_intros gz)
          show "x. x  ball z r; x  z  g x / (1 + a * g x) = (inverse  f) x"
            using * gf gnz by simp
        qed (use 0 < r in auto)
        with that show ?thesis by blast
      qed
    qed 
  qed
qed


corollary great_Picard_alt:
  assumes M: "open M" "z  M" and holf: "f holomorphic_on (M - {z})"
    and non: "l. ¬ (f  l) (at z)" "l. ¬ ((inverse  f)  l) (at z)"
  obtains a where "- {a}  f ` (M - {z})"
unfolding subset_iff image_iff
  by (metis great_Picard [OF M _ holf] non Compl_iff insertI1)
    

corollary great_Picard_infinite:
  assumes M: "open M" "z  M" and holf: "f holomorphic_on (M - {z})"
    and non: "l. ¬ (f  l) (at z)" "l. ¬ ((inverse  f)  l) (at z)"
  obtains a where "w. w  a  infinite {x. x  M - {z}  f x = w}"
proof -
  have False if "a  b" and ab: "finite {x. x  M - {z}  f x = a}" "finite {x. x  M - {z}  f x = b}" for a b
  proof -
    have finab: "finite {x. x  M - {z}  f x  {a,b}}"
      using finite_UnI [OF ab]  unfolding mem_Collect_eq insert_iff empty_iff
      by (simp add: conj_disj_distribL)
    obtain r where "0 < r" and zrM: "ball z r  M" and r: "x. x  M - {z}; f x  {a,b}  x  ball z r"
    proof -
      obtain e where "e > 0" and e: "ball z e  M"
        using assms openE by blast
      show ?thesis
      proof (cases "{x  M - {z}. f x  {a, b}} = {}")
        case True
        then show ?thesis
          using e e > 0 that by fastforce
      next
        case False
        let ?r = "min e (Min (dist z ` {x  M - {z}. f x  {a,b}}))"
        show ?thesis
        proof
          show "0 < ?r"
            using min_less_iff_conj Min_gr_iff finab False 0 < e by auto
          have "ball z ?r  ball z e"
            by (simp add: subset_ball)
          with e show "ball z ?r  M" by blast
          show "x. x  M - {z}; f x  {a, b}  x  ball z ?r"
            using min_less_iff_conj Min_gr_iff finab False 0 < e by auto
        qed
      qed
    qed
    have holfb: "f holomorphic_on (ball z r - {z})"
      apply (rule holomorphic_on_subset [OF holf])
       using zrM by auto
     show ?thesis
       apply (rule great_Picard [OF open_ball _ a  b holfb])
      using non 0 < r r zrM by auto
  qed
  with that show thesis
    by meson
qed

theorem Casorati_Weierstrass:
  assumes "open M" "z  M" "f holomorphic_on (M - {z})"
      and "l. ¬ (f  l) (at z)" "l. ¬ ((inverse  f)  l) (at z)"
  shows "closure(f ` (M - {z})) = UNIV"
proof -
  obtain a where a: "- {a}  f ` (M - {z})"
    using great_Picard_alt [OF assms] .
  have "UNIV = closure(- {a})"
    by (simp add: closure_interior)
  also have "...  closure(f ` (M - {z}))"
    by (simp add: a closure_mono)
  finally show ?thesis
    by blast 
qed
  
end