12.7. MeromorphicTrace.TraceResidue🔗

Jacobians.MeromorphicTrace.TraceResidue — source

circleIntegral_laurentMonomial

The circle integral of a single Laurent monomial c·(z − a)^n over C(c₀, ρ) with the centre a inside the contour: 0 unless n = −1, where it is c · 2πi.

theorem circleIntegral_laurentMonomial {c a c₀ : ℂ} {ρ : ℝ} {n : ℤ} (ha : a ∈ ball c₀ ρ) :
    (∮ z in C(c₀, ρ), c * (z - a) ^ n) = if n = -1 then c * (2 * π * I) else 0

resAt_laurentMonomial

The resAt residue of a single Laurent monomial c·(z − a)^n at its own centre a: c if n = −1, and 0 otherwise (a holomorphic / primitive-having power has no residue).

theorem resAt_laurentMonomial (c a : ℂ) (n : ℤ) :
    resAt (fun z => c * (z - a) ^ n) a = if n = -1 then c else 0

resAt_eq_zero_of_analyticAt

Res = 0 for an analytic integrand. If f : ℂ → ℂ is AnalyticAt c, its residue there is 0 (it is differentiable on a small ball, so every small circle integral vanishes).

theorem resAt_eq_zero_of_analyticAt {f : ℂ → ℂ} {c : ℂ} (hf : AnalyticAt ℂ f c) :
    resAt f c = 0

resAt_zero

resAt 0 c = 0 (the zero function is analytic everywhere).

theorem resAt_zero (c : ℂ) : resAt (fun _ => (0 : ℂ)) c = 0

resAtInfty

The residue at infinity of the dz-coefficient R, computed on the contour C(0, ρ): Res_∞ R = −(2πi)⁻¹ ∮_{|z|=ρ} R.

noncomputable def resAtInfty (R : ℂ → ℂ) (ρ : ℝ) : ℂ

LaurentForm

A rational 1-form on ℂℙ¹ in partial-fraction (Laurent) form: a finite family of monomials c i·(z − a i) ^ (n i) with all centres inside ball 0 ρ. R is the pointwise coefficient sum.

structure LaurentForm where

R

The dz-coefficient of the form: the pointwise sum of the Laurent monomials.

noncomputable def R : ℂ → ℂ

circleIntegrable_monomial

Each monomial z ↦ c i·(z − a i) ^ (n i) is circle-integrable on C(0, ρ): its only singularity a i lies strictly inside the contour, off the sphere.

theorem circleIntegrable_monomial (i : L.ι) :
    CircleIntegrable (fun z => L.c i * (z - L.a i) ^ L.n i) 0 L.ρ

largeCircleIntegral_eq

Multi-pole Cauchy residue theorem (partial-fraction form). The large-contour integral of the rational coefficient R equals 2πi times the sum of the simple-pole coefficients (the c i with n i = −1), all centres lying inside C(0, ρ):

∮_{|z|=ρ} R = 2πi · ∑_{i : n i = −1} c i.

Termwise: each n i ≠ −1 monomial integrates to 0, each n i = −1 to c i · 2πi.

theorem largeCircleIntegral_eq :
    (∮ z in C((0 : ℂ), L.ρ), L.R z)
      = (2 * π * I) * ∑ i ∈ Finset.univ.filter (fun i => L.n i = -1), L.c i

finiteResidueSum

The finite residue sum: the sum, over the distinct centres, of the local residues of R. Indexed over the centre images via the index set (each centre counted once through Finset.image L.a).

noncomputable def finiteResidueSum : ℂ

meromorphicAt_monomial

A Laurent monomial c·(z − b)^m is MeromorphicAt at any point p (so in particular has an isolated singularity — HoloPunctured — there): integer powers of the meromorphic z ↦ z − b are meromorphic, scaled by a constant.

theorem meromorphicAt_monomial (c b : ℂ) (m : ℤ) (p : ℂ) :
    MeromorphicAt (fun z => c * (z - b) ^ m) p

analyticAt_monomial_of_ne

A Laurent monomial centred at b ≠ p is analytic at p (its only singularity is at b): the m-th integer power of z − b is analytic where z − b ≠ 0.

theorem analyticAt_monomial_of_ne (c : ℂ) {b : ℂ} (m : ℤ) {p : ℂ} (hbp : b ≠ p) :
    AnalyticAt ℂ (fun z => c * (z - b) ^ m) p

resAt_finsum

resAt of a finite sum of functions, each with an isolated singularity at p, is the sum of the residues — finite additivity, by induction from the binary resAt_add (with HoloPunctured.add supplied through MeromorphicAt.holoPunctured).

theorem resAt_finsum {ι : Type*} (s : Finset ι) (f : ι → ℂ → ℂ) {p : ℂ}
    (hf : ∀ i ∈ s, MeromorphicAt (f i) p) :
    resAt (fun z => ∑ i ∈ s, f i z) p = ∑ i ∈ s, resAt (f i) p

resAt_center_eq

The local residue of R at a centre p. It equals the sum of the simple-pole coefficients sitting exactly at p: resAt R p = ∑_{i : a i = p, n i = −1} c i. (Monomials centred elsewhere are holomorphic at p and contribute no residue; monomials centred at p contribute by resAt_laurentMonomial.)

theorem resAt_center_eq (p : ℂ) :
    resAt L.R p
      = ∑ i ∈ Finset.univ.filter (fun i => L.a i = p ∧ L.n i = -1), L.c i

resAtInfty_eq

resAtInfty L.R L.ρ = −∑_{i : n i = −1} c i: the residue at infinity is the negative of the total simple-pole mass, by the multi-pole Cauchy formula largeCircleIntegral_eq.

theorem resAtInfty_eq :
    resAtInfty L.R L.ρ = -∑ i ∈ Finset.univ.filter (fun i => L.n i = -1), L.c i

finiteResidueSum_add_resAtInfty_eq_zero

The ℂℙ¹ residue theorem (Miranda §VIII.3, pillar 2). For a rational 1-form R dz on ℂℙ¹ in partial-fraction form, the sum of all residues — finite plus the residue at infinity — vanishes:

(∑_{centres} Res_p R) + Res_∞ R = 0.

The only Laurent terms contributing are the simple poles (n i = −1); each contributes its coefficient c i to the finite sum (resAt_center_eq) and −c i to the residue at infinity (resAtInfty_eq), so the total cancels.

theorem finiteResidueSum_add_resAtInfty_eq_zero :
    L.finiteResidueSum + resAtInfty L.R L.ρ = 0