src/HOL/Complex_Analysis/Complex_Residues.thy

new lemmas for HOL-Complex_Analysis; overhaul of isolated_zeros

theory Complex_Residues
  imports Complex_Singularities
begin

subsection \<open>Definition of residues\<close>

text\<open>Wenda Li and LC Paulson (2016). A Formal Proof of Cauchy's Residue Theorem.
    Interactive Theorem Proving\<close>

definition\<^marker>\<open>tag important\<close> residue :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where
  "residue f z = (SOME int. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon><e
    \<longrightarrow> (f has_contour_integral 2*pi* \<i> *int) (circlepath z \<epsilon>))"

lemma residue_cong:
  assumes eq: "eventually (\<lambda>z. f z = g z) (at z)" and "z = z'"
  shows   "residue f z = residue g z'"
proof -
  from assms have eq': "eventually (\<lambda>z. g z = f z) (at z)"
    by (simp add: eq_commute)
  let ?P = "\<lambda>f c e. (\<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow>
   (f has_contour_integral of_real (2 * pi) * \<i> * c) (circlepath z \<epsilon>))"
  have "residue f z = residue g z" unfolding residue_def
  proof (rule Eps_cong)
    fix c :: complex
    have "\<exists>e>0. ?P g c e"
      if "\<exists>e>0. ?P f c e" and "eventually (\<lambda>z. f z = g z) (at z)" for f g
    proof -
      from that(1) obtain e where e: "e > 0" "?P f c e"
        by blast
      from that(2) obtain e' where e': "e' > 0" "\<And>z'. z' \<noteq> z \<Longrightarrow> dist z' z < e' \<Longrightarrow> f z' = g z'"
        unfolding eventually_at by blast
      have "?P g c (min e e')"
      proof (intro allI exI impI, goal_cases)
        case (1 \<epsilon>)
        hence "(f has_contour_integral of_real (2 * pi) * \<i> * c) (circlepath z \<epsilon>)"
          using e(2) by auto
        thus ?case
        proof (rule has_contour_integral_eq)
          fix z' assume "z' \<in> path_image (circlepath z \<epsilon>)"
          hence "dist z' z < e'" and "z' \<noteq> z"
            using 1 by (auto simp: dist_commute)
          with e'(2)[of z'] show "f z' = g z'" by simp
        qed
      qed
      moreover from e and e' have "min e e' > 0" by auto
      ultimately show ?thesis by blast
    qed
    from this[OF _ eq] and this[OF _ eq']
      show "(\<exists>e>0. ?P f c e) \<longleftrightarrow> (\<exists>e>0. ?P g c e)"
      by blast
  qed
  with assms show ?thesis by simp
qed

lemma contour_integral_circlepath_eq:
  assumes "open s" and f_holo:"f holomorphic_on (s-{z})" and "0<e1" "e1\<le>e2"
    and e2_cball:"cball z e2 \<subseteq> s"
  shows
    "f contour_integrable_on circlepath z e1"
    "f contour_integrable_on circlepath z e2"
    "contour_integral (circlepath z e2) f = contour_integral (circlepath z e1) f"
proof -
  define l where "l \<equiv> linepath (z+e2) (z+e1)"
  have [simp]:"valid_path l" "pathstart l=z+e2" "pathfinish l=z+e1" unfolding l_def by auto
  have "e2>0" using \<open>e1>0\<close> \<open>e1\<le>e2\<close> by auto
  have zl_img:"z\<notin>path_image l"
    proof
      assume "z \<in> path_image l"
      then have "e2 \<le> cmod (e2 - e1)"
        using segment_furthest_le[of z "z+e2" "z+e1" "z+e2",simplified] \<open>e1>0\<close> \<open>e2>0\<close> unfolding l_def
        by (auto simp add:closed_segment_commute)
      thus False using \<open>e2>0\<close> \<open>e1>0\<close> \<open>e1\<le>e2\<close>
        apply (subst (asm) norm_of_real)
        by auto
    qed
  define g where "g \<equiv> circlepath z e2 +++ l +++ reversepath (circlepath z e1) +++ reversepath l"
  show [simp]: "f contour_integrable_on circlepath z e2" "f contour_integrable_on (circlepath z e1)"
    proof -
      show "f contour_integrable_on circlepath z e2"
        apply (intro contour_integrable_continuous_circlepath[OF
                continuous_on_subset[OF holomorphic_on_imp_continuous_on[OF f_holo]]])
        using \<open>e2>0\<close> e2_cball by auto
      show "f contour_integrable_on (circlepath z e1)"
        apply (intro contour_integrable_continuous_circlepath[OF
                      continuous_on_subset[OF holomorphic_on_imp_continuous_on[OF f_holo]]])
        using \<open>e1>0\<close> \<open>e1\<le>e2\<close> e2_cball by auto
    qed
  have [simp]:"f contour_integrable_on l"
    proof -
      have "closed_segment (z + e2) (z + e1) \<subseteq> cball z e2" using \<open>e2>0\<close> \<open>e1>0\<close> \<open>e1\<le>e2\<close>
        by (intro closed_segment_subset,auto simp add:dist_norm)
      hence "closed_segment (z + e2) (z + e1) \<subseteq> s - {z}" using zl_img e2_cball unfolding l_def
        by auto
      then show "f contour_integrable_on l" unfolding l_def
        apply (intro contour_integrable_continuous_linepath[OF
                      continuous_on_subset[OF holomorphic_on_imp_continuous_on[OF f_holo]]])
        by auto
    qed
  let ?ig="\<lambda>g. contour_integral g f"
  have "(f has_contour_integral 0) g"
    proof (rule Cauchy_theorem_global[OF _ f_holo])
      show "open (s - {z})" using \<open>open s\<close> by auto
      show "valid_path g" unfolding g_def l_def by auto
      show "pathfinish g = pathstart g" unfolding g_def l_def by auto
    next
      have path_img:"path_image g \<subseteq> cball z e2"
        proof -
          have "closed_segment (z + e2) (z + e1) \<subseteq> cball z e2" using \<open>e2>0\<close> \<open>e1>0\<close> \<open>e1\<le>e2\<close>
            by (intro closed_segment_subset,auto simp add:dist_norm)
          moreover have "sphere z \<bar>e1\<bar> \<subseteq> cball z e2" using \<open>e2>0\<close> \<open>e1\<le>e2\<close> \<open>e1>0\<close> by auto
          ultimately show ?thesis unfolding g_def l_def using \<open>e2>0\<close>
            by (simp add: path_image_join closed_segment_commute)
        qed
      show "path_image g \<subseteq> s - {z}"
        proof -
          have "z\<notin>path_image g" using zl_img
            unfolding g_def l_def by (auto simp add: path_image_join closed_segment_commute)
          moreover note \<open>cball z e2 \<subseteq> s\<close> and path_img
          ultimately show ?thesis by auto
        qed
      show "winding_number g w = 0" when"w \<notin> s - {z}" for w
        proof -
          have "winding_number g w = 0" when "w\<notin>s" using that e2_cball
            apply (intro winding_number_zero_outside[OF _ _ _ _ path_img])
            by (auto simp add:g_def l_def)
          moreover have "winding_number g z=0"
            proof -
              let ?Wz="\<lambda>g. winding_number g z"
              have "?Wz g = ?Wz (circlepath z e2) + ?Wz l + ?Wz (reversepath (circlepath z e1))
                  + ?Wz (reversepath l)"
                using \<open>e2>0\<close> \<open>e1>0\<close> zl_img unfolding g_def l_def
                by (subst winding_number_join,auto simp add:path_image_join closed_segment_commute)+
              also have "... = ?Wz (circlepath z e2) + ?Wz (reversepath (circlepath z e1))"
                using zl_img
                apply (subst (2) winding_number_reversepath)
                by (auto simp add:l_def closed_segment_commute)
              also have "... = 0"
                proof -
                  have "?Wz (circlepath z e2) = 1" using \<open>e2>0\<close>
                    by (auto intro: winding_number_circlepath_centre)
                  moreover have "?Wz (reversepath (circlepath z e1)) = -1" using \<open>e1>0\<close>
                    apply (subst winding_number_reversepath)
                    by (auto intro: winding_number_circlepath_centre)
                  ultimately show ?thesis by auto
                qed
              finally show ?thesis .
            qed
          ultimately show ?thesis using that by auto
        qed
    qed
  then have "0 = ?ig g" using contour_integral_unique by simp
  also have "... = ?ig (circlepath z e2) + ?ig l + ?ig (reversepath (circlepath z e1))
      + ?ig (reversepath l)"
    unfolding g_def
    by (auto simp add:contour_integrable_reversepath_eq)
  also have "... = ?ig (circlepath z e2)  - ?ig (circlepath z e1)"
    by (auto simp add:contour_integral_reversepath)
  finally show "contour_integral (circlepath z e2) f = contour_integral (circlepath z e1) f"
    by simp
qed

lemma base_residue:
  assumes "open s" "z\<in>s" "r>0" and f_holo:"f holomorphic_on (s - {z})"
    and r_cball:"cball z r \<subseteq> s"
  shows "(f has_contour_integral 2 * pi * \<i> * (residue f z)) (circlepath z r)"
proof -
  obtain e where "e>0" and e_cball:"cball z e \<subseteq> s"
    using open_contains_cball[of s] \<open>open s\<close> \<open>z\<in>s\<close> by auto
  define c where "c \<equiv> 2 * pi * \<i>"
  define i where "i \<equiv> contour_integral (circlepath z e) f / c"
  have "(f has_contour_integral c*i) (circlepath z \<epsilon>)" when "\<epsilon>>0" "\<epsilon><e" for \<epsilon>
    proof -
      have "contour_integral (circlepath z e) f = contour_integral (circlepath z \<epsilon>) f"
          "f contour_integrable_on circlepath z \<epsilon>"
          "f contour_integrable_on circlepath z e"
        using \<open>\<epsilon><e\<close>
        by (intro contour_integral_circlepath_eq[OF \<open>open s\<close> f_holo \<open>\<epsilon>>0\<close> _ e_cball],auto)+
      then show ?thesis unfolding i_def c_def
        by (auto intro:has_contour_integral_integral)
    qed
  then have "\<exists>e>0. \<forall>\<epsilon>>0. \<epsilon><e \<longrightarrow> (f has_contour_integral c * (residue f z)) (circlepath z \<epsilon>)"
    unfolding residue_def c_def
    apply (rule_tac someI[of _ i],intro  exI[where x=e])
    by (auto simp add:\<open>e>0\<close> c_def)
  then obtain e' where "e'>0"
      and e'_def:"\<forall>\<epsilon>>0. \<epsilon><e' \<longrightarrow> (f has_contour_integral c * (residue f z)) (circlepath z \<epsilon>)"
    by auto
  let ?int="\<lambda>e. contour_integral (circlepath z e) f"
  define  \<epsilon> where "\<epsilon> \<equiv> Min {r,e'} / 2"
  have "\<epsilon>>0" "\<epsilon>\<le>r" "\<epsilon><e'" using \<open>r>0\<close> \<open>e'>0\<close> unfolding \<epsilon>_def by auto
  have "(f has_contour_integral c * (residue f z)) (circlepath z \<epsilon>)"
    using e'_def[rule_format,OF \<open>\<epsilon>>0\<close> \<open>\<epsilon><e'\<close>] .
  then show ?thesis unfolding c_def
    using contour_integral_circlepath_eq[OF \<open>open s\<close> f_holo \<open>\<epsilon>>0\<close> \<open>\<epsilon>\<le>r\<close> r_cball]
    by (auto elim: has_contour_integral_eqpath[of _ _ "circlepath z \<epsilon>" "circlepath z r"])
