Quelle Conformal_Mappings.thy Sprache: Isabelle

section \<open>Conformal Mappings and Consequences of Cauchy's Integral Theorem\<close>

text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2016)\<close>

text\<open>Also Cauchy's residue theorem by Wenda Li (2016)\<close>

theory Conformal_Mappings
imports Cauchy_Integral_Formula

begin

subsection \<open>Analytic continuation\<close>

proposition isolated_zeros:
  assumes holf: "f holomorphic_on S"
      and "open S" "connected S" "\ \ S" "f \ = 0" "\ \ S" "f \ \ 0"
    obtains r where "0 < r" and "ball \ r \ S" and
        "\z. z \ ball \ r - {\} \ f z \ 0"
proof -
  obtain r where "0 < r" and r: "ball \ r \ S"
    using \<open>open S\<close> \<open>\<xi> \<in> S\<close> open_contains_ball_eq by blast
  have powf: "((\n. (deriv ^^ n) f \ / (fact n) * (z - \)^n) sums f z)" if "z \ ball \ r" for z
    by (intro holomorphic_power_series [OF _ that] holomorphic_on_subset [OF holf r])
  obtain m where m: "(deriv ^^ m) f \ / (fact m) \ 0"
    using holomorphic_fun_eq_0_on_connected [OF holf \<open>open S\<close> \<open>connected S\<close> _ \<open>\<xi> \<in> S\<close> \<open>\<beta> \<in> S\<close>] \<open>f \<beta> \<noteq> 0\<close>
    by auto
  then have "m \ 0" using assms(5) funpow_0 by fastforce
  obtain s where "0 < s" and s: "\z. z \ cball \ s - {\} \ f z \ 0"
    using powser_0_nonzero [OF \<open>0 < r\<close> powf \<open>f \<xi> = 0\<close> m]
    by (metis \<open>m \<noteq> 0\<close> dist_norm mem_ball norm_minus_commute not_gr_zero)
  have "0 < min r s"  by (simp add: \<open>0 < r\<close> \<open>0 < s\<close>)
  then show thesis
  proof qed (use r s in auto)
qed

proposition analytic_continuation:
  assumes holf: "f holomorphic_on S"
      and "open S" and "connected S"
      and "U \ S" and "\ \ S"
      and "\ islimpt U"
      and fU0 [simp]: "\z. z \ U \ f z = 0"
      and "w \ S"
    shows "f w = 0"
proof -
  obtain e where "0 < e" and e: "cball \ e \ S"
    using \<open>open S\<close> \<open>\<xi> \<in> S\<close> open_contains_cball_eq by blast
  define T where "T = cball \ e \ U"
  have contf: "continuous_on (closure T) f"
    by (metis T_def closed_cball closure_minimal e holf holomorphic_on_imp_continuous_on
              holomorphic_on_subset inf.cobounded1)
  have fT0 [simp]: "\x. x \ T \ f x = 0"
    by (simp add: T_def)
  have "\r. \\e>0. \x'\U. x' \ \ \ dist x' \ < e; 0 < r\ \ \x'\cball \ e \ U. x' \ \ \ dist x' \ < r"
    by (metis \<open>0 < e\<close> IntI dist_commute less_eq_real_def mem_cball min_less_iff_conj)
  then have "\ islimpt T" using \\ islimpt U\
    by (auto simp: T_def islimpt_approachable)
  then have "\ \ closure T"
    by (simp add: closure_def)
  then have "f \ = 0"
    by (auto simp: continuous_constant_on_closure [OF contf])
  moreover have "\r. \0 < r; \z. z \ ball \ r - {\} \ f z \ 0\ \ False"
    by (metis open_ball \<open>\<xi> islimpt T\<close> centre_in_ball fT0 insertE insert_Diff islimptE)
  ultimately show ?thesis
    by (metis \<open>open S\<close> \<open>connected S\<close> \<open>\<xi> \<in> S\<close> \<open>w \<in> S\<close> holf isolated_zeros)
qed

corollary analytic_continuation_open:
  assumes "open s" and "open s'" and "s \ {}" and "connected s'"
      and "s \ s'"
  assumes "f holomorphic_on s'" and "g holomorphic_on s'"
      and "\z. z \ s \ f z = g z"
  assumes "z \ s'"
  shows   "f z = g z"
proof -
  from \<open>s \<noteq> {}\<close> obtain \<xi> where "\<xi> \<in> s" by auto
  with \<open>open s\<close> have \<xi>: "\<xi> islimpt s"
    by (intro interior_limit_point) (auto simp: interior_open)
  have "f z - g z = 0"
    by (rule analytic_continuation[of "\z. f z - g z" s' s \])
       (insert assms \<open>\<xi> \<in> s\<close> \<xi>, auto intro: holomorphic_intros)
  thus ?thesis by simp
qed

corollary analytic_continuation':
  assumes "f holomorphic_on S" "open S" "connected S"
      and "U \ S" "\ \ S" "\ islimpt U"
      and "f constant_on U"
    shows "f constant_on S"
proof -
  obtain c where c: "\x. x \ U \ f x - c = 0"
    by (metis \<open>f constant_on U\<close> constant_on_def diff_self)
  have "(\z. f z - c) holomorphic_on S"
    using assms by (intro holomorphic_intros)
  with c analytic_continuation assms have "\x. x \ S \ f x - c = 0"
    by blast
  then show ?thesis
    unfolding constant_on_def by force
qed

lemma holomorphic_compact_finite_zeros:
  assumes S: "f holomorphic_on S" "open S" "connected S"
      and "compact K" "K \ S"
      and "\ f constant_on S"
    shows "finite {z\K. f z = 0}"
proof (rule ccontr)
  assume "infinite {z\K. f z = 0}"
  then obtain z where "z \ K" and z: "z islimpt {z\K. f z = 0}"
    using \<open>compact K\<close> by (auto simp: compact_eq_Bolzano_Weierstrass)
  moreover have "{z\K. f z = 0} \ S"
    using \<open>K \<subseteq> S\<close> by blast
    ultimately show False
    using assms analytic_continuation [OF S] unfolding constant_on_def
    by blast
qed

lemma holomorphic_countable_zeros:
  assumes S: "f holomorphic_on S" "open S" "connected S" and "fsigma S"
      and "\ f constant_on S"
    shows "countable {z\S. f z = 0}"
proof -
  obtain F::"nat \ complex set"
      where F: "range F \ Collect compact" and Seq: "S = (\i. F i)"
    using \<open>fsigma S\<close> by (meson fsigma_Union_compact)
  have fin: "finite {z \ F i. f z = 0}" for i
    using holomorphic_compact_finite_zeros assms F Seq Union_iff by blast
  have "{z \ S. f z = 0} = (\i. {z \ F i. f z = 0})"
    using Seq by auto
  with fin show ?thesis
    by (simp add: countable_finite)
qed

lemma holomorphic_countable_equal:
  assumes "f holomorphic_on S" "g holomorphic_on S" "open S" "connected S" and "fsigma S"
    and eq: "uncountable {z\S. f z = g z}"
  shows "S \ {z\S. f z = g z}"
proof -
  obtain z where z: "z\S" "f z = g z"
    using eq not_finite_existsD uncountable_infinite by blast
  have "(\x. f x - g x) holomorphic_on S"
    by (simp add: assms holomorphic_on_diff)
  then have "(\x. f x - g x) constant_on S"
    using holomorphic_countable_zeros assms by force
  with z have "\x. x\S \ f x - g x = 0"
    unfolding constant_on_def by force
  then show ?thesis
    by auto
qed

lemma holomorphic_countable_equal_UNIV:
  assumes fg: "f holomorphic_on UNIV" "g holomorphic_on UNIV"
    and eq: "uncountable {z. f z = g z}"
  shows "f=g"
  using holomorphic_countable_equal [OF fg] eq by fastforce

subsection\<open>Open mapping theorem\<close>

lemma holomorphic_contract_to_zero:
  assumes contf: "continuous_on (cball \ r) f"
      and holf: "f holomorphic_on ball \ r"
      and "0 < r"
      and norm_less: "\z. norm(\ - z) = r \ norm(f \) < norm(f z)"
  obtains z where "z \ ball \ r" "f z = 0"
proof -
  { assume fnz: "\w. w \ ball \ r \ f w \ 0"
    then have "0 < norm (f \)"
      by (simp add: \<open>0 < r\<close>)
    have fnz': "\w. w \ cball \ r \ f w \ 0"
      using dist_complex_def fnz norm_less order_le_less by fastforce
    have "frontier(cball \ r) \ {}"
      using \<open>0 < r\<close> by simp
    define g where [abs_def]: "g z = inverse (f z)" for z
    have contg: "continuous_on (cball \ r) g"
      unfolding g_def using contf continuous_on_inverse fnz' by blast
    have holg: "g holomorphic_on ball \ r"
      unfolding g_def using fnz holf holomorphic_on_inverse by blast
    have "frontier (cball \ r) \ cball \ r"
      by (simp add: subset_iff)
    then have contf': "continuous_on (frontier (cball \ r)) f"
          and contg': "continuous_on (frontier (cball \ r)) g"
      by (blast intro: contf contg continuous_on_subset)+
    have froc: "frontier(cball \ r) \ {}"
      using \<open>0 < r\<close> by simp
    moreover have "continuous_on (frontier (cball \ r)) (norm o f)"
      using contf' continuous_on_compose continuous_on_norm_id by blast
    ultimately obtain w where w: "w \ frontier(cball \ r)"
                          and now: "\x. x \ frontier(cball \ r) \ norm (f w) \ norm (f x)"
      using continuous_attains_inf [OF compact_frontier [OF compact_cball]]
      by (metis comp_apply)
    then have fw: "0 < norm (f w)"
      by (simp add: fnz')
    have "continuous_on (frontier (cball \ r)) (norm o g)"
      using contg' continuous_on_compose continuous_on_norm_id by blast
    then obtain v where v: "v \ frontier(cball \ r)"
               and nov: "\x. x \ frontier(cball \ r) \ norm (g v) \ norm (g x)"
      using continuous_attains_sup [OF compact_frontier [OF compact_cball] froc] by force
    then have fv: "0 < norm (f v)"
      by (simp add: fnz')
    have "norm ((deriv ^^ 0) g \) \ fact 0 * norm (g v) / r ^ 0"
      by (rule Cauchy_inequality [OF holg contg \<open>0 < r\<close>]) (simp add: dist_norm nov)
    then have "cmod (g \) \ cmod (g v)"
      by simp
    moreover have "cmod (\ - w) = r"
      by (metis (no_types) dist_norm frontier_cball mem_sphere w)
    ultimately obtain wr: "norm (\ - w) = r" and nfw: "norm (f w) \ norm (f \)"
      unfolding g_def
      by (smt (verit, del_insts) \<open>0 < cmod (f \<xi>)\<close> inverse_le_imp_le norm_inverse now v)
    with fw have False
      using norm_less by force
  }
  with that show ?thesis by blast
qed

theorem open_mapping_thm:
  assumes holf: "f holomorphic_on S"
      and S: "open S" and "connected S"
      and "open U" and "U \ S"
      and fne: "\ f constant_on S"
    shows "open (f ` U)"
proof -
  have *: "open (f ` U)"
          if "U \ {}" and U: "open U" "connected U" and "f holomorphic_on U" and fneU: "\x. \y \ U. f y \ x"
          for U
  proof (clarsimp simp: open_contains_ball)
    fix \<xi> assume \<xi>: "\<xi> \<in> U"
    show "\e>0. ball (f \) e \ f ` U"
    proof -
      have hol: "(\z. f z - f \) holomorphic_on U"
        by (rule holomorphic_intros that)+
      obtain s where "0 < s" and sbU: "ball \ s \ U"
                 and sne: "\z. z \ ball \ s - {\} \ (\z. f z - f \) z \ 0"
        using isolated_zeros [OF hol U \<xi>]  by (metis fneU right_minus_eq)
      obtain r where "0 < r" and r: "cball \ r \ ball \ s"
        using \<open>0 < s\<close> by (rule_tac r="s/2" in that) auto
      have "cball \ r \ U"
        using sbU r by blast
      then have frsbU: "frontier (cball \ r) \ U"
        using Diff_subset frontier_def order_trans by fastforce
      then have cof: "compact (frontier(cball \ r))"
        by blast
      have frne: "frontier (cball \ r) \ {}"
        using \<open>0 < r\<close> by auto
      have contfr: "continuous_on (frontier (cball \ r)) (\z. norm (f z - f \))"
        by (metis continuous_on_norm continuous_on_subset frsbU hol holomorphic_on_imp_continuous_on)
      obtain w where "norm (\ - w) = r"
                 and w: "(\z. norm (\ - z) = r \ norm (f w - f \) \ norm(f z - f \))"
        using continuous_attains_inf [OF cof frne contfr] by (auto simp: dist_norm)
      moreover define \<epsilon> where "\<epsilon> \<equiv> norm (f w - f \<xi>) / 3"
      ultimately have "0 < \"
        using \<open>0 < r\<close> dist_complex_def r sne by auto
      have "ball (f \) \ \ f ` U"
      proof
        fix \<gamma>
        assume \<gamma>: "\<gamma> \<in> ball (f \<xi>) \<epsilon>"
        have *: "cmod (\ - f \) < cmod (\ - f z)" if "cmod (\ - z) = r" for z
        proof -
          have lt: "cmod (f w - f \) / 3 < cmod (\ - f z)"
            using w [OF that] \<gamma>
            using dist_triangle2 [of "f \" "\" "f z"] dist_triangle2 [of "f \" "f z" \]
            by (simp add: \<epsilon>_def dist_norm norm_minus_commute)
          show ?thesis
            by (metis \<epsilon>_def dist_commute dist_norm less_trans lt mem_ball \<gamma>)
        qed
       have "continuous_on (cball \ r) (\z. \ - f z)"
          using \<open>cball \<xi> r \<subseteq> U\<close> \<open>f holomorphic_on U\<close>
          by (force intro: continuous_intros continuous_on_subset holomorphic_on_imp_continuous_on)
        moreover have "(\z. \ - f z) holomorphic_on ball \ r"
          using \<open>cball \<xi> r \<subseteq> U\<close> ball_subset_cball holomorphic_on_subset that(4)
          by (intro holomorphic_intros) blast
        ultimately obtain z where "z \ ball \ r" "\ - f z = 0"
          using "*" \<open>0 < r\<close> holomorphic_contract_to_zero by blast
        then show "\ \ f ` U"
          using \<open>cball \<xi> r \<subseteq> U\<close> by fastforce
      qed
      then show ?thesis using  \<open>0 < \<epsilon>\<close> by blast
    qed
  qed
  have "open (f ` X)" if "X \ components U" for X
  proof -
    have holfU: "f holomorphic_on U"
      using \<open>U \<subseteq> S\<close> holf holomorphic_on_subset by blast
    have "X \ {}"
      using that by (simp add: in_components_nonempty)
    moreover have "open X"
      using that \<open>open U\<close> open_components by auto
    moreover have "connected X"
      using that in_components_maximal by blast
    moreover have "f holomorphic_on X"
      by (meson that holfU holomorphic_on_subset in_components_maximal)
    moreover have "\y\X. f y \ x" for x
    proof (rule ccontr)
      assume not: "\ (\y\X. f y \ x)"
      have "X \ S"
        using \<open>U \<subseteq> S\<close> in_components_subset that by blast
      obtain w where w: "w \ X" using \X \ {}\ by blast
      have wis: "w islimpt X"
        using w \<open>open X\<close> interior_eq by auto
      have hol: "(\z. f z - x) holomorphic_on S"
        by (simp add: holf holomorphic_on_diff)
      with fne [unfolded constant_on_def]
           analytic_continuation[OF hol S \<open>connected S\<close> \<open>X \<subseteq> S\<close> _ wis] not \<open>X \<subseteq> S\<close> w
      show False by auto
    qed
    ultimately show ?thesis
      by (rule *)
  qed
  then have "open (f ` \(components U))"
    by (metis (no_types, lifting) imageE image_Union open_Union)
  then show ?thesis
    by force
qed

text\<open>No need for \<^term>\<open>S\<close> to be connected. But the nonconstant condition is stronger.\<close>
corollary\<^marker>\<open>tag unimportant\<close> open_mapping_thm2:
  assumes holf: "f holomorphic_on S"
      and S: "open S"
      and "open U" "U \ S"
      and fnc: "\X. \open X; X \ S; X \ {}\ \ \ f constant_on X"
    shows "open (f ` U)"
proof -
  have "S = \(components S)" by simp
  with \<open>U \<subseteq> S\<close> have "U = (\<Union>C \<in> components S. C \<inter> U)" by auto
  then have "f ` U = (\C \ components S. f ` (C \ U))"
    using image_UN by fastforce
  moreover
  { fix C assume "C \ components S"
    with S \<open>C \<in> components S\<close> open_components in_components_connected
    have C: "open C" "connected C" by auto
    have "C \ S"
      by (metis \<open>C \<in> components S\<close> in_components_maximal)
    have nf: "\ f constant_on C"
      using \<open>open C\<close> \<open>C \<in> components S\<close> \<open>C \<subseteq> S\<close> fnc in_components_nonempty by blast
    have "f holomorphic_on C"
      by (metis holf holomorphic_on_subset \<open>C \<subseteq> S\<close>)
    then have "open (f ` (C \ U))"
      by (meson C \<open>open U\<close> inf_le1 nf open_Int open_mapping_thm)
  } ultimately show ?thesis
    by force
qed

corollary\<^marker>\<open>tag unimportant\<close> open_mapping_thm3:
  assumes "f holomorphic_on S"
      and "open S" and  "inj_on f S"
    shows  "open (f ` S)"
  by (meson assms inj_on_subset injective_not_constant open_mapping_thm2 order.refl)

subsection\<open>Maximum modulus principle\<close>

text\<open>If \<^term>\<open>f\<close> is holomorphic, then its norm (modulus) cannot exhibit a true local maximum that is
   properly within the domain of \<^term>\<open>f\<close>.\<close>

proposition maximum_modulus_principle:
  assumes holf: "f holomorphic_on S"
      and S: "open S" and "connected S"
      and "open U" and "U \ S" and "\ \ U"
      and no: "\z. z \ U \ norm(f z) \ norm(f \)"
    shows "f constant_on S"
proof (rule ccontr)
  assume "\ f constant_on S"
  then have "open (f ` U)"
    using open_mapping_thm assms by blast
  moreover have "\ open (f ` U)"
  proof -
    have "\t. cmod (f \ - t) < e \ t \ f ` U" if "0 < e" for e
      using that
      apply (rule_tac x="if 0 < Re(f \) then f \ + (e/2) else f \ - (e/2)" in exI)
      apply (simp add: dist_norm)
      apply (fastforce simp: cmod_Re_le_iff dest!: no dest: sym)
      done
    then show ?thesis
      unfolding open_contains_ball by (metis \<open>\<xi> \<in> U\<close> contra_subsetD dist_norm imageI mem_ball)
  qed
  ultimately show False
    by blast
qed

proposition maximum_modulus_frontier:
  assumes holf: "f holomorphic_on (interior S)"
      and contf: "continuous_on (closure S) f"
      and bos: "bounded S"
      and leB: "\z. z \ frontier S \ norm(f z) \ B"
      and "\ \ S"
    shows "norm(f \) \ B"
proof -
  have "compact (closure S)" using bos
    by (simp add: bounded_closure compact_eq_bounded_closed)
  moreover have "continuous_on (closure S) (cmod \ f)"
    using contf continuous_on_compose continuous_on_norm_id by blast
  ultimately obtain z where "z \ closure S" and z: "\y. y \ closure S \ (cmod \ f) y \ (cmod \ f) z"
    using continuous_attains_sup [of "closure S" "norm o f"] \<open>\<xi> \<in> S\<close> by auto
  then consider "z \ frontier S" | "z \ interior S" using frontier_def by auto
  then have "norm(f z) \ B"
  proof cases
    case 1 then show ?thesis using leB by blast
  next
    case 2
    have "f constant_on (connected_component_set (interior S) z)"
    proof (rule maximum_modulus_principle)
      show "f holomorphic_on connected_component_set (interior S) z"
        by (metis connected_component_subset holf holomorphic_on_subset)
      show zin: "z \ connected_component_set (interior S) z"
        by (simp add: 2)
      show "\W. W \ connected_component_set (interior S) z \ cmod (f W) \ cmod (f z)"
        using closure_def connected_component_subset z by fastforce
    qed (auto simp: open_connected_component)
    then obtain c where c: "\w. w \ connected_component_set (interior S) z \ f w = c"
      by (auto simp: constant_on_def)
    have "f ` closure(connected_component_set (interior S) z) \ {c}"
    proof (rule image_closure_subset)
      show "continuous_on (closure (connected_component_set (interior S) z)) f"
        by (meson closure_mono connected_component_subset contf continuous_on_subset interior_subset)
    qed (use c in auto)
    then have cc: "\w. w \ closure(connected_component_set (interior S) z) \ f w = c" by blast
    have "connected_component (interior S) z z"
      by (simp add: "2")
    moreover have "connected_component_set (interior S) z \ UNIV"
      by (metis bos bounded_interior connected_component_eq_UNIV not_bounded_UNIV)
    ultimately have "frontier(connected_component_set (interior S) z) \ {}"
      by (meson "2" connected_component_eq_empty frontier_not_empty)
    then obtain w where w: "w \ frontier(connected_component_set (interior S) z)"
       by auto
    then have "norm (f z) = norm (f w)"  by (simp add: "2" c cc frontier_def)
    also have "\ \ B"
      using w frontier_interior_subset frontier_of_connected_component_subset
      by (blast intro: leB)
    finally show ?thesis .
  qed
  then show ?thesis
    using z \<open>\<xi> \<in> S\<close> closure_subset by fastforce
qed

corollary\<^marker>\<open>tag unimportant\<close> maximum_real_frontier:
  assumes holf: "f holomorphic_on (interior S)"
    and contf: "continuous_on (closure S) f"
    and bos: "bounded S"
    and leB: "\z. z \ frontier S \ Re(f z) \ B"
    and "\ \ S"
  shows "Re(f \) \ B"
  using maximum_modulus_frontier [of "exp o f" S "exp B"]
    Transcendental.continuous_on_exp holomorphic_on_compose holomorphic_on_exp assms
  by auto

subsection\<^marker>\<open>tag unimportant\<close> \<open>Factoring out a zero according to its order\<close>

lemma holomorphic_factor_order_of_zero:
  assumes holf: "f holomorphic_on S"
      and os: "open S"
      and "\ \ S" "0 < n"
      and dnz: "(deriv ^^ n) f \ \ 0"
      and dfz: "\i. \0 < i; i < n\ \ (deriv ^^ i) f \ = 0"
   obtains g r where "0 < r"
                "g holomorphic_on ball \ r"
                "\w. w \ ball \ r \ f w - f \ = (w - \)^n * g w"
                "\w. w \ ball \ r \ g w \ 0"
proof -
  obtain r where "r>0" and r: "ball \ r \ S" using assms by (blast elim!: openE)
  then have holfb: "f holomorphic_on ball \ r"
    using holf holomorphic_on_subset by blast
  define g where "g w = suminf (\i. (deriv ^^ (i + n)) f \ / (fact(i + n)) * (w - \)^i)" for w
  have sumsg: "(\i. (deriv ^^ (i + n)) f \ / (fact(i + n)) * (w - \)^i) sums g w"
   and feq: "f w - f \ = (w - \)^n * g w"
       if w: "w \ ball \ r" for w
  proof -
    define powf where "powf = (\i. (deriv ^^ i) f \/(fact i) * (w - \)^i)"
    have [simp]: "powf 0 = f \"
      by (simp add: powf_def)
    have sing: "{.. = 0 then {} else {0})"
      unfolding powf_def using \<open>0 < n\<close> dfz by (auto simp: dfz; metis funpow_0 not_gr0)
    have "powf sums f w"
      unfolding powf_def by (rule holomorphic_power_series [OF holfb w])
    moreover have "(\i"
      by (subst sum.setdiff_irrelevant [symmetric]; simp add: dfz sing)
    ultimately have fsums: "(\i. powf (i+n)) sums (f w - f \)"
      using w sums_iff_shift' by metis
    then have *: "summable (\i. (w - \) ^ n * ((deriv ^^ (i + n)) f \ * (w - \) ^ i / fact (i + n)))"
      unfolding powf_def using sums_summable
      by (auto simp: power_add mult_ac)
    have "summable (\i. (deriv ^^ (i + n)) f \ * (w - \) ^ i / fact (i + n))"
    proof (cases "w=\")
      case False then show ?thesis
        using summable_mult [OF *, of "1 / (w - \) ^ n"] by simp
    next
      case True then show ?thesis
        by (auto simp: Power.semiring_1_class.power_0_left intro!: summable_finite [of "{0}"]
                 split: if_split_asm)
    qed
    then show sumsg: "(\i. (deriv ^^ (i + n)) f \ / (fact(i + n)) * (w - \)^i) sums g w"
      by (simp add: summable_sums_iff g_def)
    show "f w - f \ = (w - \)^n * g w"
      using sums_mult [OF sumsg, of "(w - \) ^ n"]
      by (intro sums_unique2 [OF fsums]) (auto simp: power_add mult_ac powf_def)
  qed
  then have holg: "g holomorphic_on ball \ r"
    by (meson sumsg power_series_holomorphic)
  then have contg: "continuous_on (ball \ r) g"
    by (blast intro: holomorphic_on_imp_continuous_on)
  have "g \ \ 0"
    using dnz unfolding g_def
    by (subst suminf_finite [of "{0}"]) auto
  obtain d where "0 < d" and d: "\w. w \ ball \ d \ g w \ 0"
    using \<open>0 < r\<close> continuous_on_avoid [OF contg _ \<open>g \<xi> \<noteq> 0\<close>]
    by (metis centre_in_ball le_cases mem_ball mem_ball_leI)
  show ?thesis
  proof
    show "g holomorphic_on ball \ (min r d)"
      using holg by (auto simp: feq holomorphic_on_subset subset_ball d)
  qed (use \<open>0 < r\<close> \<open>0 < d\<close> in \<open>auto simp: feq d\<close>)
qed

lemma holomorphic_factor_order_of_zero_strong:
  assumes holf: "f holomorphic_on S" "open S"  "\ \ S" "0 < n"
      and "(deriv ^^ n) f \ \ 0"
      and "\i. \0 < i; i < n\ \ (deriv ^^ i) f \ = 0"
   obtains g r where "0 < r"
                "g holomorphic_on ball \ r"
                "\w. w \ ball \ r \ f w - f \ = ((w - \) * g w) ^ n"
                "\w. w \ ball \ r \ g w \ 0"
proof -
  obtain g r where "0 < r"
               and holg: "g holomorphic_on ball \ r"
               and feq: "\w. w \ ball \ r \ f w - f \ = (w - \)^n * g w"
               and gne: "\w. w \ ball \ r \ g w \ 0"
    by (auto intro: holomorphic_factor_order_of_zero [OF assms])
  have con: "continuous_on (ball \ r) (\z. deriv g z / g z)"
    by (rule continuous_intros) (auto simp: gne holg holomorphic_deriv holomorphic_on_imp_continuous_on)
  have cd: "(\z. deriv g z / g z) field_differentiable at x" if "dist \ x < r" for x
  proof (intro derivative_intros)
    show "deriv g field_differentiable at x"
      using that holg mem_ball by (blast intro: holomorphic_deriv holomorphic_on_imp_differentiable_at)
    show "g field_differentiable at x"
      by (metis that open_ball at_within_open holg holomorphic_on_def mem_ball)
    qed (simp add: gne that)
    obtain h where h: "\x. x \ ball \ r \ (h has_field_derivative deriv g x / g x) (at x)"
      using holomorphic_convex_primitive [of "ball \ r" "{}" "\z. deriv g z / g z"]
      by (metis (no_types, lifting) Diff_empty at_within_interior cd con convex_ball infinite_imp_nonempty interior_ball mem_ball)
  then have "continuous_on (ball \ r) h"
    by (metis open_ball holomorphic_on_imp_continuous_on holomorphic_on_open)
  then have con: "continuous_on (ball \ r) (\x. exp (h x) / g x)"
    by (auto intro!: continuous_intros simp add: holg holomorphic_on_imp_continuous_on gne)
  have gfd: "dist \ x < r \ g field_differentiable at x" if "dist \ x < r" for x
    using holg holomorphic_on_imp_differentiable_at by auto
  have 0: "dist \ x < r \ ((\x. exp (h x) / g x) has_field_derivative 0) (at x)" for x
    by (rule gfd h derivative_eq_intros DERIV_deriv_iff_field_differentiable [THEN iffD2] | simp add: gne)+
  obtain c where c: "\x. x \ ball \ r \ exp (h x) / g x = c"
    by (rule DERIV_zero_connected_constant [of "ball \ r" "{}" "\x. exp(h x) / g x"]) (auto simp: con 0)
  have hol: "(\z. exp ((Ln (inverse c) + h z) / of_nat n)) holomorphic_on ball \ r"
  proof (intro holomorphic_intros holomorphic_on_compose [unfolded o_def, where g = exp])
    show "h holomorphic_on ball \ r"
      using h holomorphic_on_open by blast
  qed (use \<open>0 < n\<close> in auto)
  show ?thesis
  proof
    show "\w. w \ ball \ r \ f w - f \ = ((w - \) * exp ((Ln (inverse c) + h w) / of_nat n)) ^ n"
      using \<open>0 < n\<close>
      by (auto simp: feq power_mult_distrib exp_divide_power_eq exp_add gne simp flip: c)
  qed (use hol \<open>0 < r\<close> in auto)
qed

lemma
  fixes k :: "'a::wellorder"
  assumes a_def: "a == LEAST x. P x" and P: "P k"
  shows def_LeastI: "P a" and def_Least_le: "a \ k"
  unfolding a_def
  by (rule LeastI Least_le; rule P)+

lemma holomorphic_factor_zero_nonconstant:
  assumes holf: "f holomorphic_on S" and S: "open S" "connected S"
      and "\ \ S" "f \ = 0"
      and nonconst: "\ f constant_on S"
   obtains g r n
      where "0 < n"  "0 < r"  "ball \ r \ S"
            "g holomorphic_on ball \ r"
            "\w. w \ ball \ r \ f w = (w - \)^n * g w"
            "\w. w \ ball \ r \ g w \ 0"
proof (cases "\n>0. (deriv ^^ n) f \ = 0")
  case True then show ?thesis
    using holomorphic_fun_eq_const_on_connected [OF holf S _ \<open>\<xi> \<in> S\<close>] nonconst by (simp add: constant_on_def)
next
  case False
  then obtain n0 where "n0 > 0" and n0: "(deriv ^^ n0) f \ \ 0" by blast
  obtain r0 where "r0 > 0" "ball \ r0 \ S" using S openE \\ \ S\ by auto
  define n where "n \ LEAST n. (deriv ^^ n) f \ \ 0"
  have n_ne: "(deriv ^^ n) f \ \ 0"
    by (rule def_LeastI [OF n_def]) (rule n0)
  then have "0 < n" using \<open>f \<xi> = 0\<close>
    using funpow_0 by fastforce
  have n_min: "\k. k < n \ (deriv ^^ k) f \ = 0"
    using def_Least_le [OF n_def] not_le by blast
  then obtain g r1
    where g: "0 < r1" "g holomorphic_on ball \ r1"
          and geq: "\w. w \ ball \ r1 \ f w = (w - \) ^ n * g w"
          and g0: "\w. w \ ball \ r1 \ g w \ 0"
    by (auto intro: holomorphic_factor_order_of_zero [OF holf \<open>open S\<close> \<open>\<xi> \<in> S\<close> \<open>n > 0\<close> n_ne] simp: \<open>f \<xi> = 0\<close>)
  show ?thesis
  proof
    show "g holomorphic_on ball \ (min r0 r1)"
      using g by auto
    show "\w. w \ ball \ (min r0 r1) \ f w = (w - \) ^ n * g w"
      by (simp add: geq)
  qed (use \<open>0 < n\<close> \<open>0 < r0\<close> \<open>0 < r1\<close> \<open>ball \<xi> r0 \<subseteq> S\<close> g0 in auto)
qed

lemma holomorphic_lower_bound_difference:
  assumes holf: "f holomorphic_on S" and S: "open S" "connected S"
      and "\ \ S" and "\ \ S"
      and fne: "f \ \ f \"
   obtains k n r
      where "0 < k"  "0 < r"
            "ball \ r \ S"
            "\w. w \ ball \ r \ k * norm(w - \)^n \ norm(f w - f \)"
proof -
  define n where "n = (LEAST n. 0 < n \ (deriv ^^ n) f \ \ 0)"
  obtain n0 where "0 < n0" and n0: "(deriv ^^ n0) f \ \ 0"
    using fne holomorphic_fun_eq_const_on_connected [OF holf S] \<open>\<xi> \<in> S\<close> \<open>\<phi> \<in> S\<close> by blast
  then have "0 < n" and n_ne: "(deriv ^^ n) f \ \ 0"
    unfolding n_def by (metis (mono_tags, lifting) LeastI)+
  have n_min: "\k. \0 < k; k < n\ \ (deriv ^^ k) f \ = 0"
    unfolding n_def by (blast dest: not_less_Least)
  then obtain g r
    where "0 < r" and holg: "g holomorphic_on ball \ r"
      and fne: "\w. w \ ball \ r \ f w - f \ = (w - \) ^ n * g w"
      and gnz: "\w. w \ ball \ r \ g w \ 0"
      by (auto intro: holomorphic_factor_order_of_zero  [OF holf \<open>open S\<close> \<open>\<xi> \<in> S\<close> \<open>n > 0\<close> n_ne])
  obtain e where "e>0" and e: "ball \ e \ S" using assms by (blast elim!: openE)
  then have holfb: "f holomorphic_on ball \ e"
    using holf holomorphic_on_subset by blast
  define d where "d = (min e r) / 2"
  have "0 < d" using \<open>0 < r\<close> \<open>0 < e\<close> by (simp add: d_def)
  have "d < r"
    using \<open>0 < r\<close> by (auto simp: d_def)
  then have cbb: "cball \ d \ ball \ r"
    by (auto simp: cball_subset_ball_iff)
  then have "g holomorphic_on cball \ d"
    by (rule holomorphic_on_subset [OF holg])
  then have "closed (g ` cball \ d)"
    by (simp add: compact_imp_closed compact_continuous_image holomorphic_on_imp_continuous_on)
  moreover have "g ` cball \ d \ {}"
    using \<open>0 < d\<close> by auto
  ultimately obtain x where x: "x \ g ` cball \ d" and "\y. y \ g ` cball \ d \ dist 0 x \ dist 0 y"
    by (rule distance_attains_inf) blast
  then have leg: "\w. w \ cball \ d \ norm x \ norm (g w)"
    by auto
  have "ball \ d \ cball \ d" by auto
  also have "\ \ ball \ e" using \0 < d\ d_def by auto
  also have "\ \ S" by (rule e)
  finally have dS: "ball \ d \ S" .
  have "x \ 0" using gnz x \d < r\ by auto
  show thesis
  proof
    show "\w. w \ ball \ d \ cmod x * cmod (w - \) ^ n \ cmod (f w - f \)"
      using \<open>d < r\<close> leg by (auto simp: fne norm_mult norm_power algebra_simps mult_right_mono)
  qed (use dS \<open>x \<noteq> 0\<close> \<open>d > 0\<close> in auto)
qed

lemma
  assumes holf: "f holomorphic_on (S - {\})" and \: "\ \ interior S"
    shows holomorphic_on_extend_lim:
          "(\g. g holomorphic_on S \ (\z \ S - {\}. g z = f z)) \
           ((\<lambda>z. (z - \<xi>) * f z) \<longlongrightarrow> 0) (at \<xi>)"
          (is "?P = ?Q")
     and holomorphic_on_extend_bounded:
          "(\g. g holomorphic_on S \ (\z \ S - {\}. g z = f z)) \
           (\<exists>B. eventually (\<lambda>z. norm(f z) \<le> B) (at \<xi>))"
          (is "?P = ?R")
proof -
  obtain \<delta> where "0 < \<delta>" and \<delta>: "ball \<xi> \<delta> \<subseteq> S"
    using \<xi> mem_interior by blast
  have "?R" if holg: "g holomorphic_on S" and gf: "\z. z \ S - {\} \ g z = f z" for g
  proof -
    have \<section>: "cmod (f x) \<le> cmod (g \<xi>) + 1" if "x \<noteq> \<xi>" "dist x \<xi> < \<delta>" "dist (g x) (g \<xi>) < 1" for x
    proof -
      have "x \ S"
        by (metis \<delta> dist_commute mem_ball subsetD that(2))
      with that gf [of x] show ?thesis
        using norm_triangle_ineq2 [of "f x" "g \"] dist_complex_def by auto
    qed
    then have *: "\\<^sub>F z in at \. dist (g z) (g \) < 1 \ cmod (f z) \ cmod (g \) + 1"
      using \<open>0 < \<delta>\<close> eventually_at by blast
    have "continuous_on (interior S) g"
      by (meson continuous_on_subset holg holomorphic_on_imp_continuous_on interior_subset)
    then have "\x. x \ interior S \ (g \ g x) (at x)"
      using continuous_on_interior continuous_within holg holomorphic_on_imp_continuous_on by blast
    then have "(g \ g \) (at \)"
      by (simp add: \<xi>)
    then have "\\<^sub>F z in at \. cmod (f z) \ cmod (g \) + 1"
      by (rule eventually_mp [OF * tendstoD [where e=1]], auto)
    then show ?thesis
      by blast
  qed
  moreover have "?Q" if "\\<^sub>F z in at \. cmod (f z) \ B" for B
    by (rule lim_null_mult_right_bounded [OF _ that]) (simp add: LIM_zero)
  moreover have "?P" if "(\z. (z - \) * f z) \\\ 0"
  proof -
    define h where [abs_def]: "h z = (z - \)^2 * f z" for z
    have "(\y. (y - \)\<^sup>2 * f y / (y - \)) \\\ 0"
      by (simp add: LIM_cong power2_eq_square that)
    then have h0: "(h has_field_derivative 0) (at \)"
      by (simp add: h_def has_field_derivative_iff)
    have holh: "h holomorphic_on S"
    proof (simp add: holomorphic_on_def, clarify)
      fix z assume "z \ S"
      show "h field_differentiable at z within S"
      proof (cases "z = \")
        case True then show ?thesis
          using field_differentiable_at_within field_differentiable_def h0 by blast
      next
        case False
        then have "f field_differentiable at z within S"
          using holomorphic_onD [OF holf, of z] \<open>z \<in> S\<close>
          unfolding field_differentiable_def has_field_derivative_iff
          by (force intro: exI [where x="dist \ z"] elim: Lim_transform_within_set [unfolded eventually_at])
        then show ?thesis
          by (simp add: h_def power2_eq_square derivative_intros)
      qed
    qed
    define g where [abs_def]: "g z = (if z = \ then deriv h \ else (h z - h \) / (z - \))" for z
    have \<section>: "\<forall>z\<in>S - {\<xi>}. (g z - g \<xi>) / (z - \<xi>) = f z"
      using h0 by (auto simp: g_def power2_eq_square divide_simps DERIV_imp_deriv h_def)
    have "g holomorphic_on S"
      unfolding g_def by (rule pole_lemma [OF holh \<xi>])
    then have "(\z. if z = \ then deriv g \ else (g z - g \) / (z - \)) holomorphic_on S"
      using \<xi> pole_lemma by blast
    then show ?thesis
      using "\

" by (smt (verit, best) DiffD2 singletonI)
    qed
  ultimately show "?P = ?Q" and "?P = ?R"
    by meson+
qed

lemma pole_at_infinity:
  assumes holf: "f holomorphic_on UNIV" and lim: "((inverse o f) \ l) at_infinity"
  obtains a n where "\z. f z = (\i\n. a i * z^i)"
proof (cases "l = 0")
  case False
  show thesis
  proof
    show "f z = (\i\0. inverse l * z ^ i)" for z
      using False tendsto_inverse [OF lim] by (simp add: Liouville_weak [OF holf])
  qed
next
  case True
  then have [simp]: "l = 0" .
  show ?thesis
  proof (cases "\r. 0 < r \ (\z \ ball 0 r - {0}. f(inverse z) \ 0)")
    case True
      then obtain r where "0 < r" and r: "\z. z \ ball 0 r - {0} \ f(inverse z) \ 0"
             by auto
      have 1: "inverse \ f \ inverse holomorphic_on ball 0 r - {0}"
        by (rule holomorphic_on_compose holomorphic_intros holomorphic_on_subset [OF holf] | force simp: r)+
      have 2: "0 \ interior (ball 0 r)"
        using \<open>0 < r\<close> by simp
      obtain g where holg: "g holomorphic_on ball 0 r"
                 and geq: "\z. z \ ball 0 r - {0} \ g z = (inverse \ f \ inverse) z"
        using tendstoD [OF lim [unfolded lim_at_infinity_0] zero_less_one] holomorphic_on_extend_bounded [OF 1 2]
        by (smt (verit, del_insts) \<open>l = 0\<close> eventually_mono norm_conv_dist)
      have ifi0: "(inverse \ f \ inverse) \0\ 0"
        using \<open>l = 0\<close> lim lim_at_infinity_0 by blast
      have g2g0: "g \0\ g 0"
        using \<open>0 < r\<close> centre_in_ball continuous_at continuous_on_eq_continuous_at holg
        by (blast intro: holomorphic_on_imp_continuous_on)
      have g2g1: "g \0\ 0"
      proof (rule Lim_transform_within_open [OF ifi0 open_ball])
        show "\x. \x \ ball 0 r; x \ 0\ \ (inverse \ f \ inverse) x = g x"
          by (auto simp: geq)
      qed (auto simp: \<open>0 < r\<close>)
      have [simp]: "g 0 = 0"
        by (rule tendsto_unique [OF _ g2g0 g2g1]) simp
      have "ball 0 r - {0::complex} \ {}"
        using \<open>0 < r\<close> by (metis "2" Diff_iff insert_Diff interior_ball interior_singleton)
      then obtain w::complex where "w \ 0" and w: "norm w < r" by force
      then have "g w \ 0" by (simp add: geq r)
      obtain B n e where "0 < B" "0 < e" "e \ r"
                     and leg: "\w. norm w < e \ B * cmod w ^ n \ cmod (g w)"
      proof (rule holomorphic_lower_bound_difference [OF holg open_ball connected_ball])
        show "g w \ g 0"
          by (simp add: \<open>g w \<noteq> 0\<close>)
        show "w \ ball 0 r"
          using mem_ball_0 w by blast
      qed (use \<open>0 < r\<close> in \<open>auto simp: ball_subset_ball_iff\<close>)
      have \<section>: "cmod (f z) \<le> cmod z ^ n / B" if "2/e \<le> cmod z" for z
      proof -
        have ize: "inverse z \ ball 0 e - {0}" using that \0 < e\
          by (auto simp: norm_divide field_split_simps algebra_simps)
        then have [simp]: "z \ 0" and izr: "inverse z \ ball 0 r - {0}" using \e \ r\
          by auto
        then have [simp]: "f z \ 0"
          using r [of "inverse z"] by simp
        have [simp]: "f z = inverse (g (inverse z))"
          using izr geq [of "inverse z"] by simp
        show ?thesis using ize leg [of "inverse z"]  \<open>0 < B\<close>  \<open>0 < e\<close>
          by (simp add: field_split_simps norm_divide algebra_simps)
      qed
      show thesis
      proof
        show "f z = (\i\n. (deriv ^^ i) f 0 / fact i * z ^ i)" for z
          using \<section> by (rule_tac A = "2/e" and B = "1/B" in Liouville_polynomial [OF holf], simp)
      qed
  next
    case False
    then have fi0: "\r. r > 0 \ \z\ball 0 r - {0}. f (inverse z) = 0"
      by simp
    have fz0: "f z = 0" if "0 < r" and lt1: "\x. x \ 0 \ cmod x < r \ inverse (cmod (f (inverse x))) < 1"
              for z r
    proof -
      have f0: "(f \ 0) at_infinity"
      proof -
        have DIM_complex[intro]: "2 \ DIM(complex)" \ \should not be necessary!\
          by simp
        have "f (inverse x) \ 0 \ x \ 0 \ cmod x < r \ 1 < cmod (f (inverse x))" for x
          using lt1[of x] by (auto simp: field_simps)
        then have **: "cmod (f (inverse x)) \ 1 \ x \ 0 \ cmod x < r \ f (inverse x) = 0" for x
          by force
        then have *: "(f \ inverse) ` (ball 0 r - {0}) \ {0} \ - ball 0 1"
          by force
        have "continuous_on (inverse ` (ball 0 r - {0})) f"
          using continuous_on_subset holf holomorphic_on_imp_continuous_on by blast
        then have "connected ((f \ inverse) ` (ball 0 r - {0}))"
          using connected_punctured_ball
          by (intro connected_continuous_image continuous_intros; force)
        then have "{0} \ (f \ inverse) ` (ball 0 r - {0}) = {} \ - ball 0 1 \ (f \ inverse) ` (ball 0 r - {0}) = {}"
          by (rule connected_closedD) (use * in auto)
        then have "f (inverse w) = 0" if "w \ 0" "cmod w < r" for w
          using **[of w] fi0 \<open>0 < r\<close>  that by force
        then show ?thesis
          unfolding lim_at_infinity_0
          using eventually_at \<open>r > 0\<close> by (force simp: intro: tendsto_eventually)
      qed
      obtain w where "w \ ball 0 r - {0}" and "f (inverse w) = 0"
        using False \<open>0 < r\<close> by blast
      then show ?thesis
        by (auto simp: f0 Liouville_weak [OF holf, of 0])
    qed
    show thesis
    proof
      show "\z. f z = (\i\0. 0 * z ^ i)"
        using lim
        apply (simp add: lim_at_infinity_0 Lim_at dist_norm norm_inverse)
        using fz0 zero_less_one by blast
    qed
  qed
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>Entire proper functions are precisely the non-trivial polynomials\<close>

lemma proper_map_polyfun:
    fixes c :: "nat \ 'a::{real_normed_div_algebra,heine_borel}"
  assumes "closed S" and "compact K" and c: "c i \ 0" "1 \ i" "i \ n"
    shows "compact (S \ {z. (\i\n. c i * z^i) \ K})"
proof -
  obtain B where "B > 0" and B: "\x. x \ K \ norm x \ B"
    by (metis compact_imp_bounded \<open>compact K\<close> bounded_pos)
  have *: "norm x \ b"
            if "\x. b \ norm x \ B + 1 \ norm (\i\n. c i * x ^ i)"
               "(\i\n. c i * x ^ i) \ K" for b x
  proof -
    have "norm (\i\n. c i * x ^ i) \ B"
      using B that by blast
    moreover have "\ B + 1 \ B"
      by simp
    ultimately show "norm x \ b"
      using that by (metis (no_types) less_eq_real_def not_less order_trans)
  qed
  have "bounded {z. (\i\n. c i * z ^ i) \ K}"
    using Limits.polyfun_extremal [where c=c and B="B+1", OF c]
    by (auto simp: bounded_pos eventually_at_infinity_pos *)
  moreover have "closed ((\z. (\i\n. c i * z ^ i)) -` K)"
    using \<open>compact K\<close> compact_eq_bounded_closed
    by (intro allI continuous_closed_vimage continuous_intros; force)
  ultimately show ?thesis
    using closed_Int_compact [OF \<open>closed S\<close>] compact_eq_bounded_closed
    by (auto simp add: vimage_def)
qed

lemma proper_map_polyfun_univ:
    fixes c :: "nat \ 'a::{real_normed_div_algebra,heine_borel}"
  assumes "compact K" "c i \ 0" "1 \ i" "i \ n"
    shows "compact ({z. (\i\n. c i * z^i) \ K})"
  using proper_map_polyfun [of UNIV K c i n] assms by simp

lemma proper_map_polyfun_eq:
  assumes "f holomorphic_on UNIV"
    shows "(\k. compact k \ compact {z. f z \ k}) \
           (\<exists>c n. 0 < n \<and> (c n \<noteq> 0) \<and> f = (\<lambda>z. \<Sum>i\<le>n. c i * z^i))"
          (is "?lhs = ?rhs")
proof
  assume compf [rule_format]: ?lhs
  have 2: "\k. 0 < k \ a k \ 0 \ f = (\z. \i \ k. a i * z ^ i)"
        if "\z. f z = (\i\n. a i * z ^ i)" for a n
  proof (cases "\i\n. 0 a i = 0")
    case True
    then have [simp]: "\z. f z = a 0"
      by (simp add: that sum.atMost_shift)
    have False using compf [of "{a 0}"] by simp
    then show ?thesis ..
  next
    case False
    then obtain k where k: "0 < k" "k\n" "a k \ 0" by force
    define m where "m = (GREATEST k. k\n \ a k \ 0)"
    have m: "m\n \ a m \ 0"
      unfolding m_def
      using GreatestI_nat [where b = n] k by (metis (mono_tags, lifting))
    have [simp]: "a i = 0" if "m < i" "i \ n" for i
      using Greatest_le_nat [where b = "n" and P = "\k. k\n \ a k \ 0"]
      using m_def not_le that by auto
    have "k \ m"
      unfolding m_def
      using Greatest_le_nat [where b = n] k by (metis (mono_tags, lifting))
    with k m show ?thesis
      by (rule_tac x=m in exI) (auto simp: that comm_monoid_add_class.sum.mono_neutral_right)
  qed
  have *: "((inverse \ f) \ 0) at_infinity"
  proof (rule Lim_at_infinityI)
    fix e::real assume "0 < e"
    with compf [of "cball 0 (inverse e)"]
    show "\B. \x. B \ cmod x \ dist ((inverse \ f) x) 0 \ e"
      apply (clarsimp simp: compact_eq_bounded_closed norm_divide divide_simps mult.commute elim!: bounded_normE_less)
      by (meson linorder_not_le nle_le)
  qed
  then obtain a n where "\z. f z = (\i\n. a i * z^i)"
    using assms pole_at_infinity by blast
  with * 2 show ?rhs by blast
next
  assume ?rhs
  then obtain c n where "0 < n" "c n \ 0" "f = (\z. \i\n. c i * z ^ i)" by blast
  then have "compact {z. f z \ k}" if "compact k" for k
    by (auto intro: proper_map_polyfun_univ [OF that])
  then show ?lhs by blast
qed

subsection \<open>Relating invertibility and nonvanishing of derivative\<close>

lemma has_complex_derivative_locally_injective:
  assumes holf: "f holomorphic_on S"
      and S: "\ \ S" "open S"
      and dnz: "deriv f \ \ 0"
  obtains r where "r > 0" "ball \ r \ S" "inj_on f (ball \ r)"
proof -
  have *: "\d>0. \x. dist \ x < d \ onorm (\v. deriv f x * v - deriv f \ * v) < e" if "e > 0" for e
  proof -
    have contdf: "continuous_on S (deriv f)"
      by (simp add: holf holomorphic_deriv holomorphic_on_imp_continuous_on \<open>open S\<close>)
    obtain \<delta> where "\<delta>>0" and \<delta>: "\<And>x. \<lbrakk>x \<in> S; dist x \<xi> \<le> \<delta>\<rbrakk> \<Longrightarrow> cmod (deriv f x - deriv f \<xi>) \<le> e/2"
      using continuous_onE [OF contdf \<open>\<xi> \<in> S\<close>, of "e/2"] \<open>0 < e\<close>
      by (metis dist_complex_def half_gt_zero less_imp_le)
    have \<section>: "\<And>\<zeta> z. \<lbrakk>\<zeta> \<in> S; dist \<xi> \<zeta> < \<delta>\<rbrakk> \<Longrightarrow> cmod (deriv f \<zeta> - deriv f \<xi>) * cmod z \<le> e/2 * cmod z"
      by (intro mult_right_mono [OF \<delta>]) (auto simp: dist_commute)
    obtain \<epsilon> where "\<epsilon>>0" "ball \<xi> \<epsilon> \<subseteq> S"
      by (metis openE [OF \<open>open S\<close> \<open>\<xi> \<in> S\<close>])
    with \<open>\<delta>>0\<close> have "\<exists>\<delta>>0. \<forall>x. dist \<xi> x < \<delta> \<longrightarrow> onorm (\<lambda>v. deriv f x * v - deriv f \<xi> * v) \<le> e/2"
      using \<section>
      apply (rule_tac x="min \ \" in exI)
      apply (intro conjI allI impI Operator_Norm.onorm_le)
      apply (force simp: mult_right_mono norm_mult [symmetric] left_diff_distrib \<delta>)+
      done
    with \<open>e>0\<close> show ?thesis by force
  qed
  have "inj ((*) (deriv f \))"
    using dnz by simp
  then obtain g' where g': "linear g'" "g' \ (*) (deriv f \) = id"
    using linear_injective_left_inverse [of "(*) (deriv f \)"] by auto

  have fder: "\x. x \ S \ (f has_derivative (*) (deriv f x)) (at x)"
    using \<open>open S\<close> has_field_derivative_imp_has_derivative holf holomorphic_derivI by blast
  show ?thesis
    apply (rule has_derivative_locally_injective [OF S, where f=f and f' = "\z h. deriv f z * h" and g' = g'])
    using g' * by (simp_all add: fder linear_conv_bounded_linear that)
qed

lemma has_complex_derivative_locally_invertible:
  assumes holf: "f holomorphic_on S"
      and S: "\ \ S" "open S"
      and dnz: "deriv f \ \ 0"
  obtains r where "r > 0" "ball \ r \ S" "open (f ` (ball \ r))" "inj_on f (ball \ r)"
proof -
  obtain r where "r > 0" "ball \ r \ S" "inj_on f (ball \ r)"
    by (blast intro: that has_complex_derivative_locally_injective [OF assms])
  then have \<xi>: "\<xi> \<in> ball \<xi> r" by simp
  then have nc: "\ f constant_on ball \ r"
    using \<open>inj_on f (ball \<xi> r)\<close> injective_not_constant by fastforce
  have holf': "f holomorphic_on ball \ r"
    using \<open>ball \<xi> r \<subseteq> S\<close> holf holomorphic_on_subset by blast
  have "open (f ` ball \ r)"
    by (simp add: \<open>inj_on f (ball \<xi> r)\<close> holf' open_mapping_thm3)
  then show ?thesis
    using \<open>0 < r\<close> \<open>ball \<xi> r \<subseteq> S\<close> \<open>inj_on f (ball \<xi> r)\<close> that  by blast
qed

lemma holomorphic_injective_imp_regular:
  assumes holf: "f holomorphic_on S"
      and "open S" and injf: "inj_on f S"
      and "\ \ S"
    shows "deriv f \ \ 0"
proof -
  obtain r where "r>0" and r: "ball \ r \ S" using assms by (blast elim!: openE)
  have holf': "f holomorphic_on ball \ r"
    using \<open>ball \<xi> r \<subseteq> S\<close> holf holomorphic_on_subset by blast
  show ?thesis
  proof (cases "\n>0. (deriv ^^ n) f \ = 0")
    case True
    have fcon: "f w = f \" if "w \ ball \ r" for w
      by (meson open_ball True \<open>0 < r\<close> centre_in_ball connected_ball holf'
                holomorphic_fun_eq_const_on_connected that)
    have False
      using fcon [of "\ + r/2"] \0 < r\ r injf unfolding inj_on_def
      by (metis \<open>\<xi> \<in> S\<close> contra_subsetD dist_commute fcon mem_ball perfect_choose_dist)
    then show ?thesis ..
  next
    case False
    then obtain n0 where n0: "n0 > 0 \ (deriv ^^ n0) f \ \ 0" by blast
    define n where [abs_def]: "n = (LEAST n. n > 0 \ (deriv ^^ n) f \ \ 0)"
    have n_ne: "n > 0" "(deriv ^^ n) f \ \ 0"
      using def_LeastI [OF n_def n0] by auto
    have n_min: "\k. 0 < k \ k < n \ (deriv ^^ k) f \ = 0"
      using def_Least_le [OF n_def] not_le by auto
    obtain g \<delta> where "0 < \<delta>"
             and holg: "g holomorphic_on ball \ \"
             and fd: "\w. w \ ball \ \ \ f w - f \ = ((w - \) * g w) ^ n"
             and gnz: "\w. w \ ball \ \ \ g w \ 0"
      by (blast intro: n_min holomorphic_factor_order_of_zero_strong [OF holf \<open>open S\<close> \<open>\<xi> \<in> S\<close> n_ne])
    show ?thesis
    proof (cases "n=1")
      case True
      with n_ne show ?thesis by auto
    next
      case False
      have "g holomorphic_on ball \ (min r \)"
        using holg by (simp add: holomorphic_on_subset subset_ball)
      then have holgw: "(\w. (w - \) * g w) holomorphic_on ball \ (min r \)"
        by (intro holomorphic_intros)
      have gd: "\w. dist \ w < \ \ (g has_field_derivative deriv g w) (at w)"
        using holg
        by (simp add: DERIV_deriv_iff_field_differentiable holomorphic_on_def at_within_open_NO_MATCH)
      have *: "\w. w \ ball \ (min r \)
            \<Longrightarrow> ((\<lambda>w. (w - \<xi>) * g w) has_field_derivative ((w - \<xi>) * deriv g w + g w))
                (at w)"
        by (rule gd derivative_eq_intros | simp)+
      have [simp]: "deriv (\w. (w - \) * g w) \ \ 0"
        using * [of \<xi>] \<open>0 < \<delta>\<close> \<open>0 < r\<close> by (simp add: DERIV_imp_deriv gnz)
      obtain T where "\ \ T" "open T" and Tsb: "T \ ball \ (min r \)" and oimT: "open ((\w. (w - \) * g w) ` T)"
        using \<open>0 < r\<close> \<open>0 < \<delta>\<close> has_complex_derivative_locally_invertible [OF holgw, of \<xi>]
        by force
      define U where "U = (\w. (w - \) * g w) ` T"
      have "open U" by (metis oimT U_def)
      moreover have "0 \ U"
        using \<open>\<xi> \<in> T\<close> by (auto simp: U_def intro: image_eqI [where x = \<xi>])
      ultimately obtain \<epsilon> where "\<epsilon>>0" and \<epsilon>: "cball 0 \<epsilon> \<subseteq> U"
        using \<open>open U\<close> open_contains_cball by blast
      then have "\ * exp(2 * of_real pi * \ * (0/n)) \ cball 0 \"
                "\ * exp(2 * of_real pi * \ * (1/n)) \ cball 0 \"
        by (auto simp: norm_mult)
      with \<epsilon> have "\<epsilon> * exp(2 * of_real pi * \<i> * (0/n)) \<in> U"
                  "\ * exp(2 * of_real pi * \ * (1/n)) \ U" by blast+
      then obtain y0 y1 where "y0 \ T" and y0: "(y0 - \) * g y0 = \ * exp(2 * of_real pi * \ * (0/n))"
                          and "y1 \ T" and y1: "(y1 - \) * g y1 = \ * exp(2 * of_real pi * \ * (1/n))"
        by (auto simp: U_def)
      then have "y0 \ ball \ \" "y1 \ ball \ \" using Tsb by auto
      then have "f y0 - f \ = ((y0 - \) * g y0) ^ n" "f y1 - f \ = ((y1 - \) * g y1) ^ n"
        using fd by blast+
      moreover have "y0 \ y1"
        using y0 y1 \<open>\<epsilon> > 0\<close> complex_root_unity_eq_1 [of n 1] \<open>n > 0\<close> False by auto
      moreover have "T \ S"
        by (meson Tsb min.cobounded1 order_trans r subset_ball)
      ultimately have False
        using inj_onD [OF injf, of y0 y1] \<open>y0 \<in> T\<close> \<open>y1 \<in> T\<close>
        using complex_root_unity [of n 1]
        by (auto simp: y0 y1 power_mult_distrib diff_eq_eq n_ne)
      then show ?thesis ..
    qed
  qed
qed

subsubsection \<open>Hence a nice clean inverse function theorem\<close>

lemma has_field_derivative_inverse_strong:
  fixes f :: "'a::{euclidean_space,real_normed_field} \ 'a"
  shows "\DERIV f x :> f'; f' \ 0; open S; x \ S; continuous_on S f;
         \<And>z. z \<in> S \<Longrightarrow> g (f z) = z\<rbrakk>
         \<Longrightarrow> DERIV g (f x) :> inverse (f')"
  unfolding has_field_derivative_def
  by (rule has_derivative_inverse_strong [of S x f g]) auto

lemma has_field_derivative_inverse_strong_x:
  fixes f :: "'a::{euclidean_space,real_normed_field} \ 'a"
  shows  "\DERIV f (g y) :> f'; f' \ 0; open S; continuous_on S f; g y \ S; f(g y) = y;
           \<And>z. z \<in> S \<Longrightarrow> g (f z) = z\<rbrakk>
          \<Longrightarrow> DERIV g y :> inverse (f')"
  unfolding has_field_derivative_def
  by (rule has_derivative_inverse_strong_x [of S g y f]) auto

proposition holomorphic_has_inverse:
  assumes holf: "f holomorphic_on S"
      and "open S" and injf: "inj_on f S"
  obtains g where "g holomorphic_on (f ` S)"
                  "\z. z \ S \ deriv f z * deriv g (f z) = 1"
                  "\z. z \ S \ g(f z) = z"
proof -
  have ofs: "open (f ` S)"
    by (rule open_mapping_thm3 [OF assms])
  have contf: "continuous_on S f"
    by (simp add: holf holomorphic_on_imp_continuous_on)
  have *: "(the_inv_into S f has_field_derivative inverse (deriv f z)) (at (f z))" if "z \ S" for z
  proof -
    have 1: "(f has_field_derivative deriv f z) (at z)"
      using DERIV_deriv_iff_field_differentiable \<open>z \<in> S\<close> \<open>open S\<close> holf holomorphic_on_imp_differentiable_at
      by blast
    have 2: "deriv f z \ 0"
      using \<open>z \<in> S\<close> \<open>open S\<close> holf holomorphic_injective_imp_regular injf by blast
    show ?thesis
    proof (rule has_field_derivative_inverse_strong [OF 1 2 \<open>open S\<close> \<open>z \<in> S\<close>])
      show "continuous_on S f"
        by (simp add: holf holomorphic_on_imp_continuous_on)
      show "\z. z \ S \ the_inv_into S f (f z) = z"
        by (simp add: injf the_inv_into_f_f)
    qed
  qed
  show ?thesis
    proof
      show "the_inv_into S f holomorphic_on f ` S"
        by (simp add: holomorphic_on_open ofs) (blast intro: *)
    next
      fix z assume "z \ S"
      have "deriv f z \ 0"
        using \<open>z \<in> S\<close> \<open>open S\<close> holf holomorphic_injective_imp_regular injf by blast
      then show "deriv f z * deriv (the_inv_into S f) (f z) = 1"
        using * [OF \<open>z \<in> S\<close>]  by (simp add: DERIV_imp_deriv)
    next
      fix z assume "z \ S"
      show "the_inv_into S f (f z) = z"
        by (simp add: \<open>z \<in> S\<close> injf the_inv_into_f_f)
  qed
qed

subsubsection \<open> Holomorphism of covering maps and lifts.\<close>

lemma covering_space_lift_is_holomorphic:
  assumes cov: "covering_space C p S"
      and C: "open C" "p holomorphic_on C"
      and holf: "f holomorphic_on U" and fim: "f \ U \ S" and gim: "g \ U \ C"
      and contg: "continuous_on U g" and pg_f: "\x. x \ U \ p(g x) = f x"
    shows "g holomorphic_on U"
  unfolding holomorphic_on_def
proof (intro strip)
  fix z
  assume "z \ U"
  with fim have "f z \ S" by blast
  then obtain T \<V> where "f z \<in> T" and opeT: "openin (top_of_set S) T"
        and UV: "\\ = C \ p -` T"
        and "\W. W \ \ \ openin (top_of_set C) W"
        and disV: "pairwise disjnt \" and homeV: "\W. W \ \ \ \q. homeomorphism W T p q"
    using cov fim unfolding covering_space_def by meson
  then have "\W. W \ \ \ open W \ W \ C"
    by (metis \<open>open C\<close> inf_le1 open_Int openin_open)
  then obtain V where "V \ \" "g z \ V" "open V" "V \ C"
    by (metis IntI UnionE image_subset_iff vimageI UV \<open>f z \<in> T\<close> \<open>z \<in> U\<close> gim pg_f image_subset_iff_funcset)
  have holp: "p holomorphic_on V"
    using \<open>V \<subseteq> C\<close> \<open>p holomorphic_on C\<close> holomorphic_on_subset by blast
  moreover have injp: "inj_on p V"
    by (metis \<open>V \<in> \<V>\<close> homeV homeomorphism_def inj_on_inverseI)
  ultimately
  obtain p' where holp': "p' holomorphic_on (p ` V)" and pp': "\z. z \ V \ p'(p z) = z"
    using \<open>open V\<close> holomorphic_has_inverse by metis
  have "z \ U \ g -` V"
    using \<open>g z \<in> V\<close> \<open>z \<in> U\<close> by blast
  moreover have "openin (top_of_set U) (U \ g -` V)"
    using continuous_openin_preimage [OF contg gim]
    by (meson \<open>open V\<close> contg continuous_openin_preimage_eq)
  ultimately obtain \<epsilon> where "\<epsilon>>0" and e: "ball z \<epsilon> \<inter> U \<subseteq> g -` V"
    by (force simp: openin_contains_ball)
  show "g field_differentiable at z within U"
  proof (rule field_differentiable_transform_within)
    show "(0::real) < \"
      by (simp add: \<open>0 < \<epsilon>\<close>)
    show "z \ U"
      by (simp add: \<open>z \<in> U\<close>)
    show "(p' o f) x' = g x'" if "x' \ U" "dist x' z < \" for x'
      using that
      by (metis Int_iff comp_apply dist_commute e mem_ball pg_f pp' subsetD vimage_eq)
    have "open (p ` V)"
      using \<open>open V\<close> holp injp open_mapping_thm3 by force
    moreover have "f z \ p ` V"
      by (metis \<open>z \<in> U\<close> image_iff pg_f \<open>g z \<in> V\<close>)
    ultimately have "p' field_differentiable at (f z)"
      using holomorphic_on_imp_differentiable_at holp' by blast
    moreover have "f field_differentiable at z within U"
      by (metis (no_types) \<open>z \<in> U\<close> holf holomorphic_on_def)
    ultimately show "(p' o f) field_differentiable at z within U"
      by (metis (no_types) field_differentiable_at_within field_differentiable_compose_within)
  qed
qed

lemma covering_space_lift_holomorphic:
  assumes cov: "covering_space C p S"
      and C: "open C" "p holomorphic_on C"
      and f: "f holomorphic_on U" "f \ U \ S"
      and U: "simply_connected U" "locally path_connected U"
  obtains g where "g holomorphic_on U" "g \ U \ C" "\y. y \ U \ p(g y) = f y"
proof -
  obtain g where "continuous_on U g" "g \ U \ C" "\y. y \ U \ p(g y) = f y"
    using covering_space_lift [OF cov U] f holomorphic_on_imp_continuous_on by blast
  then show ?thesis
    by (metis C cov covering_space_lift_is_holomorphic f image_subset_iff_funcset that)
qed

subsection\<open>The Schwarz Lemma\<close>

lemma Schwarz1:
  assumes holf: "f holomorphic_on S"
      and contf: "continuous_on (closure S) f"
      and S: "open S" "connected S"
      and boS: "bounded S"
      and "S \ {}"
  obtains w where "w \ frontier S"
       "\z. z \ closure S \ norm (f z) \ norm (f w)"
proof -
  have connf: "continuous_on (closure S) (norm o f)"
    using contf continuous_on_compose continuous_on_norm_id by blast
  have coc: "compact (closure S)"
    by (simp add: \<open>bounded S\<close> bounded_closure compact_eq_bounded_closed)
  then obtain x where x: "x \ closure S" and xmax: "\z. z \ closure S \ norm(f z) \ norm(f x)"
    using continuous_attains_sup [OF _ _ connf] \<open>S \<noteq> {}\<close> by auto
  then show ?thesis
  proof (cases "x \ frontier S")
    case True
    then show ?thesis using that xmax by blast
  next
    case False
    then have "x \ S"
      using \<open>open S\<close> frontier_def interior_eq x by auto
    then have "f constant_on S"
    proof (rule maximum_modulus_principle [OF holf S \<open>open S\<close> order_refl])
      show "\z. z \ S \ cmod (f z) \ cmod (f x)"
        using closure_subset by (blast intro: xmax)
    qed
    then have "f constant_on (closure S)"
      by (rule constant_on_closureI [OF _ contf])
    then obtain c where c: "\x. x \ closure S \ f x = c"
      by (meson constant_on_def)
    obtain w where "w \ frontier S"
      by (metis coc all_not_in_conv assms(6) closure_UNIV frontier_eq_empty not_compact_UNIV)
    then show ?thesis
      by (simp add: c frontier_def that)
--> --------------------

--> maximum size reached

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

quality100%

¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.