8.6. ResidueCalculus.Residue🔗

Jacobians.ResidueCalculus.Residue — source

resAt

The residue of f : ℂ → ℂ at c: (2πi)⁻¹ ∮_{|z-c|=r} f in the limit r → 0⁺. For f with an isolated singularity at c the contour integral is independent of small r (annulus Cauchy–Goursat), so this picks out that common value = the Laurent coefficient c₋₁.

noncomputable def resAt (f : ℂ → ℂ) (c : ℂ) : ℂ

resAt_eq_of_eventuallyEq_circleIntegral

Workhorse. If the contour integral ∮_{|z-c|=r} f is eventually constant = K as r → 0⁺, then resAt f c = (2πi)⁻¹ • K. Every residue computation below funnels through this.

theorem resAt_eq_of_eventuallyEq_circleIntegral {f : ℂ → ℂ} {c K : ℂ}
    (h : ∀ᶠ r in 𝓝[>] (0 : ℝ), (∮ z in C(c, r), f z) = K) :
    resAt f c = (2 * π * I : ℂ)⁻¹ • K

eventuallyEq_circleIntegral_of_forall

If the contour integral is constant = K on a punctured right-neighbourhood Ioo 0 ρ of 0, the eventual-constancy hypothesis of the workhorse holds.

theorem eventuallyEq_circleIntegral_of_forall {f : ℂ → ℂ} {c K : ℂ} {ρ : ℝ} (hρ : 0 < ρ)
    (h : ∀ r ∈ Set.Ioo (0 : ℝ) ρ, (∮ z in C(c, r), f z) = K) :
    ∀ᶠ r in 𝓝[>] (0 : ℝ), (∮ z in C(c, r), f z) = K

resAt_const_mul_sub_inv

Forster 17.6's witness, general coefficient. Res_c (a·(z-c)⁻¹) = a.

theorem resAt_const_mul_sub_inv (a c : ℂ) :
    resAt (fun z => a * (z - c)⁻¹) c = a

resAt_sub_inv

Res_c ((z-c)⁻¹) = 1.

theorem resAt_sub_inv (c : ℂ) : resAt (fun z => (z - c)⁻¹) c = 1

resAt_eq_zero_of_differentiableOn_ball

Holomorphic-difference property. If f is complex-differentiable on a ball ball c ρ (ρ > 0), its residue at c is 0. This is what makes Res well-defined on Mittag–Leffler cochains: the differences ωᵢ - ωⱼ are holomorphic, hence contribute no residue.

theorem resAt_eq_zero_of_differentiableOn_ball {f : ℂ → ℂ} {c : ℂ} {ρ : ℝ} (hρ : 0 < ρ)
    (hf : ∀ z ∈ ball c ρ, DifferentiableAt ℂ f z) :
    resAt f c = 0

HoloPunctured

f is holomorphic on a punctured ball ball c ρ \ {c}, i.e. has an isolated singularity (or none) at c. The setting in which resAt f c is contour-independent and ℂ-linear; every meromorphic-at-c function qualifies (MeromorphicAt.holoPunctured).

def HoloPunctured (f : ℂ → ℂ) (c : ℂ) : Prop

MeromorphicAt.holoPunctured

theorem MeromorphicAt.holoPunctured {f : ℂ → ℂ} {c : ℂ} (h : MeromorphicAt f c) :
    HoloPunctured f c

circleIntegral_annulus_eq

Annulus Cauchy–Goursat. For f holomorphic on ball c ρ \ {c}, the contour integral is independent of the radius: ∮_{|z-c|=R} f = ∮_{|z-c|=r} f for 0 < r ≤ R < ρ.

theorem circleIntegral_annulus_eq {f : ℂ → ℂ} {c : ℂ} {ρ : ℝ}
    (hf : ∀ z ∈ ball c ρ \ {c}, DifferentiableAt ℂ f z)
    {r R : ℝ} (hr : 0 < r) (hrR : r ≤ R) (hRρ : R < ρ) :
    (∮ z in C(c, R), f z) = ∮ z in C(c, r), f z

resAt_eq_smul_circleIntegral

Compute resAt by any small contour. For f holomorphic on ball c ρ \ {c} and 0 < r < ρ, resAt f c = (2πi)⁻¹ • ∮_{|z-c|=r} f.

theorem resAt_eq_smul_circleIntegral {f : ℂ → ℂ} {c : ℂ} {ρ : ℝ}
    (hf : ∀ z ∈ ball c ρ \ {c}, DifferentiableAt ℂ f z) {r : ℝ} (hr : 0 < r) (hrρ : r < ρ) :
    resAt f c = (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, r), f z

circleIntegrable_of_holo

CircleIntegrable f c r for f holomorphic on ball c ρ \ {c} and 0 < r < ρ (the circle of radius r avoids the singularity).

theorem circleIntegrable_of_holo {f : ℂ → ℂ} {c : ℂ} {ρ : ℝ}
    (hf : ∀ z ∈ ball c ρ \ {c}, DifferentiableAt ℂ f z) {r : ℝ} (hr : 0 < r) (hrρ : r < ρ) :
    CircleIntegrable f c r

resAt_add

resAt is additive on functions with isolated singularities at c.

theorem resAt_add {f g : ℂ → ℂ} {c : ℂ} (hf : HoloPunctured f c) (hg : HoloPunctured g c) :
    resAt (f + g) c = resAt f c + resAt g c

resAt_smul

resAt is ℂ-homogeneous on functions with an isolated singularity at c.

theorem resAt_smul {f : ℂ → ℂ} {c : ℂ} (a : ℂ) (hf : HoloPunctured f c) :
    resAt (a • f) c = a • resAt f c

resAt_congr

resAt depends only on the germ of f at c (a punctured-neighbourhood invariant). Two functions agreeing near c (off c) have the same residue — the small contour integrals coincide.

theorem resAt_congr {f g : ℂ → ℂ} {c : ℂ} (h : f =ᶠ[𝓝[≠] c] g) : resAt f c = resAt g c