definition✐‹tag important› residue :: "(complex ⇒ complex) ⇒ complex ⇒ complex" where
"residue f z = (SOME int. ∃e>0. ∀ε>0. ε<e
⟶ (f has_contour_integral 2*pi* 𝗂 *int) (circlepath z ε))"

theorem Residue_theorem:
fixes s pts::"complex set" and f::"complex ⇒ complex"
and g::"real ⇒ complex"
assumes "open s" "connected s" "finite pts" and
holo:"f holomorphic_on s-pts" and
"valid_path g" and
loop:"pathfinish g = pathstart g" and
"path_image g ⊆ s-pts" and
homo:"∀z. (z ∉ s) ⟶ winding_number g z = 0"
shows "contour_integral g f = 2 * pi * 𝗂 *(∑p∈pts. winding_number g p * residue f p)"
proof -
define c where "c ≡ 2 * pi * 𝗂"
obtain h where avoid:"∀p∈s. h p>0 ∧ (∀w∈cball p (h p). w∈s ∧ (w≠p ⟶ w ∉ pts))"
using finite_cball_avoid[OF ‹open s› ‹finite pts›] by metis
have "contour_integral g f
= (∑p∈pts. winding_number g p * contour_integral (circlepath p (h p)) f)"
using Cauchy_theorem_singularities[OF assms avoid] .
also have "... = (∑p∈pts. c * winding_number g p * residue f p)"
proof (intro sum.cong)
show "pts = pts" by simp
next
fix x assume "x ∈ pts"
show "winding_number g x * contour_integral (circlepath x (h x)) f
= c * winding_number g x * residue f x"
proof (cases "x∈s")
case False
then have "winding_number g x=0" using homo by auto
thus ?thesis by auto
next
case True
have "contour_integral (circlepath x (h x)) f = c* residue f x"
using ‹x∈pts› ‹finite pts› avoid[rule_format,OF True]
apply (intro base_residue[of "s-(pts-{x})",THEN contour_integral_unique,folded c_def])
by (auto intro:holomorphic_on_subset[OF holo] open_Diff[OF ‹open s› finite_imp_closed])
then show ?thesis by auto
qed
qed
also have "... = c * (∑p∈pts. winding_number g p * residue f p)"
by (simp add: sum_distrib_left algebra_simps)
finally show ?thesis unfolding c_def .
qed

lemma set_integral_complex_of_real:
"LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
unfolding set_lebesgue_integral_def
by (subst integral_complex_of_real[symmetric])
(auto intro!: Bochner_Integration.integral_cong split: split_indicator)

theorem Gamma_integral_complex:
assumes z: "Re z > 0"
shows "((λt. of_real t powr (z - 1) / of_real (exp t)) has_integral Gamma z) {0..}"
proof -
have A: "((λt. (of_real t) powr (z - 1) * of_real ((1 - t) ^ n))
has_integral (fact n / pochhammer z (n+1))) {0..1}"
if "Re z > 0" for n z using that
proof (induction n arbitrary: z)
case 0
have "((λt. complex_of_real t powr (z - 1)) has_integral
(of_real 1 powr z / z - of_real 0 powr z / z)) {0..1}" using 0
by (intro fundamental_theorem_of_calculus_interior)
(auto intro!: continuous_intros derivative_eq_intros has_vector_derivative_real_field)
thus ?case by simp
next
case (Suc n)
let ?f = "λt. complex_of_real t powr z / z"
let ?f' = "λt. complex_of_real t powr (z - 1)"
let ?g = "λt. (1 - complex_of_real t) ^ Suc n"
let ?g' = "λt. - ((1 - complex_of_real t) ^ n) * of_nat (Suc n)"
have "((λt. ?f' t * ?g t) has_integral
(of_nat (Suc n)) * fact n / pochhammer z (n+2)) {0..1}"
(is "(_ has_integral ?I) _")
proof (rule integration_by_parts_interior[where f' = ?f' and g = ?g])
from Suc.prems show "continuous_on {0..1} ?f" "continuous_on {0..1} ?g"
by (auto intro!: continuous_intros)
next
fix t :: real assume t: "t ∈ {0<..<1}"
show "(?f has_vector_derivative ?f' t) (at t)" using t Suc.prems
by (auto intro!: derivative_eq_intros has_vector_derivative_real_field)
show "(?g has_vector_derivative ?g' t) (at t)"
by (rule has_vector_derivative_real_field derivative_eq_intros refl)+ simp_all
next
from Suc.prems have [simp]: "z ≠ 0" by auto
from Suc.prems have A: "Re (z + of_nat n) > 0" for n by simp
have [simp]: "z + of_nat n ≠ 0" "z + 1 + of_nat n ≠ 0" for n
using A[of n] A[of "Suc n"] by (auto simp add: add.assoc simp del: plus_complex.sel)
have "((λx. of_real x powr z * of_real ((1 - x) ^ n) * (- of_nat (Suc n) / z)) has_integral
fact n / pochhammer (z+1) (n+1) * (- of_nat (Suc n) / z)) {0..1}"
(is "(?A has_integral ?B) _")
using Suc.IH[of "z+1"] Suc.prems by (intro has_integral_mult_left) (simp_all add: add_ac pochhammer_rec)
also have "?A = (λt. ?f t * ?g' t)" by (intro ext) (simp_all add: field_simps)
also have "?B = - (of_nat (Suc n) * fact n / pochhammer z (n+2))"
by (simp add: field_split_simps pochhammer_rec
prod.shift_bounds_cl_Suc_ivl del: of_nat_Suc)
finally show "((λt. ?f t * ?g' t) has_integral (?f 1 * ?g 1 - ?f 0 * ?g 0 - ?I)) {0..1}"
by simp
qed (simp_all add: bounded_bilinear_mult)
thus ?case by simp
qed

