Quelle Complex_Singularities.thy Sprache: Isabelle

theory Complex_Singularities
  imports Conformal_Mappings
begin

subsection \<open>Non-essential singular points\<close>

lemma at_to_0': "NO_MATCH 0 z \ at z = filtermap (\x. x + z) (at 0)"
  for z :: "'a::real_normed_vector"
  by (rule at_to_0)

lemma nhds_to_0: "nhds (x :: 'a :: real_normed_vector) = filtermap ((+) x) (nhds 0)"
proof -
  have "(\xa. xa - - x) = (+) x"
    by auto
  thus ?thesis
    using filtermap_nhds_shift[of "-x" 0] by simp
qed

lemma nhds_to_0': "NO_MATCH 0 x \ nhds (x :: 'a :: real_normed_vector) = filtermap ((+) x) (nhds 0)"
  by (rule nhds_to_0)

definition\<^marker>\<open>tag important\<close>
  is_pole :: "('a::topological_space \ 'b::real_normed_vector) \ 'a \ bool"
  where "is_pole f a = (LIM x (at a). f x :> at_infinity)"

lemma is_pole_cong:
  assumes "eventually (\x. f x = g x) (at a)" "a=b"
  shows "is_pole f a \ is_pole g b"
  unfolding is_pole_def using assms by (intro filterlim_cong,auto)

lemma is_pole_transform:
  assumes "is_pole f a" "eventually (\x. f x = g x) (at a)" "a=b"
  shows "is_pole g b"
  using is_pole_cong assms by auto

lemma is_pole_shift_iff:
  fixes f :: "('a::real_normed_vector \ 'b::real_normed_vector)"
  shows "is_pole (f \ (+) d) a = is_pole f (a + d)"
  by (metis add_diff_cancel_right' filterlim_shift_iff is_pole_def)

lemma is_pole_tendsto:
  fixes f:: "('a::topological_space \ 'b::real_normed_div_algebra)"
  shows "is_pole f x \ ((inverse o f) \ 0) (at x)"
  unfolding is_pole_def
  by (auto simp add: filterlim_inverse_at_iff[symmetric] comp_def filterlim_at)

lemma is_pole_shift_0:
  fixes f :: "('a::real_normed_vector \ 'b::real_normed_vector)"
  shows "is_pole f z \ is_pole (\x. f (z + x)) 0"
  unfolding is_pole_def by (subst at_to_0) (auto simp: filterlim_filtermap add_ac)

lemma is_pole_shift_0':
  fixes f :: "('a::real_normed_vector \ 'b::real_normed_vector)"
  shows "NO_MATCH 0 z \ is_pole f z \ is_pole (\x. f (z + x)) 0"
  by (metis is_pole_shift_0)

lemma is_pole_compose_iff:
  assumes "filtermap g (at x) = (at y)"
  shows   "is_pole (f \ g) x \ is_pole f y"
  unfolding is_pole_def filterlim_def filtermap_compose assms ..

lemma is_pole_inverse_holomorphic:
  assumes "open s"
    and f_holo: "f holomorphic_on (s-{z})"
    and pole: "is_pole f z"
    and non_z: "\x\s-{z}. f x\0"
  shows "(\x. if x=z then 0 else inverse (f x)) holomorphic_on s"
proof -
  define g where "g \ \x. if x=z then 0 else inverse (f x)"
  have "isCont g z" unfolding isCont_def  using is_pole_tendsto[OF pole]
    by (simp add: g_def cong: LIM_cong)
  moreover have "continuous_on (s-{z}) f" using f_holo holomorphic_on_imp_continuous_on by auto
  hence "continuous_on (s-{z}) (inverse o f)" unfolding comp_def
    by (auto elim!:continuous_on_inverse simp add: non_z)
  hence "continuous_on (s-{z}) g" unfolding g_def
    using continuous_on_eq by fastforce
  ultimately have "continuous_on s g" using open_delete[OF \<open>open s\<close>] \<open>open s\<close>
    by (auto simp add: continuous_on_eq_continuous_at)
  moreover have "(inverse o f) holomorphic_on (s-{z})"
    unfolding comp_def using f_holo
    by (auto elim!:holomorphic_on_inverse simp add: non_z)
  hence "g holomorphic_on (s-{z})"
    using g_def holomorphic_transform by force
  ultimately show ?thesis unfolding g_def using \<open>open s\<close>
    by (auto elim!: no_isolated_singularity)
qed

lemma not_is_pole_holomorphic:
  assumes "open A" "x \ A" "f holomorphic_on A"
  shows   "\is_pole f x"
proof -
  have "continuous_on A f"
    by (intro holomorphic_on_imp_continuous_on) fact
  with assms have "isCont f x"
    by (simp add: continuous_on_eq_continuous_at)
  hence "f \x\ f x"
    by (simp add: isCont_def)
  thus "\is_pole f x"
    unfolding is_pole_def
    using not_tendsto_and_filterlim_at_infinity[of "at x" f "f x"] by auto
qed

lemma is_pole_inverse_power: "n > 0 \ is_pole (\z::complex. 1 / (z - a) ^ n) a"
  unfolding is_pole_def inverse_eq_divide [symmetric]
  by (intro filterlim_compose[OF filterlim_inverse_at_infinity] tendsto_intros)
     (auto simp: filterlim_at eventually_at intro!: exI[of _ 1] tendsto_eq_intros)

lemma is_pole_cmult_iff [simp]:
  assumes "c \ 0"
  shows "is_pole (\z. c * f z :: 'a :: real_normed_field) z \ is_pole f z"
proof
  assume "is_pole (\z. c * f z) z"
  with \<open>c\<noteq>0\<close> have "is_pole (\<lambda>z. inverse c * (c * f z)) z"
    unfolding is_pole_def
    by (force intro: tendsto_mult_filterlim_at_infinity)
  thus "is_pole f z"
    using \<open>c\<noteq>0\<close> by (simp add: field_simps)
next
  assume "is_pole f z"
  with \<open>c\<noteq>0\<close> show "is_pole (\<lambda>z. c * f z) z"
    by (auto intro!: tendsto_mult_filterlim_at_infinity simp: is_pole_def)
qed

lemma is_pole_uminus_iff [simp]: "is_pole (\z. -f z :: 'a :: real_normed_field) z \ is_pole f z"
  using is_pole_cmult_iff[of "-1" f] by (simp del: is_pole_cmult_iff)

lemma is_pole_inverse: "is_pole (\z::complex. 1 / (z - a)) a"
  using is_pole_inverse_power[of 1 a] by simp

lemma is_pole_divide:
  fixes f :: "'a :: t2_space \ 'b :: real_normed_field"
  assumes "isCont f z" "filterlim g (at 0) (at z)" "f z \ 0"
  shows   "is_pole (\z. f z / g z) z"
proof -
  have "filterlim (\z. f z * inverse (g z)) at_infinity (at z)"
    using assms filterlim_compose filterlim_inverse_at_infinity isCont_def
      tendsto_mult_filterlim_at_infinity by blast
  thus ?thesis by (simp add: field_split_simps is_pole_def)
qed

lemma is_pole_basic:
  assumes "f holomorphic_on A" "open A" "z \ A" "f z \ 0" "n > 0"
  shows   "is_pole (\w. f w / (w-z) ^ n) z"
proof (rule is_pole_divide)
  have "continuous_on A f" by (rule holomorphic_on_imp_continuous_on) fact
  with assms show "isCont f z" by (auto simp: continuous_on_eq_continuous_at)
  have "filterlim (\w. (w-z) ^ n) (nhds 0) (at z)"
    using assms by (auto intro!: tendsto_eq_intros)
  thus "filterlim (\w. (w-z) ^ n) (at 0) (at z)"
    by (intro filterlim_atI tendsto_eq_intros)
       (use assms in \<open>auto simp: eventually_at_filter\<close>)
qed fact+

lemma is_pole_basic':
  assumes "f holomorphic_on A" "open A" "0 \ A" "f 0 \ 0" "n > 0"
  shows   "is_pole (\w. f w / w ^ n) 0"
  using is_pole_basic[of f A 0] assms by simp

lemma is_pole_compose:
  assumes "is_pole f w" "g \z\ w" "eventually (\z. g z \ w) (at z)"
  shows   "is_pole (\x. f (g x)) z"
  using assms(1) unfolding is_pole_def
  by (rule filterlim_compose) (use assms in \<open>auto simp: filterlim_at\<close>)

lemma is_pole_plus_const_iff:
  "is_pole f z \ is_pole (\x. f x + c) z"
proof
  assume "is_pole f z"
  then have "filterlim f at_infinity (at z)" unfolding is_pole_def .
  moreover have "((\_. c) \ c) (at z)" by auto
  ultimately have " LIM x (at z). f x + c :> at_infinity"
    using tendsto_add_filterlim_at_infinity'[of f "at z"] by auto
  then show "is_pole (\x. f x + c) z" unfolding is_pole_def .
next
  assume "is_pole (\x. f x + c) z"
  then have "filterlim (\x. f x + c) at_infinity (at z)"
    unfolding is_pole_def .
  moreover have "((\_. -c) \ -c) (at z)" by auto
  ultimately have "LIM x (at z). f x :> at_infinity"
    using tendsto_add_filterlim_at_infinity'[of "(\x. f x + c)"
        "at z" "(\_. - c)" "-c"]
    by auto
  then show "is_pole f z" unfolding is_pole_def .
