Theory Complex_Residues
theory Complex_Residues
imports Complex_Singularities
begin
subsection ‹Definition of residues›
text‹Wenda Li and LC Paulson (2016). A Formal Proof of Cauchy's Residue Theorem.
Interactive Theorem Proving›
definition residue :: "(complex ⇒ complex) ⇒ complex ⇒ complex" where
"residue f z = (SOME int. ∃e>0. ∀ε>0. ε<e
⟶ (f has_contour_integral 2*pi* 𝗂 *int) (circlepath z ε))"
lemma residue_cong:
assumes eq: "eventually (λz. f z = g z) (at z)" and "z = z'"
shows "residue f z = residue g z'"
proof -
from assms have eq': "eventually (λz. g z = f z) (at z)"
by (simp add: eq_commute)
let ?P = "λf c e. (∀ε>0. ε < e ⟶
(f has_contour_integral of_real (2 * pi) * 𝗂 * c) (circlepath z ε))"
have "residue f z = residue g z" unfolding residue_def
proof (rule Eps_cong)
fix c :: complex
have "∃e>0. ?P g c e"
if "∃e>0. ?P f c e" and "eventually (λ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" "⋀z'. z' ≠ z ⟹ dist z' z < e' ⟹ 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 ε)
hence "(f has_contour_integral of_real (2 * pi) * 𝗂 * c) (circlepath z ε)"
using e(2) by auto
thus ?case
proof (rule has_contour_integral_eq)
fix z' assume "z' ∈ path_image (circlepath z ε)"
hence "dist z' z < e'" and "z' ≠ 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 "(∃e>0. ?P f c e) ⟷ (∃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≤e2"
and e2_cball:"cball z e2 ⊆ 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 ≡ 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 ‹e1>0› ‹e1≤e2› by auto
have zl_img:"z∉path_image l"
proof
assume "z ∈ path_image l"
then have "e2 ≤ cmod (e2 - e1)"
using segment_furthest_le[of z "z+e2" "z+e1" "z+e2",simplified] ‹e1>0› ‹e2>0› unfolding l_def
by (auto simp add:closed_segment_commute)
thus False using ‹e2>0› ‹e1>0› ‹e1≤e2›
apply (subst (asm) norm_of_real)
by auto
qed
define g where "g ≡ 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 ‹e2>0› 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 ‹e1>0› ‹e1≤e2› e2_cball by auto
qed
have [simp]:"f contour_integrable_on l"
proof -
have "closed_segment (z + e2) (z + e1) ⊆ cball z e2" using ‹e2>0› ‹e1>0› ‹e1≤e2›
by (intro closed_segment_subset,auto simp add:dist_norm)
hence "closed_segment (z + e2) (z + e1) ⊆ 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="λ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 s› 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 ⊆ cball z e2"
proof -
have "closed_segment (z + e2) (z + e1) ⊆ cball z e2" using ‹e2>0› ‹e1>0› ‹e1≤e2›
by (intro closed_segment_subset,auto simp add:dist_norm)
moreover have "sphere z ¦e1¦ ⊆ cball z e2" using ‹e2>0› ‹e1≤e2› ‹e1>0› by auto
ultimately show ?thesis unfolding g_def l_def using ‹e2>0›
by (simp add: path_image_join closed_segment_commute)
qed
show "path_image g ⊆ s - {z}"
proof -
have "z∉path_image g" using zl_img
unfolding g_def l_def by (auto simp add: path_image_join closed_segment_commute)
moreover note ‹cball z e2 ⊆ s› and path_img
ultimately show ?thesis by auto
qed
show "winding_number g w = 0" when"w ∉ s - {z}" for w
proof -
have "winding_number g w = 0" when "w∉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="λg. winding_number g z"
have "?Wz g = ?Wz (circlepath z e2) + ?Wz l + ?Wz (reversepath (circlepath z e1))
+ ?Wz (reversepath l)"
using ‹e2>0› ‹e1>0› 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 ‹e2>0›
by (auto intro: winding_number_circlepath_centre)
moreover have "?Wz (reversepath (circlepath z e1)) = -1" using ‹e1>0›
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∈s" "r>0" and f_holo:"f holomorphic_on (s - {z})"
and r_cball:"cball z r ⊆ s"
shows "(f has_contour_integral 2 * pi * 𝗂 * (residue f z)) (circlepath z r)"
proof -
obtain e where "e>0" and e_cball:"cball z e ⊆ s"
using open_contains_cball[of s] ‹open s› ‹z∈s› by auto
define c where "c ≡ 2 * pi * 𝗂"
define i where "i ≡ contour_integral (circlepath z e) f / c"
have "(f has_contour_integral c*i) (circlepath z ε)" when "ε>0" "ε<e" for ε
proof -
have "contour_integral (circlepath z e) f = contour_integral (circlepath z ε) f"
"f contour_integrable_on circlepath z ε"
"f contour_integrable_on circlepath z e"
using ‹ε<e›
by (intro contour_integral_circlepath_eq[OF ‹open s› f_holo ‹ε>0› _ e_cball],auto)+
then show ?thesis unfolding i_def c_def
by (auto intro:has_contour_integral_integral)
qed
then have "∃e>0. ∀ε>0. ε<e ⟶ (f has_contour_integral c * (residue f z)) (circlepath z ε)"
unfolding residue_def c_def
apply (rule_tac someI[of _ i],intro exI[where x=e])
by (auto simp add:‹e>0› c_def)
then obtain e' where "e'>0"
and e'_def:"∀ε>0. ε<e' ⟶ (f has_contour_integral c * (residue f z)) (circlepath z ε)"
by auto
let ?int="λe. contour_integral (circlepath z e) f"
define ε where "ε ≡ Min {r,e'} / 2"
have "ε>0" "ε≤r" "ε<e'" using ‹r>0› ‹e'>0› unfolding ε_def by auto
have "(f has_contour_integral c * (residue f z)) (circlepath z ε)"
using e'_def[rule_format,OF ‹ε>0› ‹ε<e'›] .
then show ?thesis unfolding c_def
using contour_integral_circlepath_eq[OF ‹open s› f_holo ‹ε>0› ‹ε≤r› r_cball]
by (auto elim: has_contour_integral_eqpath[of _ _ "circlepath z ε" "circlepath z r"])
qed
lemma residue_holo:
assumes "open s" "z ∈ s" and f_holo: "f holomorphic_on s"
shows "residue f z = 0"
proof -
define c where "c ≡ 2 * pi * 𝗂"
obtain e where "e>0" and e_cball:"cball z e ⊆ s" using ‹open s› ‹z∈s›
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 s› ‹z∈s› ‹e>0› _ e_cball,folded c_def])
moreover have "(f has_contour_integral 0) (circlepath z e)"
using f_holo e_cball ‹e>0›
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 (λ_. c) z = 0"
by (intro residue_holo[of "UNIV::complex set"],auto intro:holomorphic_intros)
lemma residue_add:
assumes "open s" "z ∈ s" and f_holo: "f holomorphic_on s - {z}"
and g_holo:"g holomorphic_on s - {z}"
shows "residue (λz. f z + g z) z= residue f z + residue g z"
proof -
define c where "c ≡ 2 * pi * 𝗂"
define fg where "fg ≡ (λz. f z+g z)"
obtain e where "e>0" and e_cball:"cball z e ⊆ s" using ‹open s› ‹z∈s›
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 s› ‹z∈s› ‹e>0› _ 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 s› ‹z∈s› ‹e>0› _ 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 ∈ s" and f_holo: "f holomorphic_on s - {z}"
shows "residue (λ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' ≡ 2 * pi * 𝗂"
define f' where "f' ≡ (λz. c * (f z))"
obtain e where "e>0" and e_cball:"cball z e ⊆ s" using ‹open s› ‹z∈s›
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 s› ‹z∈s› ‹e>0› _ 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 s› ‹z∈s› ‹e>0› _ 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 ∈ s" and f_holo: "f holomorphic_on s - {z}"
shows "residue (λ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 ∈ s" and f_holo: "f holomorphic_on s - {z}"
shows "residue (λ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 ∈ s" and f_holo: "f holomorphic_on s - {z}"
shows "residue (λz. - (f z)) z= - residue f z"
using residue_lmul[OF assms,of "-1"] by auto
lemma residue_diff:
assumes "open s" "z ∈ s" and f_holo: "f holomorphic_on s - {z}"
and g_holo:"g holomorphic_on s - {z}"
shows "residue (λz. f z - g z) z= residue f z - residue g z"
using residue_add[OF assms(1,2,3),of "λz. - g z"] residue_neg[OF assms(1,2,4)]
by (auto intro:holomorphic_intros g_holo)
lemma residue_simple:
assumes "open s" "z∈s" and f_holo:"f holomorphic_on s"
shows "residue (λw. f w / (w - z)) z = f z"
proof -
define c where "c ≡ 2 * pi * 𝗂"
define f' where "f' ≡ λw. f w / (w - z)"
obtain e where "e>0" and e_cball:"cball z e ⊆ s" using ‹open s› ‹z∈s›
using open_contains_cball_eq by blast
have "(f' has_contour_integral c * f z) (circlepath z e)"
unfolding f'_def c_def using ‹e>0› 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 s› ‹z∈s› ‹e>0› _ 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 ∈ s" and holo: "f holomorphic_on (s - {z})"
and lim: "((λw. f w * (w - z)) ⤏ c) (at z)"
shows "residue f z = c"
proof -
define g where "g = (λw. if w = z then c else f w * (w - z))"
from holo have "(λw. f w * (w - z)) holomorphic_on (s - {z})" (is "?P")
by (force intro: holomorphic_intros)
also have "?P ⟷ 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 "(λw. f w * (w - z)) ─z→ c ⟷ g ─z→ g z"
by (intro filterlim_cong refl) (simp_all add: g_def [abs_def] eventually_at_filter)
finally have **: "g ─z→ 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 (λw. g w / (w - z)) z = g z"
by (rule residue_simple)
also have "∀⇩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 (λ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 ∈ A" "f holomorphic_on A"
shows "residue (λz. f z / (z - z0) ^ Suc n) z0 = (deriv ^^ n) f z0 / fact n"
proof -
let ?f = "λz. f z / (z - z0) ^ Suc n"
from assms(1,2) obtain r where r: "r > 0" "cball z0 r ⊆ A"
by (auto simp: open_contains_cball)
have "(?f has_contour_integral 2 * pi * 𝗂 * 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 * 𝗂 / 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 * 𝗂 * residue ?f z0 = 2 * pi * 𝗂 / 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 ∈ A" "f holomorphic_on A"
shows "residue (λ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 (λ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 ∈ s" "f holomorphic_on s" "⋀z. z ∈ s ⟹ f z = eval_fps F z"
by auto
with assms have "residue (λ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 "… = fps_nth F n"
by (subst fps_nth_fps_expansion) auto
finally show ?thesis by simp
qed
lemma residue_pole_order:
fixes f::"complex ⇒ complex" and z::complex
defines "n ≡ nat (- zorder f z)" and "h ≡ 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 ≡ λ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 ⊆ ball z e" and h_holo: "h holomorphic_on cball z r"
and h_divide:"(∀w∈cball z r. (w≠z ⟶ f w = h w / (w - z) ^ n) ∧ h w ≠ 0)"
proof -
obtain r where r:"zorder f z < 0" "h z ≠ 0" "r>0" "cball z r ⊆ ball z e" "h holomorphic_on cball z r"
"(∀w∈cball z r - {z}. f w = h w / (w - z) ^ n ∧ h w ≠ 0)"
using zorder_exist_pole[OF f_holo,simplified,OF ‹is_pole f z›,folded n_def h_def] by auto
have "n>0" using ‹zorder f z < 0› unfolding n_def by simp
moreover have "(∀w∈cball z r. (w≠z ⟶ f w = h w / (w - z) ^ n) ∧ h w ≠ 0)"
using ‹h z≠0› r(6) by blast
ultimately show ?thesis using r(3,4,5) that by blast
qed
have r_nonzero:"⋀w. w ∈ ball z r - {z} ⟹ f w ≠ 0"
using h_divide by simp
define c where "c ≡ 2 * pi * 𝗂"
define der_f where "der_f ≡ ((deriv ^^ (n - 1)) h z / fact (n-1))"
define h' where "h' ≡ λ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 ‹n>0›]])
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 ∈ ball z r" using ‹r>0› 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 ∈ path_image (circlepath z r)"
hence "x∈cball z r - {z}" using ‹r>0› 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 ‹ball z e› z,simplified,OF ‹r>0› 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 "((λx. f (g x) * (g x - z0)) ⤏ c) F"
assumes "filterlim g (at z0) F" "F ≠ bot"
shows "residue f z0 = c"
proof -
have "residue f z0 = zor_poly f z0 z0"
by (rule residue_simple_pole assms)+
also have "… = 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 ∈ s"
assumes g_deriv:"(g has_field_derivative g') (at z)"
assumes "f z ≠ 0" "g z = 0" "g' ≠ 0"
shows porder_simple_pole_deriv: "zorder (λw. f w / g w) z = - 1"
and residue_simple_pole_deriv: "residue (λ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 s› ‹z∈s›] 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:"∃⇩F w in at z. g w ≠0 "
proof (rule ccontr)
assume "¬ (∃⇩F w in at z. g w ≠ 0)"
then have "∀⇩F w in nhds z. g w = 0"
unfolding eventually_at eventually_nhds frequently_at using ‹g z = 0›
by (metis open_ball UNIV_I centre_in_ball dist_commute mem_ball)
then have "deriv g z = deriv (λ_. 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 ‹g'≠0› by auto
qed
have "zorder (λw. f w / g w) z = zorder f z - zorder g z"
proof -
have "∀⇩F w in at z. f w ≠0 ∧ w∈s"
apply (rule non_zero_neighbour_alt)
using assms by auto
with g_nconst have "∃⇩F w in at z. f w * g w ≠ 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 s› ‹z∈s›])
using ‹f z≠0› by auto
moreover have "zorder g z=1"
apply (rule zorder_zero_eqI[OF g_holo ‹open s› ‹z∈s›])
subgoal using assms(8) by auto
subgoal using DERIV_imp_deriv assms(9) g_deriv by auto
subgoal by simp
done
ultimately show "zorder (λw. f w / g w) z = - 1" by auto
show "residue (λ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 (λw. f w / g w) z = - 1" by fact
show "isolated_singularity_at (λw. f w / g w) z"
by (auto intro: singularity_intros)
show "is_pole (λw. f w / g w) z"
proof (rule is_pole_divide)
have "∀⇩F x in at z. g x ≠ 0"
apply (rule non_zero_neighbour)
using g_nconst by auto
moreover have "g ─z→ 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 ≠ 0" by fact
qed
show "filterlim id (at z) (at z)" by (simp add: filterlim_iff)
have "((λw. (f w * (w - z)) / g w) ⤏ f z / g') (at z)"
proof (rule lhopital_complex_simple)
show "((λ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 "((λw. (f w / g w) * (w - z)) ⤏ f z / g') (at z)"
by (simp add: field_split_simps)
qed
qed
subsection ‹Poles and residues of some well-known 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 (- (ℤ⇩≤⇩0 - {-of_nat n}) :: complex set)"
by (intro open_Compl closed_subset_Ints) auto
show "Gamma holomorphic_on (- (ℤ⇩≤⇩0 - {-of_nat n}) - {- of_nat n})"
by (rule holomorphic_Gamma) auto
show "(λw. Gamma w * (w - (-of_nat n))) ─(-of_nat n)→ (- 1) ^ n / fact n"
using Gamma_residues[of n] by simp
qed auto
end