have B: "((λt. if t ∈ {0..of_nat n} then
of_real t powr (z - 1) * (1 - of_real t / of_nat n) ^ n else 0)
has_integral (of_nat n powr z * fact n / pochhammer z (n+1))) {0..}" for n
proof (cases "n > 0")
case [simp]: True
hence [simp]: "n ≠ 0" by auto
with has_integral_affinity01[OF A[OF z, of n], of "inverse (of_nat n)" 0]
have "((λx. (of_nat n - of_real x) ^ n * (of_real x / of_nat n) powr (z - 1) / of_nat n ^ n)
has_integral fact n * of_nat n / pochhammer z (n+1)) ((λx. real n * x)`{0..1})"
(is "(?f has_integral ?I) ?ivl") by (simp add: field_simps scaleR_conv_of_real)
also from True have "((λx. real n*x)`{0..1}) = {0..real n}"
by (subst image_mult_atLeastAtMost) simp_all
also have "?f = (λx. (of_real x / of_nat n) powr (z - 1) * (1 - of_real x / of_nat n) ^ n)"
using True by (intro ext) (simp add: field_simps)
finally have "((λx. (of_real x / of_nat n) powr (z - 1) * (1 - of_real x / of_nat n) ^ n)
has_integral ?I) {0..real n}" (is ?P) .
also have "?P ⟷ ((λx. exp ((z - 1) * of_real (ln (x / of_nat n))) * (1 - of_real x / of_nat n) ^ n)
has_integral ?I) {0..real n}"
by (intro has_integral_spike_finite_eq[of "{0}"]) (auto simp: powr_def Ln_of_real [symmetric])
also have "… ⟷ ((λx. exp ((z - 1) * of_real (ln x - ln (of_nat n))) * (1 - of_real x / of_nat n) ^ n)
has_integral ?I) {0..real n}"
by (intro has_integral_spike_finite_eq[of "{0}"]) (simp_all add: ln_div)
finally have … .
note B = has_integral_mult_right[OF this, of "exp ((z - 1) * ln (of_nat n))"]
have "((λx. exp ((z - 1) * of_real (ln x)) * (1 - of_real x / of_nat n) ^ n)
has_integral (?I * exp ((z - 1) * ln (of_nat n)))) {0..real n}" (is ?P)
by (insert B, subst (asm) mult.assoc [symmetric], subst (asm) exp_add [symmetric])
(simp add: algebra_simps)
also have "?P ⟷ ((λx. of_real x powr (z - 1) * (1 - of_real x / of_nat n) ^ n)
has_integral (?I * exp ((z - 1) * ln (of_nat n)))) {0..real n}"
by (intro has_integral_spike_finite_eq[of "{0}"]) (simp_all add: powr_def Ln_of_real)
also have "fact n * of_nat n / pochhammer z (n+1) * exp ((z - 1) * Ln (of_nat n)) =
(of_nat n powr z * fact n / pochhammer z (n+1))"
by (auto simp add: powr_def algebra_simps exp_diff exp_of_real)
finally show ?thesis by (subst has_integral_restrict) simp_all
next
case False
thus ?thesis by (subst has_integral_restrict) (simp_all add: has_integral_refl)
qed