qed

lemma is_pole_minus_const_iff:
  "is_pole (\x. f x - c) z \ is_pole f z"
  using is_pole_plus_const_iff [of f z "-c"] by simp

lemma is_pole_alt:
  "is_pole f x = (\B>0. \U. open U \ x\U \ (\y\U. y\x \ norm (f y)\B))"
  unfolding is_pole_def
  unfolding filterlim_at_infinity[of 0,simplified] eventually_at_topological
  by auto

lemma is_pole_mult_analytic_nonzero1:
  assumes "is_pole g x" "f analytic_on {x}" "f x \ 0"
  shows   "is_pole (\x. f x * g x) x"
  unfolding is_pole_def
proof (rule tendsto_mult_filterlim_at_infinity)
  show "f \x\ f x"
    using assms by (simp add: analytic_at_imp_isCont isContD)
qed (use assms in \<open>auto simp: is_pole_def\<close>)

lemma is_pole_mult_analytic_nonzero2:
  assumes "is_pole f x" "g analytic_on {x}" "g x \ 0"
  shows   "is_pole (\x. f x * g x) x"
proof -
  have g: "g analytic_on {x}"
    using assms by auto
  show ?thesis
    using is_pole_mult_analytic_nonzero1 [OF \<open>is_pole f x\<close> g] \<open>g x \<noteq> 0\<close>
    by (simp add: mult.commute)
qed

lemma is_pole_mult_analytic_nonzero1_iff:
  assumes "f analytic_on {x}" "f x \ 0"
  shows   "is_pole (\x. f x * g x) x \ is_pole g x"
proof
  assume "is_pole g x"
  thus "is_pole (\x. f x * g x) x"
    by (intro is_pole_mult_analytic_nonzero1 assms)
next
  assume "is_pole (\x. f x * g x) x"
  hence "is_pole (\x. inverse (f x) * (f x * g x)) x"
    by (rule is_pole_mult_analytic_nonzero1)
       (use assms in \<open>auto intro!: analytic_intros\<close>)
  also have "?this \ is_pole g x"
  proof (rule is_pole_cong)
    have "eventually (\x. f x \ 0) (at x)"
      using assms by (simp add: analytic_at_neq_imp_eventually_neq)
    thus "eventually (\x. inverse (f x) * (f x * g x) = g x) (at x)"
      by eventually_elim auto
  qed auto
  finally show "is_pole g x" .
qed

lemma is_pole_mult_analytic_nonzero2_iff:
  assumes "g analytic_on {x}" "g x \ 0"
  shows   "is_pole (\x. f x * g x) x \ is_pole f x"
  by (subst mult.commute, rule is_pole_mult_analytic_nonzero1_iff) (fact assms)+

lemma frequently_const_imp_not_is_pole:
  fixes z :: "'a::first_countable_topology"
  assumes "frequently (\w. f w = c) (at z)"
  shows   "\ is_pole f z"
proof
  assume "is_pole f z"
  from assms have "z islimpt {w. f w = c}"
    by (simp add: islimpt_conv_frequently_at)
  then obtain g where g: "\n. g n \ {w. f w = c} - {z}" "g \ z"
    unfolding islimpt_sequential by blast
  then have "(f \ g) \ c"
    by (simp add: tendsto_eventually)
  moreover have "filterlim g (at z) sequentially"
    using g by (auto simp: filterlim_at)
  then have "filterlim (f \ g) at_infinity sequentially"
    unfolding o_def
    using \<open>is_pole f z\<close> filterlim_compose is_pole_def by blast
  ultimately show False
    using not_tendsto_and_filterlim_at_infinity trivial_limit_sequentially by blast
qed

subsection \<open>Isolated singularities\<close>

text \<open>The proposition
              \<^term>\<open>\<exists>x. ((f::complex\<Rightarrow>complex) \<longlongrightarrow> x) (at z) \<or> is_pole f z\<close>
can be interpreted as the complex function \<^term>\<open>f\<close> has a non-essential singularity at \<^term>\<open>z\<close>
(i.e. the singularity is either removable or a pole).\<close>
definition not_essential:: "[complex \ complex, complex] \ bool" where
  "not_essential f z = (\x. f\z\x \ is_pole f z)"

definition isolated_singularity_at:: "[complex \ complex, complex] \ bool" where
  "isolated_singularity_at f z = (\r>0. f analytic_on ball z r-{z})"

lemma not_essential_cong:
  assumes "eventually (\x. f x = g x) (at z)" "z = z'"
  shows   "not_essential f z \ not_essential g z'"
  unfolding not_essential_def using assms filterlim_cong is_pole_cong by fastforce

lemma not_essential_compose_iff:
  assumes "filtermap g (at z) = at z'"
  shows   "not_essential (f \ g) z = not_essential f z'"
  unfolding not_essential_def filterlim_def filtermap_compose assms is_pole_compose_iff[OF assms]
  by blast

lemma isolated_singularity_at_cong:
  assumes "eventually (\x. f x = g x) (at z)" "z = z'"
  shows   "isolated_singularity_at f z \ isolated_singularity_at g z'"
