Quelle Great_Picard.thy Sprache: Isabelle

section \<open>The Great Picard Theorem and its Applications\<close>

text\<open>Ported from HOL Light (cauchy.ml) by L C Paulson, 2017\<close>

theory Great_Picard
  imports Conformal_Mappings
begin

subsection\<open>Schottky's theorem\<close>

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 \<open>3 \<le> pi\<close> 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)\<^sup>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)\<^sup>2 - 1)) / pi \ x"
    then have "ln (n + sqrt ((real n)\<^sup>2 - 1)) \ x * pi"
      by (simp add: field_split_simps)
    then have *: "exp (ln (n + sqrt ((real n)\<^sup>2 - 1))) \ exp (x * pi)"
      by blast
    have 0: "0 \ sqrt ((real n)\<^sup>2 - 1)"
      using \<open>0 < n\<close> by auto
    have "n + sqrt ((real n)\<^sup>2 - 1) = exp (ln (n + sqrt ((real n)\<^sup>2 - 1)))"
      by (simp add: Suc_leI \<open>0 < n\<close> 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 ln (n + sqrt ((real n)\<^sup>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)\<^sup>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)\<^sup>2 - 1)) - ln (real n + sqrt ((real n)\<^sup>2 - 1)) =
         ln ((1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / (real n + sqrt ((real n)\<^sup>2 - 1)))"
      by (simp add: \<open>0 < n\<close> Schottky_lemma1 add_pos_nonneg ln_divide_pos [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 \<open>0 < n\<close> have "1 < n" "2 \<le> 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"]  \<open>2 \<le> n\<close>
        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)\<^sup>2 - 1) \ 2 * sqrt ((real n)\<^sup>2 - 1)"
        by (auto simp: real_le_lsqrt power2_eq_square algebra_simps 1 **)
      then
      have "((1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / (real n + sqrt ((real n)\<^sup>2 - 1))) \ 2"
        using Schottky_lemma1 \<open>0 < n\<close>  by (simp add: field_split_simps)
      then have "ln ((1 + real n + sqrt ((1 + real n)\<^sup>2 - 1)) / (real n + sqrt ((real n)\<^sup>2 - 1))) \ ln 2"
        using Schottky_lemma1 [of n] \<open>0 < n\<close>
        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 \<open>0 < n\<close>)
  next
    assume "\x - b\ < 1/2"
    then show ?thesis
      by (rule_tac n="Suc n" in that) (auto simp: b_def \<open>0 < n\<close>)
  qed
qed

lemma Schottky_lemma3:
  fixes z::complex
  assumes "z \ (\m \ Ints. \n \ {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)})
             \<union> (\<Union>m \<in> Ints. \<Union>n \<in> {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)\<^sup>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)\<^sup>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 \<open>z \<in> ball 0 1\<close> 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] \<open>z \<in> ball 0 1\<close> 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 \<open>norm z \<le> t\<close> segment_bound1 [OF \<open>w \<in> closed_segment 0 z\<close>] 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)}) \
                    (\<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
        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)\<^sup>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)\<^sup>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)\<^sup>2 - 1)) / pi)) < 1"
              by (simp add: dist_triangle_lt [of b "Complex m (Im b)"] dist_commute)
            with le m \<open>0 < n\<close> show ?thesis
              apply (rule_tac x = "Complex m (ln (real n + sqrt ((real n)\<^sup>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)\<^sup>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)\<^sup>2 - 1)) / pi)) (Complex m (Im b))
                = \<bar> - Im b - ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi\<bar>"
              by (simp add: complex_norm dist_norm cmod_eq_Re complex_diff)
            ultimately have "dist b (Complex m (- ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi)) < 1"
              using n by (simp add: dist_triangle_lt [of b "Complex m (Im b)"] dist_commute)
            with ge m \<open>0 < n\<close> show ?thesis
              by (rule_tac x = "Complex m (- ln (real n + sqrt ((real n)\<^sup>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)}) \
                    (\<Union>m \<in> Ints. \<Union>n \<in> {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 \<open>cmod z \<le> t\<close> \<open>t < 1\<close> show ?thesis
      by (simp add: field_split_simps)
  qed
  have fz: "f z = (1 + cos(of_real pi * h z)) / 2"
    using h \<open>z \<in> ball 0 1\<close> 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 \<open>t < 1\<close> 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 \<open>z \<in> ball 0 1\<close> by (simp add: g norm_cos_le)
    also have "... \ exp (pi * (2 + 2 * r + 12 * t / (1 - t)))"
      using \<open>t < 1\<close> 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\<open>The Little Picard Theorem\<close>

theorem Landau_Picard:
  obtains R
    where "\z. 0 < R z"
          "\f. \f holomorphic_on cball 0 (R(f 0));
                 \<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"
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));
                      \<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"
    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\<open>A couple of little applications of Little Picard\<close>

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 \<open>p \<noteq> 0\<close> 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 \<open>c \<noteq> 1\<close> 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 \<open>c \<noteq> 0\<close> 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>open (range f)\<close> 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\<open>The Arzelà--Ascoli theorem\<close>

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.
                   \<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)"
   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::nat\nat)" "\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 \<open>countable S\<close> obtain \<sigma> :: "nat \<Rightarrow> 'a" where \<sigma>: "S = range \<sigma>"
    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::nat\nat. 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: \<sigma> 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 :: "nat\nat"
      using that
      by (simp add: lim_sequentially) (metis (no_types, opaque_lifting) le_cases order_trans)
  qed auto
  with \<sigma> that show ?thesis
    by force