have "eventually (λn. Gamma_series z n =
of_nat n powr z * fact n / pochhammer z (n+1)) sequentially"
using eventually_gt_at_top[of "0::nat"]
by eventually_elim (simp add: powr_def algebra_simps Gamma_series_def)
from this and Gamma_series_LIMSEQ[of z]
have C: "(λk. of_nat k powr z * fact k / pochhammer z (k+1)) ⇢ Gamma z"
by (blast intro: Lim_transform_eventually)
{
fix x :: real assume x: "x ≥ 0"
have lim_exp: "(λk. (1 - x / real k) ^ k) ⇢ exp (-x)"
using tendsto_exp_limit_sequentially[of "-x"] by simp
have "(λk. of_real x powr (z - 1) * of_real ((1 - x / of_nat k) ^ k))
⇢ of_real x powr (z - 1) * of_real (exp (-x))" (is ?P)
by (intro tendsto_intros lim_exp)
also from eventually_gt_at_top[of "nat ⌈x⌉"]
have "eventually (λk. of_nat k > x) sequentially" by eventually_elim linarith
hence "?P ⟷ (λk. if x ≤ of_nat k then
of_real x powr (z - 1) * of_real ((1 - x / of_nat k) ^ k) else 0)
⇢ of_real x powr (z - 1) * of_real (exp (-x))"
by (intro tendsto_cong) (auto elim!: eventually_mono)
finally have … .
}
hence D: "∀x∈{0..}. (λk. if x ∈ {0..real k} then
of_real x powr (z - 1) * (1 - of_real x / of_nat k) ^ k else 0)
⇢ of_real x powr (z - 1) / of_real (exp x)"
by (simp add: exp_minus field_simps cong: if_cong)

have "((λx. (Re z - 1) * (ln x / x)) ⤏ (Re z - 1) * 0) at_top"
by (intro tendsto_intros ln_x_over_x_tendsto_0)
hence "((λx. ((Re z - 1) * ln x) / x) ⤏ 0) at_top" by simp
from order_tendstoD(2)[OF this, of "1/2"]
have "eventually (λx. (Re z - 1) * ln x / x < 1/2) at_top" by simp
from eventually_conj[OF this eventually_gt_at_top[of 0]]
obtain x0 where "∀x≥x0. (Re z - 1) * ln x / x < 1/2 ∧ x > 0"
by (auto simp: eventually_at_top_linorder)
hence x0: "x0 > 0" "⋀x. x ≥ x0 ⟹ (Re z - 1) * ln x < x / 2" by auto

define h where "h = (λx. if x ∈ {0..x0} then x powr (Re z - 1) else exp (-x/2))"
have le_h: "x powr (Re z - 1) * exp (-x) ≤ h x" if x: "x ≥ 0" for x
proof (cases "x > x0")
case True
from True x0(1) have "x powr (Re z - 1) * exp (-x) = exp ((Re z - 1) * ln x - x)"
by (simp add: powr_def exp_diff exp_minus field_simps exp_add)
also from x0(2)[of x] True have "… < exp (-x/2)"
by (simp add: field_simps)
finally show ?thesis using True by (auto simp add: h_def)
next
case False
from x have "x powr (Re z - 1) * exp (- x) ≤ x powr (Re z - 1) * 1"
by (intro mult_left_mono) simp_all
with False show ?thesis by (auto simp add: h_def)
qed

have E: "∀x∈{0..}. cmod (if x ∈ {0..real k} then of_real x powr (z - 1) *
(1 - complex_of_real x / of_nat k) ^ k else 0) ≤ h x"
(is "∀x∈_. ?f x ≤ _") for k
proof safe
fix x :: real assume x: "x ≥ 0"
{
fix x :: real and n :: nat assume x: "x ≤ of_nat n"
have "(1 - complex_of_real x / of_nat n) = complex_of_real ((1 - x / of_nat n))" by simp
also have "norm … = ¦(1 - x / real n)¦" by (subst norm_of_real) (rule refl)
also from x have "… = (1 - x / real n)" by (intro abs_of_nonneg) (simp_all add: field_split_simps)
finally have "cmod (1 - complex_of_real x / of_nat n) = 1 - x / real n" .
} note D = this
from D[of x k] x
have "?f x ≤ (if of_nat k ≥ x ∧ k > 0 then x powr (Re z - 1) * (1 - x / real k) ^ k else 0)"
by (auto simp: norm_mult norm_powr_real_powr norm_power intro!: mult_nonneg_nonneg)
also have "… ≤ x powr (Re z - 1) * exp (-x)"
by (auto intro!: mult_left_mono exp_ge_one_minus_x_over_n_power_n)
also from x have "… ≤ h x" by (rule le_h)
finally show "?f x ≤ h x" .
qed

have F: "h integrable_on {0..}" unfolding h_def
by (rule integrable_Gamma_integral_bound) (insert assms x0(1), simp_all)
show ?thesis
by (rule has_integral_dominated_convergence[OF B F E D C])
qed

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 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_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_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_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_const:"residue (λ_. c) z = 0"
by (intro residue_holo[of "UNIV::complex set"],auto intro:holomorphic_intros)

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 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_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_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 integral_complex_of_real[simp]: "integral⇧^L M (λx. complex_of_real (f x)) = of_real (integral⇧^L M f)"
by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_Re]) simp

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_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 stirling_integral_continuous_on_complex [continuous_intros]:
assumes m: "m > 0" and "A ∩ ℝ⇩_≤⇩₀ = {}"
shows "continuous_on A (stirling_integral m :: _ ⇒ complex)"
by (intro holomorphic_on_imp_continuous_on stirling_integral_holomorphic assms)

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 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