proof -
  have "isolated_singularity_at g z"
    if "isolated_singularity_at f z" "eventually (\x. f x = g x) (at z)" for f g
  proof -
    from that(1) obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
      by (auto simp: isolated_singularity_at_def)
    from that(2) obtain r' where r': "r' > 0" "\x\ball z r'-{z}. f x = g x"
      unfolding eventually_at_filter eventually_nhds_metric by (auto simp: dist_commute)

    have "f holomorphic_on ball z r - {z}"
      using r(2) by (subst (asm) analytic_on_open) auto
    hence "f holomorphic_on ball z (min r r') - {z}"
      by (rule holomorphic_on_subset) auto
    also have "?this \ g holomorphic_on ball z (min r r') - {z}"
      using r' by (intro holomorphic_cong) auto
    also have "\ \ g analytic_on ball z (min r r') - {z}"
      by (subst analytic_on_open) auto
    finally show ?thesis
      unfolding isolated_singularity_at_def
      by (intro exI[of _ "min r r'"]) (use \<open>r > 0\<close> \<open>r' > 0\<close> in auto)
  qed
  from this[of f g] this[of g f] assms show ?thesis
    by (auto simp: eq_commute)
qed

lemma removable_singularity:
  assumes "f holomorphic_on A - {x}" "open A"
  assumes "f \x\ c"
  shows   "(\y. if y = x then c else f y) holomorphic_on A" (is "?g holomorphic_on _")
proof -
  have "continuous_on A ?g"
    unfolding continuous_on_def
  proof
    fix y assume y: "y \ A"
    show "(?g \ ?g y) (at y within A)"
    proof (cases "y = x")
      case False
      have "continuous_on (A - {x}) f"
        using assms(1) by (meson holomorphic_on_imp_continuous_on)
      hence "(f \ ?g y) (at y within A - {x})"
        using False y by (auto simp: continuous_on_def)
      also have "?this \ (?g \ ?g y) (at y within A - {x})"
        by (intro filterlim_cong refl) (auto simp: eventually_at_filter)
      also have "at y within A - {x} = at y within A"
        using y assms False
        by (intro at_within_nhd[of _ "A - {x}"]) auto
      finally show ?thesis .
    next
      case [simp]: True
      have "f \x\ c"
        by fact
      also have "?this \ (?g \ ?g y) (at y)"
        by (simp add: LIM_equal)
      finally show ?thesis
        by (meson Lim_at_imp_Lim_at_within)
    qed
  qed
  moreover {
    have "?g holomorphic_on A - {x}"
      using assms(1) holomorphic_transform by fastforce
  }
  ultimately show ?thesis
    using assms by (simp add: no_isolated_singularity)
qed

lemma removable_singularity':
  assumes "isolated_singularity_at f z"
  assumes "f \z\ c"
  shows   "(\y. if y = z then c else f y) analytic_on {z}"
proof -
  from assms obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
    by (auto simp: isolated_singularity_at_def)
  have "(\y. if y = z then c else f y) holomorphic_on ball z r"
  proof (rule removable_singularity)
    show "f holomorphic_on ball z r - {z}"
      using r(2) by (subst (asm) analytic_on_open) auto
  qed (use assms in auto)
  thus ?thesis
    using r(1) unfolding analytic_at by (intro exI[of _ "ball z r"]) auto
qed

named_theorems singularity_intros "introduction rules for singularities"

lemma holomorphic_factor_unique:
  fixes f:: "complex \ complex" and z::complex and r::real and m n::int
  assumes "r>0" "g z\0" "h z\0"
    and asm: "\w\ball z r-{z}. f w = g w * (w-z) powi n \ g w\0 \ f w = h w * (w-z) powi m \ h w\0"
    and g_holo: "g holomorphic_on ball z r" and h_holo: "h holomorphic_on ball z r"
  shows "n=m"
proof -
  have [simp]: "at z within ball z r \ bot" using \r>0\
      by (auto simp add: at_within_ball_bot_iff)
  have False when "n>m"
  proof -
    have "(h \ 0) (at z within ball z r)"
    proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w-z) powi (n - m) * g w"])
      have "\w\ball z r-{z}. h w = (w-z)powi(n-m) * g w"
        using \<open>n>m\<close> asm \<open>r>0\<close> by (simp add: field_simps power_int_diff) force
      then show "\x' \ ball z r; 0 < dist x' z;dist x' z < r\
            \<Longrightarrow> (x' - z) powi (n - m) * g x' = h x'" for x' by auto
    next
      define F where "F \ at z within ball z r"
      define f' where "f' \<equiv> \<lambda>x. (x - z) powi (n-m)"
      have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto
      moreover have "continuous F f'" unfolding f'_def F_def continuous_def
        using \<open>n>m\<close>
          by (auto simp add: Lim_ident_at  intro!:tendsto_powr_complex_0 tendsto_eq_intros)
      ultimately have "(f' \ 0) F" unfolding F_def
        by (simp add: continuous_within)
      moreover have "(g \ g z) F"
        unfolding F_def
        using \<open>r>0\<close> centre_in_ball continuous_on_def g_holo holomorphic_on_imp_continuous_on by blast
      ultimately show " ((\w. f' w * g w) \ 0) F" using tendsto_mult by fastforce
    qed
    moreover have "(h \ h z) (at z within ball z r)"
      using holomorphic_on_imp_continuous_on[OF h_holo]
      by (auto simp add: continuous_on_def \<open>r>0\<close>)
    ultimately have "h z=0" by (auto intro!: tendsto_unique)
    thus False using \<open>h z\<noteq>0\<close> by auto
  qed
  moreover have False when "m>n"
  proof -
    have "(g \ 0) (at z within ball z r)"
    proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w-z) powi (m - n) * h w"])
      have "\w\ball z r -{z}. g w = (w-z) powi (m-n) * h w" using \m>n\ asm
        by (simp add: field_simps power_int_diff) force
      then show "\x' \ ball z r; 0 < dist x' z;dist x' z < r\
            \<Longrightarrow> (x' - z) powi (m - n) * h x' = g x'" for x' by auto
    next
      define F where "F \ at z within ball z r"
      define f' where "f' \<equiv>\<lambda>x. (x - z) powi (m-n)"
      have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto
      moreover have "continuous F f'" unfolding f'_def F_def continuous_def
        using \<open>m>n\<close>
        by (auto simp: Lim_ident_at intro!:tendsto_powr_complex_0 tendsto_eq_intros)
      ultimately have "(f' \ 0) F" unfolding F_def
        by (simp add: continuous_within)
      moreover have "(h \ h z) F"
        using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] \<open>r>0\<close>
        unfolding F_def by auto
      ultimately show " ((\w. f' w * h w) \ 0) F" using tendsto_mult by fastforce
    qed
    moreover have "(g \ g z) (at z within ball z r)"
      using holomorphic_on_imp_continuous_on[OF g_holo]
      by (auto simp add: continuous_on_def \<open>r>0\<close>)
    ultimately have "g z=0" by (auto intro!: tendsto_unique)
    thus False using \<open>g z\<noteq>0\<close> by auto
  qed
  ultimately show "n=m" by fastforce
qed

lemma holomorphic_factor_puncture:
  assumes f_iso: "isolated_singularity_at f z"
      and "not_essential f z" \<comment> \<open>\<^term>\<open>f\<close> has either a removable singularity or a pole at \<^term>\<open>z\<close>\<close>
      and non_zero: "\\<^sub>Fw in (at z). f w\0" \ \\<^term>\f\ will not be constantly zero in a neighbour of \<^term>\z\\
  shows "\!n::int. \g r. 0 < r \ g holomorphic_on cball z r \ g z\0
          \<and> (\<forall>w\<in>cball z r-{z}. f w = g w * (w-z) powi n \<and> g w\<noteq>0)"