qed

lemma residue_holo:
  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s"
  shows "residue f z = 0"
proof -
  define c where "c \<equiv> 2 * pi * \<i>"
  obtain e where "e>0" and e_cball:"cball z e \<subseteq> s" using \<open>open s\<close> \<open>z\<in>s\<close>
    using open_contains_cball_eq by blast
  have "(f has_contour_integral c*residue f z) (circlepath z e)"
    using f_holo
    by (auto intro: base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c_def])
  moreover have "(f has_contour_integral 0) (circlepath z e)"
    using f_holo e_cball \<open>e>0\<close>
    by (auto intro: Cauchy_theorem_convex_simple[of _ "cball z e"])
  ultimately have "c*residue f z =0"
    using has_contour_integral_unique by blast
  thus ?thesis unfolding c_def  by auto
qed

lemma residue_const:"residue (\<lambda>_. c) z = 0"
  by (intro residue_holo[of "UNIV::complex set"],auto intro:holomorphic_intros)

lemma residue_add:
  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}"
      and g_holo:"g holomorphic_on s - {z}"
  shows "residue (\<lambda>z. f z + g z) z= residue f z + residue g z"
proof -
  define c where "c \<equiv> 2 * pi * \<i>"
  define fg where "fg \<equiv> (\<lambda>z. f z+g z)"
  obtain e where "e>0" and e_cball:"cball z e \<subseteq> s" using \<open>open s\<close> \<open>z\<in>s\<close>
    using open_contains_cball_eq by blast
  have "(fg has_contour_integral c * residue fg z) (circlepath z e)"
    unfolding fg_def using f_holo g_holo
    apply (intro base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c_def])
    by (auto intro:holomorphic_intros)
  moreover have "(fg has_contour_integral c*residue f z + c* residue g z) (circlepath z e)"
    unfolding fg_def using f_holo g_holo
    by (auto intro: has_contour_integral_add base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c_def])
  ultimately have "c*(residue f z + residue g z) = c * residue fg z"
    using has_contour_integral_unique by (auto simp add:distrib_left)
  thus ?thesis unfolding fg_def
    by (auto simp add:c_def)
