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%

¤ Dauer der Verarbeitung: 0.39 Sekunden (vorverarbeitet) ¤

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.