
diff -r 0c073854e6ce -r 607e1e345e8f src/HOL/Complex_Analysis/Complex_Singularities.thy
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy	Tue Feb 07 14:10:15 2023 +0000
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy	Wed Feb 08 15:05:24 2023 +0000
@@ -26,8 +26,18 @@
 lemma is_pole_tendsto:
   fixes f::"('a::topological_space \<Rightarrow> 'b::real_normed_div_algebra)"
   shows "is_pole f x \<Longrightarrow> ((inverse o f) \<longlongrightarrow> 0) (at x)"
-unfolding is_pole_def
-by (auto simp add:filterlim_inverse_at_iff[symmetric] comp_def filterlim_at)
+  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 \<Rightarrow> 'b::real_normed_vector)"
+  shows "is_pole f z \<longleftrightarrow> is_pole (\<lambda>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 \<Rightarrow> 'b::real_normed_vector)"
+  shows "NO_MATCH 0 z \<Longrightarrow> is_pole f z \<longleftrightarrow> is_pole (\<lambda>x. f (z + x)) 0"
+  by (metis is_pole_shift_0)
 
 lemma is_pole_inverse_holomorphic:
   assumes "open s"
@@ -71,6 +81,23 @@
   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]:
+  "c \<noteq> 0 \<Longrightarrow> is_pole (\<lambda>z. c * f z :: 'a :: real_normed_field) z \<longleftrightarrow> is_pole f z"
+proof
+  assume *: "c \<noteq> 0" "is_pole (\<lambda>z. c * f z) z"
+  have "is_pole (\<lambda>z. inverse c * (c * f z)) z" unfolding is_pole_def
+    by (rule tendsto_mult_filterlim_at_infinity tendsto_const)+ (use * in \<open>auto simp: is_pole_def\<close>)
+  thus "is_pole f z"
+    using *(1) by (simp add: field_simps)
+next
+  assume *: "c \<noteq> 0" "is_pole f z"
+  show "is_pole (\<lambda>z. c * f z) z" unfolding is_pole_def 
+    by (rule tendsto_mult_filterlim_at_infinity tendsto_const)+ (use * in \<open>auto simp: is_pole_def\<close>)
+qed
+
+lemma is_pole_uminus_iff [simp]: "is_pole (\<lambda>z. -f z :: 'a :: real_normed_field) z \<longleftrightarrow> 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 (\<lambda>z::complex. 1 / (z - a)) a"
   using is_pole_inverse_power[of 1 a] by simp
 
@@ -80,7 +107,7 @@
   shows   "is_pole (\<lambda>z. f z / g z) z"
 proof -
   have "filterlim (\<lambda>z. f z * inverse (g z)) at_infinity (at z)"
-    using assms filterlim_compose filterlim_inverse_at_infinity isCont_def 
+    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
@@ -113,6 +140,62 @@
 definition isolated_singularity_at::"[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where
   "isolated_singularity_at f z = (\<exists>r>0. f analytic_on ball z r-{z})"
 
