Theory Riemann_Mapping
section ‹Moebius functions, Equivalents of Simply Connected Sets, Riemann Mapping Theorem›
theory Riemann_Mapping
imports Great_Picard
begin
subsection‹Moebius functions are biholomorphisms of the unit disc›
definition Moebius_function :: "[real,complex,complex] ⇒ 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))⇧2 = (1 - cmod (w * w)) / (cmod (1 - cnj w * z))⇧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 ‹1 - cnj w * z ≠ 0› 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
unfolding Moebius_function_def
apply (intro holomorphic_intros)
by (metis "*" mult.commute complex_cnj_cnj complex_cnj_mult complex_cnj_one complex_mod_cnj mem_ball_0 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) ‹cmod w2 < 1› 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‹A big chain of equivalents of simple connectedness for an open set›
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⟧
⟹ ∃g. g holomorphic_on S ∧ (∀z ∈ S. f z = (g z)⇧2)"
shows "∃f g. f holomorphic_on S ∧ g holomorphic_on ball 0 1 ∧
(∀z ∈ S. f z ∈ ball 0 1 ∧ g(f z) = z) ∧
(∀z ∈ ball 0 1. g z ∈ S ∧ 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 S› ‹0 ∈ S› 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 ‹r > 0› 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))"
by (metis holomorphic_derivI [OF holF ‹open S›] ‹f ∈ F› image_subset_iff r01 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 ‹r > 0› 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
proof (rule order_antisym [OF _ le])
show "cmod (deriv f 0) ≤ l"
using ‹f ∈ F› bdd cSUP_upper by (fastforce simp: l_def)
qed
obtain ℱ where ℱin: "⋀n. ℱ n ∈ F" and ℱlim: "(λn. norm (deriv (ℱ n) 0)) ⇢ 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: l_def)
then have "¦norm (deriv f 0) - l¦ < 1 / (Suc n)"
by (fastforce simp: abs_if not_less eql)
with ‹f ∈ F› show ?thesis
by blast
qed
then obtain ℱ where fF: "⋀n. (ℱ n) ∈ 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 ‹N ≤ n› 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 ‹⋀n. ℱ n ∈ F› 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 ℱ, OF ‹open S› holF] by auto+
have der: "⋀n x. x ∈ S ⟹ ((ℱ ∘ r) n has_field_derivative ((λn. deriv (ℱ n)) ∘ r) n x) (at x)"
using ‹⋀n. ℱ n ∈ F› ‹open S› 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 S› 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 S› der ulim] ‹0 ∈ S› 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 ℱlim r] have no_df0: "norm(deriv f 0) = l"
by (force simp: o_def intro: tendsto_unique)
have nonconstf: "¬ f constant_on S"
using ‹open S› ‹0 ∈ S› no_df0 holomorphic_nonconstant [OF holf] eql [OF _ idF]
by force
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: ℱ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 S› ‹connected S› ‹open S›] nonconstf that
by fastforce
then show "f ` S ⊆ ball 0 1"
by auto
have "(λn. ℱ (r n) 0) ⇢ 0"
using ℱin by (auto simp: F_def)
then show "f 0 = 0"
using tendsto_unique [OF _ limf ] ‹0 ∈ S› trivial_limit_sequentially by blast
show "inj_on f S"
proof (rule Hurwitz_injective [OF ‹open S› ‹connected S› _ holf])
show "⋀n. (ℱ ∘ r) n holomorphic_on S"
by (simp add: ℱ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 ℱ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 ‹f ∈ F› 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 S› 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 ‹f ∈ F› by (auto simp: F_def)
have 1: "h ∘ f holomorphic_on S"
using F_def ‹f ∈ F› holh holomorphic_on_compose holomorphic_on_subset by blast
have 2: "⋀z. z ∈ S ⟹ (h ∘ f) z ≠ 0"
by (metis ‹h a = 0› 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 ‹f ∈ F› comp_inj_on inj_on_inverseI injf kh mem_Collect_eq subset_inj_on)
obtain ψ where holψ: "ψ holomorphic_on ((h ∘ f) ` S)"
and ψ2: "⋀z. z ∈ S ⟹ ψ(h (f z)) ^ 2 = h(f z)"
proof (rule exE [OF prev [OF 1 2 3]], safe)
fix θ
assume holθ: "θ holomorphic_on S" and θ2: "(∀z∈S. (h ∘ f) z = (θ z)⇧2)"
show thesis
proof
show "(θ ∘ g ∘ k) holomorphic_on (h ∘ f) ` S"
proof (intro holomorphic_on_compose)
show "k holomorphic_on (h ∘ f) ` S"
using holomorphic_on_subset [OF holk] f01 h01 by force
show "g holomorphic_on k ` (h ∘ f) ` S"
using holomorphic_on_subset [OF holg] by (force simp: kh nf1)
show "θ holomorphic_on g ` k ` (h ∘ f) ` S"
using holomorphic_on_subset [OF holθ] by (force simp: gf kh nf1)
qed
show "((θ ∘ g ∘ k) (h (f z)))⇧2 = h (f z)" if "z ∈ S" for z
using θ2 gf kh nf1 that by fastforce
qed
qed
have normψ1: "norm(ψ (h (f z))) < 1" if "z ∈ S" for z
proof -
have "norm (ψ (h (f z)) ^ 2) < 1"
by (metis (no_types) that DIM_complex ψ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 ψ01: "ψ (h (f 0)) ∈ ball 0 1"
by (simp add: ‹0 ∈ S›)
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 ψ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"
using holomorphic_on_subset [OF holh] f01 by fastforce
show "ψ holomorphic_on h ` f ` S"
using holomorphic_on_subset [OF holψ] by fastforce
show "p holomorphic_on ψ ` h ` f ` S"
using holomorphic_on_subset [OF holp] by (simp add: image_subset_iff normψ1)
qed
show "(p ∘ ψ ∘ h ∘ f) ` S ⊆ ball 0 1"
using normψ1 p01 by fastforce
show "(p ∘ ψ ∘ h ∘ f) 0 = 0"
by (simp add: ‹p (ψ (h (f 0))) = 0›)
show "inj_on (p ∘ ψ ∘ h ∘ f) S"
unfolding inj_on_def o_def
by (metis ψ2 dist_0_norm gf kh mem_ball nf1 normψ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"
using q01 holomorphic_on_subset [OF holk]
by (force simp: norm_power abs_square_less_1)
qed
have 2: "(k ∘ power2 ∘ q) 0 = 0"
using p0 F_def ‹f ∈ F› ψ01 ψ2 ‹0 ∈ S› 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: ‹c ≠ 0› 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 ‹p ∘ ψ ∘ h ∘ f ∈ F› ‹open S› ‹0 ∈ S› holF holomorphic_derivI by blast
show "⋀x. x ∈ S ⟹ (k ∘ power2 ∘ q ∘ (p ∘ ψ ∘ h ∘ f)) x = f x"
using ψ2 f01 kh normψ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 fS: "f ` S = ball 0 1"
using F_def ‹f ∈ F› by blast
then have "∀z∈ball 0 1. g z ∈ S ∧ f (g z) = z"
by (metis gf imageE)
with fS show ?thesis
by (metis gf holf holg image_eqI)
qed
locale SC_Chain =
fixes S :: "complex set"
assumes openS: "open S"
begin
lemma winding_number_zero:
assumes "simply_connected S"
shows "connected S ∧
(∀γ z. path γ ∧ path_image γ ⊆ S ∧
pathfinish γ = pathstart γ ∧ z ∉ S ⟶ winding_number γ 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)) *⇩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 ‹x ∈ S› 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 ‹x ∈ S› 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 ‹e > 0› in auto)
with ‹e > 0› have "inverse (norm (y - x)) * norm (z - f x * (y - x)) ≤ e/2"
by (simp add: field_split_simps)
also have "… < e"
using ‹e > 0› by simp
finally show ?thesis
by (simp add: contour_integral_unique [OF z])
qed
with ‹d1 > 0› ‹d2 > 0›
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)) *⇩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)) /⇩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 ‹connected S› ‹a ∈ S›]] ‹x ∈ S› ‹y ∈ S›
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)) *⇩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)) /⇩R norm (z - x))
─x→ 0"
apply (rule tendsto_eventually)
apply (simp add: eventually_at)
apply (rule_tac x=d in exI)
using ‹d > 0› * 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 Df: "⋀x. x ∈ S ⟹ DERIV f x :> deriv f x"
using holf holomorphic_derivI openS by force
have hfd: "⋀x. x ∈ S ⟹ ((λz. exp (g z) / f z) has_field_derivative 0) (at x)"
by (rule derivative_eq_intros Df g nz| simp)+
obtain c where c: "⋀x. x ∈ S ⟹ exp (g x) / f x = c"
proof (rule DERIV_zero_connected_constant[OF ‹connected S› 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 ‹connected S› openS finite.emptyI, of "λz. exp(g z) / f z"])
qed auto
show ?thesis
proof (intro exI ballI conjI)
have "g holomorphic_on S"
using openS g holomorphic_on_open by blast
then show "(λz. Ln(inverse c) + g z) holomorphic_on S"
by (intro holomorphic_intros)
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 ‹z ∈ S› 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)⇧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))⇧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)⇧2)"
shows "∃f g. f holomorphic_on S ∧ g holomorphic_on ball 0 1 ∧
(∀z ∈ S. f z ∈ ball 0 1 ∧ g(f z) = z) ∧
(∀z ∈ ball 0 1. g z ∈ S ∧ f(g z) = z)"
proof -
obtain a b where "a ∈ S" "b ∉ S"
using S by blast
then obtain δ where "δ > 0" and δ: "ball a δ ⊆ S"
using openS openE by blast
obtain g where holg: "g holomorphic_on S" and eqg: "⋀z. z ∈ S ⟹ z - b = (g z)⇧2"
proof (rule exE [OF prev [of "λz. z - b"]])
show "(λz. z - b) holomorphic_on S"
by (intro holomorphic_intros)
qed (use ‹b ∉ S› in auto)
have "¬ g constant_on S"
proof -
have "(a + δ/2) ∈ ball a δ" "a + (δ/2) ≠ a"
using ‹δ > 0› 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 ‹0 < δ› 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
with δ have "w ∈ S"
by force
then have "w = z"
by (metis diff_add_cancel eqg power_minus_Bit0 that w(1))
then have "g z = 0"
using ‹- g z = g w› by auto
with eqg that ‹b ∉ S› show False
by force
qed
then have nz: "⋀z. z ∈ S ⟹ g z + g a ≠ 0"
by (metis ‹0 < r› 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 ‹r > 0› g_not_r [OF ‹z ∈ S›] g_not_r [OF ‹a ∈ S›]
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 ‹r > 0› 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 ‹inj_on h S›] by metis
have 1: "open (h ` S)"
by (simp add: ‹inj_on h S› holh openS open_mapping_thm3)
have 2: "connected (h ` S)"
by (simp add: connected_continuous_image ‹connected S› holh holomorphic_on_imp_continuous_on)
have 3: "0 ∈ h ` S"
using ‹a ∈ S› ‹h a = 0› by auto
have 4: "∃g. g holomorphic_on h ` S ∧ (∀z∈h ` S. f z = (g z)⇧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)⇧2"
by (smt (verit) comp_def holf holh holomorphic_on_compose image_eqI nz(1) prev)
show ?thesis
proof (intro exI conjI)
show "g ∘ k holomorphic_on h ` S"
by (smt (verit) holg holk holomorphic_on_compose holomorphic_on_subset imageE image_subset_iff kh)
show "∀z∈h ` S. f z = ((g ∘ k) z)⇧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 ∨
(∃f g. f holomorphic_on S ∧ g holomorphic_on ball 0 1 ∧
(∀z ∈ S. f z ∈ ball 0 1 ∧ g(f z) = z) ∧
(∀z ∈ ball 0 1. g z ∈ S ∧ f(g z) = z))" (is "_ ∨ ?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 ∧
(∀g z. path g ∧ path_image g ⊆ S ∧
pathfinish g = pathstart g ∧ (z ∉ S)
⟶ winding_number g z = 0)" (is "?wn0")
and simply_connected_eq_contour_integral_zero:
"simply_connected S ⟷
connected S ∧
(∀g f. valid_path g ∧ path_image g ⊆ S ∧
pathfinish g = pathstart g ∧ f holomorphic_on S
⟶ (f has_contour_integral 0) g)" (is "?ci0")
and simply_connected_eq_global_primitive:
"simply_connected S ⟷
connected S ∧
(∀f. f holomorphic_on S ⟶
(∃h. ∀z. z ∈ S ⟶ (h has_field_derivative f z) (at z)))" (is "?gp")
and simply_connected_eq_holomorphic_log:
"simply_connected S ⟷
connected S ∧
(∀f. f holomorphic_on S ∧ (∀z ∈ S. f z ≠ 0)
⟶ (∃g. g holomorphic_on S ∧ (∀z ∈ S. f z = exp(g z))))" (is "?log")
and simply_connected_eq_holomorphic_sqrt:
"simply_connected S ⟷
connected S ∧
(∀f. f holomorphic_on S ∧ (∀z ∈ S. f z ≠ 0)
⟶ (∃g. g holomorphic_on S ∧ (∀z ∈ S. f z = (g z)⇧2)))" (is "?sqrt")
and simply_connected_eq_biholomorphic_to_disc:
"simply_connected S ⟷
S = {} ∨ S = UNIV ∨
(∃f g. f holomorphic_on S ∧ g holomorphic_on ball 0 1 ∧
(∀z ∈ S. f z ∈ ball 0 1 ∧ g(f z) = z) ∧
(∀z ∈ ball 0 1. g z ∈ S ∧ 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 *: "⟦α ⟹ β; β ⟹ γ; γ ⟹ δ; δ ⟹ ζ; ζ ⟹ η; η ⟹ θ; θ ⟹ ξ; ξ ⟹ α⟧
⟹ (α ⟷ β) ∧ (α ⟷ γ) ∧ (α ⟷ δ) ∧ (α ⟷ ζ) ∧
(α ⟷ η) ∧ (α ⟷ θ) ∧ (α ⟷ ξ)" for α β γ δ ζ η θ ξ
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"
assumes "open S"
shows "contractible S ⟷ simply_connected S"
proof
show "contractible S ⟹ simply_connected S"
by (simp add: contractible_imp_simply_connected)
show "simply_connected S ⟹ contractible S"
using assms convex_imp_contractible homeomorphic_contractible_eq
simply_connected_eq_homeomorphic_to_disc by auto
qed
subsection‹A further chain of equivalences about components of the complement of a simply connected set›
text‹(following 1.35 in Burckel'S book)›
context SC_Chain
begin
lemma frontier_properties:
assumes "simply_connected S"
shows "if bounded S then connected(frontier S)
else ∀C ∈ components(frontier S). ¬ 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 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 "connected (A n)" for n
using connected_annulus [of _ "0::complex"] by (simp add: A_def)
then have connX: "connected(X n)" for n
unfolding X_def
by (metis A01 connected_continuous_image connected_imp_connected_closure contf continuous_on_subset)
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 Seq X_def ‹x ∈ closure S› ‹x ∉ S› clo_fim by fastforce
qed
qed
moreover have "(⋂n. X n) ⊆ closure S - S"
proof -
have "(⋂n. X n) ⊆ closure S"
using Xsubclo by blast
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 ‹cmod x < 1› 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 ‹cmod x < 1› 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
by (meson True Xsubclo bounded_closure bounded_subset)
have compaX: "compact (X n)" for n
by (simp add: bouX cloX compact_eq_bounded_closed)
have "connected (⋂n. X n)"
by (metis nestX compaX connX connected_nest)
then show ?thesis
by (simp add: True ‹frontier S = (⋂n. X n)›)
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 ‹compact C›] 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 ‹compact L› ‹C ⊆ L› 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 ‹compact K› 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 ‹compact (closure U)› ‹open U› 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 ‹finite ℱ› ℱ] 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 ‹K ⊆ U› ‹C ⊆ K› by blast
moreover have "U ≠ UNIV"
using ‹compact (closure U)› by auto
ultimately show False
using ‹open U› ‹closed U› clopen by blast
next
case False
define j where "j ≡ Max J"
have "j ∈ J"
by (simp add: False ‹finite J› j_def)
have jmax: "⋀m. m ∈ J ⟹ m ≤ j"
by (simp add: j_def ‹finite J›)
have "⋂ ((λn. X n ∩ closure U) ` J) = X j ∩ closure U"
using False jmax nestX ‹j ∈ J› by auto
then have XU: "X j ∩ closure U = X j ∩ U"
using J closure_subset empty by fastforce
then have "openin (top_of_set (X j)) (X j ∩ closure U)"
by (simp add: openin_open_Int ‹open U›)
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 ‹compact (closure U)› bounded_subset compact_eq_bounded_closed inf.order_iff)
moreover have "X j ∩ closure U ≠ {}"
by (metis Cco Ksub UNIV_I ‹C ⊆ K› ‹K ⊆ U› XU bot.extremum_uniqueI in_components_maximal le_INF_iff le_inf_iff)
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 ‹U ∩ V = {}› ‹open V› closure_iff_nhds_not_empty that(2) by blast
then show ?thesis
by (metis (no_types) Diff_iff INT_I V ‹K ⊆ U› subsetD that(1))
qed
ultimately show False
by (auto simp: open_Int_closure_eq_empty [OF ‹open V›, 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 ∀C ∈ components(frontier S). ¬ 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)
moreover have "closed C"
using C_ccsw clo_ccs by blast
ultimately show False
by (metis C False ‹S ≠ UNIV› C_ccsw bot_eq_sup_iff connected_component_eq_UNIV frontier_Int_closed
frontier_closed frontier_complement frontier_eq_empty frontier_of_components_subset in_components_maximal inf.orderE)
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 ≠ {}"
unfolding connected_component_eq_empty
using confr openS ‹bounded C› ‹w ∉ S›
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) ≠ {}"
by (metis False ‹S ≠ UNIV› connected_component_eq_UNIV frontier_complement frontier_eq_empty)
qed
then show "connected_component_set (- S) z ∩ frontier S ≠ {}"
by auto
qed
then show False
by (metis C_ccsw Compl_iff ‹w ∉ S› ‹z ∉ C› 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: ‹z ∈ frontier S› 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 SC_Chain.openS SC_Chain_axioms bounded_subset closed_Compl connected_component_mono frontier_complement frontier_subset_eq)
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 ∧
(if bounded S then connected(frontier S)
else (∀C ∈ components(frontier S). ¬bounded C))" (is "?fp")
and simply_connected_eq_unbounded_complement_components:
"simply_connected S ⟷
connected S ∧ (∀C ∈ components(- S). ¬bounded C)" (is "?ucc")
and simply_connected_eq_empty_inside:
"simply_connected S ⟷
connected S ∧ inside S = {}" (is "?ei")
proof -
interpret SC_Chain
using assms by (simp add: SC_Chain_def)
have "?fp ∧ ?ucc ∧ ?ei"
using empty_inside empty_inside_imp_simply_connected frontier_properties
unbounded_complement_components winding_number_zero by blast
then show ?fp ?ucc ?ei
by blast+
qed
lemma simply_connected_iff_simple:
fixes S :: "complex set"
assumes "open S" "bounded S"
shows "simply_connected S ⟷ connected S ∧ connected(- S)" (is "?lhs = ?rhs")
proof
show "?lhs ⟹ ?rhs"
by (metis DIM_complex assms cobounded_has_bounded_component double_complement dual_order.order_iff_strict
simply_connected_eq_unbounded_complement_components)
show "?rhs ⟹ ?lhs"
by (simp add: assms connected_frontier_simple simply_connected_eq_frontier_properties)
qed
lemma subset_simply_connected_imp_inside_subset:
fixes A :: "complex set"
assumes "simply_connected A" "open A" "B ⊆ A"
shows "inside B ⊆ A"
by (metis assms Diff_eq_empty_iff inside_mono subset_empty simply_connected_eq_empty_inside)
subsection‹Further equivalences based on continuous logs and sqrts›
context SC_Chain
begin
lemma continuous_log:
fixes f :: "complex⇒complex"
assumes S: "simply_connected S"
and contf: "continuous_on S f" and nz: "⋀z. z ∈ S ⟹ f z ≠ 0"
shows "∃g. continuous_on S g ∧ (∀z ∈ S. f z = exp(g z))"
proof -
consider "S = {}" | "S homeomorphic ball (0::complex) 1"
using simply_connected_eq_homeomorphic_to_disc [OF openS] S by metis
then show ?thesis
proof cases
case 1 then show ?thesis
by simp
next
case 2
then obtain h k :: "complex⇒complex"
where kh: "⋀x. x ∈ S ⟹ k(h x) = x" and him: "h ` S = ball 0 1"
and conth: "continuous_on S h"
and hk: "⋀y. y ∈ ball 0 1 ⟹ h(k y) = y" and kim: "k ` ball 0 1 = S"
and contk: "continuous_on (ball 0 1) k"
unfolding homeomorphism_def homeomorphic_def by metis
obtain g where contg: "continuous_on (ball 0 1) g"
and expg: "⋀z. z ∈ ball 0 1 ⟹ (f ∘ k) z = exp (g z)"
proof (rule continuous_logarithm_on_ball)
show "continuous_on (ball 0 1) (f ∘ k)"
using contf continuous_on_compose contk kim by blast
show "⋀z. z ∈ ball 0 1 ⟹ (f ∘ k) z ≠ 0"
using kim nz by auto
qed auto
then show ?thesis
by (metis comp_apply conth continuous_on_compose him imageI kh)
qed
qed
lemma continuous_sqrt:
fixes f :: "complex⇒complex"
assumes contf: "continuous_on S f" and nz: "⋀z. z ∈ S ⟹ f z ≠ 0"
and prev: "⋀f::complex⇒complex.
⟦continuous_on S f; ⋀z. z ∈ S ⟹ f z ≠ 0⟧
⟹ ∃g. continuous_on S g ∧ (∀z ∈ S. f z = exp(g z))"
shows "∃g. continuous_on S g ∧ (∀z ∈ S. f z = (g z)⇧2)"
proof -
obtain g where contg: "continuous_on S g" and geq: "⋀z. z ∈ S ⟹ f z = exp(g z)"
using contf nz prev by metis
show ?thesis
proof (intro exI ballI conjI)
show "continuous_on S (λz. exp(g z/2))"
by (intro continuous_intros) (auto simp: contg)
show "⋀z. z ∈ S ⟹ f z = (exp (g z/2))⇧2"
by (metis (no_types, lifting) divide_inverse exp_double geq mult.left_commute mult.right_neutral right_inverse zero_neq_numeral)
qed
qed
lemma continuous_sqrt_imp_simply_connected:
assumes "connected S"
and prev: "⋀f::complex⇒complex. ⟦continuous_on S f; ∀z ∈ S. f z ≠ 0⟧
⟹ ∃g. continuous_on S g ∧ (∀z ∈ S. f z = (g z)⇧2)"
shows "simply_connected S"
proof (clarsimp simp add: simply_connected_eq_holomorphic_sqrt [OF openS] ‹connected S›)
fix f
assume "f holomorphic_on S" and nz: "∀z∈S. f z ≠ 0"
then obtain g where contg: "continuous_on S g" and geq: "⋀z. z ∈ S ⟹ f z = (g z)⇧2"
by (metis holomorphic_on_imp_continuous_on prev)
show "∃g. g holomorphic_on S ∧ (∀z∈S. f z = (g z)⇧2)"
proof (intro exI ballI conjI)
show "g holomorphic_on S"
proof (clarsimp simp add: holomorphic_on_open [OF openS])
fix z
assume "z ∈ S"
with nz geq have "g z ≠ 0"
by auto
obtain δ where "0 < δ" "⋀w. ⟦w ∈ S; dist w z < δ⟧ ⟹ dist (g w) (g z) < cmod (g z)"
using contg [unfolded continuous_on_iff] by (metis ‹g z ≠ 0› ‹z ∈ S› zero_less_norm_iff)
then have δ: "⋀w. ⟦w ∈ S; w ∈ ball z δ⟧ ⟹ g w + g z ≠ 0"
apply (clarsimp simp: dist_norm)
by (metis add_diff_cancel_left' dist_0_norm dist_complex_def less_le_not_le norm_increases_online norm_minus_commute)
have *: "(λx. (f x - f z) / (x - z) / (g x + g z)) ─z→ deriv f z / (g z + g z)"
proof (intro tendsto_intros)
show "(λx. (f x - f z) / (x - z)) ─z→ deriv f z"
using ‹f holomorphic_on S› ‹z ∈ S› has_field_derivative_iff holomorphic_derivI openS by blast
show "g ─z→ g z"
using ‹z ∈ S› contg continuous_on_eq_continuous_at isCont_def openS by blast
qed (simp add: ‹g z ≠ 0›)
then have "(g has_field_derivative deriv f z / (g z + g z)) (at z)"
unfolding has_field_derivative_iff
proof (rule Lim_transform_within_open)
show "open (ball z δ ∩ S)"
by (simp add: openS open_Int)
show "z ∈ ball z δ ∩ S"
using ‹z ∈ S› ‹0 < δ› by simp
show "⋀x. ⟦x ∈ ball z δ ∩ S; x ≠ z⟧
⟹ (f x - f z) / (x - z) / (g x + g z) = (g x - g z) / (x - z)"
using δ
apply (simp add: geq ‹z ∈ S› divide_simps)
apply (auto simp: algebra_simps power2_eq_square)
done
qed
then show "∃f'. (g has_field_derivative f') (at z)" ..
qed
qed (use geq in auto)
qed
end
proposition
fixes S :: "complex set"
assumes "open S"
shows simply_connected_eq_continuous_log:
"simply_connected S ⟷
connected S ∧
(∀f::complex⇒complex. continuous_on S f ∧ (∀z ∈ S. f z ≠ 0)
⟶ (∃g. continuous_on S g ∧ (∀z ∈ S. f z = exp (g z))))" (is "?log")
and simply_connected_eq_continuous_sqrt:
"simply_connected S ⟷
connected S ∧
(∀f::complex⇒complex. continuous_on S f ∧ (∀z ∈ S. f z ≠ 0)
⟶ (∃g. continuous_on S g ∧ (∀z ∈ S. f z = (g z)⇧2)))" (is "?sqrt")
proof -
interpret SC_Chain
using assms by (simp add: SC_Chain_def)
show ?log ?sqrt
using local.continuous_log winding_number_zero continuous_sqrt continuous_sqrt_imp_simply_connected
by auto
qed
subsection ‹More Borsukian results›
lemma Borsukian_componentwise_eq:
fixes S :: "'a::euclidean_space set"
assumes S: "locally connected S ∨ compact S"
shows "Borsukian S ⟷ (∀C ∈ components S. Borsukian C)"
proof -
have *: "ANR(-{0::complex})"
by (simp add: ANR_delete open_Compl open_imp_ANR)
show ?thesis
using cohomotopically_trivial_on_components [OF assms *] by (auto simp: Borsukian_alt)
qed
lemma Borsukian_componentwise:
fixes S :: "'a::euclidean_space set"
assumes "locally connected S ∨ compact S" "⋀C. C ∈ components S ⟹ Borsukian C"
shows "Borsukian S"
by (metis Borsukian_componentwise_eq assms)
lemma simply_connected_eq_Borsukian:
fixes S :: "complex set"
shows "open S ⟹ (simply_connected S ⟷ connected S ∧ Borsukian S)"
by (auto simp: simply_connected_eq_continuous_log Borsukian_continuous_logarithm)
lemma Borsukian_eq_simply_connected:
fixes S :: "complex set"
shows "open S ⟹ Borsukian S ⟷ (∀C ∈ components S. simply_connected C)"
by (meson Borsukian_componentwise_eq in_components_connected open_components open_imp_locally_connected simply_connected_eq_Borsukian)
lemma Borsukian_separation_open_closed:
fixes S :: "complex set"
assumes S: "open S ∨ closed S" and "bounded S"
shows "Borsukian S ⟷ connected(- S)"
using S
proof
assume "open S"
show ?thesis
unfolding Borsukian_eq_simply_connected [OF ‹open S›]
by (metis ‹open S› ‹bounded S› bounded_subset in_components_maximal nonseparation_by_component_eq open_components simply_connected_iff_simple)
next
assume "closed S"
with ‹bounded S› show ?thesis
by (simp add: Borsukian_separation_compact compact_eq_bounded_closed)
qed
subsection‹Finally, the Riemann Mapping Theorem›
theorem Riemann_mapping_theorem:
"open S ∧ simply_connected S ⟷
S = {} ∨ S = UNIV ∨
(∃f g. f holomorphic_on S ∧ g holomorphic_on ball 0 1 ∧
(∀z ∈ S. f z ∈ ball 0 1 ∧ g(f z) = z) ∧
(∀z ∈ ball 0 1. g z ∈ S ∧ f(g z) = z))"
(is "_ = ?rhs")
proof -
have "simply_connected S ⟷ ?rhs" if "open S"
by (simp add: simply_connected_eq_biholomorphic_to_disc that)
moreover have "open S" if "?rhs"
proof -
{ fix f g
assume g: "g holomorphic_on ball 0 1" "∀z∈ball 0 1. g z ∈ S ∧ f (g z) = z"
and "∀z∈S. cmod (f z) < 1 ∧ g (f z) = z"
then have "S = g ` (ball 0 1)"
by (force simp:)
then have "open S"
by (metis open_ball g inj_on_def open_mapping_thm3)
}
with that show "open S" by auto
qed
ultimately show ?thesis by metis
qed
subsection ‹Applications to Winding Numbers›
lemma simply_connected_inside_simple_path:
fixes p :: "real ⇒ complex"
shows "simple_path p ⟹ simply_connected(inside(path_image p))"
using Jordan_inside_outside connected_simple_path_image inside_simple_curve_imp_closed simply_connected_eq_frontier_properties
by fastforce
lemma simply_connected_Int:
fixes S :: "complex set"
assumes "open S" "open T" "simply_connected S" "simply_connected T" "connected (S ∩ T)"
shows "simply_connected (S ∩ T)"
using assms by (force simp: simply_connected_eq_winding_number_zero open_Int)
subsection ‹The winding number defines a continuous logarithm for the path itself›
lemma winding_number_as_continuous_log:
assumes "path p" and ζ: "ζ ∉ path_image p"
obtains q where "path q"
"pathfinish q - pathstart q = 2 * of_real pi * 𝗂 * winding_number p ζ"
"⋀t. t ∈ {0..1} ⟹ p t = ζ + exp(q t)"
proof -
let ?q = "λt. 2 * of_real pi * 𝗂 * winding_number(subpath 0 t p) ζ + Ln(pathstart p - ζ)"
show ?thesis
proof
have *: "continuous (at t within {0..1}) (λx. winding_number (subpath 0 x p) ζ)"
if t: "t ∈ {0..1}" for t
proof -
let ?B = "ball (p t) (norm(p t - ζ))"
have "p t ≠ ζ"
using path_image_def that ζ by blast
then have "simply_connected ?B"
by (simp add: convex_imp_simply_connected)
then have "⋀f::complex⇒complex. continuous_on ?B f ∧ (∀ζ ∈ ?B. f ζ ≠ 0)
⟶ (∃g. continuous_on ?B g ∧ (∀ζ ∈ ?B. f ζ = exp (g ζ)))"
by (simp add: simply_connected_eq_continuous_log)
moreover have "continuous_on ?B (λw. w - ζ)"
by (intro continuous_intros)
moreover have "(∀z ∈ ?B. z - ζ ≠ 0)"
by (auto simp: dist_norm)
ultimately obtain g where contg: "continuous_on ?B g"
and geq: "⋀z. z ∈ ?B ⟹ z - ζ = exp (g z)" by blast
obtain d where "0 < d" and d:
"⋀x. ⟦x ∈ {0..1}; dist x t < d⟧ ⟹ dist (p x) (p t) < cmod (p t - ζ)"
using ‹path p› t unfolding path_def continuous_on_iff
by (metis ‹p t ≠ ζ› right_minus_eq zero_less_norm_iff)
have "((λx. winding_number (λw. subpath 0 x p w - ζ) 0 -
winding_number (λw. subpath 0 t p w - ζ) 0) ⤏ 0)
(at t within {0..1})"
proof (rule Lim_transform_within [OF _ ‹d > 0›])
have "continuous (at t within {0..1}) (g o p)"
proof (rule continuous_within_compose)
show "continuous (at t within {0..1}) p"
using ‹path p› continuous_on_eq_continuous_within path_def that by blast
show "continuous (at (p t) within p ` {0..1}) g"
by (metis (no_types, lifting) open_ball UNIV_I ‹p t ≠ ζ› centre_in_ball contg continuous_on_eq_continuous_at continuous_within_topological right_minus_eq zero_less_norm_iff)
qed
with LIM_zero have "((λu. (g (subpath t u p 1) - g (subpath t u p 0))) ⤏ 0) (at t within {0..1})"
by (auto simp: subpath_def continuous_within o_def)
then show "((λu. (g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * 𝗂)) ⤏ 0)
(at t within {0..1})"
by (simp add: tendsto_divide_zero)
show "(g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * 𝗂) =
winding_number (λw. subpath 0 u p w - ζ) 0 - winding_number (λw. subpath 0 t p w - ζ) 0"
if "u ∈ {0..1}" "0 < dist u t" "dist u t < d" for u
proof -
have "closed_segment t u ⊆ {0..1}"
using closed_segment_eq_real_ivl t that by auto
then have piB: "path_image(subpath t u p) ⊆ ?B"
apply (clarsimp simp add: path_image_subpath_gen)
by (metis subsetD le_less_trans ‹dist u t < d› d dist_commute dist_in_closed_segment)
have *: "path (g ∘ subpath t u p)"
proof (rule path_continuous_image)
show "path (subpath t u p)"
using ‹path p› t that by auto
show "continuous_on (path_image (subpath t u p)) g"
using piB contg continuous_on_subset by blast
qed
have "(g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * 𝗂)
= winding_number (exp ∘ g ∘ subpath t u p) 0"
using winding_number_compose_exp [OF *]
by (simp add: pathfinish_def pathstart_def o_assoc)
also have "… = winding_number (λw. subpath t u p w - ζ) 0"
proof (rule winding_number_cong)
have "exp(g y) = y - ζ" if "y ∈ (subpath t u p) ` {0..1}" for y
by (metis that geq path_image_def piB subset_eq)
then show "⋀x. ⟦0 ≤ x; x ≤ 1⟧ ⟹ (exp ∘ g ∘ subpath t u p) x = subpath t u p x - ζ"
by auto
qed
also have "… = winding_number (λw. subpath 0 u p w - ζ) 0 -
winding_number (λw. subpath 0 t p w - ζ) 0"
apply (simp add: winding_number_offset [symmetric])
using winding_number_subpath_combine [OF ‹path p› ζ, of 0 t u] ‹t ∈ {0..1}› ‹u ∈ {0..1}›
by (simp add: add.commute eq_diff_eq)
finally show ?thesis .
qed
qed
then show ?thesis
by (subst winding_number_offset) (simp add: continuous_within LIM_zero_iff)
qed
show "path ?q"
unfolding path_def
by (intro continuous_intros) (simp add: continuous_on_eq_continuous_within *)
have "ζ ≠ p 0"
by (metis ζ pathstart_def pathstart_in_path_image)
then show "pathfinish ?q - pathstart ?q = 2 * of_real pi * 𝗂 * winding_number p ζ"
by (simp add: pathfinish_def pathstart_def)
show "p t = ζ + exp (?q t)" if "t ∈ {0..1}" for t
proof -
have "path (subpath 0 t p)"
using ‹path p› that by auto
moreover
have "ζ ∉ path_image (subpath 0 t p)"
using ζ [unfolded path_image_def] that by (auto simp: path_image_subpath)
ultimately show ?thesis
using winding_number_exp_2pi [of "subpath 0 t p" ζ] ‹ζ ≠ p 0›
by (auto simp: exp_add algebra_simps pathfinish_def pathstart_def subpath_def)
qed
qed
qed
subsection ‹Winding number equality is the same as path/loop homotopy in C - {0}›
lemma winding_number_homotopic_loops_null_eq:
assumes "path p" and ζ: "ζ ∉ path_image p"
shows "winding_number p ζ = 0 ⟷ (∃a. homotopic_loops (-{ζ}) p (λt. a))"
(is "?lhs = ?rhs")
proof
assume [simp]: ?lhs
obtain q where "path q"
and qeq: "pathfinish q - pathstart q = 2 * of_real pi * 𝗂 * winding_number p ζ"
and peq: "⋀t. t ∈ {0..1} ⟹ p t = ζ + exp(q t)"
using winding_number_as_continuous_log [OF assms] by blast
have *: "homotopic_with_canon (λr. pathfinish r = pathstart r)
{0..1} (-{ζ}) ((λw. ζ + exp w) ∘ q) ((λw. ζ + exp w) ∘ (λt. 0))"
proof (rule homotopic_with_compose_continuous_left)
show "homotopic_with_canon (λf. pathfinish ((λw. ζ + exp w) ∘ f) = pathstart ((λw. ζ + exp w) ∘ f))
{0..1} UNIV q (λt. 0)"
proof (rule homotopic_with_mono, simp_all add: pathfinish_def pathstart_def)
have "homotopic_loops UNIV q (λt. 0)"
by (rule homotopic_loops_linear) (use qeq ‹path q› in ‹auto simp: path_defs›)
then have "homotopic_with (λr. r 1 = r 0) (top_of_set {0..1}) euclidean q (λt. 0)"
by (simp add: homotopic_loops_def pathfinish_def pathstart_def)
then show "homotopic_with (λh. exp (h 1) = exp (h 0)) (top_of_set {0..1}) euclidean q (λt. 0)"
by (rule homotopic_with_mono) simp
qed
show "continuous_on UNIV (λw. ζ + exp w)"
by (rule continuous_intros)+
show "(λw. ζ + exp w) ∈ UNIV → -{ζ}"
by auto
qed
then have "homotopic_with_canon (λr. pathfinish r = pathstart r) {0..1} (-{ζ}) p (λx. ζ + 1)"
by (rule homotopic_with_eq) (auto simp: o_def peq pathfinish_def pathstart_def)
then have "homotopic_loops (-{ζ}) p (λt. ζ + 1)"
by (simp add: homotopic_loops_def)
then show ?rhs ..
next
assume ?rhs
then obtain a where "homotopic_loops (-{ζ}) p (λt. a)" ..
then have "winding_number p ζ = winding_number (λt. a) ζ" "a ≠ ζ"
using winding_number_homotopic_loops homotopic_loops_imp_subset by (force simp:)+
then show ?lhs
using winding_number_zero_const by auto
qed
lemma winding_number_homotopic_paths_null_explicit_eq:
assumes "path p" and ζ: "ζ ∉ path_image p"
shows "winding_number p ζ = 0 ⟷ homotopic_paths (-{ζ}) p (linepath (pathstart p) (pathstart p))"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
using homotopic_loops_imp_homotopic_paths_null
by (force simp: linepath_refl winding_number_homotopic_loops_null_eq [OF assms])
next
assume ?rhs
then show ?lhs
by (metis ζ pathstart_in_path_image winding_number_homotopic_paths winding_number_trivial)
qed
lemma winding_number_homotopic_paths_null_eq:
assumes "path p" and ζ: "ζ ∉ path_image p"
shows "winding_number p ζ = 0 ⟷ (∃a. homotopic_paths (-{ζ}) p (λt. a))"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
by (auto simp: winding_number_homotopic_paths_null_explicit_eq [OF assms] linepath_refl)
next
assume ?rhs
then show ?lhs
by (metis ζ homotopic_paths_imp_pathfinish pathfinish_def pathfinish_in_path_image winding_number_homotopic_paths winding_number_zero_const)
qed
proposition winding_number_homotopic_paths_eq:
assumes "path p" and ζp: "ζ ∉ path_image p"
and "path q" and ζq: "ζ ∉ path_image q"
and qp: "pathstart q = pathstart p" "pathfinish q = pathfinish p"
shows "winding_number p ζ = winding_number q ζ ⟷ homotopic_paths (-{ζ}) p q"
(is "?lhs = ?rhs")
proof
assume ?lhs
then have "winding_number (p +++ reversepath q) ζ = 0"
using assms by (simp add: winding_number_join winding_number_reversepath)
moreover
have "path (p +++ reversepath q)" "ζ ∉ path_image (p +++ reversepath q)"
using assms by (auto simp: not_in_path_image_join)
ultimately obtain a where "homotopic_paths (- {ζ}) (p +++ reversepath q) (linepath a a)"
using winding_number_homotopic_paths_null_explicit_eq by blast
then show ?rhs
using homotopic_paths_imp_pathstart assms
by (fastforce simp: dest: homotopic_paths_imp_homotopic_loops homotopic_paths_loop_parts)
qed (simp add: winding_number_homotopic_paths)
lemma winding_number_homotopic_loops_eq:
assumes "path p" and ζp: "ζ ∉ path_image p"
and "path q" and ζq: "ζ ∉ path_image q"
and loops: "pathfinish p = pathstart p" "pathfinish q = pathstart q"
shows "winding_number p ζ = winding_number q ζ ⟷ homotopic_loops (-{ζ}) p q"
(is "?lhs = ?rhs")
proof
assume L: ?lhs
have "pathstart p ≠ ζ" "pathstart q ≠ ζ"
using ζp ζq by blast+
moreover have "path_connected (-{ζ})"
by (simp add: path_connected_punctured_universe)
ultimately obtain r where "path r" and rim: "path_image r ⊆ -{ζ}"
and pas: "pathstart r = pathstart p" and paf: "pathfinish r = pathstart q"
by (auto simp: path_connected_def)
then have "pathstart r ≠ ζ" by blast
have "homotopic_loops (- {ζ}) p (r +++ q +++ reversepath r)"
proof (rule homotopic_paths_imp_homotopic_loops)
have "path (r +++ q +++ reversepath r)"
by (simp add: ‹path r› ‹path q› loops paf)
moreover have "ζ ∉ path_image (r +++ q +++ reversepath r)"
by (metis ζq not_in_path_image_join path_image_reversepath rim subset_Compl_singleton)
moreover have "homotopic_loops (- {ζ}) (r +++ q +++ reversepath r) q"
using ‹path q› ‹path r› ζq homotopic_loops_conjugate loops(2) paf rim by blast
ultimately show "homotopic_paths (- {ζ}) p (r +++ q +++ reversepath r)"
using loops pathfinish_join pathfinish_reversepath pathstart_join
by (metis L ζp ‹path p› pas winding_number_homotopic_loops winding_number_homotopic_paths_eq)
qed (use loops pas in auto)
moreover have "homotopic_loops (- {ζ}) (r +++ q +++ reversepath r) q"
using rim ζq by (auto simp: homotopic_loops_conjugate paf ‹path q› ‹path r› loops)
ultimately show ?rhs
using homotopic_loops_trans by metis
qed (simp add: winding_number_homotopic_loops)
end