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_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 \<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, hide_lams) 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, 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)"
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, hide_lams) 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, hide_lams) 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, hide_lams) 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"
apply (rule isolated_zeros [of "\z. g z - g z1" S z2 z0])
using S \<open>z0 \<in> S\<close> 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 (simp add: ul_g 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 (rule eventually_mono [OF eventually_conj [OF K z1]])
by (metis (no_types, hide_lams) 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
--> --------------------
¤ Dauer der Verarbeitung: 0.119 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