+lemma removable_singularity:
+  assumes "f holomorphic_on A - {x}" "open A"
+  assumes "f \<midarrow>x\<rightarrow> c"
+  shows   "(\<lambda>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 \<in> A"
+    show "(?g \<longlongrightarrow> ?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 \<longlongrightarrow> ?g y) (at y within A - {x})"
+        using False y by (auto simp: continuous_on_def)
+      also have "?this \<longleftrightarrow> (?g \<longlongrightarrow> ?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 \<midarrow>x\<rightarrow> c"
+        by fact
+      also have "?this \<longleftrightarrow> (?g \<longlongrightarrow> ?g y) (at y)"
+        by (intro filterlim_cong) (auto simp: eventually_at_filter)
+      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
+    by (rule no_isolated_singularity) (use assms in auto)
+qed
+
+lemma removable_singularity':
+  assumes "isolated_singularity_at f z"
+  assumes "f \<midarrow>z\<rightarrow> c"
+  shows   "(\<lambda>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 "(\<lambda>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:
@@ -137,7 +220,7 @@
       define f' where "f' \<equiv> \<lambda>x. (x - z) powr (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> 
+        using \<open>n>m\<close>
           by (auto simp add: Lim_ident_at  intro!:tendsto_powr_complex_0 tendsto_eq_intros)
       ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
         by (simp add: continuous_within)
@@ -165,7 +248,7 @@
       define f' where "f' \<equiv>\<lambda>x. (x - z) powr (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> 
+        using \<open>m>n\<close>
         by (auto simp: Lim_ident_at intro!:tendsto_powr_complex_0 tendsto_eq_intros)
       ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
         by (simp add: continuous_within)
@@ -272,7 +355,7 @@
     ultimately show ?thesis by auto
   qed
 
-  have ?thesis when "\<exists>x. (f \<longlongrightarrow> x) (at z)"  
+  have ?thesis when "\<exists>x. (f \<longlongrightarrow> 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"
@@ -312,7 +395,7 @@
     have "P f (-n) (inverse o g) r"
     proof -
       have "f w = inverse (g w) * (w - z) powr of_int (- n)" when "w\<in>cball z r - {z}" for w
-        by (metis g_fac h_def inverse_inverse_eq inverse_mult_distrib of_int_minus 
+        by (metis g_fac h_def inverse_inverse_eq inverse_mult_distrib of_int_minus
             powr_minus that)
       then show ?thesis
         unfolding P_def comp_def
@@ -398,7 +481,7 @@
     have "(\<lambda>w. inverse ((f w) ^ (nat (-n)))) \<midarrow>z\<rightarrow>?xx"
       using assms False unfolding filterlim_at by (auto intro!:tendsto_eq_intros)
     then have "fp \<midarrow>z\<rightarrow> ?xx"
-      by (smt (verit) LIM_cong fp_def inverse_nonzero_iff_nonzero power_eq_0_iff powr_eq_0_iff 
+      by (smt (verit) LIM_cong fp_def inverse_nonzero_iff_nonzero power_eq_0_iff powr_eq_0_iff
           powr_of_int that zero_less_nat_eq)
     then show ?thesis unfolding fp_def not_essential_def by auto
   qed
@@ -520,7 +603,7 @@
         using that by (auto intro!:tendsto_eq_intros)
       then have "fg \<midarrow>z\<rightarrow> 0"
         using Lim_transform_within[OF _ \<open>r1>0\<close>]
-        by (smt (verit, ccfv_SIG) DiffI dist_commute dist_nz fg_times mem_ball powr_of_int right_minus_eq 
+        by (smt (verit, ccfv_SIG) DiffI dist_commute dist_nz fg_times mem_ball powr_of_int right_minus_eq
             singletonD that)
       then show ?thesis unfolding not_essential_def fg_def by auto
     qed
@@ -629,7 +712,7 @@
       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 
+    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}"
@@ -712,9 +795,114 @@
   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_shift:
+  assumes "isolated_singularity_at (\<lambda>x. f (x + w)) z"
+  shows   "isolated_singularity_at f (z + w)"
+proof -
+  from assms obtain r where r: "r > 0" and ana: "(\<lambda>x. f (x + w)) analytic_on ball z r - {z}"
+    unfolding isolated_singularity_at_def by blast
+  have "((\<lambda>x. f (x + w)) \<circ> (\<lambda>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) \<longleftrightarrow> isolated_singularity_at (\<lambda>x. f (x + w)) z"
+  using isolated_singularity_at_shift[of f w z]
+        isolated_singularity_at_shift[of "\<lambda>x. f (x + w)" "-w" "w + z"]
+  by (auto simp: algebra_simps)
+
+lemma isolated_singularity_at_shift_0:
+  "NO_MATCH 0 z \<Longrightarrow> isolated_singularity_at f z \<longleftrightarrow> isolated_singularity_at (\<lambda>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 (\<lambda>x. f (x + w)) z"
+  shows   "not_essential f (z + w)"
+proof -
+  from assms consider c where "(\<lambda>x. f (x + w)) \<midarrow>z\<rightarrow> c" | "is_pole (\<lambda>x. f (x + w)) z"
+    unfolding not_essential_def by blast
+  thus ?thesis
+  proof cases
+    case (1 c)
+    hence "f \<midarrow>z + w\<rightarrow> 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) \<longleftrightarrow> not_essential (\<lambda>x. f (x + w)) z"
+  using not_essential_shift[of f w z]
+        not_essential_shift[of "\<lambda>x. f (x + w)" "-w" "w + z"]
+  by (auto simp: algebra_simps)
+
+lemma not_essential_shift_0:
+  "NO_MATCH 0 z \<Longrightarrow> not_essential f z \<longleftrightarrow> not_essential (\<lambda>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 \<in> A" "open A"
+  shows   "not_essential f x"
+proof -
+  have "continuous_on A f"
+    using assms holomorphic_on_imp_continuous_on by blast
+  hence "f \<midarrow>x\<rightarrow> f x"
+    using assms continuous_on_eq_continuous_at isContD by blast
+  thus ?thesis
+    by (auto simp: not_essential_def)
+qed
+
+lemma eventually_not_pole:
+  assumes "isolated_singularity_at f z"
+  shows   "eventually (\<lambda>w. \<not>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 (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+    by (intro eventually_at_in_open) auto
+  thus "eventually (\<lambda>w. \<not>is_pole f w) (at z)"
+  proof eventually_elim
+    case (elim w)
+    with r show ?case
+      using analytic_imp_holomorphic not_is_pole_holomorphic open_delete by blast
+  qed
+qed
+
+lemma not_islimpt_poles:
+  assumes "isolated_singularity_at f z"
+  shows   "\<not>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} \<Longrightarrow> \<not>is_pole f z"
+  using analytic_at not_is_pole_holomorphic by blast
+
+lemma not_essential_const [singularity_intros]: "not_essential (\<lambda>_. c) z"
+  unfolding not_essential_def by (rule exI[of _ c]) auto
+
+lemma not_essential_uminus [singularity_intros]:
+  assumes f_ness: "not_essential f z"
+  assumes f_iso:"isolated_singularity_at f z"
+  shows "not_essential (\<lambda>w. -f w) z"
+proof -
+  have "not_essential (\<lambda>w. -1 * f w) z"
+    by (intro assms singularity_intros)
+  thus ?thesis by simp
+qed
+
 subsubsection \<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. (\<exists>h r. r>0 \<and> h holomorphic_on cball z r \<and> h z\<noteq>0
                    \<and> (\<forall>w\<in>cball z r - {z}. f w =  h w * (w-z) powr (of_int n)
@@ -749,6 +937,29 @@
   then show ?thesis unfolding P_def by auto
 qed
 
+lemma zorder_shift:
+  shows  "zorder f z = zorder (\<lambda>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 (\<lambda>u. u-z)" in exI)
+    apply (rule_tac x="r" in exI)
+    apply (intro conjI holomorphic_on_compose holomorphic_intros)
+       apply (simp_all add: 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 \<Longrightarrow> zorder f z = zorder (\<lambda>u. f (u + z)) 0"
+  by (rule zorder_shift)
+
 lemma
   fixes f::"complex \<Rightarrow> complex" and z::complex
   assumes f_iso:"isolated_singularity_at f z"
@@ -819,6 +1030,99 @@
     by (metis DiffI dist_commute mem_ball singletonD)
 qed
 
+lemma zor_poly_shift:
+  assumes iso1: "isolated_singularity_at f z"
+    and ness1: "not_essential f z"
+    and nzero1: "\<exists>\<^sub>F w in at z. f w \<noteq> 0"
+  shows "\<forall>\<^sub>F w in nhds z. zor_poly f z w = zor_poly (\<lambda>u. f (z + u)) 0 (w-z)"
+proof -
+  obtain r1 where "r1>0" "zor_poly f z z \<noteq> 0" and
+      holo1:"zor_poly f z holomorphic_on cball z r1" and
+      rball1:"\<forall>w\<in>cball z r1 - {z}.
+           f w = zor_poly f z w * (w - z) powr of_int (zorder f z) \<and>
+           zor_poly f z w \<noteq> 0"
+    using zorder_exist[OF iso1 ness1 nzero1] by blast
+
+  define ff where "ff=(\<lambda>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 "\<exists>\<^sub>F w in at 0. ff w \<noteq> 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 \<noteq> 0" and
+      holo2:"zor_poly ff 0 holomorphic_on cball 0 r2" and
+      rball2:"\<forall>w\<in>cball 0 r2 - {0}.
+           ff w = zor_poly ff 0 w * w powr of_int (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\<in>ball z r - {z}" for w
+  proof -
+    define n::complex where "n= of_int (zorder f z)"
+
+    have "f w = zor_poly f z w * (w - z) powr n"
+    proof -
+      have "w\<in>cball z r1 - {z}"
+        using r_def that by auto
+      from rball1[rule_format, OF this]
+      show ?thesis unfolding n_def by auto
+    qed
+
+    moreover have "f w = zor_poly ff 0 (w - z) * (w - z) powr n"
+    proof -
+      have "w-z\<in>cball 0 r2 - {0}"
+        using r_def that by (auto simp:dist_complex_def)
+      from rball2[rule_format, OF this]
+      have "ff (w - z) = zor_poly ff 0 (w - z) * (w - z)
+                            powr of_int (zorder ff 0)"
+        by simp
+      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) powr n
+                = zor_poly ff 0 (w - z) * (w - z) powr n"
+      by auto
+    moreover have "(w - z) powr n \<noteq>0"
+      using that by auto
+    ultimately show ?thesis
+      apply (subst (asm) mult_cancel_right)
+      by (simp add:ff_def)
+  qed
+  then have "\<forall>\<^sub>F w in at z. zor_poly f z w
+                  = zor_poly ff 0 (w - z)"
+    unfolding eventually_at
+    apply (rule_tac x=r in exI)
+    using \<open>r>0\<close> by (auto simp:dist_commute)
+  moreover have "isCont (zor_poly f z) z"
+    using holo1[THEN holomorphic_on_imp_continuous_on]
+    apply (elim continuous_on_interior)
+    using \<open>r1>0\<close> by auto
+  moreover have "isCont (\<lambda>w. zor_poly ff 0 (w - z)) z"
+  proof -
+    have "isCont (zor_poly ff 0) 0"
+      using holo2[THEN holomorphic_on_imp_continuous_on]
+      apply (elim continuous_on_interior)
+      using \<open>r2>0\<close> by auto
+    then show ?thesis
+      unfolding isCont_iff by simp
+  qed
+  ultimately show "\<forall>\<^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 \<Rightarrow> complex" and z::complex
   assumes f_iso:"isolated_singularity_at f z" and g_iso:"isolated_singularity_at g z"
@@ -979,7 +1283,7 @@
   have fz_lim: "f\<midarrow> z \<rightarrow> f z"
     by (metis assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on)
   have gz_lim: "g \<midarrow>z\<rightarrow>g z"
-    by (metis r open_ball at_within_open ball_subset_cball centre_in_ball 
+    by (metis r open_ball at_within_open ball_subset_cball centre_in_ball
         continuous_on_def continuous_on_subset holomorphic_on_imp_continuous_on)
   have if_0:"if f z=0 then n > 0 else n=0"
   proof -
@@ -1185,7 +1489,7 @@
         unfolding z'_def using \<open>d>0\<close> \<open>r>0\<close> by (auto simp add:dist_norm)
       moreover have "f z' \<noteq> 0"
       proof (subst fg_eq[OF _ \<open>z'\<noteq>z\<close>])
-        have "z' \<in> cball z r" 
+        have "z' \<in> cball z r"
           unfolding z'_def using \<open>r>0\<close> \<open>d>0\<close> by (auto simp add:dist_norm)
         then show " z' \<in> s" using r(2) by blast
         show "g z' * (z' - z) powr of_int n \<noteq> 0"
@@ -1493,4 +1797,476 @@
   from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis .
 qed
 
-end
\ No newline at end of file
+lemma
+  assumes "is_pole f (x :: complex)" "open A" "x \<in> A"
+  assumes "\<And>y. y \<in> A - {x} \<Longrightarrow> (f has_field_derivative f' y) (at y)"
+  shows   is_pole_deriv': "is_pole f' x"
+    and   zorder_deriv':  "zorder f' x = zorder f x - 1"
+proof -
+  have holo: "f holomorphic_on A - {x}"
+    using assms by (subst holomorphic_on_open) auto
+  obtain r where r: "r > 0" "ball x r \<subseteq> A"
+    using assms(2,3) openE by blast
+  moreover have "open (ball x r - {x})"
+    by auto
+  ultimately have "isolated_singularity_at f x"
+    by (auto simp: isolated_singularity_at_def analytic_on_open
+             intro!: exI[of _ r] holomorphic_on_subset[OF holo])
+  hence ev: "\<forall>\<^sub>F w in at x. zor_poly f x w = f w * (w - x) ^ nat (- zorder f x)"
+    using \<open>is_pole f x\<close> zor_poly_pole_eq by blast
+
+  define P where "P = zor_poly f x"
+  define n where "n = nat (-zorder f x)"
+
+  obtain r where r: "r > 0" "cball x r \<subseteq> A" "P holomorphic_on cball x r" "zorder f x < 0" "P x \<noteq> 0"
+    "\<forall>w\<in>cball x r - {x}. f w = P w / (w - x) ^ n \<and> P w \<noteq> 0"
+    unfolding P_def n_def using zorder_exist_pole[OF holo assms(2,3,1)] by blast
+  have n: "n > 0"
+    using r(4) by (auto simp: n_def)
+
+  have [derivative_intros]: "(P has_field_derivative deriv P w) (at w)"
+    if "w \<in> ball x r" for w
+    using that by (intro holomorphic_derivI[OF holomorphic_on_subset[OF r(3), of "ball x r"]]) auto
+
+  define D where "D = (\<lambda>w. (deriv P w * (w - x) - of_nat n * P w) / (w - x) ^ (n + 1))"
+  define n' where "n' = n - 1"
+  have n': "n = Suc n'"
+    using n by (simp add: n'_def)
+
+  have "eventually (\<lambda>w. w \<in> ball x r) (nhds x)"
+    using \<open>r > 0\<close> by (intro eventually_nhds_in_open) auto
+  hence ev'': "eventually (\<lambda>w. w \<in> ball x r - {x}) (at x)"
+    by (auto simp: eventually_at_filter elim: eventually_mono)
+
+  {
+    fix w assume w: "w \<in> ball x r - {x}"
+    have ev': "eventually (\<lambda>w. w \<in> ball x r - {x}) (nhds w)"
+      using w by (intro eventually_nhds_in_open) auto
+
+    have "((\<lambda>w. P w / (w - x) ^ n) has_field_derivative D w) (at w)"
+      apply (rule derivative_eq_intros refl | use w in force)+
+      using w
+      apply (simp add: divide_simps D_def)
+      apply (simp add: n' algebra_simps)
+      done
+    also have "?this \<longleftrightarrow> (f has_field_derivative D w) (at w)"
+      using r by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev']) auto
+    finally have "(f has_field_derivative D w) (at w)" .
+    moreover have "(f has_field_derivative f' w) (at w)"
+      using w r by (intro assms) auto
+    ultimately have "D w = f' w"
+      using DERIV_unique by blast
+  } note D_eq = this
+
+  have "is_pole D x"
+    unfolding D_def using n \<open>r > 0\<close> \<open>P x \<noteq> 0\<close>
+    by (intro is_pole_basic[where A = "ball x r"] holomorphic_intros holomorphic_on_subset[OF r(3)]) auto
+  also have "?this \<longleftrightarrow> is_pole f' x"
+    by (intro is_pole_cong eventually_mono[OF ev''] D_eq) auto
+  finally show "is_pole f' x" .
+
+  have "zorder f' x = -int (Suc n)"
+  proof (rule zorder_eqI)
+    show "open (ball x r)" "x \<in> ball x r"
+      using \<open>r > 0\<close> by auto
+    show "f' w = (deriv P w * (w - x) - of_nat n * P w) * (w - x) powr of_int (- int (Suc n))"
+      if "w \<in> ball x r" "w \<noteq> x" for w
+      using that D_eq[of w] n by (auto simp: D_def powr_diff powr_minus powr_nat' divide_simps)
+  qed (use r n in \<open>auto intro!: holomorphic_intros\<close>)
+  thus "zorder f' x = zorder f x - 1"
+    using n by (simp add: n_def)
+qed
+
+lemma
+  assumes "is_pole f (x :: complex)" "isolated_singularity_at f x"
+  shows   is_pole_deriv: "is_pole (deriv f) x"
+    and   zorder_deriv:  "zorder (deriv f) x = zorder f x - 1"
+proof -
+  from assms(2) obtain r where r: "r > 0" "f analytic_on ball x r - {x}"
+    by (auto simp: isolated_singularity_at_def)
+  hence holo: "f holomorphic_on ball x r - {x}"
+    by (subst (asm) analytic_on_open) auto
+  have *: "x \<in> ball x r" "open (ball x r)" "open (ball x r - {x})"
+    using \<open>r > 0\<close> by auto
+  show "is_pole (deriv f) x" "zorder (deriv f) x = zorder f x - 1"
+    by (rule is_pole_deriv' zorder_deriv', (rule assms * holomorphic_derivI holo | assumption)+)+
+qed
+
+lemma removable_singularity_deriv':
+  assumes "f \<midarrow>x\<rightarrow> c" "x \<in> A" "open (A :: complex set)"
+  assumes "\<And>y. y \<in> A - {x} \<Longrightarrow> (f has_field_derivative f' y) (at y)"
+  shows   "\<exists>c. f' \<midarrow>x\<rightarrow> c"
+proof -
+  have holo: "f holomorphic_on A - {x}"
+    using assms by (subst holomorphic_on_open) auto
+
+  define g where "g = (\<lambda>y. if y = x then c else f y)"
+  have deriv_g_eq: "deriv g y = f' y" if "y \<in> A - {x}" for y
+  proof -
+    have ev: "eventually (\<lambda>y. y \<in> A - {x}) (nhds y)"
+      using that assms by (intro eventually_nhds_in_open) auto
+    have "(f has_field_derivative f' y) (at y)"
+      using assms that by auto
+    also have "?this \<longleftrightarrow> (g has_field_derivative f' y) (at y)"
+      by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev]) (auto simp: g_def)
+    finally show ?thesis
+      by (intro DERIV_imp_deriv assms)
+  qed
+
+  have "g holomorphic_on A"
+    unfolding g_def using assms assms(1) holo by (intro removable_singularity) auto
+  hence "deriv g holomorphic_on A"
+    by (intro holomorphic_deriv assms)
+  hence "continuous_on A (deriv g)"
+    by (meson holomorphic_on_imp_continuous_on)
+  hence "(deriv g \<longlongrightarrow> deriv g x) (at x within A)"
+    using assms by (auto simp: continuous_on_def)
+  also have "?this \<longleftrightarrow> (f' \<longlongrightarrow> deriv g x) (at x within A)"
+    by (intro filterlim_cong refl) (auto simp: eventually_at_filter deriv_g_eq)
+  finally have "f' \<midarrow>x\<rightarrow> deriv g x"
+    using \<open>open A\<close> \<open>x \<in> A\<close> by (meson tendsto_within_open)
+  thus ?thesis
+    by blast
+qed
+
+lemma removable_singularity_deriv:
+  assumes "f \<midarrow>x\<rightarrow> c" "isolated_singularity_at f x"
+  shows   "\<exists>c. deriv f \<midarrow>x\<rightarrow> c"
+proof -
+  from assms(2) obtain r where r: "r > 0" "f analytic_on ball x r - {x}"
+    by (auto simp: isolated_singularity_at_def)
+  hence holo: "f holomorphic_on ball x r - {x}"
+    using analytic_imp_holomorphic by blast
+  show ?thesis
+    using assms(1)
+  proof (rule removable_singularity_deriv')
+    show "x \<in> ball x r" "open (ball x r)"
+      using \<open>r > 0\<close> by auto
+  qed (auto intro!: holomorphic_derivI[OF holo])
+qed
+
+lemma not_essential_deriv':
+  assumes "not_essential f x" "x \<in> A" "open A"
+  assumes "\<And>y. y \<in> A - {x} \<Longrightarrow> (f has_field_derivative f' y) (at y)"
+  shows   "not_essential f' x"
+proof -
+  have holo: "f holomorphic_on A - {x}"
+    using assms by (subst holomorphic_on_open) auto
+  from assms consider "is_pole f x" | c where "f \<midarrow>x\<rightarrow> c"
+    by (auto simp: not_essential_def)
+  thus ?thesis
+  proof cases
+    case 1
+    hence "is_pole f' x"
+      using is_pole_deriv' assms by blast
+    thus ?thesis by (auto simp: not_essential_def)
+  next
+    case (2 c)
+    from 2 have "\<exists>c. f' \<midarrow>x\<rightarrow> c"
+      by (rule removable_singularity_deriv'[OF _ assms(2-4)])
+    thus ?thesis
+      by (auto simp: not_essential_def)
+  qed
+qed
+
+lemma not_essential_deriv[singularity_intros]:
+  assumes "not_essential f x" "isolated_singularity_at f x"
+  shows   "not_essential (deriv f) x"
+proof -
+  from assms(2) obtain r where r: "r > 0" "f analytic_on ball x r - {x}"
+    by (auto simp: isolated_singularity_at_def)
+  hence holo: "f holomorphic_on ball x r - {x}"
+    by (subst (asm) analytic_on_open) auto
+  show ?thesis
+    using assms(1)
+  proof (rule not_essential_deriv')
+    show "x \<in> ball x r" "open (ball x r)"
+      using \<open>r > 0\<close> by auto
+  qed (auto intro!: holomorphic_derivI[OF holo])
+qed
+
+lemma not_essential_frequently_0_imp_tendsto_0:
+  fixes f :: "complex \<Rightarrow> complex"
+  assumes sing: "isolated_singularity_at f z" "not_essential f z"
+  assumes freq: "frequently (\<lambda>z. f z = 0) (at z)"
+  shows   "f \<midarrow>z\<rightarrow> 0"
+proof -
+  from freq obtain g :: "nat \<Rightarrow> complex" where g: "filterlim g (at z) at_top" "\<And>n. f (g n) = 0"
+    using frequently_atE by blast
+  have "eventually (\<lambda>x. f (g x) = 0) sequentially"
+    using g by auto
+  hence fg: "(\<lambda>x. f (g x)) \<longlonglongrightarrow> 0"
+    by (simp add: tendsto_eventually)
+
+  from assms(2) consider c where "f \<midarrow>z\<rightarrow> c" | "is_pole f z"
+    unfolding not_essential_def by blast
+  thus ?thesis
+  proof cases
+    case (1 c)
+    have "(\<lambda>x. f (g x)) \<longlonglongrightarrow> c"
+      by (rule filterlim_compose[OF 1 g(1)])
+    with fg have "c = 0"
+      using LIMSEQ_unique by blast
+    with 1 show ?thesis by simp
+  next
+    case 2
+    have "filterlim (\<lambda>x. f (g x)) at_infinity sequentially"
+      by (rule filterlim_compose[OF _ g(1)]) (use 2 in \<open>auto simp: is_pole_def\<close>)
+    with fg have False
+      by (meson not_tendsto_and_filterlim_at_infinity sequentially_bot)
+    thus ?thesis ..
+  qed
+qed
+
+lemma not_essential_frequently_0_imp_eventually_0:
+  fixes f :: "complex \<Rightarrow> complex"
+  assumes sing: "isolated_singularity_at f z" "not_essential f z"
+  assumes freq: "frequently (\<lambda>z. f z = 0) (at z)"
+  shows   "eventually (\<lambda>z. f z = 0) (at z)"
+proof -
+  from sing obtain r where r: "r > 0" and "f analytic_on ball z r - {z}"
+    by (auto simp: isolated_singularity_at_def)
+  hence holo: "f holomorphic_on ball z r - {z}"
+    by (subst (asm) analytic_on_open) auto
+  have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+    using r by (intro eventually_at_in_open) auto
+  from freq and this have "frequently (\<lambda>w. f w = 0 \<and> w \<in> ball z r - {z}) (at z)"
+    using frequently_eventually_frequently by blast
+  hence "frequently (\<lambda>w. w \<in> {w\<in>ball z r - {z}. f w = 0}) (at z)"
+    by (simp add: conj_commute)
+  hence limpt: "z islimpt {w\<in>ball z r - {z}. f w = 0}"
+    using islimpt_conv_frequently_at by blast
+
+  define g where "g = (\<lambda>w. if w = z then 0 else f w)"
+  have "f \<midarrow>z\<rightarrow> 0"
+    by (intro not_essential_frequently_0_imp_tendsto_0 assms)
+  hence g_holo: "g holomorphic_on ball z r"
+    unfolding g_def by (intro removable_singularity holo) auto
+
+  have g_eq_0: "g w = 0" if "w \<in> ball z r" for w
+  proof (rule analytic_continuation[where f = g])
+    show "open (ball z r)" "connected (ball z r)"
+      using r by auto
+    show "z islimpt {w\<in>ball z r - {z}. f w = 0}"
+      by fact
+    show "g w = 0" if "w \<in> {w \<in> ball z r - {z}. f w = 0}" for w
+      using that by (auto simp: g_def)
+  qed (use r that g_holo in auto)
+
+  have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+    using r by (intro eventually_at_in_open) auto
+  thus "eventually (\<lambda>w. f w = 0) (at z)"
+  proof eventually_elim
+    case (elim w)
+    thus ?case using g_eq_0[of w]
+      by (auto simp: g_def)
+  qed
+qed
+
+lemma pole_imp_not_constant:
+  fixes f :: "'a :: {perfect_space} \<Rightarrow> _"
+  assumes "is_pole f x" "open A" "x \<in> A" "A \<subseteq> insert x B"
+  shows   "\<not>f constant_on B"
+proof
+  assume *: "f constant_on B"
+  then obtain c where c: "\<forall>x\<in>B. f x = c"
+    by (auto simp: constant_on_def)
+  have "eventually (\<lambda>y. y \<in> A - {x}) (at x)"
+    using assms by (intro eventually_at_in_open) auto
+  hence "eventually (\<lambda>y. f y = c) (at x)"
+    by eventually_elim (use c assms in auto)
+  hence **: "f \<midarrow>x\<rightarrow> c"
+    by (simp add: tendsto_eventually)
+  show False
+    using not_tendsto_and_filterlim_at_infinity[OF _ ** assms(1)[unfolded is_pole_def]] by simp
+qed
+
+
+lemma neg_zorder_imp_is_pole:
+  assumes iso:"isolated_singularity_at f z" and f_ness:"not_essential f z"
+      and "zorder f z < 0" and fre_nz:"\<exists>\<^sub>F w in at z. f w \<noteq> 0 "
+    shows "is_pole f z"
+proof -
+  define P where "P = zor_poly f z"
+  define n where "n = zorder f z"
+  have "n<0" unfolding n_def by (simp add: assms(3))
+  define nn where "nn = nat (-n)"
+
+  obtain r where "P z \<noteq> 0" "r>0" and r_holo:"P holomorphic_on cball z r" and
+       w_Pn:"(\<forall>w\<in>cball z r - {z}. f w = P w * (w - z) powr of_int n \<and> P w \<noteq> 0)"
+    using zorder_exist[OF iso f_ness fre_nz,folded P_def n_def] by auto
+
+  have "is_pole (\<lambda>w. P w * (w - z) powr of_int n) z"
+    unfolding is_pole_def
+  proof (rule tendsto_mult_filterlim_at_infinity)
+    show "P \<midarrow>z\<rightarrow> P z"
+      by (meson open_ball \<open>0 < r\<close> ball_subset_cball centre_in_ball
+          continuous_on_eq_continuous_at continuous_on_subset
+          holomorphic_on_imp_continuous_on isContD r_holo)
+    show "P z\<noteq>0" by (simp add: \<open>P z \<noteq> 0\<close>)
+
+    have "LIM x at z. inverse ((x - z) ^ nat (-n)) :> at_infinity"
+      apply (subst filterlim_inverse_at_iff[symmetric])
+      using \<open>n<0\<close>
+      by (auto intro!:tendsto_eq_intros filterlim_atI
+              simp add:eventually_at_filter)
+    then show "LIM x at z. (x - z) powr of_int n :> at_infinity"
+    proof (elim filterlim_mono_eventually)
+      have "inverse ((x - z) ^ nat (-n)) = (x - z) powr of_int n"
+        if "x\<noteq>z" for x
+        apply (subst powr_of_int)
+        using \<open>n<0\<close> using that by auto
+      then show "\<forall>\<^sub>F x in at z. inverse ((x - z) ^ nat (-n))
+                  = (x - z) powr of_int n"
+        by (simp add: eventually_at_filter)
+    qed auto
+  qed
+  moreover have "\<forall>\<^sub>F w in at z. f w =  P w * (w - z) powr of_int n"
+    unfolding eventually_at_le
+    apply (rule exI[where x=r])
+    using w_Pn \<open>r>0\<close> by (simp add: dist_commute)
+  ultimately show ?thesis using is_pole_cong by fast
+qed
+
+lemma is_pole_divide_zorder:
+  fixes f g::"complex \<Rightarrow> 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: "\<exists>\<^sub>Fw in (at z). f w * g w\<noteq> 0"
+      and z_less:"zorder f z < zorder g z"
+    shows "is_pole (\<lambda>z. f z / g z) z"
+proof -
+  define fn gn fg where "fn=zorder f z" and "gn=zorder g z"
+                        and "fg=(\<lambda>w. f w / g w)"
+
+  have "isolated_singularity_at fg z"
+    unfolding fg_def using f_iso g_iso g_ness
+    by (auto intro:singularity_intros)
+  moreover have "not_essential fg z"
+    unfolding fg_def using f_iso g_iso g_ness f_ness
+    by (auto intro:singularity_intros)
+  moreover have "zorder fg z < 0"
+  proof -
+    have "zorder fg z = fn - gn"
+      using zorder_divide[OF f_iso g_iso f_ness g_ness
+            fg_nconst,folded fn_def gn_def fg_def] .
+    then show ?thesis
+      using z_less by (simp add: fn_def gn_def)
+  qed
+  moreover have "\<exists>\<^sub>F w in at z. fg w \<noteq> 0"
+    using fg_nconst unfolding fg_def by force
+  ultimately show "is_pole fg z"
+    using neg_zorder_imp_is_pole by auto
+qed
+
+lemma isolated_pole_imp_nzero_times:
+  assumes f_iso:"isolated_singularity_at f z"
+    and "is_pole f z"
+  shows "\<exists>\<^sub>Fw in (at z). deriv f w * f w \<noteq> 0"
+proof (rule ccontr)
+  assume "\<not> (\<exists>\<^sub>F w in at z.  deriv f w  * f w \<noteq> 0)"
+  then have "\<forall>\<^sub>F x in at z. deriv f x * f x = 0"
+    unfolding not_frequently by simp
+  moreover have "\<forall>\<^sub>F w in at z. f w \<noteq> 0"
+    using non_zero_neighbour_pole[OF \<open>is_pole f z\<close>] .
+  moreover have "\<forall>\<^sub>F w in at z. deriv f w \<noteq> 0"
+    using is_pole_deriv[OF \<open>is_pole f z\<close> f_iso,THEN non_zero_neighbour_pole]
+    .
+  ultimately have "\<forall>\<^sub>F w in at z. False"
+    apply eventually_elim
+    by auto
+  then show False by auto
+qed
+
+lemma isolated_pole_imp_neg_zorder:
+  assumes f_iso:"isolated_singularity_at f z"
+    and "is_pole f z"
+  shows "zorder f z<0"
+proof -
+  obtain e where [simp]:"e>0" and f_holo:"f holomorphic_on ball z e - {z}"
+    using f_iso analytic_imp_holomorphic unfolding isolated_singularity_at_def by blast
+  show ?thesis
+    using zorder_exist_pole[OF f_holo,simplified,OF \<open>is_pole f z\<close>]
+    by auto
+qed
+
+lemma isolated_singularity_at_deriv[singularity_intros]:
+  assumes "isolated_singularity_at f x"
+  shows "isolated_singularity_at (deriv f) x"
+proof -
+  obtain r where "r>0" "f analytic_on ball x r - {x}"
+    using assms unfolding isolated_singularity_at_def by auto
+  from analytic_deriv[OF this(2)]
+  have "deriv f analytic_on ball x r - {x}" .
+  with \<open>r>0\<close> show ?thesis
+    unfolding isolated_singularity_at_def by auto
+qed
+
+lemma zorder_deriv_minus_1:
+  fixes f g::"complex \<Rightarrow> complex" and z::complex
+  assumes f_iso:"isolated_singularity_at f z"
+      and f_ness:"not_essential f z"
+      and f_nconst:"\<exists>\<^sub>F w in at z. f w \<noteq> 0"
+      and f_ord:"zorder f z \<noteq>0"
+    shows "zorder (deriv f) z = zorder f z - 1"
+proof -
+  define P where "P = zor_poly f z"
+  define n where "n = zorder f z"
+  have "n\<noteq>0" unfolding n_def using f_ord by auto
+
+  obtain r where "P z \<noteq> 0" "r>0" and P_holo:"P holomorphic_on cball z r"
+          and "(\<forall>w\<in>cball z r - {z}. f w
+                            = P w * (w - z) powr of_int n \<and> P w \<noteq> 0)"
+    using zorder_exist[OF f_iso f_ness f_nconst,folded P_def n_def] by auto
+  from this(4)
+  have f_eq:"(\<forall>w\<in>cball z r - {z}. f w
+                            = P w * (w - z) powi n \<and> P w \<noteq> 0)"
+    using complex_powr_of_int f_ord n_def by presburger
+
+  define D where "D = (\<lambda>w. (deriv P w * (w - z) + of_int n * P w)
+                          * (w - z) powi (n - 1))"
+
+  have deriv_f_eq:"deriv f w = D w" if "w \<in> ball z r - {z}" for w
+  proof -
+    have ev': "eventually (\<lambda>w. w \<in> ball z r - {z}) (nhds w)"
+      using that by (intro eventually_nhds_in_open) auto
+
+    define wz where "wz = w - z"
+
+    have "wz \<noteq>0" unfolding wz_def using that by auto
+    moreover have "(P has_field_derivative deriv P w) (at w)"
+      by (meson DiffD1 Elementary_Metric_Spaces.open_ball P_holo
+          ball_subset_cball holomorphic_derivI holomorphic_on_subset that)
+    ultimately have "((\<lambda>w. P w * (w - z) powi n) has_field_derivative D w) (at w)"
+      unfolding D_def using that
+      apply (auto intro!: derivative_eq_intros)
+      apply (fold wz_def)
+      by (auto simp:algebra_simps simp flip:power_int_add_1')
+    also have "?this \<longleftrightarrow> (f has_field_derivative D w) (at w)"
+      using f_eq
+      by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev']) auto
+    ultimately have "(f has_field_derivative D w) (at w)" by simp
+    moreover have "(f has_field_derivative deriv f w) (at w)"
+      by (metis DERIV_imp_deriv calculation)
+    ultimately show ?thesis using DERIV_imp_deriv by blast
+  qed
+
+  show "zorder (deriv f) z = n - 1"
+  proof (rule zorder_eqI)
+    show "open (ball z r)" "z \<in> ball z r"
+      using \<open>r > 0\<close> by auto
+    define g where "g=(\<lambda>w. (deriv P w * (w - z) + of_int n * P w))"
+    show "g holomorphic_on ball z r"
+      unfolding g_def using P_holo
+      by (auto intro!:holomorphic_intros)
+    show "g z \<noteq> 0"
+      unfolding g_def using \<open>P z \<noteq> 0\<close> \<open>n\<noteq>0\<close> by auto
+    show "deriv f w =
+         (deriv P w * (w - z) + of_int n * P w) * (w - z) powr of_int (n - 1)"
+      if "w \<in> ball z r" "w \<noteq> z" for w
+      apply (subst complex_powr_of_int)
+      using deriv_f_eq that unfolding D_def by auto
+  qed
+qed
+
+end




