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 Further_Topology 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 "(n-1)^2 ≤ n^2 - 1" using assms by (simp add: algebra_simps power2_eq_square) then have "real (n - 1) ≤ sqrt (real (n⇧2 - 1))" by (metis Extended_Nonnegative_Real.of_nat_le_iff of_nat_power real_le_rsqrt) then have "n-1 ≤ sqrt(real n ^ 2 - 1)" by (simp add: Suc_leI assms of_nat_diff) then show ?thesis using assms by linarith 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: divide_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, hide_lams) 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: divide_simps) then have "ln ((1 + real n + sqrt ((1 + real n)⇧2 - 1)) / (real n + sqrt ((real n)⇧2 - 1))) ≤ ln 2" apply (subst ln_le_cancel_iff) using Schottky_lemma1 ‹0 < n› by auto (force simp: divide_simps) 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 divide_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) have 1: "∃k. exp (𝗂 * (of_int m * complex_of_real pi) - (ln (real n + sqrt ((real n)⇧2 - 1)))) + inverse (exp (𝗂 * (of_int m * complex_of_real pi) - (ln (real n + sqrt ((real n)⇧2 - 1))))) = of_int k * 2" if "n > 0" for m n proof - have eeq: "e ≠ 0 ⟹ e + inverse e = n*2 ⟷ inverse e^2 - 2 * n*inverse e + 1 = 0" for n e::complex by (auto simp: 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) show ?thesis apply (simp add: eeq) using Schottky_lemma1 [OF that] apply (auto simp: eeq exp_diff exp_Euler exp_of_real algebra_simps sin_int_times_real cos_int_times_real) apply (rule_tac x="int n" in exI) apply (auto simp: power2_eq_square algebra_simps) apply (rule_tac x="- int n" in exI) apply (auto simp: power2_eq_square algebra_simps) done qed have 2: "∃k. exp (𝗂 * (of_int m * complex_of_real pi) + (ln (real n + sqrt ((real n)⇧2 - 1)))) + inverse (exp (𝗂 * (of_int m * complex_of_real pi) + (ln (real n + sqrt ((real n)⇧2 - 1))))) = of_int k * 2" if "n > 0" for m n proof - have eeq: "e ≠ 0 ⟹ e + inverse e = n*2 ⟷ e^2 - 2 * n*e + 1 = 0" for n e::complex by (auto simp: 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) show ?thesis apply (simp add: eeq) using Schottky_lemma1 [OF that] apply (auto simp: exp_add exp_Euler exp_of_real algebra_simps sin_int_times_real cos_int_times_real) apply (rule_tac x="int n" in exI) apply (auto simp: power2_eq_square algebra_simps) apply (rule_tac x="- int n" in exI) apply (auto simp: power2_eq_square algebra_simps) done qed have "∃x. cos (complex_of_real pi * z) = of_int x" using assms apply safe apply (auto simp: Ints_def cos_exp_eq exp_minus Complex_eq) 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 "... ≤ 2 + cmod (f 0) * 3" by simp finally have "1 + norm(2 * f 0 - 1) / 3 ≤ (2 + norm(f 0) - 1) * 3" apply (simp add: divide_simps) using norm_ge_zero [of "2 * f 0 - 1"] by linarith 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 ttt: "⋀z. z ∈ frontier (cball 0 1) ⟹ 1 - t ≤ dist w z" using ‹norm z ≤ t› segment_bound1 [OF ‹w ∈ closed_segment 0 z›] apply (simp add: dist_complex_def) by (metis diff_left_mono dist_commute dist_complex_def norm_triangle_ineq2 order_trans) 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 "∄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) apply (simp_all del: Complex_eq greaterThan_0) by blast 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)) < 1/2" using n apply (simp add: complex_norm cmod_eq_Re complex_diff dist_norm del: Complex_eq) by (metis add.commute add_uminus_conv_diff) 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 ge m ‹0 < n› show ?thesis apply (rule_tac x = "Complex m (- ln (real n + sqrt ((real n)⇧2 - 1)) / pi)" in bexI) apply (simp_all del: Complex_eq greaterThan_0) by blast 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 Topology_Euclidean_Space.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: divide_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› lemma 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 apply (intro holomorphic_intros holomorphic_on_compose holomorphic_on_subset [OF holf]) using Rpos by (auto simp: less_imp_le norm_mult) 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" apply (rule DERIV_imp_deriv) apply (simp add: g_def) by (metis 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 obtain c where "⋀x. f(x) = c" apply (rule DERIV_zero_connected_constant [OF connected_UNIV open_UNIV finite.emptyI contf]) apply (metis True DiffE holf holomorphic_derivI open_UNIV, auto) done 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)" apply (simp add: fw_def) apply (rule DERIV_chain) using holf holomorphic_derivI apply force apply (intro derivative_eq_intros w) apply (auto simp: field_simps) done 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" apply (intro holomorphic_intros holf holomorphic_on_compose [unfolded o_def, OF holf]) using non_fp by auto qed auto then obtain "c ≠ 0" "c ≠ 1" by (metis (no_types, hide_lams) 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)" apply (intro derivative_eq_intros) apply (rule DERIV_chain [unfolded o_def, of f]) apply (auto simp: algebra_simps intro!: holomorphic_derivI [OF holfU]) done 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 "op + 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] apply (simp add: algebra_simps) by (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 apply simp using seq_suble [OF sub_kk] order_trans strict_mono_less_eq [OF sub_rr] by blast 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)" apply (simp add: strict_mono_Suc_iff) by (meson lessI less_le_trans seq_suble strict_monoD sub_kk sub_rr) have "∃j. i ≤ j ∧ rr (n+d) i = rr n j" for d n i apply (induction d arbitrary: i, auto) by (meson order_trans seq_suble sub_kk) 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 ‹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::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: σ M) then show ?thesis using compact_def [of "cball (0::'b) M"] apply simp apply (drule_tac x="(λn. f (r n) (σ i))" in spec) apply (force simp: o_def) done qed show "⋀i r k1 k2 N. ⟦∃l. (λn. (f ∘ (r ∘ k1)) n (σ i)) ⇢ l; ⋀j. N ≤ j ⟹ ∃j'≥j. k2 j = k1 j'⟧ ⟹ ∃l. (λn. (f ∘ (r ∘ k2)) n (σ i)) ⇢ l" apply (simp add: lim_sequentially) apply (erule ex_forward all_forward imp_forward)+ apply auto by (metis (no_types, hide_lams) 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"]) show "∀⇩F n in sequentially. continuous_on S ((ℱ ∘ r) n)" apply (simp add: eventually_sequentially) apply (rule_tac x=0 in exI) using UEQ apply (force simp: continuous_on_iff) done show "uniform_limit S (ℱ ∘ r) g sequentially" apply (simp add: uniform_limit_iff eventually_sequentially) by (metis dist_norm that) 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" apply (rule function_convergent_subsequence [OF ‹countable R› M]) using ‹R ⊆ S› apply force+ done 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 ⊆ (⋃c∈T. ball c d)" proof (rule compactE_image [OF ‹compact S›, of R "(λx. ball x d)"]) have "closure R ⊆ (⋃c∈R. ball c d)" apply clarsimp using ‹0 < d› closure_approachable by blast 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 ‹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 have "∃g. ∀e>0. ∃N. ∀n≥N. ∀x ∈ S. norm(ℱ(k n) x - g x) < e" using uniformly_convergent_eq_cauchy [of "λx. x ∈ S" "ℱ ∘ k"] apply (simp add: o_def dist_norm) by meson ultimately show thesis by (metis that ‹strict_mono k›) qed subsubsection‹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. ∀n≥N. 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::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 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: "∀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 ‹⋀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))" apply (rule *) using that ‹0 < r› by (simp only: dist_norm norm_minus_commute) have z: "((λw. ℱ n w / (w - z)) has_contour_integral (2 * pi) * 𝗂 * ℱ n z) (circlepath z (2 / 3 * r))" apply (rule *) using ‹0 < r› by simp 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: divide_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: divide_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)))" apply (rule mult_mono) apply (rule leM) using ‹r > 0› ‹M > 0› neq by 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 apply (simp add: field_simps mult_less_0_iff norm_minus_commute) done also have "... ≤ e/r" using ‹e > 0› ‹r > 0› r4_le_xy by (simp add: divide_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))" apply (rule has_contour_integral_bound_circlepath [OF has_contour_integral_diff [OF y z], of "e/r"]) using ‹e > 0› ‹r > 0› le_er by auto also have "... = (2 * pi) * e * ((2 / 3))" using ‹r > 0› by (simp add: divide_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 qed (use comK in ‹fastforce+›) then show ?thesis by fastforce qed have "∃k g. strict_mono (k::nat⇒nat) ∧ (∀e > 0. ∃N. ∀n≥N. ∀x ∈ K i. norm((ℱ ∘ r ∘ k) n x - g x) < e)" for i r apply (rule *) using rng_f by auto then have **: "⋀i r. ∃k. strict_mono (k::nat⇒nat) ∧ (∃g. ∀e>0. ∃N. ∀n≥N. ∀x ∈ K i. norm((ℱ ∘ (r ∘ k)) n x - g x) < e)" by (force simp: o_assoc) obtain k :: "nat ⇒ nat" where "strict_mono k" and "⋀i. ∃g. ∀e>0. ∃N. ∀n≥N. ∀x∈K i. cmod ((ℱ ∘ (id ∘ k)) n x - g x) < e" apply (rule subsequence_diagonalization_lemma [OF **, of id]) apply (erule ex_forward all_forward imp_forward)+ apply auto apply (rule_tac x="max N Na" in exI, fastforce+) done then have lt_e: "⋀i. ∃g. ∀e>0. ∃N. ∀n≥N. ∀x∈K i. cmod ((ℱ ∘ k) n x - g x) < e" by simp 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 lt_e by metis obtain N where "⋀n. n ≥ N ⟹ z ∈ K n" using subK [of "{z}"] that ‹z ∈ S› 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 lt_e by blast have geq: "g w = h w" if "w ∈ T" for w apply (rule LIMSEQ_unique [of "λn. ℱ(k n) w"]) using ‹T ⊆ S› g_lim that apply blast using h N that by (force simp: lim_sequentially dist_norm) 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: "⋀c. ∃z ∈ S. g z ≠ c" 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 [of _ z0 r]) show "(λz. deriv (ℱ n) z / ℱ n z) holomorphic_on ball z0 r" apply (intro holomorphic_intros holomorphic_deriv holf holf0 open_ball nz) using ‹ball z0 r ⊆ S› by blast 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)" apply (intro holomorphic_on_imp_continuous_on holomorphic_on_subset [OF hol_dg]) using ‹0 < r› subS by 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)" apply (intro continuous_intros holomorphic_on_imp_continuous_on holomorphic_on_subset [OF holg]) using ‹0 < r› subS by 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" 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: "dist w 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› by (simp_all add: ball_subset_ball_iff cball_subset_ball_iff w) 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 "⋀y. dist w y < r / 4 ⟹ dist z0 y ≤ 3 * r / 4" apply (rule dist_triangle_le [where z=w]) using w by (simp add: dist_commute) 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" apply (rule Cauchy_higher_deriv_bound [OF hol cont in_ball, of 1, simplified]) using ‹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 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. ∀x∈cball z0 (3 * r / 4). dist (ℱ n x) (g x) < r / 4 * e / 2" using ‹0 < e› ‹0 < r› by (force simp: intro!: uniform_limitD) then show "∀⇩F n in sequentially. ∀x ∈ sphere z0 (r/2). dist (deriv (ℱ n) x) (deriv g x) < e" apply (simp add: eventually_sequentially) apply (elim ex_forward all_forward imp_forward asm_rl) using * apply (force simp: dist_commute) done 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" apply (rule uniform_limitD) using ‹0 < e› by force 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) apply (metis Suc_pred mult.commute power_Suc) done then show ?thesis apply (rule DERIV_imp_deriv [OF DERIV_transform_within_open [where s = "ball z0 r"]]) using that ‹m > 0› ‹0 < r› apply (simp_all add: hnz geq) done 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 divide_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))" apply (rule Cauchy_theorem_disc_simple [of _ z0 r]) using hnz holh holomorphic_deriv holomorphic_on_divide ‹0 < r› apply force+ done 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: "⋀c. ∃z ∈ S. g z ≠ c" 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 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 have "∀⇩F n in sequentially. ∀x∈K. dist (ℱ n x - ℱ n z1) (g x - g z1) < e/2 + e/2" apply (rule eventually_mono [OF eventually_conj [OF K z1]]) apply (simp add: dist_norm algebra_simps del: divide_const_simps) by (metis add.commute dist_commute dist_norm dist_triangle_add_half) have "∀⇩F n in sequentially. ∀x∈K. dist (ℱ n x - ℱ n z1) (g x - g z1) < e/2 + e/2" using eventually_conj [OF K z1] apply (rule eventually_mono) by (metis (no_types, hide_lams) diff_add_eq diff_diff_eq2 dist_commute dist_norm dist_triangle_add_half real_sum_of_halves) then show "∀⇩F n in sequentially. ∀x∈K. dist (ℱ n x - ℱ n z1) (g x - g z1) < e" by simp qed show "⋀c. ∃z∈S - {z1}. g z - g z1 ≠ c" 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 with holX have "h holomorphic_on S" by auto then have "h holomorphic_on cball w e" by (metis e holomorphic_on_subset) then have hol_h_o: "(h ∘ (λz. (w + of_real e * z))) holomorphic_on cball 0 1" apply (intro holomorphic_intros holomorphic_on_compose) apply (erule holomorphic_on_subset) using that ‹e > 0› by (auto simp: dist_norm norm_mult) 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: "⋀z::complex. cmod z ≤ 1 ⟹ h (w + e * z) ≠ 0 ∧ h (w + e * z) ≠ 1" apply (rule X01 [OF ‹h ∈ X›]) apply (rule subsetD [OF e]) using ‹0 < e› by (auto simp: dist_norm norm_mult) have "cmod (h z) ≤ cmod (h (w + of_real e * (inverse e * (z - w))))" using ‹0 < e› by (simp add: divide_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" apply (rule GPicard1 [OF S zero_less_one ‹Y ⊆ X› holX]) using no_hw_le1 X01 by force+ 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. ∃h∈Y. r < cmod (h v))" proof assume "∀r>0. ∃h∈Y. r < cmod (h v)" then have "∀n. ∃h∈Y. 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 apply (simp add: 𝒢_def) using FY X01 ‹Y ⊆ X› holX apply (blast intro: holomorphic_on_inverse) done 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. ∀h∈range 𝒢. ∀z∈K. 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 seq_harmonic]) 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 "∃z∈ball v e. h z ≠ c" for c proof - 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 "norm (𝒢 (j n) y) < inverse C" by (simp add: ‹h v = 0›) then have "C < norm (ℱ (j n) y)" apply (simp add: 𝒢_def) by (metis FY X01 ‹0 < C› ‹y ∈ S› ‹Y ⊆ X› inverse_less_iff_less norm_inverse subsetD zero_less_norm_iff) show False using ‹C < cmod (ℱ (j n) y)› le_C not_less by blast qed then show ?thesis 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 show "v ∈ U" apply (clarsimp simp add: U_def v) apply (rule GPicard1[OF ‹open S› ‹connected S› ‹v ∈ S› _ ‹Y ⊆ X› holX]) using X01 no_hw_le1 apply (meson | force simp: not_less)+ done 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 with ‹finite L› show ?thesis apply (rule_tac x = "Max (F ` L)" in exI) apply (simp add: linorder_class.Max_ge_iff) using * F by (metis L UN_E subsetD) 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)" apply (rule holomorphic_on_subset [OF holf]) using ‹ε < k› ‹0 < d› that by auto show "continuous_on (closure (cball 0 ε - ball 0 d)) f" apply (rule holomorphic_on_imp_continuous_on) apply (rule holomorphic_on_subset [OF holf]) using ‹0 < d› ‹ε < k› by auto show "⋀z. z ∈ frontier (cball 0 ε - ball 0 d) ⟹ cmod (f z) ≤ B" apply (simp add: frontier_def) using ε d less_eq_real_def by blast 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 divide_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 apply (rule f01) using * by force 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)}" apply clarsimp apply (intro conjI holomorphic_intros holomorphic_on_compose holh) using h01 apply auto done 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 ∧ (∀z∈sphere 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 apply (rule that [OF ‹0 < ε› ‹ε < 1›]) using ε by auto 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} ∧ (∀z∈ball 0 1 - {0}. g z ≠ 0 ∧ g z ≠ 1)}" apply clarsimp apply (intro conjI holomorphic_intros holomorphic_on_compose_gen [unfolded o_def, OF _ holh] holomorphic_on_compose) using h01 apply auto done 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 ∧ (∀z∈sphere 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: divide_simps) then show ?thesis apply (rule that [OF ‹0 < ε› ‹ε < 1›]) using ε by auto 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}" apply (intro holomorphic_intros holomorphic_on_compose_gen [unfolded o_def, OF _ holf]) using ‹0 < r› ‹a ≠ 0› r by (auto simp: dist_norm norm_mult subset_eq) show "⋀w. w ∈ ball 0 1 - {0} ⟹ f (z + of_real r * w) / a ≠ 0 ∧ f (z + of_real r * w) / a ≠ 1" apply (simp add: divide_simps ‹a ≠ 0›) apply (rule f0a) using ‹0 < r› r by (auto simp: 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 divide_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 divide_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}" apply (rule holomorphic_on_subset [OF holf]) using zrM by auto have holfb_i: "(λz. inverse(f z - a)) holomorphic_on ball z r - {z}" apply (intro holomorphic_intros holfb) using fab zrM by fastforce 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) have "∀⇩F w in at z. cmod (f w - a) ≤ B" apply (simp add: eventually_at) apply (rule_tac x=r in exI) using ‹0 < r› by (auto simp: dist_commute intro!: B) then have "∃B. ∀⇩F w in at z. cmod (f w) ≤ B" apply (rule_tac x="B + norm a" in exI) apply (erule eventually_mono) by (metis add.commute add_le_cancel_right norm_triangle_sub order.trans) 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" apply (simp add: 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)" apply (rule Lim_transform_within_open [of g "g z" z UNIV "ball z r"]) using ‹0 < r› by (auto simp: gf) 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) have "∀⇩F w in at z. cmod (inverse (f w - a)) ≤ B" apply (simp add: eventually_at) apply (rule_tac x=r in exI) using ‹0 < r› by (auto simp: dist_commute intro!: B) 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" apply (simp add: 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" apply (rule tendsto_eq_intros refl gz ‹g z ≠ 0›)+ by (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 divide_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})" apply (simp add: subset_iff image_iff) by (metis great_Picard [OF M _ holf] non) 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 apply (rule_tac r=e in that) using e ‹e > 0› by auto 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 corollary 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