proof -
  define P where "P = (\f n g r. 0 < r \ g holomorphic_on cball z r \ g z\0
          \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n  \<and> g w\<noteq>0))"
  have imp_unique: "\!n::int. \g r. P f n g r" when "\n g r. P f n g r"
  proof (rule ex_ex1I[OF that])
    fix n1 n2 :: int
    assume g1_asm: "\g1 r1. P f n1 g1 r1" and g2_asm: "\g2 r2. P f n2 g2 r2"
    define fac where "fac \ \n g r. \w\cball z r-{z}. f w = g w * (w-z) powi n \ g w \ 0"
    obtain g1 r1 where "0 < r1" and g1_holo: "g1 holomorphic_on cball z r1" and "g1 z\0"
        and "fac n1 g1 r1" using g1_asm unfolding P_def fac_def by auto
    obtain g2 r2 where "0 < r2" and g2_holo: "g2 holomorphic_on cball z r2" and "g2 z\0"
        and "fac n2 g2 r2" using g2_asm unfolding P_def fac_def by auto
    define r where "r \ min r1 r2"
    have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> unfolding r_def by auto
    moreover have "\w\ball z r-{z}. f w = g1 w * (w-z) powi n1 \ g1 w\0
        \<and> f w = g2 w * (w-z) powi n2  \<and> g2 w\<noteq>0"
      using \<open>fac n1 g1 r1\<close> \<open>fac n2 g2 r2\<close>   unfolding fac_def r_def
      by fastforce
    ultimately show "n1=n2"
      using g1_holo g2_holo \<open>g1 z\<noteq>0\<close> \<open>g2 z\<noteq>0\<close>
      apply (elim holomorphic_factor_unique)
      by (auto simp add: r_def)
  qed

  have P_exist: "\ n g r. P h n g r" when
      "\z'. (h \ z') (at z)" "isolated_singularity_at h z" "\\<^sub>Fw in (at z). h w\0"
    for h
  proof -
    from that(2) obtain r where "r>0" and r: "h analytic_on ball z r - {z}"
      unfolding isolated_singularity_at_def by auto
    obtain z' where "(h \ z') (at z)" using \\z'. (h \ z') (at z)\ by auto
    define h' where "h'=(\<lambda>x. if x=z then z' else h x)"
    have "h' holomorphic_on ball z r"
    proof (rule no_isolated_singularity'[of "{z}"])
      show "\w. w \ {z} \ (h' \ h' w) (at w within ball z r)"
        by (simp add: LIM_cong Lim_at_imp_Lim_at_within \<open>h \<midarrow>z\<rightarrow> z'\<close> h'_def)
      show "h' holomorphic_on ball z r - {z}"
        using r analytic_imp_holomorphic h'_def holomorphic_transform by fastforce
    qed auto
    have ?thesis when "z'=0"
    proof -
      have "h' z=0" using that unfolding h'_def by auto
      moreover have "\ h' constant_on ball z r"
        using \<open>\<exists>\<^sub>Fw in (at z). h w\<noteq>0\<close> unfolding constant_on_def frequently_def eventually_at h'_def
        by (metis \<open>0 < r\<close> centre_in_ball dist_commute mem_ball that)
      moreover note \<open>h' holomorphic_on ball z r\<close>
      ultimately obtain g r1 n where "0 < n" "0 < r1" "ball z r1 \ ball z r" and
          g: "g holomorphic_on ball z r1"
          "\w. w \ ball z r1 \ h' w = (w-z) ^ n * g w"
          "\w. w \ ball z r1 \ g w \ 0"
        using holomorphic_factor_zero_nonconstant[of _ "ball z r" z thesis,simplified,
                OF \<open>h' holomorphic_on ball z r\<close> \<open>r>0\<close> \<open>h' z=0\<close> \<open>\<not> h' constant_on ball z r\<close>]
        by (auto simp add: dist_commute)
      define rr where "rr=r1/2"
      have "P h' n g rr"
        unfolding P_def rr_def
        using \<open>n>0\<close> \<open>r1>0\<close> g by (auto simp add: powr_nat)
      then have "P h n g rr"
        unfolding h'_def P_def by auto
      then show ?thesis unfolding P_def by blast
    qed
    moreover have ?thesis when "z'\0"
    proof -
      have "h' z\0" using that unfolding h'_def by auto
      obtain r1 where "r1>0" "cball z r1 \ ball z r" "\x\cball z r1. h' x\0"
      proof -
        have "isCont h' z" "h' z\0"
          by (auto simp add: Lim_cong_within \<open>h \<midarrow>z\<rightarrow> z'\<close> \<open>z'\<noteq>0\<close> continuous_at h'_def)
        then obtain r2 where r2: "r2>0" "\x\ball z r2. h' x\0"
          using continuous_at_avoid[of z h' 0 ] unfolding ball_def by auto
        define r1 where "r1=min r2 r / 2"
        have "0 < r1" "cball z r1 \ ball z r"
          using \<open>r2>0\<close> \<open>r>0\<close> unfolding r1_def by auto
        moreover have "\x\cball z r1. h' x \ 0"
          using r2 unfolding r1_def by simp
        ultimately show ?thesis using that by auto
      qed
      then have "P h' 0 h' r1" using \<open>h' holomorphic_on ball z r\<close> unfolding P_def by auto
      then have "P h 0 h' r1" unfolding P_def h'_def by auto
      then show ?thesis unfolding P_def by blast
    qed
    ultimately show ?thesis by auto
  qed

  have ?thesis when "\x. (f \ x) (at z)"
    apply (rule_tac imp_unique[unfolded P_def])
    using P_exist[OF that(1) f_iso non_zero] unfolding P_def .
  moreover have ?thesis when "is_pole f z"
  proof (rule imp_unique[unfolded P_def])
    obtain e where [simp]: "e>0" and e_holo: "f holomorphic_on ball z e - {z}" and e_nz: "\x\ball z e-{z}. f x\0"
    proof -
      have "\\<^sub>F z in at z. f z \ 0"
        using \<open>is_pole f z\<close> filterlim_at_infinity_imp_eventually_ne unfolding is_pole_def
        by auto
      then obtain e1 where e1: "e1>0" "\x\ball z e1-{z}. f x\0"
        using that eventually_at[of "\x. f x\0" z UNIV,simplified] by (auto simp add: dist_commute)
      obtain e2 where e2: "e2>0" "f holomorphic_on ball z e2 - {z}"
        using f_iso analytic_imp_holomorphic unfolding isolated_singularity_at_def by auto
      show ?thesis
        using e1 e2 by (force intro: that[of "min e1 e2"])
    qed

    define h where "h \ \x. inverse (f x)"
    have "\n g r. P h n g r"
    proof -
      have "(\x. inverse (f x)) analytic_on ball z e - {z}"
        by (metis e_holo e_nz open_ball analytic_on_open holomorphic_on_inverse open_delete)
      moreover have "h \z\ 0"
        using Lim_transform_within_open assms(2) h_def is_pole_tendsto that by fastforce
      moreover have "\\<^sub>Fw in (at z). h w\0"
        using non_zero by (simp add: h_def)
      ultimately show ?thesis
        using P_exist[of h] \<open>e > 0\<close>
        unfolding isolated_singularity_at_def h_def
        by blast
    qed
    then obtain n g r
      where "0 < r" and
            g_holo: "g holomorphic_on cball z r" and "g z\0" and
            g_fac: "(\w\cball z r-{z}. h w = g w * (w-z) powi n \ g w \ 0)"
      unfolding P_def by auto
    have "P f (-n) (inverse o g) r"
    proof -
      have "f w = inverse (g w) * (w-z) powi (- n)" when "w\cball z r - {z}" for w
        by (metis g_fac h_def inverse_inverse_eq inverse_mult_distrib power_int_minus that)
      then show ?thesis
        unfolding P_def comp_def
        using \<open>r>0\<close> g_holo g_fac \<open>g z\<noteq>0\<close> by (auto intro: holomorphic_intros)
    qed
    then show "\x g r. 0 < r \ g holomorphic_on cball z r \ g z \ 0
                  \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi x  \<and> g w \<noteq> 0)"
      unfolding P_def by blast
  qed
  ultimately show ?thesis
    using \<open>not_essential f z\<close> unfolding not_essential_def by presburger
qed

lemma not_essential_transform:
  assumes "not_essential g z"
  assumes "\\<^sub>F w in (at z). g w = f w"
  shows "not_essential f z"
  using assms unfolding not_essential_def
  by (simp add: filterlim_cong is_pole_cong)

lemma isolated_singularity_at_transform:
  assumes "isolated_singularity_at g z"
  assumes "\\<^sub>F w in (at z). g w = f w"
  shows "isolated_singularity_at f z"
  using assms isolated_singularity_at_cong by blast

lemma not_essential_powr[singularity_intros]:
  assumes "LIM w (at z). f w :> (at x)"
  shows "not_essential (\w. (f w) powi n) z"
proof -
  define fp where "fp=(\w. (f w) powi n)"
  have ?thesis when "n>0"
  proof -
    have "(\w. (f w) ^ (nat n)) \z\ x ^ nat n"
      using that assms unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
    then have "fp \z\ x ^ nat n" unfolding fp_def
      by (smt (verit) LIM_cong power_int_def that)
    then show ?thesis unfolding not_essential_def fp_def by auto
  qed
  moreover have ?thesis when "n=0"
  proof -
    have "\\<^sub>F x in at z. fp x = 1"
      using that filterlim_at_within_not_equal[OF assms] by (auto simp: fp_def)
    then have "fp \z\ 1"
      by (simp add: tendsto_eventually)
    then show ?thesis unfolding fp_def not_essential_def by auto
  qed
  moreover have ?thesis when "n<0"
  proof (cases "x=0")
    case True
    have "(\x. f x ^ nat (- n)) \z\ 0"
      using assms True that unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
    moreover have "\\<^sub>F x in at z. f x ^ nat (- n) \ 0"
      by (smt (verit) True assms eventually_at_topological filterlim_at power_eq_0_iff)
    ultimately have "LIM w (at z). inverse ((f w) ^ (nat (-n))) :> at_infinity"
      by (metis filterlim_atI filterlim_compose filterlim_inverse_at_infinity)
    then have "LIM w (at z). fp w :> at_infinity"
    proof (elim filterlim_mono_eventually)
      show "\\<^sub>F x in at z. inverse (f x ^ nat (- n)) = fp x"
        using filterlim_at_within_not_equal[OF assms,of 0] unfolding fp_def
        by (smt (verit) eventuallyI power_int_def power_inverse that)
    qed auto
    then show ?thesis unfolding fp_def not_essential_def is_pole_def by auto
  next
    case False
    let ?xx= "inverse (x ^ (nat (-n)))"
    have "(\w. inverse ((f w) ^ (nat (-n)))) \z\?xx"
      using assms False unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
    then have "fp \z\ ?xx"
      by (smt (verit, best) LIM_cong fp_def power_int_def power_inverse that)
    then show ?thesis unfolding fp_def not_essential_def by auto
  qed
  ultimately show ?thesis by linarith
qed

lemma isolated_singularity_at_powr[singularity_intros]:
  assumes "isolated_singularity_at f z" "\\<^sub>F w in (at z). f w\0"
  shows "isolated_singularity_at (\w. (f w) powi n) z"
proof -
  obtain r1 where "r1>0" "f analytic_on ball z r1 - {z}"
    using assms(1) unfolding isolated_singularity_at_def by auto
  then have r1: "f holomorphic_on ball z r1 - {z}"
    using analytic_on_open[of "ball z r1-{z}" f] by blast
  obtain r2 where "r2>0" and r2: "\w. w \ z \ dist w z < r2 \ f w \ 0"
    using assms(2) unfolding eventually_at by auto
  define r3 where "r3=min r1 r2"
  have "(\w. (f w) powi n) holomorphic_on ball z r3 - {z}"
    by (intro holomorphic_on_power_int) (use r1 r2 in \<open>auto simp: dist_commute r3_def\<close>)
  moreover have "r3>0" unfolding r3_def using \<open>0 < r1\<close> \<open>0 < r2\<close> by linarith
  ultimately show ?thesis
    by (meson open_ball analytic_on_open isolated_singularity_at_def open_delete)
qed

lemma non_zero_neighbour:
  assumes f_iso: "isolated_singularity_at f z"
      and f_ness: "not_essential f z"
      and f_nconst: "\\<^sub>Fw in (at z). f w\0"
    shows "\\<^sub>F w in (at z). f w\0"
proof -
  obtain fn fp fr
    where [simp]: "fp z \ 0" and "fr > 0"
      and fr: "fp holomorphic_on cball z fr"
              "\w. w \ cball z fr - {z} \ f w = fp w * (w-z) powi fn \ fp w \ 0"
    using holomorphic_factor_puncture[OF f_iso f_ness f_nconst] by auto
  have "f w \ 0" when " w \ z" "dist w z < fr" for w
  proof -
    have "f w = fp w * (w-z) powi fn" "fp w \ 0"
      using fr that by (auto simp add: dist_commute)
    moreover have "(w-z) powi fn \0"
      unfolding powr_eq_0_iff using \<open>w\<noteq>z\<close> by auto
    ultimately show ?thesis by auto
  qed
  then show ?thesis using \<open>fr>0\<close> unfolding eventually_at by auto
qed

lemma non_zero_neighbour_pole:
  assumes "is_pole f z"
  shows "\\<^sub>F w in (at z). f w\0"
  using assms filterlim_at_infinity_imp_eventually_ne[of f "at z" 0]
  unfolding is_pole_def by auto

lemma non_zero_neighbour_alt:
  assumes holo: "f holomorphic_on S"
      and "open S" "connected S" "z \ S" "\ \ S" "f \ \ 0"
    shows "\\<^sub>F w in (at z). f w\0 \ w\S"
proof (cases "f z = 0")
  case True
  from isolated_zeros[OF holo \<open>open S\<close> \<open>connected S\<close> \<open>z \<in> S\<close> True \<open>\<beta> \<in> S\<close> \<open>f \<beta> \<noteq> 0\<close>]
  obtain r where "0 < r" "ball z r \ S" "\w \ ball z r - {z}.f w \ 0" by metis
  then show ?thesis
    by (smt (verit) open_ball centre_in_ball eventually_at_topological insertE insert_Diff subsetD)
next
  case False
  obtain r1 where r1: "r1>0" "\y. dist z y < r1 \ f y \ 0"
    using continuous_at_avoid[of z f, OF _ False] assms continuous_on_eq_continuous_at
      holo holomorphic_on_imp_continuous_on by blast
  obtain r2 where r2: "r2>0" "ball z r2 \ S"
    using assms openE by blast
  show ?thesis unfolding eventually_at
    by (metis (no_types) dist_commute order.strict_trans linorder_less_linear mem_ball r1 r2 subsetD)
qed

lemma not_essential_times[singularity_intros]:
  assumes f_ness: "not_essential f z" and g_ness: "not_essential g z"
  assumes f_iso: "isolated_singularity_at f z" and g_iso: "isolated_singularity_at g z"
  shows "not_essential (\w. f w * g w) z"
proof -
  define fg where "fg = (\w. f w * g w)"
  have ?thesis when "\ ((\\<^sub>Fw in (at z). f w\0) \ (\\<^sub>Fw in (at z). g w\0))"
  proof -
    have "\\<^sub>Fw in (at z). fg w=0"
      using fg_def frequently_elim1 not_eventually that by fastforce
    from tendsto_cong[OF this] have "fg \z\0" by auto
    then show ?thesis unfolding not_essential_def fg_def by auto
  qed
  moreover have ?thesis when f_nconst: "\\<^sub>Fw in (at z). f w\0" and g_nconst: "\\<^sub>Fw in (at z). g w\0"
  proof -
    obtain fn fp fr where [simp]: "fp z \ 0" and "fr > 0"
          and fr: "fp holomorphic_on cball z fr"
                  "\w\cball z fr - {z}. f w = fp w * (w-z) powi fn \ fp w \ 0"
      using holomorphic_factor_puncture[OF f_iso f_ness f_nconst] by auto
    obtain gn gp gr where [simp]: "gp z \ 0" and "gr > 0"
          and gr: "gp holomorphic_on cball z gr"
                  "\w\cball z gr - {z}. g w = gp w * (w-z) powi gn \ gp w \ 0"
      using holomorphic_factor_puncture[OF g_iso g_ness g_nconst] by auto

    define r1 where "r1=(min fr gr)"
    have "r1>0" unfolding r1_def using  \<open>fr>0\<close> \<open>gr>0\<close> by auto
    have fg_times: "fg w = (fp w * gp w) * (w-z) powi (fn+gn)" and fgp_nz: "fp w*gp w\0"
      when "w\ball z r1 - {z}" for w
    proof -
      have "f w = fp w * (w-z) powi fn" "fp w\0"
        using fr that unfolding r1_def by auto
      moreover have "g w = gp w * (w-z) powi gn" "gp w \ 0"
        using gr that unfolding r1_def by auto
      ultimately show "fg w = (fp w * gp w) * (w-z) powi (fn+gn)" "fp w*gp w\0"
        using that by (auto simp add: fg_def power_int_add)
    qed

    obtain [intro]: "fp \z\fp z" "gp \z\gp z"
        using fr(1) \<open>fr>0\<close> gr(1) \<open>gr>0\<close>
        by (metis centre_in_ball continuous_at continuous_on_interior
            holomorphic_on_imp_continuous_on interior_cball)
    have ?thesis when "fn+gn>0"
    proof -
      have "(\w. (fp w * gp w) * (w-z) ^ (nat (fn+gn))) \z\0"
        using that by (auto intro!:tendsto_eq_intros)
      then have "fg \z\ 0"
        using Lim_transform_within[OF _ \<open>r1>0\<close>]
        by (smt (verit, best) Diff_iff dist_commute fg_times mem_ball power_int_def singletonD that zero_less_dist_iff)
      then show ?thesis unfolding not_essential_def fg_def by auto
    qed
    moreover have ?thesis when "fn+gn=0"
    proof -
      have "(\w. fp w * gp w) \z\fp z*gp z"
        using that by (auto intro!:tendsto_eq_intros)
      then have "fg \z\ fp z*gp z"
        apply (elim Lim_transform_within[OF _ \<open>r1>0\<close>])
        apply (subst fg_times)
        by (auto simp add: dist_commute that)
      then show ?thesis unfolding not_essential_def fg_def by auto
    qed
    moreover have ?thesis when "fn+gn<0"
    proof -
      have "LIM x at z. (x - z) ^ nat (- (fn + gn)) :> at 0"
        using eventually_at_topological that
        by (force intro!: tendsto_eq_intros filterlim_atI)
      moreover have "\c. (\c. fp c * gp c) \z\ c \ 0 \ c"
        using \<open>fp \<midarrow>z\<rightarrow> fp z\<close> \<open>gp \<midarrow>z\<rightarrow> gp z\<close> tendsto_mult by fastforce
      ultimately have "LIM w (at z). fp w * gp w / (w-z)^nat (-(fn+gn)) :> at_infinity"
        using filterlim_divide_at_infinity by blast
      then have "is_pole fg z" unfolding is_pole_def
        apply (elim filterlim_transform_within[OF _ _ \<open>r1>0\<close>])
        using that
        by (simp_all add: dist_commute fg_times of_int_of_nat divide_simps power_int_def del: minus_add_distrib)
      then show ?thesis unfolding not_essential_def fg_def by auto
    qed
    ultimately show ?thesis unfolding not_essential_def fg_def by fastforce
  qed
  ultimately show ?thesis by auto
qed

lemma not_essential_inverse[singularity_intros]:
  assumes f_ness: "not_essential f z"
  assumes f_iso: "isolated_singularity_at f z"
  shows "not_essential (\w. inverse (f w)) z"
proof -
  define vf where "vf = (\w. inverse (f w))"
  have ?thesis when "\(\\<^sub>Fw in (at z). f w\0)"
  proof -
    have "\\<^sub>Fw in (at z). f w=0"
      using not_eventually that by fastforce
    then have "vf \z\0"
      unfolding vf_def by (simp add: tendsto_eventually)
    then show ?thesis
      unfolding not_essential_def vf_def by auto
  qed
  moreover have ?thesis when "is_pole f z"
    by (metis (mono_tags, lifting) filterlim_at filterlim_inverse_at_iff is_pole_def
        not_essential_def that)
  moreover have ?thesis when "\x. f\z\x " and f_nconst: "\\<^sub>Fw in (at z). f w\0"
  proof -
    from that obtain fz where fz: "f\z\fz" by auto
    have ?thesis when "fz=0"

    proof -
      have "(\w. inverse (vf w)) \z\0"
        using fz that unfolding vf_def by auto
      moreover have "\\<^sub>F w in at z. inverse (vf w) \ 0"
        using non_zero_neighbour[OF f_iso f_ness f_nconst]
        unfolding vf_def by auto
      ultimately show ?thesis unfolding not_essential_def vf_def
         using filterlim_atI filterlim_inverse_at_iff is_pole_def by blast
    qed
    moreover have ?thesis when "fz\0"
      using fz not_essential_def tendsto_inverse that by blast
    ultimately show ?thesis by auto
  qed
  ultimately show ?thesis using f_ness unfolding not_essential_def by auto
qed

lemma isolated_singularity_at_inverse[singularity_intros]:
  assumes f_iso: "isolated_singularity_at f z"
      and f_ness: "not_essential f z"
  shows "isolated_singularity_at (\w. inverse (f w)) z"
proof -
  define vf where "vf = (\w. inverse (f w))"
  have ?thesis when "\(\\<^sub>Fw in (at z). f w\0)"
  proof -
    have "\\<^sub>Fw in (at z). f w=0"
      using that[unfolded frequently_def, simplified] by (auto elim: eventually_rev_mp)
    then have "\\<^sub>Fw in (at z). vf w=0"
      unfolding vf_def by auto
    then obtain d1 where "d1>0" and d1: "\x. x \ z \ dist x z < d1 \ vf x = 0"
      unfolding eventually_at by auto
    then have "vf holomorphic_on ball z d1-{z}"
      using holomorphic_transform[of "\_. 0"]
      by (metis Diff_iff dist_commute holomorphic_on_const insert_iff mem_ball)
    then have "vf analytic_on ball z d1 - {z}"
      by (simp add: analytic_on_open open_delete)
    then show ?thesis
      using \<open>d1>0\<close> unfolding isolated_singularity_at_def vf_def by auto
  qed
  moreover have ?thesis when f_nconst: "\\<^sub>Fw in (at z). f w\0"
  proof -
    have "\\<^sub>F w in at z. f w \ 0" using non_zero_neighbour[OF f_iso f_ness f_nconst] .
    then obtain d1 where d1: "d1>0" "\x. x \ z \ dist x z < d1 \ f x \ 0"
      unfolding eventually_at by auto
    obtain d2 where "d2>0" and d2: "f analytic_on ball z d2 - {z}"
      using f_iso unfolding isolated_singularity_at_def by auto
    define d3 where "d3=min d1 d2"
    have "d3>0" unfolding d3_def using \<open>d1>0\<close> \<open>d2>0\<close> by auto
    moreover
    have "f analytic_on ball z d3 - {z}"
      by (smt (verit, best) Diff_iff analytic_on_analytic_at d2 d3_def mem_ball)
    then have "vf analytic_on ball z d3 - {z}"
      unfolding vf_def
      by (intro analytic_on_inverse; simp add: d1(2) d3_def dist_commute)
    ultimately show ?thesis
      unfolding isolated_singularity_at_def vf_def by auto
  qed
  ultimately show ?thesis by auto
qed

lemma not_essential_divide[singularity_intros]:
  assumes f_ness: "not_essential f z" and g_ness: "not_essential g z"
  assumes f_iso: "isolated_singularity_at f z" and g_iso: "isolated_singularity_at g z"
  shows "not_essential (\w. f w / g w) z"
proof -
  have "not_essential (\w. f w * inverse (g w)) z"
    by (simp add: f_iso f_ness g_iso g_ness isolated_singularity_at_inverse
        not_essential_inverse not_essential_times)
  then show ?thesis by (simp add: field_simps)
qed

lemma
  assumes f_iso: "isolated_singularity_at f z"
      and g_iso: "isolated_singularity_at g z"
    shows isolated_singularity_at_times[singularity_intros]:
              "isolated_singularity_at (\w. f w * g w) z"
      and isolated_singularity_at_add[singularity_intros]:
              "isolated_singularity_at (\w. f w + g w) z"
proof -
  obtain d1 d2 where "d1>0" "d2>0"
      and d1: "f analytic_on ball z d1 - {z}" and d2: "g analytic_on ball z d2 - {z}"
    using f_iso g_iso unfolding isolated_singularity_at_def by auto
  define d3 where "d3=min d1 d2"
  have "d3>0" unfolding d3_def using \<open>d1>0\<close> \<open>d2>0\<close> by auto

  have fan: "f analytic_on ball z d3 - {z}"
    by (smt (verit, best) Diff_iff analytic_on_analytic_at d1 d3_def mem_ball)
  have gan: "g analytic_on ball z d3 - {z}"
    by (smt (verit, best) Diff_iff analytic_on_analytic_at d2 d3_def mem_ball)
  have "(\w. f w * g w) analytic_on ball z d3 - {z}"
    using analytic_on_mult fan gan by blast
  then show "isolated_singularity_at (\w. f w * g w) z"
    using \<open>d3>0\<close> unfolding isolated_singularity_at_def by auto
  have "(\w. f w + g w) analytic_on ball z d3 - {z}"
    using analytic_on_add fan gan by blast
  then show "isolated_singularity_at (\w. f w + g w) z"
    using \<open>d3>0\<close> unfolding isolated_singularity_at_def by auto
qed

lemma isolated_singularity_at_uminus[singularity_intros]:
  assumes f_iso: "isolated_singularity_at f z"
  shows "isolated_singularity_at (\w. - f w) z"
  using assms unfolding isolated_singularity_at_def using analytic_on_neg by blast

lemma isolated_singularity_at_id[singularity_intros]:
     "isolated_singularity_at (\w. w) z"
  unfolding isolated_singularity_at_def by (simp add: gt_ex)

lemma isolated_singularity_at_minus[singularity_intros]:
  assumes "isolated_singularity_at f z" and "isolated_singularity_at g z"
  shows "isolated_singularity_at (\w. f w - g w) z"
  unfolding diff_conv_add_uminus
  using assms isolated_singularity_at_add isolated_singularity_at_uminus by blast

lemma isolated_singularity_at_divide[singularity_intros]:
  assumes "isolated_singularity_at f z"
      and "isolated_singularity_at g z"
      and "not_essential g z"
    shows "isolated_singularity_at (\w. f w / g w) z"
  unfolding divide_inverse
  by (simp add: assms isolated_singularity_at_inverse isolated_singularity_at_times)

lemma isolated_singularity_at_const[singularity_intros]:
    "isolated_singularity_at (\w. c) z"
  unfolding isolated_singularity_at_def by (simp add: gt_ex)

lemma isolated_singularity_at_holomorphic:
  assumes "f holomorphic_on s-{z}" "open s" "z\s"
  shows "isolated_singularity_at f z"
  using assms unfolding isolated_singularity_at_def
  by (metis analytic_on_holomorphic centre_in_ball insert_Diff openE open_delete subset_insert_iff)

lemma isolated_singularity_at_altdef:
  "isolated_singularity_at f z \ eventually (\z. f analytic_on {z}) (at z)"
proof
  assume "isolated_singularity_at f z"
  then obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
    unfolding isolated_singularity_at_def by blast
  have "eventually (\w. w \ ball z r - {z}) (at z)"
    using r(1) by (intro eventually_at_in_open) auto
  thus "eventually (\z. f analytic_on {z}) (at z)"
    by eventually_elim (use r analytic_on_subset in auto)
next
  assume "eventually (\z. f analytic_on {z}) (at z)"
  then obtain A where A: "open A" "z \ A" "\w. w \ A - {z} \ f analytic_on {w}"
    unfolding eventually_at_topological by blast
  then show "isolated_singularity_at f z"
    by (meson analytic_imp_holomorphic analytic_on_analytic_at isolated_singularity_at_holomorphic)
qed

lemma isolated_singularity_at_shift:
  assumes "isolated_singularity_at (\x. f (x + w)) z"
  shows   "isolated_singularity_at f (z + w)"
proof -
  from assms obtain r where r: "r > 0" and ana: "(\x. f (x + w)) analytic_on ball z r - {z}"
    unfolding isolated_singularity_at_def by blast
  have "((\x. f (x + w)) \ (\x. x - w)) analytic_on (ball (z + w) r - {z + w})"
    by (rule analytic_on_compose_gen[OF _ ana])
       (auto simp: dist_norm algebra_simps intro!: analytic_intros)
  hence "f analytic_on (ball (z + w) r - {z + w})"
    by (simp add: o_def)
  thus ?thesis using r
    unfolding isolated_singularity_at_def by blast
qed

lemma isolated_singularity_at_shift_iff:
  "isolated_singularity_at f (z + w) \ isolated_singularity_at (\x. f (x + w)) z"
  using isolated_singularity_at_shift[of f w z]
        isolated_singularity_at_shift[of "\x. f (x + w)" "-w" "w + z"]
  by (auto simp: algebra_simps)

lemma isolated_singularity_at_shift_0:
  "NO_MATCH 0 z \ isolated_singularity_at f z \ isolated_singularity_at (\x. f (z + x)) 0"
  using isolated_singularity_at_shift_iff[of f 0 z] by (simp add: add_ac)

lemma not_essential_shift:
  assumes "not_essential (\x. f (x + w)) z"
  shows   "not_essential f (z + w)"
proof -
  from assms consider c where "(\x. f (x + w)) \z\ c" | "is_pole (\x. f (x + w)) z"
    unfolding not_essential_def by blast
  thus ?thesis
  proof cases
    case (1 c)
    hence "f \z + w\ c"
      by (smt (verit, ccfv_SIG) LIM_cong add.assoc filterlim_at_to_0)
    thus ?thesis
      by (auto simp: not_essential_def)
  next
    case 2
    hence "is_pole f (z + w)"
      by (subst is_pole_shift_iff [symmetric]) (auto simp: o_def add_ac)
    thus ?thesis
      by (auto simp: not_essential_def)
  qed
qed

lemma not_essential_shift_iff: "not_essential f (z + w) \ not_essential (\x. f (x + w)) z"
  using not_essential_shift[of f w z]
        not_essential_shift[of "\x. f (x + w)" "-w" "w + z"]
  by (auto simp: algebra_simps)

lemma not_essential_shift_0:
  "NO_MATCH 0 z \ not_essential f z \ not_essential (\x. f (z + x)) 0"
  using not_essential_shift_iff[of f 0 z] by (simp add: add_ac)

lemma not_essential_holomorphic:
  assumes "f holomorphic_on A" "x \ A" "open A"
  shows   "not_essential f x"
  by (metis assms at_within_open continuous_on holomorphic_on_imp_continuous_on not_essential_def)

lemma not_essential_analytic:
  assumes "f analytic_on {z}"
  shows   "not_essential f z"
  using analytic_at assms not_essential_holomorphic by blast

lemma not_essential_id [singularity_intros]: "not_essential (\w. w) z"
  by (simp add: not_essential_analytic)

lemma is_pole_imp_not_essential [intro]: "is_pole f z \ not_essential f z"
  by (auto simp: not_essential_def)

lemma tendsto_imp_not_essential [intro]: "f \z\ c \ not_essential f z"
  by (auto simp: not_essential_def)

lemma eventually_not_pole:
  assumes "isolated_singularity_at f z"
  shows   "eventually (\w. \is_pole f w) (at z)"
proof -
  from assms obtain r where "r > 0" and r: "f analytic_on ball z r - {z}"
    by (auto simp: isolated_singularity_at_def)
  then have "eventually (\w. w \ ball z r - {z}) (at z)"
    by (intro eventually_at_in_open) auto
  thus "eventually (\w. \is_pole f w) (at z)"
    by (metis (no_types, lifting) analytic_at analytic_on_analytic_at eventually_mono not_is_pole_holomorphic r)
qed

lemma not_islimpt_poles:
  assumes "isolated_singularity_at f z"
  shows   "\z islimpt {w. is_pole f w}"
  using eventually_not_pole [OF assms]
  by (auto simp: islimpt_conv_frequently_at frequently_def)

lemma analytic_at_imp_no_pole: "f analytic_on {z} \ \is_pole f z"
  using analytic_at not_is_pole_holomorphic by blast

lemma not_essential_const [singularity_intros]: "not_essential (\_. c) z"
  by blast

lemma not_essential_uminus [singularity_intros]:
  assumes f_ness: "not_essential f z"
  assumes f_iso: "isolated_singularity_at f z"
  shows "not_essential (\w. -f w) z"
proof -
  have "not_essential (\w. -1 * f w) z"
    by (intro assms singularity_intros)
  thus ?thesis by simp
qed

lemma isolated_singularity_at_analytic:
  assumes "f analytic_on {z}"
  shows   "isolated_singularity_at f z"
  by (meson Diff_subset analytic_at assms holomorphic_on_subset isolated_singularity_at_holomorphic)

lemma isolated_singularity_sum [singularity_intros]:
  assumes "\x. x \ A \ isolated_singularity_at (f x) z"
  shows   "isolated_singularity_at (\w. \x\A. f x w) z"
  using assms by (induction A rule: infinite_finite_induct) (auto intro!: singularity_intros)

lemma isolated_singularity_prod [singularity_intros]:
  assumes "\x. x \ A \ isolated_singularity_at (f x) z"
  shows   "isolated_singularity_at (\w. \x\A. f x w) z"
  using assms by (induction A rule: infinite_finite_induct) (auto intro!: singularity_intros)

lemma isolated_singularity_sum_list [singularity_intros]:
  assumes "\f. f \ set fs \ isolated_singularity_at f z"
  shows   "isolated_singularity_at (\w. \f\fs. f w) z"
  using assms by (induction fs) (auto intro!: singularity_intros)

lemma isolated_singularity_prod_list [singularity_intros]:
  assumes "\f. f \ set fs \ isolated_singularity_at f z"
  shows   "isolated_singularity_at (\w. \f\fs. f w) z"
  using assms by (induction fs) (auto intro!: singularity_intros)

lemma isolated_singularity_sum_mset [singularity_intros]:
  assumes "\f. f \# F \ isolated_singularity_at f z"
  shows   "isolated_singularity_at (\w. \f\#F. f w) z"
  using assms by (induction F) (auto intro!: singularity_intros)

lemma isolated_singularity_prod_mset [singularity_intros]:
  assumes "\f. f \# F \ isolated_singularity_at f z"
  shows   "isolated_singularity_at (\w. \f\#F. f w) z"
  using assms by (induction F) (auto intro!: singularity_intros)

lemma analytic_nhd_imp_isolated_singularity:
  assumes "f analytic_on A - {x}" "x \ A" "open A"
  shows   "isolated_singularity_at f x"
  unfolding isolated_singularity_at_def using assms
  using analytic_imp_holomorphic isolated_singularity_at_def isolated_singularity_at_holomorphic by blast

lemma isolated_singularity_at_iff_analytic_nhd:
  "isolated_singularity_at f x \ (\A. x \ A \ open A \ f analytic_on A - {x})"
  by (meson open_ball analytic_nhd_imp_isolated_singularity
            centre_in_ball isolated_singularity_at_def)

subsection \<open>The order of non-essential singularities (i.e. removable singularities or poles)\<close>

definition\<^marker>\<open>tag important\<close> zorder :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> int" where
  "zorder f z = (THE n. (\h r. r>0 \ h holomorphic_on cball z r \ h z\0
                   \<and> (\<forall>w\<in>cball z r - {z}. f w =  h w * (w-z) powi n
                   \<and> h w \<noteq>0)))"

definition\<^marker>\<open>tag important\<close> zor_poly
    :: "[complex \ complex, complex] \ complex \ complex" where
  "zor_poly f z = (SOME h. \r. r > 0 \ h holomorphic_on cball z r \ h z \ 0
                   \<and> (\<forall>w\<in>cball z r - {z}. f w =  h w * (w-z) powi (zorder f z)
                   \<and> h w \<noteq>0))"

lemma zorder_exist:
  fixes f:: "complex \ complex" and z::complex
  defines "n \ zorder f z" and "g \ zor_poly f z"
  assumes f_iso: "isolated_singularity_at f z"
      and f_ness: "not_essential f z"
      and f_nconst: "\\<^sub>Fw in (at z). f w\0"
  shows "g z\0 \ (\r. r>0 \ g holomorphic_on cball z r
    \<and> (\<forall>w\<in>cball z r - {z}. f w  = g w * (w-z) powi n  \<and> g w \<noteq>0))"