qed

lemma residue_lmul:
  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}"
  shows "residue (\<lambda>z. c * (f z)) z= c * residue f z"
proof (cases "c=0")
  case True
  thus ?thesis using residue_const by auto
next
  case False
  define c' where "c' \<equiv> 2 * pi * \<i>"
  define f' where "f' \<equiv> (\<lambda>z. c * (f z))"
  obtain e where "e>0" and e_cball:"cball z e \<subseteq> s" using \<open>open s\<close> \<open>z\<in>s\<close>
    using open_contains_cball_eq by blast
  have "(f' has_contour_integral c' * residue f' z) (circlepath z e)"
    unfolding f'_def using f_holo
    apply (intro base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c'_def])
    by (auto intro:holomorphic_intros)
  moreover have "(f' has_contour_integral c * (c' * residue f z)) (circlepath z e)"
    unfolding f'_def using f_holo
    by (auto intro: has_contour_integral_lmul
      base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c'_def])
  ultimately have "c' * residue f' z  = c * (c' * residue f z)"
    using has_contour_integral_unique by auto
  thus ?thesis unfolding f'_def c'_def using False
    by (auto simp add:field_simps)
qed

lemma residue_rmul:
  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}"
  shows "residue (\<lambda>z. (f z) * c) z= residue f z * c"
using residue_lmul[OF assms,of c] by (auto simp add:algebra_simps)

lemma residue_div:
  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}"
  shows "residue (\<lambda>z. (f z) / c) z= residue f z / c "
