(* Title: HOL/Analysis/Riemann_Mapping.thy
Authors: LC Paulson, based on material from HOL Light
*)
section \<open>Moebius functions, Equivalents of Simply Connected Sets, Riemann Mapping Theorem\<close>
theory Riemann_Mapping
imports Great_Picard
begin
subsection\<open>Moebius functions are biholomorphisms of the unit disc\<close>
definition\<^marker>\<open>tag important\<close> Moebius_function :: "[real,complex,complex] \<Rightarrow> complex" where
"Moebius_function \ \t w z. exp(\ * of_real t) * (z - w) / (1 - cnj w * z)"
lemma Moebius_function_simple:
"Moebius_function 0 w z = (z - w) / (1 - cnj w * z)"
by (simp add: Moebius_function_def)
lemma Moebius_function_eq_zero:
"Moebius_function t w w = 0"
by (simp add: Moebius_function_def)
lemma Moebius_function_of_zero:
"Moebius_function t w 0 = - exp(\ * of_real t) * w"
by (simp add: Moebius_function_def)
lemma Moebius_function_norm_lt_1:
assumes w1: "norm w < 1" and z1: "norm z < 1"
shows "norm (Moebius_function t w z) < 1"
proof -
have "1 - cnj w * z \ 0"
by (metis complex_cnj_cnj complex_mod_sqrt_Re_mult_cnj mult.commute mult_less_cancel_right1 norm_ge_zero norm_mult norm_one order.asym right_minus_eq w1 z1)
then have VV: "1 - w * cnj z \ 0"
by (metis complex_cnj_cnj complex_cnj_mult complex_cnj_one right_minus_eq)
then have "1 - norm (Moebius_function t w z) ^ 2 =
((1 - norm w ^ 2) / (norm (1 - cnj w * z) ^ 2)) * (1 - norm z ^ 2)"
apply (cases w)
apply (cases z)
apply (simp add: Moebius_function_def divide_simps norm_divide norm_mult)
apply (simp add: complex_norm complex_diff complex_mult one_complex.code complex_cnj)
apply (auto simp: algebra_simps power2_eq_square)
done
then have "1 - (cmod (Moebius_function t w z))\<^sup>2 = (1 - cmod (w * w)) / (cmod (1 - cnj w * z))\<^sup>2 * (1 - cmod (z * z))"
by (simp add: norm_mult power2_eq_square)
moreover have "0 < 1 - cmod (z * z)"
by (metis (no_types) z1 diff_gt_0_iff_gt mult.left_neutral norm_mult_less)
ultimately have "0 < 1 - norm (Moebius_function t w z) ^ 2"
using \<open>1 - cnj w * z \<noteq> 0\<close> w1 norm_mult_less by fastforce
then show ?thesis
using linorder_not_less by fastforce
qed
lemma Moebius_function_holomorphic:
assumes "norm w < 1"
shows "Moebius_function t w holomorphic_on ball 0 1"
proof -
have *: "1 - z * w \ 0" if "norm z < 1" for z
proof -
have "norm (1::complex) \ norm (z * w)"
using assms that norm_mult_less by fastforce
then show ?thesis by auto
qed
show ?thesis
apply (simp add: Moebius_function_def)
apply (intro holomorphic_intros)
using assms *
by (metis complex_cnj_cnj complex_cnj_mult complex_cnj_one complex_mod_cnj mem_ball_0 mult.commute right_minus_eq)
qed
lemma Moebius_function_compose:
assumes meq: "-w1 = w2" and "norm w1 < 1" "norm z < 1"
shows "Moebius_function 0 w1 (Moebius_function 0 w2 z) = z"
proof -
have "norm w2 < 1"
using assms by auto
then have "-w1 = z" if "cnj w2 * z = 1"
by (metis assms(3) complex_mod_cnj less_irrefl mult.right_neutral norm_mult_less norm_one that)
moreover have "z=0" if "1 - cnj w2 * z = cnj w1 * (z - w2)"
proof -
have "w2 * cnj w2 = 1"
using that meq by (auto simp: algebra_simps)
then show "z = 0"
by (metis (no_types) \<open>cmod w2 < 1\<close> complex_mod_cnj less_irrefl mult.right_neutral norm_mult_less norm_one)
qed
moreover have "z - w2 - w1 * (1 - cnj w2 * z) = z * (1 - cnj w2 * z - cnj w1 * (z - w2))"
using meq by (fastforce simp: algebra_simps)
ultimately
show ?thesis
by (simp add: Moebius_function_def divide_simps norm_divide norm_mult)
qed
lemma ball_biholomorphism_exists:
assumes "a \ ball 0 1"
obtains f g where "f a = 0"
"f holomorphic_on ball 0 1" "f ` ball 0 1 \ ball 0 1"
"g holomorphic_on ball 0 1" "g ` ball 0 1 \ ball 0 1"
"\z. z \ ball 0 1 \ f (g z) = z"
"\z. z \ ball 0 1 \ g (f z) = z"
proof
show "Moebius_function 0 a holomorphic_on ball 0 1" "Moebius_function 0 (-a) holomorphic_on ball 0 1"
using Moebius_function_holomorphic assms mem_ball_0 by auto
show "Moebius_function 0 a a = 0"
by (simp add: Moebius_function_eq_zero)
show "Moebius_function 0 a ` ball 0 1 \ ball 0 1"
"Moebius_function 0 (- a) ` ball 0 1 \ ball 0 1"
using Moebius_function_norm_lt_1 assms by auto
show "Moebius_function 0 a (Moebius_function 0 (- a) z) = z"
"Moebius_function 0 (- a) (Moebius_function 0 a z) = z" if "z \ ball 0 1" for z
using Moebius_function_compose assms that by auto
qed
subsection\<open>A big chain of equivalents of simple connectedness for an open set\<close>
lemma biholomorphic_to_disc_aux:
assumes "open S" "connected S" "0 \ S" and S01: "S \ ball 0 1"
and prev: "\f. \f holomorphic_on S; \z. z \ S \ f z \ 0; inj_on f S\
\<Longrightarrow> \<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S. f z = (g z)\<^sup>2)"
shows "\f g. f holomorphic_on S \ g holomorphic_on ball 0 1 \
(\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
(\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z)"
proof -
define F where "F \ {h. h holomorphic_on S \ h ` S \ ball 0 1 \ h 0 = 0 \ inj_on h S}"
have idF: "id \ F"
using S01 by (auto simp: F_def)
then have "F \ {}"
by blast
have imF_ne: "((\h. norm(deriv h 0)) ` F) \ {}"
using idF by auto
have holF: "\h. h \ F \ h holomorphic_on S"
by (auto simp: F_def)
obtain f where "f \ F" and normf: "\h. h \ F \ norm(deriv h 0) \ norm(deriv f 0)"
proof -
obtain r where "r > 0" and r: "ball 0 r \ S"
using \<open>open S\<close> \<open>0 \<in> S\<close> openE by auto
have bdd: "bdd_above ((\h. norm(deriv h 0)) ` F)"
proof (intro bdd_aboveI exI ballI, clarify)
show "norm (deriv f 0) \ 1 / r" if "f \ F" for f
proof -
have r01: "(*) (complex_of_real r) ` ball 0 1 \ S"
using that \<open>r > 0\<close> by (auto simp: norm_mult r [THEN subsetD])
then have "f holomorphic_on (*) (complex_of_real r) ` ball 0 1"
using holomorphic_on_subset [OF holF] by (simp add: that)
then have holf: "f \ (\z. (r * z)) holomorphic_on (ball 0 1)"
by (intro holomorphic_intros holomorphic_on_compose)
have f0: "(f \ (*) (complex_of_real r)) 0 = 0"
using F_def that by auto
have "f ` S \ ball 0 1"
using F_def that by blast
with r01 have fr1: "\z. norm z < 1 \ norm ((f \ (*)(of_real r))z) < 1"
by force
have *: "((\w. f (r * w)) has_field_derivative deriv f (r * z) * r) (at z)"
if "z \ ball 0 1" for z::complex
proof (rule DERIV_chain' [where g=f])
show "(f has_field_derivative deriv f (of_real r * z)) (at (of_real r * z))"
apply (rule holomorphic_derivI [OF holF \<open>open S\<close>])
apply (rule \<open>f \<in> F\<close>)
by (meson imageI r01 subset_iff that)
qed simp
have df0: "((\w. f (r * w)) has_field_derivative deriv f 0 * r) (at 0)"
using * [of 0] by simp
have deq: "deriv (\x. f (complex_of_real r * x)) 0 = deriv f 0 * complex_of_real r"
using DERIV_imp_deriv df0 by blast
have "norm (deriv (f \ (*) (complex_of_real r)) 0) \ 1"
by (auto intro: Schwarz_Lemma [OF holf f0 fr1, of 0])
with \<open>r > 0\<close> show ?thesis
by (simp add: deq norm_mult divide_simps o_def)
qed
qed
define l where "l \ SUP h\F. norm (deriv h 0)"
have eql: "norm (deriv f 0) = l" if le: "l \ norm (deriv f 0)" and "f \ F" for f
apply (rule order_antisym [OF _ le])
using \<open>f \<in> F\<close> bdd cSUP_upper by (fastforce simp: l_def)
obtain \<F> where \<F>in: "\<And>n. \<F> n \<in> F" and \<F>lim: "(\<lambda>n. norm (deriv (\<F> n) 0)) \<longlonglongrightarrow> l"
proof -
have "\f. f \ F \ \norm (deriv f 0) - l\ < 1 / (Suc n)" for n
proof -
obtain f where "f \ F" and f: "l < norm (deriv f 0) + 1/(Suc n)"
using cSup_least [OF imF_ne, of "l - 1/(Suc n)"] by (fastforce simp add: l_def)
then have "\norm (deriv f 0) - l\ < 1 / (Suc n)"
by (fastforce simp add: abs_if not_less eql)
with \<open>f \<in> F\<close> show ?thesis
by blast
qed
then obtain \<F> where fF: "\<And>n. (\<F> n) \<in> F"
and fless: "\n. \norm (deriv (\ n) 0) - l\ < 1 / (Suc n)"
by metis
have "(\n. norm (deriv (\ n) 0)) \ l"
proof (rule metric_LIMSEQ_I)
fix e::real
assume "e > 0"
then obtain N::nat where N: "e > 1/(Suc N)"
using nat_approx_posE by blast
show "\N. \n\N. dist (norm (deriv (\ n) 0)) l < e"
proof (intro exI allI impI)
fix n assume "N \ n"
have "dist (norm (deriv (\ n) 0)) l < 1 / (Suc n)"
using fless by (simp add: dist_norm)
also have "... < e"
using N \<open>N \<le> n\<close> inverse_of_nat_le le_less_trans by blast
finally show "dist (norm (deriv (\ n) 0)) l < e" .
qed
qed
with fF show ?thesis
using that by blast
qed
have "\K. \compact K; K \ S\ \ \B. \h\F. \z\K. norm (h z) \ B"
by (rule_tac x=1 in exI) (force simp: F_def)
moreover have "range \ \ F"
using \<open>\<And>n. \<F> n \<in> F\<close> by blast
ultimately obtain f and r :: "nat \ nat"
where holf: "f holomorphic_on S" and r: "strict_mono r"
and limf: "\x. x \ S \ (\n. \ (r n) x) \ f x"
and ulimf: "\K. \compact K; K \ S\ \ uniform_limit K (\ \ r) f sequentially"
using Montel [of S F \<F>, OF \<open>open S\<close> holF] by auto+
have der: "\n x. x \ S \ ((\ \ r) n has_field_derivative ((\n. deriv (\ n)) \ r) n x) (at x)"
using \<open>\<And>n. \<F> n \<in> F\<close> \<open>open S\<close> holF holomorphic_derivI by fastforce
have ulim: "\x. x \ S \ \d>0. cball x d \ S \ uniform_limit (cball x d) (\ \ r) f sequentially"
by (meson ulimf \<open>open S\<close> compact_cball open_contains_cball)
obtain f' :: "complex\complex" where f': "(f has_field_derivative f' 0) (at 0)"
and tof'0: "(\n. ((\n. deriv (\ n)) \ r) n 0) \ f' 0"
using has_complex_derivative_uniform_sequence [OF \<open>open S\<close> der ulim] \<open>0 \<in> S\<close> by metis
then have derf0: "deriv f 0 = f' 0"
by (simp add: DERIV_imp_deriv)
have "f field_differentiable (at 0)"
using field_differentiable_def f' by blast
have "(\x. (norm (deriv (\ (r x)) 0))) \ norm (deriv f 0)"
using isCont_tendsto_compose [OF continuous_norm [OF continuous_ident] tof'0] derf0 by auto
with LIMSEQ_subseq_LIMSEQ [OF \<F>lim r] have no_df0: "norm(deriv f 0) = l"
by (force simp: o_def intro: tendsto_unique)
have nonconstf: "\ f constant_on S"
proof -
have False if "\x. x \ S \ f x = c" for c
proof -
have "deriv f 0 = 0"
by (metis that \<open>open S\<close> \<open>0 \<in> S\<close> DERIV_imp_deriv [OF has_field_derivative_transform_within_open [OF DERIV_const]])
with no_df0 have "l = 0"
by auto
with eql [OF _ idF] show False by auto
qed
then show ?thesis
by (meson constant_on_def)
qed
show ?thesis
proof
show "f \ F"
unfolding F_def
proof (intro CollectI conjI holf)
have "norm(f z) \ 1" if "z \ S" for z
proof (intro Lim_norm_ubound [OF _ limf] always_eventually allI that)
fix n
have "\ (r n) \ F"
by (simp add: \<F>in)
then show "norm (\ (r n) z) \ 1"
using that by (auto simp: F_def)
qed simp
then have fless1: "norm(f z) < 1" if "z \ S" for z
using maximum_modulus_principle [OF holf \<open>open S\<close> \<open>connected S\<close> \<open>open S\<close>] nonconstf that
by fastforce
then show "f ` S \ ball 0 1"
by auto
have "(\n. \ (r n) 0) \ 0"
using \<F>in by (auto simp: F_def)
then show "f 0 = 0"
using tendsto_unique [OF _ limf ] \<open>0 \<in> S\<close> trivial_limit_sequentially by blast
show "inj_on f S"
proof (rule Hurwitz_injective [OF \<open>open S\<close> \<open>connected S\<close> _ holf])
show "\n. (\ \ r) n holomorphic_on S"
by (simp add: \<F>in holF)
show "\K. \compact K; K \ S\ \ uniform_limit K(\ \ r) f sequentially"
by (metis ulimf)
show "\ f constant_on S"
using nonconstf by auto
show "\n. inj_on ((\ \ r) n) S"
using \<F>in by (auto simp: F_def)
qed
qed
show "\h. h \ F \ norm (deriv h 0) \ norm (deriv f 0)"
by (metis eql le_cases no_df0)
qed
qed
have holf: "f holomorphic_on S" and injf: "inj_on f S" and f01: "f ` S \ ball 0 1"
using \<open>f \<in> F\<close> by (auto simp: F_def)
obtain g where holg: "g holomorphic_on (f ` S)"
and derg: "\z. z \ S \ deriv f z * deriv g (f z) = 1"
and gf: "\z. z \ S \ g(f z) = z"
using holomorphic_has_inverse [OF holf \<open>open S\<close> injf] by metis
have "ball 0 1 \ f ` S"
proof
fix a::complex
assume a: "a \ ball 0 1"
have False if "\x. x \ S \ f x \ a"
proof -
obtain h k where "h a = 0"
and holh: "h holomorphic_on ball 0 1" and h01: "h ` ball 0 1 \ ball 0 1"
and holk: "k holomorphic_on ball 0 1" and k01: "k ` ball 0 1 \ ball 0 1"
and hk: "\z. z \ ball 0 1 \ h (k z) = z"
and kh: "\z. z \ ball 0 1 \ k (h z) = z"
using ball_biholomorphism_exists [OF a] by blast
have nf1: "\z. z \ S \ norm(f z) < 1"
using \<open>f \<in> F\<close> by (auto simp: F_def)
have 1: "h \ f holomorphic_on S"
using F_def \<open>f \<in> F\<close> holh holomorphic_on_compose holomorphic_on_subset by blast
have 2: "\z. z \ S \ (h \ f) z \ 0"
by (metis \<open>h a = 0\<close> a comp_eq_dest_lhs nf1 kh mem_ball_0 that)
have 3: "inj_on (h \ f) S"
by (metis (no_types, lifting) F_def \<open>f \<in> F\<close> comp_inj_on inj_on_inverseI injf kh mem_Collect_eq subset_inj_on)
obtain \<psi> where hol\<psi>: "\<psi> holomorphic_on ((h \<circ> f) ` S)"
and \<psi>2: "\<And>z. z \<in> S \<Longrightarrow> \<psi>(h (f z)) ^ 2 = h(f z)"
proof (rule exE [OF prev [OF 1 2 3]], safe)
fix \<theta>
assume hol\<theta>: "\<theta> holomorphic_on S" and \<theta>2: "(\<forall>z\<in>S. (h \<circ> f) z = (\<theta> z)\<^sup>2)"
show thesis
proof
show "(\ \ g \ k) holomorphic_on (h \ f) ` S"
proof (intro holomorphic_on_compose)
show "k holomorphic_on (h \ f) ` S"
apply (rule holomorphic_on_subset [OF holk])
using f01 h01 by force
show "g holomorphic_on k ` (h \ f) ` S"
apply (rule holomorphic_on_subset [OF holg])
by (auto simp: kh nf1)
show "\ holomorphic_on g ` k ` (h \ f) ` S"
apply (rule holomorphic_on_subset [OF hol\<theta>])
by (auto simp: gf kh nf1)
qed
show "((\ \ g \ k) (h (f z)))\<^sup>2 = h (f z)" if "z \ S" for z
proof -
have "f z \ ball 0 1"
by (simp add: nf1 that)
then have "(\ (g (k (h (f z)))))\<^sup>2 = (\ (g (f z)))\<^sup>2"
by (metis kh)
also have "... = h (f z)"
using \<theta>2 gf that by auto
finally show ?thesis
by (simp add: o_def)
qed
qed
qed
have norm\<psi>1: "norm(\<psi> (h (f z))) < 1" if "z \<in> S" for z
proof -
have "norm (\ (h (f z)) ^ 2) < 1"
by (metis (no_types) that DIM_complex \<psi>2 h01 image_subset_iff mem_ball_0 nf1)
then show ?thesis
by (metis le_less_trans mult_less_cancel_left2 norm_ge_zero norm_power not_le power2_eq_square)
qed
then have \<psi>01: "\<psi> (h (f 0)) \<in> ball 0 1"
by (simp add: \<open>0 \<in> S\<close>)
obtain p q where p0: "p (\ (h (f 0))) = 0"
and holp: "p holomorphic_on ball 0 1" and p01: "p ` ball 0 1 \ ball 0 1"
and holq: "q holomorphic_on ball 0 1" and q01: "q ` ball 0 1 \ ball 0 1"
and pq: "\z. z \ ball 0 1 \ p (q z) = z"
and qp: "\z. z \ ball 0 1 \ q (p z) = z"
using ball_biholomorphism_exists [OF \<psi>01] by metis
have "p \ \ \ h \ f \ F"
unfolding F_def
proof (intro CollectI conjI holf)
show "p \ \ \ h \ f holomorphic_on S"
proof (intro holomorphic_on_compose holf)
show "h holomorphic_on f ` S"
apply (rule holomorphic_on_subset [OF holh])
using f01 by force
show "\ holomorphic_on h ` f ` S"
apply (rule holomorphic_on_subset [OF hol\<psi>])
by auto
show "p holomorphic_on \ ` h ` f ` S"
apply (rule holomorphic_on_subset [OF holp])
by (auto simp: norm\<psi>1)
qed
show "(p \ \ \ h \ f) ` S \ ball 0 1"
apply clarsimp
by (meson norm\<psi>1 p01 image_subset_iff mem_ball_0)
show "(p \ \ \ h \ f) 0 = 0"
by (simp add: \<open>p (\<psi> (h (f 0))) = 0\<close>)
show "inj_on (p \ \ \ h \ f) S"
unfolding inj_on_def o_def
by (metis \<psi>2 dist_0_norm gf kh mem_ball nf1 norm\<psi>1 qp)
qed
then have le_norm_df0: "norm (deriv (p \ \ \ h \ f) 0) \ norm (deriv f 0)"
by (rule normf)
have 1: "k \ power2 \ q holomorphic_on ball 0 1"
proof (intro holomorphic_on_compose holq)
show "power2 holomorphic_on q ` ball 0 1"
using holomorphic_on_subset holomorphic_on_power
by (blast intro: holomorphic_on_ident)
show "k holomorphic_on power2 ` q ` ball 0 1"
apply (rule holomorphic_on_subset [OF holk])
using q01 by (auto simp: norm_power abs_square_less_1)
qed
have 2: "(k \ power2 \ q) 0 = 0"
using p0 F_def \<open>f \<in> F\<close> \<psi>01 \<psi>2 \<open>0 \<in> S\<close> kh qp by force
have 3: "norm ((k \ power2 \ q) z) < 1" if "norm z < 1" for z
proof -
have "norm ((power2 \ q) z) < 1"
using that q01 by (force simp: norm_power abs_square_less_1)
with k01 show ?thesis
by fastforce
qed
have False if c: "\z. norm z < 1 \ (k \ power2 \ q) z = c * z" and "norm c = 1" for c
proof -
have "c \ 0" using that by auto
have "norm (p(1/2)) < 1" "norm (p(-1/2)) < 1"
using p01 by force+
then have "(k \ power2 \ q) (p(1/2)) = c * p(1/2)" "(k \ power2 \ q) (p(-1/2)) = c * p(-1/2)"
using c by force+
then have "p (1/2) = p (- (1/2))"
by (auto simp: \<open>c \<noteq> 0\<close> qp o_def)
then have "q (p (1/2)) = q (p (- (1/2)))"
by simp
then have "1/2 = - (1/2::complex)"
by (auto simp: qp)
then show False
by simp
qed
moreover
have False if "norm (deriv (k \ power2 \ q) 0) \ 1" "norm (deriv (k \ power2 \ q) 0) \ 1"
and le: "\\. norm \ < 1 \ norm ((k \ power2 \ q) \) \ norm \"
proof -
have "norm (deriv (k \ power2 \ q) 0) < 1"
using that by simp
moreover have eq: "deriv f 0 = deriv (k \ (\z. z ^ 2) \ q) 0 * deriv (p \ \ \ h \ f) 0"
proof (intro DERIV_imp_deriv has_field_derivative_transform_within_open [OF DERIV_chain])
show "(k \ power2 \ q has_field_derivative deriv (k \ power2 \ q) 0) (at ((p \ \ \ h \ f) 0))"
using "1" holomorphic_derivI p0 by auto
show "(p \ \ \ h \ f has_field_derivative deriv (p \ \ \ h \ f) 0) (at 0)"
using \<open>p \<circ> \<psi> \<circ> h \<circ> f \<in> F\<close> \<open>open S\<close> \<open>0 \<in> S\<close> holF holomorphic_derivI by blast
show "\x. x \ S \ (k \ power2 \ q \ (p \ \ \ h \ f)) x = f x"
using \<psi>2 f01 kh norm\<psi>1 qp by auto
qed (use assms in simp_all)
ultimately have "cmod (deriv (p \ \ \ h \ f) 0) \ 0"
using le_norm_df0
by (metis linorder_not_le mult.commute mult_less_cancel_left2 norm_mult)
moreover have "1 \ norm (deriv f 0)"
using normf [of id] by (simp add: idF)
ultimately show False
by (simp add: eq)
qed
ultimately show ?thesis
using Schwarz_Lemma [OF 1 2 3] norm_one by blast
qed
then show "a \ f ` S"
by blast
qed
then have "f ` S = ball 0 1"
using F_def \<open>f \<in> F\<close> by blast
then show ?thesis
apply (rule_tac x=f in exI)
apply (rule_tac x=g in exI)
using holf holg derg gf by safe force+
qed
locale SC_Chain =
fixes S :: "complex set"
assumes openS: "open S"
begin
lemma winding_number_zero:
assumes "simply_connected S"
shows "connected S \
(\<forall>\<gamma> z. path \<gamma> \<and> path_image \<gamma> \<subseteq> S \<and>
pathfinish \<gamma> = pathstart \<gamma> \<and> z \<notin> S \<longrightarrow> winding_number \<gamma> z = 0)"
using assms
by (auto simp: simply_connected_imp_connected simply_connected_imp_winding_number_zero)
lemma contour_integral_zero:
assumes "valid_path g" "path_image g \ S" "pathfinish g = pathstart g" "f holomorphic_on S"
"\\ z. \path \; path_image \ \ S; pathfinish \ = pathstart \; z \ S\ \ winding_number \ z = 0"
shows "(f has_contour_integral 0) g"
using assms by (meson Cauchy_theorem_global openS valid_path_imp_path)
lemma global_primitive:
assumes "connected S" and holf: "f holomorphic_on S"
and prev: "\\ f. \valid_path \; path_image \ \ S; pathfinish \ = pathstart \; f holomorphic_on S\ \ (f has_contour_integral 0) \"
shows "\h. \z \ S. (h has_field_derivative f z) (at z)"
proof (cases "S = {}")
case True then show ?thesis
by simp
next
case False
then obtain a where "a \ S"
by blast
show ?thesis
proof (intro exI ballI)
fix x assume "x \ S"
then obtain d where "d > 0" and d: "cball x d \ S"
using openS open_contains_cball_eq by blast
let ?g = "\z. (SOME g. polynomial_function g \ path_image g \ S \ pathstart g = a \ pathfinish g = z)"
show "((\z. contour_integral (?g z) f) has_field_derivative f x)
(at x)"
proof (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right, rule Lim_transform)
show "(\y. inverse(norm(y - x)) *\<^sub>R (contour_integral(linepath x y) f - f x * (y - x))) \x\ 0"
proof (clarsimp simp add: Lim_at)
fix e::real assume "e > 0"
moreover have "continuous (at x) f"
using openS \<open>x \<in> S\<close> holf continuous_on_eq_continuous_at holomorphic_on_imp_continuous_on by auto
ultimately obtain d1 where "d1 > 0"
and d1: "\x'. dist x' x < d1 \ dist (f x') (f x) < e/2"
unfolding continuous_at_eps_delta
by (metis less_divide_eq_numeral1(1) mult_zero_left)
obtain d2 where "d2 > 0" and d2: "ball x d2 \ S"
using openS \<open>x \<in> S\<close> open_contains_ball_eq by blast
have "inverse (norm (y - x)) * norm (contour_integral (linepath x y) f - f x * (y - x)) < e"
if "0 < d1" "0 < d2" "y \ x" "dist y x < d1" "dist y x < d2" for y
proof -
have "f contour_integrable_on linepath x y"
proof (rule contour_integrable_continuous_linepath [OF continuous_on_subset])
show "continuous_on S f"
by (simp add: holf holomorphic_on_imp_continuous_on)
have "closed_segment x y \ ball x d2"
by (meson dist_commute_lessI dist_in_closed_segment le_less_trans mem_ball subsetI that(5))
with d2 show "closed_segment x y \ S"
by blast
qed
then obtain z where z: "(f has_contour_integral z) (linepath x y)"
by (force simp: contour_integrable_on_def)
have con: "((\w. f x) has_contour_integral f x * (y - x)) (linepath x y)"
using has_contour_integral_const_linepath [of "f x" y x] by metis
have "norm (z - f x * (y - x)) \ (e/2) * norm (y - x)"
proof (rule has_contour_integral_bound_linepath)
show "((\w. f w - f x) has_contour_integral z - f x * (y - x)) (linepath x y)"
by (rule has_contour_integral_diff [OF z con])
show "\w. w \ closed_segment x y \ norm (f w - f x) \ e/2"
by (metis d1 dist_norm less_le_trans not_less not_less_iff_gr_or_eq segment_bound1 that(4))
qed (use \<open>e > 0\<close> in auto)
with \<open>e > 0\<close> have "inverse (norm (y - x)) * norm (z - f x * (y - x)) \<le> e/2"
by (simp add: field_split_simps)
also have "... < e"
using \<open>e > 0\<close> by simp
finally show ?thesis
by (simp add: contour_integral_unique [OF z])
qed
with \<open>d1 > 0\<close> \<open>d2 > 0\<close>
show "\d>0. \z. z \ x \ dist z x < d \
inverse (norm (z - x)) * norm (contour_integral (linepath x z) f - f x * (z - x)) < e"
by (rule_tac x="min d1 d2" in exI) auto
qed
next
have *: "(1 / norm (y - x)) *\<^sub>R (contour_integral (?g y) f -
(contour_integral (?g x) f + f x * (y - x))) =
(contour_integral (linepath x y) f - f x * (y - x)) /\<^sub>R norm (y - x)"
if "0 < d" "y \ x" and yx: "dist y x < d" for y
proof -
have "y \ S"
by (metis subsetD d dist_commute less_eq_real_def mem_cball yx)
have gxy: "polynomial_function (?g x) \ path_image (?g x) \ S \ pathstart (?g x) = a \ pathfinish (?g x) = x"
"polynomial_function (?g y) \ path_image (?g y) \ S \ pathstart (?g y) = a \ pathfinish (?g y) = y"
using someI_ex [OF connected_open_polynomial_connected [OF openS \<open>connected S\<close> \<open>a \<in> S\<close>]] \<open>x \<in> S\<close> \<open>y \<in> S\<close>
by meson+
then have vp: "valid_path (?g x)" "valid_path (?g y)"
by (simp_all add: valid_path_polynomial_function)
have f0: "(f has_contour_integral 0) ((?g x) +++ linepath x y +++ reversepath (?g y))"
proof (rule prev)
show "valid_path ((?g x) +++ linepath x y +++ reversepath (?g y))"
using gxy vp by (auto simp: valid_path_join)
have "closed_segment x y \ cball x d"
using yx by (auto simp: dist_commute dest!: dist_in_closed_segment)
then have "closed_segment x y \ S"
using d by blast
then show "path_image ((?g x) +++ linepath x y +++ reversepath (?g y)) \ S"
using gxy by (auto simp: path_image_join)
qed (use gxy holf in auto)
then have fintxy: "f contour_integrable_on linepath x y"
by (metis (no_types, lifting) contour_integrable_joinD1 contour_integrable_joinD2 gxy(2) has_contour_integral_integrable pathfinish_linepath pathstart_reversepath valid_path_imp_reverse valid_path_join valid_path_linepath vp(2))
have fintgx: "f contour_integrable_on (?g x)" "f contour_integrable_on (?g y)"
using openS contour_integrable_holomorphic_simple gxy holf vp by blast+
show ?thesis
apply (clarsimp simp add: divide_simps)
using contour_integral_unique [OF f0]
apply (simp add: fintxy gxy contour_integrable_reversepath contour_integral_reversepath fintgx vp)
apply (simp add: algebra_simps)
done
qed
show "(\z. (1 / norm (z - x)) *\<^sub>R
(contour_integral (?g z) f - (contour_integral (?g x) f + f x * (z - x))) -
(contour_integral (linepath x z) f - f x * (z - x)) /\<^sub>R norm (z - x))
\<midarrow>x\<rightarrow> 0"
apply (rule tendsto_eventually)
apply (simp add: eventually_at)
apply (rule_tac x=d in exI)
using \<open>d > 0\<close> * by simp
qed
qed
qed
lemma holomorphic_log:
assumes "connected S" and holf: "f holomorphic_on S" and nz: "\z. z \ S \ f z \ 0"
and prev: "\f. f holomorphic_on S \ \h. \z \ S. (h has_field_derivative f z) (at z)"
shows "\g. g holomorphic_on S \ (\z \ S. f z = exp(g z))"
proof -
have "(\z. deriv f z / f z) holomorphic_on S"
by (simp add: openS holf holomorphic_deriv holomorphic_on_divide nz)
then obtain g where g: "\z. z \ S \ (g has_field_derivative deriv f z / f z) (at z)"
using prev [of "\z. deriv f z / f z"] by metis
have hfd: "\x. x \ S \ ((\z. exp (g z) / f z) has_field_derivative 0) (at x)"
apply (rule derivative_eq_intros g| simp)+
apply (subst DERIV_deriv_iff_field_differentiable)
using openS holf holomorphic_on_imp_differentiable_at nz apply auto
done
obtain c where c: "\x. x \ S \ exp (g x) / f x = c"
proof (rule DERIV_zero_connected_constant[OF \<open>connected S\<close> openS finite.emptyI])
show "continuous_on S (\z. exp (g z) / f z)"
by (metis (full_types) openS g continuous_on_divide continuous_on_exp holf holomorphic_on_imp_continuous_on holomorphic_on_open nz)
then show "\x\S - {}. ((\z. exp (g z) / f z) has_field_derivative 0) (at x)"
using hfd by (blast intro: DERIV_zero_connected_constant [OF \<open>connected S\<close> openS finite.emptyI, of "\<lambda>z. exp(g z) / f z"])
qed auto
show ?thesis
proof (intro exI ballI conjI)
show "(\z. Ln(inverse c) + g z) holomorphic_on S"
apply (intro holomorphic_intros)
using openS g holomorphic_on_open by blast
fix z :: complex
assume "z \ S"
then have "exp (g z) / c = f z"
by (metis c divide_divide_eq_right exp_not_eq_zero nonzero_mult_div_cancel_left)
moreover have "1 / c \ 0"
using \<open>z \<in> S\<close> c nz by fastforce
ultimately show "f z = exp (Ln (inverse c) + g z)"
by (simp add: exp_add inverse_eq_divide)
qed
qed
lemma holomorphic_sqrt:
assumes holf: "f holomorphic_on S" and nz: "\z. z \ S \ f z \ 0"
and prev: "\f. \f holomorphic_on S; \z \ S. f z \ 0\ \ \g. g holomorphic_on S \ (\z \ S. f z = exp(g z))"
shows "\g. g holomorphic_on S \ (\z \ S. f z = (g z)\<^sup>2)"
proof -
obtain g where holg: "g holomorphic_on S" and g: "\z. z \ S \ f z = exp (g z)"
using prev [of f] holf nz by metis
show ?thesis
proof (intro exI ballI conjI)
show "(\z. exp(g z/2)) holomorphic_on S"
by (intro holomorphic_intros) (auto simp: holg)
show "\z. z \ S \ f z = (exp (g z/2))\<^sup>2"
by (metis (no_types) g exp_double nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral)
qed
qed
lemma biholomorphic_to_disc:
assumes "connected S" and S: "S \ {}" "S \ UNIV"
and prev: "\f. \f holomorphic_on S; \z \ S. f z \ 0\ \ \g. g holomorphic_on S \ (\z \ S. f z = (g z)\<^sup>2)"
shows "\f g. f holomorphic_on S \ g holomorphic_on ball 0 1 \
(\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
(\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z)"
proof -
obtain a b where "a \ S" "b \ S"
using S by blast
then obtain \<delta> where "\<delta> > 0" and \<delta>: "ball a \<delta> \<subseteq> S"
using openS openE by blast
obtain g where holg: "g holomorphic_on S" and eqg: "\z. z \ S \ z - b = (g z)\<^sup>2"
proof (rule exE [OF prev [of "\z. z - b"]])
show "(\z. z - b) holomorphic_on S"
by (intro holomorphic_intros)
qed (use \<open>b \<notin> S\<close> in auto)
have "\ g constant_on S"
proof -
have "(a + \/2) \ ball a \" "a + (\/2) \ a"
using \<open>\<delta> > 0\<close> by (simp_all add: dist_norm)
then show ?thesis
unfolding constant_on_def
using eqg [of a] eqg [of "a + \/2"] \a \ S\ \
by (metis diff_add_cancel subset_eq)
qed
then have "open (g ` ball a \)"
using open_mapping_thm [of g S "ball a \", OF holg openS \connected S\] \ by blast
then obtain r where "r > 0" and r: "ball (g a) r \ (g ` ball a \)"
by (metis \<open>0 < \<delta>\<close> centre_in_ball imageI openE)
have g_not_r: "g z \ ball (-(g a)) r" if "z \ S" for z
proof
assume "g z \ ball (-(g a)) r"
then have "- g z \ ball (g a) r"
by (metis add.inverse_inverse dist_minus mem_ball)
with r have "- g z \ (g ` ball a \)"
by blast
then obtain w where w: "- g z = g w" "dist a w < \"
by auto
then have "w \ ball a \"
by simp
then have "w \ S"
using \<delta> by blast
then have "w = z"
by (metis diff_add_cancel eqg power_minus_Bit0 that w(1))
then have "g z = 0"
using \<open>- g z = g w\<close> by auto
with eqg [OF that] have "z = b"
by auto
with that \<open>b \<notin> S\<close> show False
by simp
qed
then have nz: "\z. z \ S \ g z + g a \ 0"
by (metis \<open>0 < r\<close> add.commute add_diff_cancel_left' centre_in_ball diff_0)
let ?f = "\z. (r/3) / (g z + g a) - (r/3) / (g a + g a)"
obtain h where holh: "h holomorphic_on S" and "h a = 0" and h01: "h ` S \ ball 0 1" and "inj_on h S"
proof
show "?f holomorphic_on S"
by (intro holomorphic_intros holg nz)
have 3: "\norm x \ 1/3; norm y \ 1/3\ \ norm(x - y) < 1" for x y::complex
using norm_triangle_ineq4 [of x y] by simp
have "norm ((r/3) / (g z + g a) - (r/3) / (g a + g a)) < 1" if "z \ S" for z
apply (rule 3)
unfolding norm_divide
using \<open>r > 0\<close> g_not_r [OF \<open>z \<in> S\<close>] g_not_r [OF \<open>a \<in> S\<close>]
by (simp_all add: field_split_simps dist_commute dist_norm)
then show "?f ` S \ ball 0 1"
by auto
show "inj_on ?f S"
using \<open>r > 0\<close> eqg apply (clarsimp simp: inj_on_def)
by (metis diff_add_cancel)
qed auto
obtain k where holk: "k holomorphic_on (h ` S)"
and derk: "\z. z \ S \ deriv h z * deriv k (h z) = 1"
and kh: "\z. z \ S \ k(h z) = z"
using holomorphic_has_inverse [OF holh openS \<open>inj_on h S\<close>] by metis
have 1: "open (h ` S)"
by (simp add: \<open>inj_on h S\<close> holh openS open_mapping_thm3)
have 2: "connected (h ` S)"
by (simp add: connected_continuous_image \<open>connected S\<close> holh holomorphic_on_imp_continuous_on)
have 3: "0 \ h ` S"
using \<open>a \<in> S\<close> \<open>h a = 0\<close> by auto
have 4: "\g. g holomorphic_on h ` S \ (\z\h ` S. f z = (g z)\<^sup>2)"
if holf: "f holomorphic_on h ` S" and nz: "\z. z \ h ` S \ f z \ 0" "inj_on f (h ` S)" for f
proof -
obtain g where holg: "g holomorphic_on S" and eqg: "\z. z \ S \ (f \ h) z = (g z)\<^sup>2"
proof -
have "f \ h holomorphic_on S"
by (simp add: holh holomorphic_on_compose holf)
moreover have "\z\S. (f \ h) z \ 0"
by (simp add: nz)
ultimately show thesis
using prev that by blast
qed
show ?thesis
proof (intro exI conjI)
show "g \ k holomorphic_on h ` S"
proof -
have "k ` h ` S \ S"
by (simp add: \<open>\<And>z. z \<in> S \<Longrightarrow> k (h z) = z\<close> image_subset_iff)
then show ?thesis
by (meson holg holk holomorphic_on_compose holomorphic_on_subset)
qed
show "\z\h ` S. f z = ((g \ k) z)\<^sup>2"
using eqg kh by auto
qed
qed
obtain f g where f: "f holomorphic_on h ` S" and g: "g holomorphic_on ball 0 1"
and gf: "\z\h ` S. f z \ ball 0 1 \ g (f z) = z" and fg:"\z\ball 0 1. g z \ h ` S \ f (g z) = z"
using biholomorphic_to_disc_aux [OF 1 2 3 h01 4] by blast
show ?thesis
proof (intro exI conjI)
show "f \ h holomorphic_on S"
by (simp add: f holh holomorphic_on_compose)
show "k \ g holomorphic_on ball 0 1"
by (metis holomorphic_on_subset image_subset_iff fg holk g holomorphic_on_compose)
qed (use fg gf kh in auto)
qed
lemma homeomorphic_to_disc:
assumes S: "S \ {}"
and prev: "S = UNIV \
(\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
(\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
(\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z))" (is "_ \<or> ?P")
shows "S homeomorphic ball (0::complex) 1"
using prev
proof
assume "S = UNIV" then show ?thesis
using homeomorphic_ball01_UNIV homeomorphic_sym by blast
next
assume ?P
then show ?thesis
unfolding homeomorphic_minimal
using holomorphic_on_imp_continuous_on by blast
qed
lemma homeomorphic_to_disc_imp_simply_connected:
assumes "S = {} \ S homeomorphic ball (0::complex) 1"
shows "simply_connected S"
using assms homeomorphic_simply_connected_eq convex_imp_simply_connected by auto
end
proposition
assumes "open S"
shows simply_connected_eq_winding_number_zero:
"simply_connected S \
connected S \<and>
(\<forall>g z. path g \<and> path_image g \<subseteq> S \<and>
pathfinish g = pathstart g \<and> (z \<notin> S)
\<longrightarrow> winding_number g z = 0)" (is "?wn0")
and simply_connected_eq_contour_integral_zero:
"simply_connected S \
connected S \<and>
(\<forall>g f. valid_path g \<and> path_image g \<subseteq> S \<and>
pathfinish g = pathstart g \<and> f holomorphic_on S
\<longrightarrow> (f has_contour_integral 0) g)" (is "?ci0")
and simply_connected_eq_global_primitive:
"simply_connected S \
connected S \<and>
(\<forall>f. f holomorphic_on S \<longrightarrow>
(\<exists>h. \<forall>z. z \<in> S \<longrightarrow> (h has_field_derivative f z) (at z)))" (is "?gp")
and simply_connected_eq_holomorphic_log:
"simply_connected S \
connected S \<and>
(\<forall>f. f holomorphic_on S \<and> (\<forall>z \<in> S. f z \<noteq> 0)
\<longrightarrow> (\<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S. f z = exp(g z))))" (is "?log")
and simply_connected_eq_holomorphic_sqrt:
"simply_connected S \
connected S \<and>
(\<forall>f. f holomorphic_on S \<and> (\<forall>z \<in> S. f z \<noteq> 0)
\<longrightarrow> (\<exists>g. g holomorphic_on S \<and> (\<forall>z \<in> S. f z = (g z)\<^sup>2)))" (is "?sqrt")
and simply_connected_eq_biholomorphic_to_disc:
"simply_connected S \
S = {} \<or> S = UNIV \<or>
(\<exists>f g. f holomorphic_on S \<and> g holomorphic_on ball 0 1 \<and>
(\<forall>z \<in> S. f z \<in> ball 0 1 \<and> g(f z) = z) \<and>
(\<forall>z \<in> ball 0 1. g z \<in> S \<and> f(g z) = z))" (is "?bih")
and simply_connected_eq_homeomorphic_to_disc:
"simply_connected S \ S = {} \ S homeomorphic ball (0::complex) 1" (is "?disc")
proof -
interpret SC_Chain
using assms by (simp add: SC_Chain_def)
have "?wn0 \ ?ci0 \ ?gp \ ?log \ ?sqrt \ ?bih \ ?disc"
proof -
have *: "\\ \ \; \ \ \; \ \ \; \ \ \; \ \ \; \ \ \; \ \ \; \ \ \\
\<Longrightarrow> (\<alpha> \<longleftrightarrow> \<beta>) \<and> (\<alpha> \<longleftrightarrow> \<gamma>) \<and> (\<alpha> \<longleftrightarrow> \<delta>) \<and> (\<alpha> \<longleftrightarrow> \<zeta>) \<and>
(\<alpha> \<longleftrightarrow> \<eta>) \<and> (\<alpha> \<longleftrightarrow> \<theta>) \<and> (\<alpha> \<longleftrightarrow> \<xi>)" for \<alpha> \<beta> \<gamma> \<delta> \<zeta> \<eta> \<theta> \<xi>
by blast
show ?thesis
apply (rule *)
using winding_number_zero apply metis
using contour_integral_zero apply metis
using global_primitive apply metis
using holomorphic_log apply metis
using holomorphic_sqrt apply simp
using biholomorphic_to_disc apply blast
using homeomorphic_to_disc apply blast
using homeomorphic_to_disc_imp_simply_connected apply blast
done
qed
then show ?wn0 ?ci0 ?gp ?log ?sqrt ?bih ?disc
by safe
qed
corollary contractible_eq_simply_connected_2d:
fixes S :: "complex set"
shows "open S \ (contractible S \ simply_connected S)"
apply safe
apply (simp add: contractible_imp_simply_connected)
using convex_imp_contractible homeomorphic_contractible_eq simply_connected_eq_homeomorphic_to_disc by auto
subsection\<open>A further chain of equivalences about components of the complement of a simply connected set\<close>
text\<open>(following 1.35 in Burckel'S book)\<close>
context SC_Chain
begin
lemma frontier_properties:
assumes "simply_connected S"
shows "if bounded S then connected(frontier S)
else \<forall>C \<in> components(frontier S). \<not> bounded C"
proof -
have "S = {} \ S homeomorphic ball (0::complex) 1"
using simply_connected_eq_homeomorphic_to_disc assms openS by blast
then show ?thesis
proof
assume "S = {}"
then have "bounded S"
by simp
with \<open>S = {}\<close> show ?thesis
by simp
next
assume S01: "S homeomorphic ball (0::complex) 1"
then obtain g f
where gim: "g ` S = ball 0 1" and fg: "\x. x \ S \ f(g x) = x"
and fim: "f ` ball 0 1 = S" and gf: "\y. cmod y < 1 \ g(f y) = y"
and contg: "continuous_on S g" and contf: "continuous_on (ball 0 1) f"
by (fastforce simp: homeomorphism_def homeomorphic_def)
define D where "D \ \n. ball (0::complex) (1 - 1/(of_nat n + 2))"
define A where "A \ \n. {z::complex. 1 - 1/(of_nat n + 2) < norm z \ norm z < 1}"
define X where "X \ \n::nat. closure(f ` A n)"
have D01: "D n \ ball 0 1" for n
by (simp add: D_def ball_subset_ball_iff)
have A01: "A n \ ball 0 1" for n
by (auto simp: A_def)
have cloX: "closed(X n)" for n
by (simp add: X_def)
have Xsubclo: "X n \ closure S" for n
unfolding X_def by (metis A01 closure_mono fim image_mono)
have connX: "connected(X n)" for n
unfolding X_def
apply (rule connected_imp_connected_closure)
apply (rule connected_continuous_image)
apply (simp add: continuous_on_subset [OF contf A01])
using connected_annulus [of _ "0::complex"] by (simp add: A_def)
have nestX: "X n \ X m" if "m \ n" for m n
proof -
have "1 - 1 / (real m + 2) \ 1 - 1 / (real n + 2)"
using that by (auto simp: field_simps)
then show ?thesis
by (auto simp: X_def A_def intro!: closure_mono)
qed
have "closure S - S \ (\n. X n)"
proof
fix x
assume "x \ closure S - S"
then have "x \ closure S" "x \ S" by auto
show "x \ (\n. X n)"
proof
fix n
have "ball 0 1 = closure (D n) \ A n"
by (auto simp: D_def A_def le_less_trans)
with fim have Seq: "S = f ` (closure (D n)) \ f ` (A n)"
by (simp add: image_Un)
have "continuous_on (closure (D n)) f"
by (simp add: D_def cball_subset_ball_iff continuous_on_subset [OF contf])
moreover have "compact (closure (D n))"
by (simp add: D_def)
ultimately have clo_fim: "closed (f ` closure (D n))"
using compact_continuous_image compact_imp_closed by blast
have *: "(f ` cball 0 (1 - 1 / (real n + 2))) \ S"
by (force simp: D_def Seq)
show "x \ X n"
using \<open>x \<in> closure S\<close> unfolding X_def Seq
using \<open>x \<notin> S\<close> * D_def clo_fim by auto
qed
qed
moreover have "(\n. X n) \ closure S - S"
proof -
have "(\n. X n) \ closure S"
proof -
have "(\n. X n) \ X 0"
by blast
also have "... \ closure S"
apply (simp add: X_def fim [symmetric])
apply (rule closure_mono)
by (auto simp: A_def)
finally show "(\n. X n) \ closure S" .
qed
moreover have "(\n. X n) \ S \ {}"
proof (clarify, clarsimp simp: X_def fim [symmetric])
fix x assume x [rule_format]: "\n. f x \ closure (f ` A n)" and "cmod x < 1"
then obtain n where n: "1 / (1 - norm x) < of_nat n"
using reals_Archimedean2 by blast
with \<open>cmod x < 1\<close> gr0I have XX: "1 / of_nat n < 1 - norm x" and "n > 0"
by (fastforce simp: field_split_simps algebra_simps)+
have "f x \ f ` (D n)"
using n \<open>cmod x < 1\<close> by (auto simp: field_split_simps algebra_simps D_def)
moreover have " f ` D n \ closure (f ` A n) = {}"
proof -
have op_fDn: "open(f ` (D n))"
proof (rule invariance_of_domain)
show "continuous_on (D n) f"
by (rule continuous_on_subset [OF contf D01])
show "open (D n)"
by (simp add: D_def)
show "inj_on f (D n)"
unfolding inj_on_def using D01 by (metis gf mem_ball_0 subsetCE)
qed
have injf: "inj_on f (ball 0 1)"
by (metis mem_ball_0 inj_on_def gf)
have "D n \ A n \ ball 0 1"
using D01 A01 by simp
moreover have "D n \ A n = {}"
by (auto simp: D_def A_def)
ultimately have "f ` D n \ f ` A n = {}"
by (metis A01 D01 image_is_empty inj_on_image_Int injf)
then show ?thesis
by (simp add: open_Int_closure_eq_empty [OF op_fDn])
qed
ultimately show False
using x [of n] by blast
qed
ultimately
show "(\n. X n) \ closure S - S"
using closure_subset disjoint_iff_not_equal by blast
qed
ultimately have "closure S - S = (\n. X n)" by blast
then have frontierS: "frontier S = (\n. X n)"
by (simp add: frontier_def openS interior_open)
show ?thesis
proof (cases "bounded S")
case True
have bouX: "bounded (X n)" for n
apply (simp add: X_def)
apply (rule bounded_closure)
by (metis A01 fim image_mono bounded_subset [OF True])
have compaX: "compact (X n)" for n
apply (simp add: compact_eq_bounded_closed bouX)
apply (auto simp: X_def)
done
have "connected (\n. X n)"
by (metis nestX compaX connX connected_nest)
then show ?thesis
by (simp add: True \<open>frontier S = (\<Inter>n. X n)\<close>)
next
case False
have unboundedX: "\ bounded(X n)" for n
proof
assume bXn: "bounded(X n)"
have "continuous_on (cball 0 (1 - 1 / (2 + real n))) f"
by (simp add: cball_subset_ball_iff continuous_on_subset [OF contf])
then have "bounded (f ` cball 0 (1 - 1 / (2 + real n)))"
by (simp add: compact_imp_bounded [OF compact_continuous_image])
moreover have "bounded (f ` A n)"
by (auto simp: X_def closure_subset image_subset_iff bounded_subset [OF bXn])
ultimately have "bounded (f ` (cball 0 (1 - 1/(2 + real n)) \ A n))"
by (simp add: image_Un)
then have "bounded (f ` ball 0 1)"
apply (rule bounded_subset)
apply (auto simp: A_def algebra_simps)
done
then show False
using False by (simp add: fim [symmetric])
qed
have clo_INTX: "closed(\(range X))"
by (metis cloX closed_INT)
then have lcX: "locally compact (\(range X))"
by (metis closed_imp_locally_compact)
have False if C: "C \ components (frontier S)" and boC: "bounded C" for C
proof -
have "closed C"
by (metis C closed_components frontier_closed)
then have "compact C"
by (metis boC compact_eq_bounded_closed)
have Cco: "C \ components (\(range X))"
by (metis frontierS C)
obtain K where "C \ K" "compact K"
and Ksub: "K \ \(range X)" and clo: "closed(\(range X) - K)"
proof (cases "{k. C \ k \ compact k \ openin (top_of_set (\(range X))) k} = {}")
case True
then show ?thesis
using Sura_Bura [OF lcX Cco \<open>compact C\<close>] boC
by (simp add: True)
next
case False
then obtain L where "compact L" "C \ L" and K: "openin (top_of_set (\x. X x)) L"
by blast
show ?thesis
proof
show "L \ \(range X)"
by (metis K openin_imp_subset)
show "closed (\(range X) - L)"
by (metis closedin_diff closedin_self closedin_closed_trans [OF _ clo_INTX] K)
qed (use \<open>compact L\<close> \<open>C \<subseteq> L\<close> in auto)
qed
obtain U V where "open U" and "compact (closure U)" and "open V" "K \ U"
and V: "\(range X) - K \ V" and "U \ V = {}"
using separation_normal_compact [OF \<open>compact K\<close> clo] by blast
then have "U \ (\ (range X) - K) = {}"
by blast
have "(closure U - U) \ (\n. X n \ closure U) \ {}"
proof (rule compact_imp_fip)
show "compact (closure U - U)"
by (metis \<open>compact (closure U)\<close> \<open>open U\<close> compact_diff)
show "\T. T \ range (\n. X n \ closure U) \ closed T"
by clarify (metis cloX closed_Int closed_closure)
show "(closure U - U) \ \\ \ {}"
if "finite \" and \: "\ \ range (\n. X n \ closure U)" for \
proof
assume empty: "(closure U - U) \ \\ = {}"
obtain J where "finite J" and J: "\ = (\n. X n \ closure U) ` J"
using finite_subset_image [OF \<open>finite \<F>\<close> \<F>] by auto
show False
proof (cases "J = {}")
case True
with J empty have "closed U"
by (simp add: closure_subset_eq)
have "C \ {}"
using C in_components_nonempty by blast
then have "U \ {}"
using \<open>K \<subseteq> U\<close> \<open>C \<subseteq> K\<close> by blast
moreover have "U \ UNIV"
using \<open>compact (closure U)\<close> by auto
ultimately show False
using \<open>open U\<close> \<open>closed U\<close> clopen by blast
next
case False
define j where "j \ Max J"
have "j \ J"
by (simp add: False \<open>finite J\<close> j_def)
have jmax: "\m. m \ J \ m \ j"
by (simp add: j_def \<open>finite J\<close>)
have "\ ((\n. X n \ closure U) ` J) = X j \ closure U"
using False jmax nestX \<open>j \<in> J\<close> by auto
then have "X j \ closure U = X j \ U"
apply safe
using DiffI J empty apply auto[1]
using closure_subset by blast
then have "openin (top_of_set (X j)) (X j \ closure U)"
by (simp add: openin_open_Int \<open>open U\<close>)
moreover have "closedin (top_of_set (X j)) (X j \ closure U)"
by (simp add: closedin_closed_Int)
moreover have "X j \ closure U \ X j"
by (metis unboundedX \<open>compact (closure U)\<close> bounded_subset compact_eq_bounded_closed inf.order_iff)
moreover have "X j \ closure U \ {}"
proof -
have "C \ {}"
using C in_components_nonempty by blast
moreover have "C \ X j \ closure U"
using \<open>C \<subseteq> K\<close> \<open>K \<subseteq> U\<close> Ksub closure_subset by blast
ultimately show ?thesis by blast
qed
ultimately show False
using connX [of j] by (force simp: connected_clopen)
qed
qed
qed
moreover have "(\n. X n \ closure U) = (\n. X n) \ closure U"
by blast
moreover have "x \ U" if "\n. x \ X n" "x \ closure U" for x
proof -
have "x \ V"
using \<open>U \<inter> V = {}\<close> \<open>open V\<close> closure_iff_nhds_not_empty that(2) by blast
then show ?thesis
by (metis (no_types) Diff_iff INT_I V \<open>K \<subseteq> U\<close> contra_subsetD that(1))
qed
ultimately show False
by (auto simp: open_Int_closure_eq_empty [OF \<open>open V\<close>, of U])
qed
then show ?thesis
by (auto simp: False)
qed
qed
qed
lemma unbounded_complement_components:
assumes C: "C \ components (- S)" and S: "connected S"
and prev: "if bounded S then connected(frontier S)
else \<forall>C \<in> components(frontier S). \<not> bounded C"
shows "\ bounded C"
proof (cases "bounded S")
case True
with prev have "S \ UNIV" and confr: "connected(frontier S)"
by auto
obtain w where C_ccsw: "C = connected_component_set (- S) w" and "w \ S"
using C by (auto simp: components_def)
show ?thesis
proof (cases "S = {}")
case True with C show ?thesis by auto
next
case False
show ?thesis
proof
assume "bounded C"
then have "outside C \ {}"
using outside_bounded_nonempty by metis
then obtain z where z: "\ bounded (connected_component_set (- C) z)" and "z \ C"
by (auto simp: outside_def)
have clo_ccs: "closed (connected_component_set (- S) x)" for x
by (simp add: closed_Compl closed_connected_component openS)
have "connected_component_set (- S) w = connected_component_set (- S) z"
proof (rule joinable_connected_component_eq [OF confr])
show "frontier S \ - S"
using openS by (auto simp: frontier_def interior_open)
have False if "connected_component_set (- S) w \ frontier (- S) = {}"
proof -
have "C \ frontier S = {}"
using that by (simp add: C_ccsw)
then show False
by (metis C_ccsw ComplI Compl_eq_Compl_iff Diff_subset False \<open>w \<notin> S\<close> clo_ccs closure_closed compl_bot_eq connected_component_eq_UNIV connected_component_eq_empty empty_subsetI frontier_complement frontier_def frontier_not_empty frontier_of_connected_component_subset le_inf_iff subset_antisym)
qed
then show "connected_component_set (- S) w \ frontier S \ {}"
by auto
have *: "\frontier C \ C; frontier C \ F; frontier C \ {}\ \ C \ F \ {}" for C F::"complex set"
by blast
have "connected_component_set (- S) z \ frontier (- S) \ {}"
proof (rule *)
show "frontier (connected_component_set (- S) z) \ connected_component_set (- S) z"
by (auto simp: closed_Compl closed_connected_component frontier_def openS)
show "frontier (connected_component_set (- S) z) \ frontier (- S)"
using frontier_of_connected_component_subset by fastforce
have "\ bounded (-S)"
by (simp add: True cobounded_imp_unbounded)
then have "connected_component_set (- S) z \ {}"
apply (simp only: connected_component_eq_empty)
using confr openS \<open>bounded C\<close> \<open>w \<notin> S\<close>
apply (simp add: frontier_def interior_open C_ccsw)
by (metis ComplI Compl_eq_Diff_UNIV connected_UNIV closed_closure closure_subset connected_component_eq_self
connected_diff_open_from_closed subset_UNIV)
then show "frontier (connected_component_set (- S) z) \ {}"
apply (simp add: frontier_eq_empty connected_component_eq_UNIV)
apply (metis False compl_top_eq double_compl)
done
qed
then show "connected_component_set (- S) z \ frontier S \ {}"
by auto
qed
then show False
by (metis C_ccsw Compl_iff \<open>w \<notin> S\<close> \<open>z \<notin> C\<close> connected_component_eq_empty connected_component_idemp)
qed
qed
next
case False
obtain w where C_ccsw: "C = connected_component_set (- S) w" and "w \ S"
using C by (auto simp: components_def)
have "frontier (connected_component_set (- S) w) \ connected_component_set (- S) w"
by (simp add: closed_Compl closed_connected_component frontier_subset_eq openS)
moreover have "frontier (connected_component_set (- S) w) \ frontier S"
using frontier_complement frontier_of_connected_component_subset by blast
moreover have "frontier (connected_component_set (- S) w) \ {}"
by (metis C C_ccsw False bounded_empty compl_top_eq connected_component_eq_UNIV double_compl frontier_not_empty in_components_nonempty)
ultimately obtain z where zin: "z \ frontier S" and z: "z \ connected_component_set (- S) w"
by blast
have *: "connected_component_set (frontier S) z \ components(frontier S)"
by (simp add: \<open>z \<in> frontier S\<close> componentsI)
with prev False have "\ bounded (connected_component_set (frontier S) z)"
by simp
moreover have "connected_component (- S) w = connected_component (- S) z"
using connected_component_eq [OF z] by force
ultimately show ?thesis
by (metis C_ccsw * zin bounded_subset closed_Compl closure_closed connected_component_maximal
connected_component_refl connected_connected_component frontier_closures in_components_subset le_inf_iff mem_Collect_eq openS)
qed
lemma empty_inside:
assumes "connected S" "\C. C \ components (- S) \ \ bounded C"
shows "inside S = {}"
using assms by (auto simp: components_def inside_def)
lemma empty_inside_imp_simply_connected:
"\connected S; inside S = {}\ \ simply_connected S"
by (metis ComplI inside_Un_outside openS outside_mono simply_connected_eq_winding_number_zero subsetCE sup_bot.left_neutral winding_number_zero_in_outside)
end
proposition
fixes S :: "complex set"
assumes "open S"
shows simply_connected_eq_frontier_properties:
"simply_connected S \
connected S \<and>
(if bounded S then connected(frontier S)
else (\<forall>C \<in> components(frontier S). \<not>bounded C))" (is "?fp")
and simply_connected_eq_unbounded_complement_components:
"simply_connected S \
connected S \<and> (\<forall>C \<in> components(- S). \<not>bounded C)" (is "?ucc")
and simply_connected_eq_empty_inside:
"simply_connected S \
connected S \<and> inside S = {}" (is "?ei")
proof -
interpret SC_Chain
using assms by (simp add: SC_Chain_def)
have "?fp \ ?ucc \ ?ei"
proof -
have *: "\\ \ \; \ \ \; \ \ \; \ \ \\
\<Longrightarrow> (\<alpha> \<longleftrightarrow> \<beta>) \<and> (\<alpha> \<longleftrightarrow> \<gamma>) \<and> (\<alpha> \<longleftrightarrow> \<delta>)" for \<alpha> \<beta> \<gamma> \<delta>
by blast
show ?thesis
apply (rule *)
using frontier_properties simply_connected_imp_connected apply blast
apply clarify
using unbounded_complement_components simply_connected_imp_connected apply blast
using empty_inside apply blast
using empty_inside_imp_simply_connected apply blast
done
qed
then show ?fp ?ucc ?ei
by safe
qed
lemma simply_connected_iff_simple:
fixes S :: "complex set"
assumes "open S" "bounded S"
shows "simply_connected S \ connected S \ connected(- S)"
apply (simp add: simply_connected_eq_unbounded_complement_components assms, safe)
apply (metis DIM_complex assms(2) cobounded_has_bounded_component double_compl order_refl)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.66 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