proof -
  define P where "P = (\n g r. 0 < r \ g holomorphic_on cball z r \ g z\0
          \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powi n \<and> g w\<noteq>0))"
  have "\!k. \g r. P k g r"
    using holomorphic_factor_puncture[OF assms(3-)] unfolding P_def by auto
  then have "\g r. P n g r"
    unfolding n_def P_def zorder_def by (rule theI')
  then have "\r. P n g r"
    unfolding P_def zor_poly_def g_def n_def by (rule someI_ex)
  then obtain r1 where "P n g r1"
    by auto
  then show ?thesis
    unfolding P_def by auto
qed

lemma zorder_shift:
  shows  "zorder f z = zorder (\u. f (u + z)) 0"
  unfolding zorder_def
  apply (rule arg_cong [of concl: The])
  apply (auto simp: fun_eq_iff Ball_def dist_norm)
  subgoal for x h r
    apply (rule_tac x="h o (+)z" in exI)
    apply (rule_tac x="r" in exI)
    apply (intro conjI holomorphic_on_compose holomorphic_intros)
       apply (simp_all flip: cball_translation)
    apply (simp add: add.commute)
    done
  subgoal for x h r
    apply (rule_tac x="h o (\u. u-z)" in exI)
    apply (rule_tac x="r" in exI)
    apply (intro conjI holomorphic_on_compose holomorphic_intros)
       apply (simp_all flip: cball_translation_subtract)
    by (metis diff_add_cancel eq_iff_diff_eq_0 norm_minus_commute)
  done

lemma zorder_shift': "NO_MATCH 0 z \ zorder f z = zorder (\u. f (u + z)) 0"
  by (rule zorder_shift)

lemma
  fixes f:: "complex \ complex" and z::complex
  assumes f_iso: "isolated_singularity_at f z"
      and f_ness: "not_essential f z"
      and f_nconst: "\\<^sub>Fw in (at z). f w\0"
    shows zorder_inverse: "zorder (\w. inverse (f w)) z = - zorder f z"
      and zor_poly_inverse: "\\<^sub>Fw in (at z). zor_poly (\w. inverse (f w)) z w
                                                = inverse (zor_poly f z w)"
proof -
  define vf where "vf = (\w. inverse (f w))"
  define fn vfn where
    "fn = zorder f z"  and "vfn = zorder vf z"
  define fp vfp where
    "fp = zor_poly f z" and "vfp = zor_poly vf z"

  obtain fr where [simp]: "fp z \ 0" and "fr > 0"
          and fr: "fp holomorphic_on cball z fr"
                  "\w\cball z fr - {z}. f w = fp w * (w-z) powi fn \ fp w \ 0"
    using zorder_exist[OF f_iso f_ness f_nconst,folded fn_def fp_def]
    by auto
  have fr_inverse: "vf w = (inverse (fp w)) * (w-z) powi (-fn)"
        and fr_nz: "inverse (fp w) \ 0"
    when "w\ball z fr - {z}" for w
  proof -
    have "f w = fp w * (w-z) powi fn" "fp w \ 0"
      using fr(2) that by auto
    then show "vf w = (inverse (fp w)) * (w-z) powi (-fn)" "inverse (fp w)\0"
      by (simp_all add: power_int_minus vf_def)
  qed
  obtain vfr where [simp]: "vfp z \ 0" and "vfr>0" and vfr: "vfp holomorphic_on cball z vfr"
      "(\w\cball z vfr - {z}. vf w = vfp w * (w-z) powi vfn \ vfp w \ 0)"
  proof -
    have "isolated_singularity_at vf z"
      using isolated_singularity_at_inverse[OF f_iso f_ness] unfolding vf_def .
    moreover have "not_essential vf z"
      using not_essential_inverse[OF f_ness f_iso] unfolding vf_def .
    moreover have "\\<^sub>F w in at z. vf w \ 0"
      using f_nconst unfolding vf_def by (auto elim: frequently_elim1)
    ultimately show ?thesis using zorder_exist[of vf z, folded vfn_def vfp_def] that by auto
  qed

  define r1 where "r1 = min fr vfr"
  have "r1>0" using \<open>fr>0\<close> \<open>vfr>0\<close> unfolding r1_def by simp
  show "vfn = - fn"
  proof (rule holomorphic_factor_unique)
    have \<section>: "\<And>w. \<lbrakk>fp w = 0; dist z w < fr\<rbrakk> \<Longrightarrow> False"
      using fr_nz by force
    then show "\w\ball z r1 - {z}.
               vf w = vfp w * (w-z) powi vfn \<and>
               vfp w \<noteq> 0 \<and> vf w = inverse (fp w) * (w-z) powi (- fn) \<and>
               inverse (fp w) \<noteq> 0"
      using fr_inverse r1_def vfr(2)
      by (smt (verit) Diff_iff inverse_nonzero_iff_nonzero mem_ball mem_cball)
    show "vfp holomorphic_on ball z r1"
      using r1_def vfr(1) by auto
    show "(\w. inverse (fp w)) holomorphic_on ball z r1"
      by (metis \<section> ball_subset_cball fr(1) holomorphic_on_inverse holomorphic_on_subset mem_ball min.cobounded2 min.commute r1_def subset_ball)
  qed (use \<open>r1>0\<close> in auto)
  have "vfp w = inverse (fp w)" when "w\ball z r1-{z}" for w
  proof -
    have "w \ ball z fr - {z}" "w \ cball z vfr - {z}" "w\z"
      using that unfolding r1_def by auto
    then show ?thesis
      by (metis \<open>vfn = - fn\<close> power_int_not_zero right_minus_eq  fr_inverse vfr(2)
          vector_space_over_itself.scale_right_imp_eq)
  qed
  then show "\\<^sub>Fw in (at z). vfp w = inverse (fp w)"
    unfolding eventually_at by (metis DiffI dist_commute mem_ball singletonD \<open>r1>0\<close>)
qed

lemma zor_poly_shift:
  assumes iso1: "isolated_singularity_at f z"
    and ness1: "not_essential f z"
    and nzero1: "\\<^sub>F w in at z. f w \ 0"
  shows "\\<^sub>F w in nhds z. zor_poly f z w = zor_poly (\u. f (z + u)) 0 (w-z)"
proof -
  obtain r1 where "r1>0" "zor_poly f z z \ 0" and
      holo1: "zor_poly f z holomorphic_on cball z r1" and
      rball1: "\w\cball z r1 - {z}.
           f w = zor_poly f z w * (w-z) powi (zorder f z) \<and>
           zor_poly f z w \<noteq> 0"
    using zorder_exist[OF iso1 ness1 nzero1] by blast

  define ff where "ff=(\u. f (z + u))"
  have "isolated_singularity_at ff 0"
    unfolding ff_def
    using iso1 isolated_singularity_at_shift_iff[of f 0 z]
    by (simp add: algebra_simps)
  moreover have "not_essential ff 0"
    unfolding ff_def
    using ness1 not_essential_shift_iff[of f 0 z]
    by (simp add: algebra_simps)
  moreover have "\\<^sub>F w in at 0. ff w \ 0"
    unfolding ff_def using nzero1
    by (smt (verit, ccfv_SIG) add.commute eventually_at_to_0
        eventually_mono not_frequently)
  ultimately
  obtain r2 where "r2>0" "zor_poly ff 0 0 \ 0"
          and holo2: "zor_poly ff 0 holomorphic_on cball 0 r2"
          and rball2: "\w\cball 0 r2 - {0}.
               ff w = zor_poly ff 0 w * w powi (zorder ff 0) \<and> zor_poly ff 0 w \<noteq> 0"
    using zorder_exist[of ff 0] by auto

  define r where "r=min r1 r2"
  have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> unfolding r_def by auto

  have "zor_poly f z w = zor_poly ff 0 (w-z)"
    if "w\ball z r - {z}" for w
  proof -
    define n where "n \ zorder f z"

    have "f w = zor_poly f z w * (w-z) powi n"
      using n_def r_def rball1 that by auto
    moreover have "f w = zor_poly ff 0 (w-z) * (w-z) powi n"
    proof -
      have "w-z\cball 0 r2 - {0}"
        using r_def that by (auto simp: dist_complex_def)
      then have "ff (w-z) = zor_poly ff 0 (w-z) * (w-z) powi (zorder ff 0)"
        using rball2 by blast
      moreover have "of_int (zorder ff 0) = n"
        unfolding n_def ff_def by (simp add:zorder_shift' add.commute)
      ultimately show ?thesis unfolding ff_def by auto
    qed
    ultimately have "zor_poly f z w * (w-z) powi n = zor_poly ff 0 (w-z) * (w-z) powi n"
      by auto
    moreover have "(w-z) powi n \0"
      using that by auto
    ultimately show ?thesis
      using mult_cancel_right by blast
  qed
  then have "\\<^sub>F w in at z. zor_poly f z w = zor_poly ff 0 (w-z)"
    unfolding eventually_at
    by (metis DiffI \<open>0 < r\<close> dist_commute mem_ball singletonD)
  moreover have "isCont (zor_poly f z) z"
    using holo1[THEN holomorphic_on_imp_continuous_on]
    by (simp add: \<open>0 < r1\<close> continuous_on_interior)
  moreover
  have "isCont (zor_poly ff 0) 0"
    using \<open>0 < r2\<close> continuous_on_interior holo2 holomorphic_on_imp_continuous_on
    by fastforce
  then have "isCont (\w. zor_poly ff 0 (w-z)) z"
      unfolding isCont_iff by simp
  ultimately show "\\<^sub>F w in nhds z. zor_poly f z w = zor_poly ff 0 (w-z)"
    by (elim at_within_isCont_imp_nhds;auto)
qed

lemma
  fixes f g:: "complex \ complex" and z::complex
  assumes f_iso: "isolated_singularity_at f z" and g_iso: "isolated_singularity_at g z"
      and f_ness: "not_essential f z" and g_ness: "not_essential g z"
      and fg_nconst: "\\<^sub>Fw in (at z). f w * g w\ 0"
  shows zorder_times: "zorder (\w. f w * g w) z = zorder f z + zorder g z" and
        zor_poly_times: "\\<^sub>Fw in (at z). zor_poly (\w. f w * g w) z w
                                                  = zor_poly f z w *zor_poly g z w"
proof -
  define fg where "fg = (\w. f w * g w)"
  define fn gn fgn where
    "fn = zorder f z" and "gn = zorder g z" and "fgn = zorder fg z"
  define fp gp fgp where
    "fp = zor_poly f z" and "gp = zor_poly g z" and "fgp = zor_poly fg z"
  have f_nconst: "\\<^sub>Fw in (at z). f w \ 0" and g_nconst: "\\<^sub>Fw in (at z).g w\ 0"
    using fg_nconst by (auto elim!:frequently_elim1)
  obtain fr where [simp]: "fp z \ 0" and "fr > 0"
          and fr: "fp holomorphic_on cball z fr"
                  "\w\cball z fr - {z}. f w = fp w * (w-z) powi fn \ fp w \ 0"
    using zorder_exist[OF f_iso f_ness f_nconst,folded fp_def fn_def] by auto
  obtain gr where [simp]: "gp z \ 0" and "gr > 0"
          and gr: "gp holomorphic_on cball z gr"
                  "\w\cball z gr - {z}. g w = gp w * (w-z) powi gn \ gp w \ 0"
    using zorder_exist[OF g_iso g_ness g_nconst,folded gn_def gp_def] by auto
  define r1 where "r1=min fr gr"
  have "r1>0" unfolding r1_def using \<open>fr>0\<close> \<open>gr>0\<close> by auto
  have fg_times: "fg w = (fp w * gp w) * (w-z) powi (fn+gn)" and fgp_nz: "fp w*gp w\0"
    when "w\ball z r1 - {z}" for w
  proof -
    have "f w = fp w * (w-z) powi fn" "fp w \ 0"
      using fr(2) r1_def that by auto
    moreover have "g w = gp w * (w-z) powi gn" "gp w \ 0"
      using gr(2) that unfolding r1_def by auto
--> --------------------

--> maximum size reached

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

quality99%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.10Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders