The circle-integral bridge (residue-calculus) #
The one honest integration atom this unit budgets for: ∮_{C(z₀,R)} f = 2πi · resAt f z₀, for
f meromorphic at z₀ and differentiable on the punctured closed disk. A small-radius
(∀ᶠ in the radius) convenience form is also provided for consumers who only know meromorphy.
Main exports: RS.circleIntegral_eq_two_pi_I_mul_resAt,
RS.MeromorphicAt.eventually_circleIntegral_eq_two_pi_I_mul_resAt.
theorem
RS.circleIntegral_eq_two_pi_I_mul_resAt
{f : ℂ → ℂ}
{z₀ : ℂ}
{R : ℝ}
(hR : 0 < R)
(hf : MeromorphicAt f z₀)
(hd : ∀ z ∈ Metric.closedBall z₀ R \ {z₀}, DifferentiableAt ℂ f z)
:
Fixed-radius residue formula: if f is meromorphic at z₀ and differentiable on the
punctured closed disk, the circle integral computes the residue.
theorem
RS.MeromorphicAt.eventually_circleIntegral_eq_two_pi_I_mul_resAt
{f : ℂ → ℂ}
{z₀ : ℂ}
(hf : MeromorphicAt f z₀)
:
Small-radius form for consumers that only know meromorphy (they pick their own ρ).