qed

theorem Arzela_Ascoli:
  fixes \<F> :: "[nat,'a::euclidean_space] \<Rightarrow> '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\
                 \<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)"
  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 \<open>compact S\<close>, of "range \<F>"])
    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 "\\<^sub>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 \<open>R \<subseteq> S\<close> by (force intro: function_convergent_subsequence [OF \<open>countable R\<close> 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 \<open>0 < e\<close> divide_pos_pos zero_less_numeral)
    obtain T where "T \ R" and "finite T" and T: "S \ (\c\T. ball c d)"
    proof (rule compactE_image [OF  \<open>compact S\<close>, of R "(\<lambda>x. ball x d)"])
      have "closure R \ (\c\R. ball c d)"
        using \<open>0 < d\<close> by (auto simp: closure_approachable)
      with SR show "S \ (\c\R. ball c d)"
        by auto
    qed auto
    have "\M. \m\M. \n\M. dist (\ (k m) x) (\ (k n) x) < e/3" if "x \ R" for x
      using Cauchy \<open>0 < e\<close> 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 \<open>x \<in> S\<close> T by auto
      have "norm(\ (k m) t - \ (k m) x) < e / 3"
        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>)
      moreover
      have "norm(\ (k n) t - \ (k n) x) < e / 3"
        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>)
      moreover
      have "norm(\ (k m) t - \ (k n) t) < e / 3"
      proof (rule MF)
        show "t \ R"
          using \<open>T \<subseteq> R\<close> \<open>t \<in> T\<close> by blast
        show "MF t \ m" "MF t \ n"
          by (meson Max_ge \<open>finite T\<close> \<open>t \<in> T\<close> 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 \<open>strict_mono k\<close> comp_apply that)
qed

subsubsection\<^marker>\<open>tag important\<close>\<open>Montel's theorem\<close>

text\<open>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.\<close>