using residue_lmul[OF assms,of "1/c"] by (auto simp add:algebra_simps)

lemma residue_neg:
  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}"
  shows "residue (\<lambda>z. - (f z)) z= - residue f z"
using residue_lmul[OF assms,of "-1"] by auto

lemma residue_diff:
  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}"
      and g_holo:"g holomorphic_on s - {z}"
  shows "residue (\<lambda>z. f z - g z) z= residue f z - residue g z"
using residue_add[OF assms(1,2,3),of "\<lambda>z. - g z"] residue_neg[OF assms(1,2,4)]
by (auto intro:holomorphic_intros g_holo)

lemma residue_simple:
  assumes "open s" "z\<in>s" and f_holo:"f holomorphic_on s"
  shows "residue (\<lambda>w. f w / (w - z)) z = f z"
proof -
  define c where "c \<equiv> 2 * pi * \<i>"
  define f' where "f' \<equiv> \<lambda>w. f w / (w - z)"
  obtain e where "e>0" and e_cball:"cball z e \<subseteq> s" using \<open>open s\<close> \<open>z\<in>s\<close>
    using open_contains_cball_eq by blast
  have "(f' has_contour_integral c * f z) (circlepath z e)"
    unfolding f'_def c_def using \<open>e>0\<close> f_holo e_cball
    by (auto intro!: Cauchy_integral_circlepath_simple holomorphic_intros)
  moreover have "(f' has_contour_integral c * residue f' z) (circlepath z e)"
    unfolding f'_def using f_holo
    apply (intro base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c_def])
    by (auto intro!:holomorphic_intros)
  ultimately have "c * f z = c * residue f' z"
    using has_contour_integral_unique by blast
  thus ?thesis unfolding c_def f'_def  by auto