theorem Montel:
  fixes \<F> :: "[nat,complex] \<Rightarrow> complex"
  assumes "open S"
      and \<H>: "\<And>h. h \<in> \<H> \<Longrightarrow> 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. \n\N. X \ K n"
    using open_Union_compact_subsets [OF \<open>open S\<close>] 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::nat\nat) \ (\e > 0. \N. \n\N. \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::nat\nat)"
                    "\e. 0 < e \ \N. \n\N. \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>open S\<close> by (force simp: open_contains_cball)
        have "cball z (2/3 * r) \ cball z r"
          using \<open>0 < r\<close> 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: "\n\N. 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 \<open>\<And>n. \<F> n \<in> \<H>\<close> 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) * \<i> * winding_number (circlepath z (2/3 * r)) \<xi> * \<F> n \<xi>)
                (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: \<H> \<open>\<And>n. \<F> n \<in> \<H>\<close>)
            with z23S show "\ n holomorphic_on cball z (2/3 * r)"
              using holomorphic_on_subset by blast
          qed (use that \<open>0 < r\<close> in \<open>auto simp: dist_commute\<close>)
          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 \<open>0 < r\<close> 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 \<open>0 < r\<close> 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 \<open>M > 0\<close> \<open>r > 0\<close>
               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 \<open>r > 0\<close> by simp
             then have neq: "x \ y" "x \ z"
               using that \<open>r > 0\<close> 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 \<open>r > 0\<close> \<open>M > 0\<close> 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) \<open>M > 0\<close> \<open>r > 0\<close> neq
               by (simp add: field_simps mult_less_0_iff norm_minus_commute)
             also have "... \ e/r"
               using \<open>e > 0\<close> \<open>r > 0\<close> 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 \<open>e > 0\<close> \<open>r > 0\<close> in auto)
           also have "... = (2 * pi) * e * ((2/3))"
             using \<open>r > 0\<close> by (simp add: field_split_simps)
           finally have "cmod (\ n y - \ n z) \ e * (2/3)"
             by simp
           also have "... < e"
             using \<open>e > 0\<close> 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 \<open>0 < e\<close> \<open>0 < r\<close> \<open>0 < M\<close> by simp
      qed
      show "\n x. x \ K i \ cmod (\ n x) \ B i"
        using B \<open>\<And>n. \<F> n \<in> \<H>\<close> by blast
    next
      fix g :: "complex \ complex" and k :: "nat \ nat"
      assume *: "\(g::complex\complex) (k::nat\nat). continuous_on (K i) g \
                  strict_mono k \<Longrightarrow>
                  (\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>K i. cmod (\<F> (k n) x - g x) < e) \<Longrightarrow> 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 \<Phi> where "\<Phi> \<equiv> \<lambda>g i r. \<lambda>k::nat\<Rightarrow>nat. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>K i. cmod ((\<F> \<circ> (r \<circ> 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::"nat\nat"
    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: \<Phi>_def) (metis (no_types, opaque_lifting) le_trans linear)
      then show ?thesis
        by metis
    qed
    have "\k g. strict_mono (k::nat\nat) \ \ g i id (r \ k)" for i r
      unfolding \<Phi>_def o_assoc using rng_f by (force intro!: *)
    then show "\i r. \k. strict_mono (k::nat\nat) \ (\g. \ g i id (r \ k))"
      by force
  qed fastforce
  have "\l. \e>0. \N. \n\N. norm(\ (k n) z - l) < e" if "z \ S" for z
  proof -
    obtain G where G: "\i e. e > 0 \ \M. \n\M. \x\K i. cmod ((\ \ k) n x - G i x) < e"
      using k unfolding \<Phi>_def by (metis id_comp)
    obtain N where "\n. n \ N \ z \ K n"
      using subK [of "{z}"] that \<open>z \<in> S\<close> by auto
    moreover have "\e. e > 0 \ \M. \n\M. \x\K 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. \n\N. 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. \n\N. \x\T. 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. \n\M. \x\K N. cmod ((\ \ k) n x - h x) < e"
        using k unfolding \<Phi>_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 \<open>T \<subseteq> S\<close> 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 \<open>0 < e\<close> by (fastforce simp add: geq)
    qed
    then show "\K. \compact K; K \ S\
         \<Longrightarrow> uniform_limit K (\<F> \<circ> 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>open S\<close> \<H>])
      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>open S\<close> \<open>z \<in> S\<close> 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: \<open>strict_mono k\<close>)
qed