qed

lemma residue_simple':
  assumes s: "open s" "z \<in> s" and holo: "f holomorphic_on (s - {z})"
      and lim: "((\<lambda>w. f w * (w - z)) \<longlongrightarrow> c) (at z)"
  shows   "residue f z = c"
proof -
  define g where "g = (\<lambda>w. if w = z then c else f w * (w - z))"
  from holo have "(\<lambda>w. f w * (w - z)) holomorphic_on (s - {z})" (is "?P")
    by (force intro: holomorphic_intros)
  also have "?P \<longleftrightarrow> g holomorphic_on (s - {z})"
    by (intro holomorphic_cong refl) (simp_all add: g_def)
  finally have *: "g holomorphic_on (s - {z})" .

  note lim
  also have "(\<lambda>w. f w * (w - z)) \<midarrow>z\<rightarrow> c \<longleftrightarrow> g \<midarrow>z\<rightarrow> g z"
    by (intro filterlim_cong refl) (simp_all add: g_def [abs_def] eventually_at_filter)
  finally have **: "g \<midarrow>z\<rightarrow> g z" .

  have g_holo: "g holomorphic_on s"
    by (rule no_isolated_singularity'[where K = "{z}"])
       (insert assms * **, simp_all add: at_within_open_NO_MATCH)
  from s and this have "residue (\<lambda>w. g w / (w - z)) z = g z"
    by (rule residue_simple)
  also have "\<forall>\<^sub>F za in at z. g za / (za - z) = f za"
    unfolding eventually_at by (auto intro!: exI[of _ 1] simp: field_simps g_def)
  hence "residue (\<lambda>w. g w / (w - z)) z = residue f z"
    by (intro residue_cong refl)
  finally show ?thesis
    by (simp add: g_def)
qed

lemma residue_holomorphic_over_power:
  assumes "open A" "z0 \<in> A" "f holomorphic_on A"
  shows   "residue (\<lambda>z. f z / (z - z0) ^ Suc n) z0 = (deriv ^^ n) f z0 / fact n"
proof -
  let ?f = "\<lambda>z. f z / (z - z0) ^ Suc n"
  from assms(1,2) obtain r where r: "r > 0" "cball z0 r \<subseteq> A"
    by (auto simp: open_contains_cball)
  have "(?f has_contour_integral 2 * pi * \<i> * residue ?f z0) (circlepath z0 r)"
    using r assms by (intro base_residue[of A]) (auto intro!: holomorphic_intros)
  moreover have "(?f has_contour_integral 2 * pi * \<i> / fact n * (deriv ^^ n) f z0) (circlepath z0 r)"
    using assms r
    by (intro Cauchy_has_contour_integral_higher_derivative_circlepath)
       (auto intro!: holomorphic_on_subset[OF assms(3)] holomorphic_on_imp_continuous_on)
  ultimately have "2 * pi * \<i> * residue ?f z0 = 2 * pi * \<i> / fact n * (deriv ^^ n) f z0"
    by (rule has_contour_integral_unique)
  thus ?thesis by (simp add: field_simps)
qed

lemma residue_holomorphic_over_power':
  assumes "open A" "0 \<in> A" "f holomorphic_on A"
  shows   "residue (\<lambda>z. f z / z ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n"
  using residue_holomorphic_over_power[OF assms] by simp

theorem residue_fps_expansion_over_power_at_0:
  assumes "f has_fps_expansion F"
  shows   "residue (\<lambda>z. f z / z ^ Suc n) 0 = fps_nth F n"
proof -
  from has_fps_expansion_imp_holomorphic[OF assms] obtain s
    where "open s" "0 \<in> s" "f holomorphic_on s" "\<And>z. z \<in> s \<Longrightarrow> f z = eval_fps F z"
    by auto
  with assms have "residue (\<lambda>z. f z / (z - 0) ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n"
    unfolding has_fps_expansion_def
    by (intro residue_holomorphic_over_power[of s]) (auto simp: zero_ereal_def)
  also from assms have "\<dots> = fps_nth F n"
    by (subst fps_nth_fps_expansion) auto
  finally show ?thesis by simp
qed

lemma residue_pole_order:
  fixes f::"complex \<Rightarrow> complex" and z::complex
  defines "n \<equiv> nat (- zorder f z)" and "h \<equiv> zor_poly f z"
  assumes f_iso:"isolated_singularity_at f z"
    and pole:"is_pole f z"
  shows "residue f z = ((deriv ^^ (n - 1)) h z / fact (n-1))"
proof -
  define g where "g \<equiv> \<lambda>x. if x=z then 0 else inverse (f x)"
  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
  obtain r where "0 < n" "0 < r" and r_cball:"cball z r \<subseteq> ball z e" and h_holo: "h holomorphic_on cball z r"
      and h_divide:"(\<forall>w\<in>cball z r. (w\<noteq>z \<longrightarrow> f w = h w / (w - z) ^ n) \<and> h w \<noteq> 0)"
  proof -
    obtain r where r:"zorder f z < 0" "h z \<noteq> 0" "r>0" "cball z r \<subseteq> ball z e" "h holomorphic_on cball z r"
        "(\<forall>w\<in>cball z r - {z}. f w = h w / (w - z) ^ n \<and> h w \<noteq> 0)"
      using zorder_exist_pole[OF f_holo,simplified,OF \<open>is_pole f z\<close>,folded n_def h_def] by auto
    have "n>0" using \<open>zorder f z < 0\<close> unfolding n_def by simp
    moreover have "(\<forall>w\<in>cball z r. (w\<noteq>z \<longrightarrow> f w = h w / (w - z) ^ n) \<and> h w \<noteq> 0)"
      using \<open>h z\<noteq>0\<close> r(6) by blast
    ultimately show ?thesis using r(3,4,5) that by blast
  qed
  have r_nonzero:"\<And>w. w \<in> ball z r - {z} \<Longrightarrow> f w \<noteq> 0"
    using h_divide by simp
  define c where "c \<equiv> 2 * pi * \<i>"
  define der_f where "der_f \<equiv> ((deriv ^^ (n - 1)) h z / fact (n-1))"
  define h' where "h' \<equiv> \<lambda>u. h u / (u - z) ^ n"
  have "(h' has_contour_integral c / fact (n - 1) * (deriv ^^ (n - 1)) h z) (circlepath z r)"
    unfolding h'_def
    proof (rule Cauchy_has_contour_integral_higher_derivative_circlepath[of z r h z "n-1",
        folded c_def Suc_pred'[OF \<open>n>0\<close>]])
      show "continuous_on (cball z r) h" using holomorphic_on_imp_continuous_on h_holo by simp
      show "h holomorphic_on ball z r" using h_holo by auto
      show " z \<in> ball z r" using \<open>r>0\<close> by auto
    qed
  then have "(h' has_contour_integral c * der_f) (circlepath z r)" unfolding der_f_def by auto
  then have "(f has_contour_integral c * der_f) (circlepath z r)"
    proof (elim has_contour_integral_eq)
      fix x assume "x \<in> path_image (circlepath z r)"
      hence "x\<in>cball z r - {z}" using \<open>r>0\<close> by auto
      then show "h' x = f x" using h_divide unfolding h'_def by auto
    qed
  moreover have "(f has_contour_integral c * residue f z) (circlepath z r)"
    using base_residue[of \<open>ball z e\<close> z,simplified,OF \<open>r>0\<close> f_holo r_cball,folded c_def]
    unfolding c_def by simp
  ultimately have "c * der_f =  c * residue f z" using has_contour_integral_unique by blast
  hence "der_f = residue f z" unfolding c_def by auto
  thus ?thesis unfolding der_f_def by auto
qed

lemma residue_simple_pole:
  assumes "isolated_singularity_at f z0"
  assumes "is_pole f z0" "zorder f z0 = - 1"
  shows   "residue f z0 = zor_poly f z0 z0"
  using assms by (subst residue_pole_order) simp_all

lemma residue_simple_pole_limit:
  assumes "isolated_singularity_at f z0"
  assumes "is_pole f z0" "zorder f z0 = - 1"
  assumes "((\<lambda>x. f (g x) * (g x - z0)) \<longlongrightarrow> c) F"
  assumes "filterlim g (at z0) F" "F \<noteq> bot"
  shows   "residue f z0 = c"
proof -
  have "residue f z0 = zor_poly f z0 z0"
    by (rule residue_simple_pole assms)+
  also have "\<dots> = c"
    apply (rule zor_poly_pole_eqI)
    using assms by auto
  finally show ?thesis .
qed

lemma
  assumes f_holo:"f holomorphic_on s" and g_holo:"g holomorphic_on s"
          and "open s" "connected s" "z \<in> s"
  assumes g_deriv:"(g has_field_derivative g') (at z)"
  assumes "f z \<noteq> 0" "g z = 0" "g' \<noteq> 0"
  shows   porder_simple_pole_deriv: "zorder (\<lambda>w. f w / g w) z = - 1"
    and   residue_simple_pole_deriv: "residue (\<lambda>w. f w / g w) z = f z / g'"
proof -
  have [simp]:"isolated_singularity_at f z" "isolated_singularity_at g z"
    using isolated_singularity_at_holomorphic[OF _ \<open>open s\<close> \<open>z\<in>s\<close>] f_holo g_holo
    by (meson Diff_subset holomorphic_on_subset)+
  have [simp]:"not_essential f z" "not_essential g z"
    unfolding not_essential_def using f_holo g_holo assms(3,5)
    by (meson continuous_on_eq_continuous_at continuous_within holomorphic_on_imp_continuous_on)+
  have g_nconst:"\<exists>\<^sub>F w in at z. g w \<noteq>0 "
  proof (rule ccontr)
    assume "\<not> (\<exists>\<^sub>F w in at z. g w \<noteq> 0)"
    then have "\<forall>\<^sub>F w in nhds z. g w = 0"
      unfolding eventually_at eventually_nhds frequently_at using \<open>g z = 0\<close>
      by (metis open_ball UNIV_I centre_in_ball dist_commute mem_ball)
    then have "deriv g z = deriv (\<lambda>_. 0) z"
      by (intro deriv_cong_ev) auto
    then have "deriv g z = 0" by auto
    then have "g' = 0" using g_deriv DERIV_imp_deriv by blast
    then show False using \<open>g'\<noteq>0\<close> by auto
  qed

  have "zorder (\<lambda>w. f w / g w) z = zorder f z - zorder g z"
  proof -
    have "\<forall>\<^sub>F w in at z. f w \<noteq>0 \<and> w\<in>s"
      apply (rule non_zero_neighbour_alt)
      using assms by auto
    with g_nconst have "\<exists>\<^sub>F w in at z. f w * g w \<noteq> 0"
      by (elim frequently_rev_mp eventually_rev_mp,auto)
    then show ?thesis using zorder_divide[of f z g] by auto
  qed
  moreover have "zorder f z=0"
    apply (rule zorder_zero_eqI[OF f_holo \<open>open s\<close> \<open>z\<in>s\<close>])
    using \<open>f z\<noteq>0\<close> by auto
  moreover have "zorder g z=1"
    apply (rule zorder_zero_eqI[OF g_holo \<open>open s\<close> \<open>z\<in>s\<close>])
    subgoal using assms(8) by auto
    subgoal using DERIV_imp_deriv assms(9) g_deriv by auto
    subgoal by simp
    done
  ultimately show "zorder (\<lambda>w. f w / g w) z = - 1" by auto

  show "residue (\<lambda>w. f w / g w) z = f z / g'"
  proof (rule residue_simple_pole_limit[where g=id and F="at z",simplified])
    show "zorder (\<lambda>w. f w / g w) z = - 1" by fact
    show "isolated_singularity_at (\<lambda>w. f w / g w) z"
      by (auto intro: singularity_intros)
    show "is_pole (\<lambda>w. f w / g w) z"
    proof (rule is_pole_divide)
      have "\<forall>\<^sub>F x in at z. g x \<noteq> 0"
        apply (rule non_zero_neighbour)
        using g_nconst by auto
      moreover have "g \<midarrow>z\<rightarrow> 0"
        using DERIV_isCont assms(8) continuous_at g_deriv by force
      ultimately show "filterlim g (at 0) (at z)" unfolding filterlim_at by simp
      show "isCont f z"
        using assms(3,5) continuous_on_eq_continuous_at f_holo holomorphic_on_imp_continuous_on
        by auto
      show "f z \<noteq> 0" by fact
    qed
    show "filterlim id (at z) (at z)" by (simp add: filterlim_iff)
    have "((\<lambda>w. (f w * (w - z)) / g w) \<longlongrightarrow> f z / g') (at z)"
    proof (rule lhopital_complex_simple)
      show "((\<lambda>w. f w * (w - z)) has_field_derivative f z) (at z)"
        using assms by (auto intro!: derivative_eq_intros holomorphic_derivI[OF f_holo])
      show "(g has_field_derivative g') (at z)" by fact
    qed (insert assms, auto)
    then show "((\<lambda>w. (f w / g w) * (w - z)) \<longlongrightarrow> f z / g') (at z)"
      by (simp add: field_split_simps)
  qed
qed


subsection \<open>Poles and residues of some well-known functions\<close>

(* TODO: add more material here for other functions *)
lemma is_pole_Gamma: "is_pole Gamma (-of_nat n)"
  unfolding is_pole_def using Gamma_poles .

lemma Gamma_residue:
  "residue Gamma (-of_nat n) = (-1) ^ n / fact n"
proof (rule residue_simple')
  show "open (- (\<int>\<^sub>\<le>\<^sub>0 - {-of_nat n}) :: complex set)"
    by (intro open_Compl closed_subset_Ints) auto
  show "Gamma holomorphic_on (- (\<int>\<^sub>\<le>\<^sub>0 - {-of_nat n}) - {- of_nat n})"
    by (rule holomorphic_Gamma) auto
  show "(\<lambda>w. Gamma w * (w - (-of_nat n))) \<midarrow>(-of_nat n)\<rightarrow> (- 1) ^ n / fact n"
    using Gamma_residues[of n] by simp
qed auto

end