subsection\<open>Some simple but useful cases of Hurwitz's theorem\<close>

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 \<open>z0 \<in> S\<close> 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>open S\<close> holf holomorphic_deriv holomorphic_on_divide holomorphic_on_subset nz subS)
  qed (use \<open>0 < r\<close> in auto)
  have hol_dg: "deriv g holomorphic_on S"
    by (simp add: \<open>open S\<close> holg holomorphic_deriv)
  have "continuous_on (sphere z0 (r/2)) (deriv g)"
    using \<open>0 < r\<close> 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 \<open>0 < r\<close> 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 \<open>0 < r\<close> 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)) (\<lambda>z. deriv g z / g z)"
  proof (rule contour_integral_uniform_limit_circlepath)
    show "\\<^sub>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 "\\<^sub>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 \<open>0 < r\<close> 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 \<open>0 < r\<close> 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 \<open>w \<in> S\<close> holf \<open>open S\<close>)
            moreover
            have "g field_differentiable at w"
              using \<open>w \<in> S\<close> \<open>open S\<close> 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] \<open>r > 0\<close> by auto
            ultimately have "dist (deriv (\ n) w) (deriv g w) \ e/2"
              by (simp add: dist_norm)
            then show ?thesis
              using \<open>e > 0\<close> by auto
          qed
          moreover
          have "cball z0 (3 * r / 4) \ ball z0 r"
            by (simp add: cball_subset_ball_iff \<open>0 < r\<close>)
          with subS have "uniform_limit (cball z0 (3 * r/4)) \ g sequentially"
            by (force intro: ul_g)
          then have "\\<^sub>F n in sequentially. \x\cball z0 (3 * r / 4). dist (\ n x) (g x) < r / 4 * e / 2"
            using \<open>0 < e\<close> \<open>0 < r\<close> 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 \<open>0 < r\<close> by auto
        with subS have "uniform_limit (sphere z0 (r/2)) \ g sequentially"
          by (force intro: ul_g)
        then show "\\<^sub>F n in sequentially. \x \ sphere z0 (r/2). dist (\ n x) (g x) < e"
          using \<open>0 < e\<close> uniform_limit_iff by blast
      qed
      show "b > 0" "\x. x \ sphere z0 (r/2) \ b \ cmod (g x)"
        using b \<open>0 < r\<close> by (fastforce simp: geq hnz)+
    qed
  qed (use \<open>0 < r\<close> 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)) (\<lambda>z. m / (z - z0) + deriv h z / h z)"
  proof (rule contour_integral_eq, use \<open>0 < r\<close> in simp)
    fix w
    assume w: "dist z0 w * 2 = r"
    then have w_inb: "w \ ball z0 r"
      using \<open>0 < r\<close> 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 \<open>m > 0\<close> \<open>0 < r\<close> 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 \<open>m > 0\<close> \<open>0 < r\<close> in auto)
    qed
    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"
      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 * \<i> * 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: \<open>0 < r\<close> 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 \<open>0 < r\<close>
      by (fastforce intro!: Cauchy_theorem_disc_simple [of _ z0 r])
  qed
  ultimately show False using \<open>0 < m\<close> 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"
      using isolated_zeros [of "\z. g z - g z1" S z2 z0] 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: "\\<^sub>F n in sequentially. \x \ K. dist (\ n x) (g x) < e/2"
          using \<open>0 < e\<close> by (force simp: intro!: uniform_limitD)
        have "uniform_limit {z1} \ g sequentially"
          by (intro ul_g) (auto simp: z12)
        then have "\\<^sub>F n in sequentially. \x \ {z1}. dist (\ n x) (g x) < e/2"
          using \<open>0 < e\<close> by (force simp: intro!: uniform_limitD)
        then have z1: "\\<^sub>F n in sequentially. dist (\ n z1) (g z1) < e/2"
          by simp
        show "\\<^sub>F n in sequentially. \x\K. dist (\ n x - \ n z1) (g x - g z1) < e"
          apply (intro 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 \<open>z0 \<in> S\<close> 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 \<open>z1 \<in> S\<close>)
      show "z2 \ S - {z1}"
        using \<open>z2 \<in> S\<close> \<open>z1 \<noteq> z2\<close> by auto
    qed
    with z12 show False by auto
  qed
  then show ?thesis by (auto simp: inj_on_def)
qed

subsection\<open>The Great Picard theorem\<close>

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 -
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.