The residue of a meromorphic function

For f : ℂ → ℂ and z₀ : ℂ, the residue TauCeti.Contour.residue f z₀ is the order-(−1) Laurent coefficient of f at z₀ — the quantity summed in Cauchy's residue theorem. It is built directly on Mathlib's meromorphicOrderAt / analytic-part API rather than a parallel order-of-vanishing notion: writing f z = (z − z₀) ^ n • g z near z₀ with g analytic and g z₀ ≠ 0 (where n = meromorphicOrderAt f z₀), the order-(−1) coefficient is the Taylor coefficient of g at index −1 − n, i.e. iteratedDeriv (−1 − n) g z₀ / (−1 − n)!. The residue is 0 at a point where f is analytic (n ≥ 0), and at a simple pole (n = −1) it is the leading Laurent coefficient meromorphicTrailingCoeffAt f z₀ = lim_{z→z₀} (z − z₀) · f z.

As an unconditional value it is junk (0) when f is not meromorphic at z₀.

Main definitions

• TauCeti.Contour.residue — the residue of f at z₀.

Main results

• TauCeti.Contour.residue_eq_of_order_lt_zero — the characteristic value: from a reduced local presentation f =ᶠ[𝓝[≠] z₀] (· − z₀) ^ n • g with g analytic, g z₀ ≠ 0, and n < 0, the residue is iteratedDeriv (−1 − n) g z₀ / (−1 − n)!, independently of the presentation.
• TauCeti.Contour.residue_eq_of_eventuallyEq_zpow_smul — the same value from any presentation f =ᶠ[𝓝[≠] z₀] (· − z₀) ^ n • g with g analytic and n ≤ −1, dropping g z₀ ≠ 0.
• TauCeti.Contour.residue_add, TauCeti.Contour.residue_sub, TauCeti.Contour.residue_sum — additivity of the residue, over functions meromorphic at z₀, including over finite sums. The hypotheses are essential: two functions that are not meromorphic can sum to one that is.
• TauCeti.Contour.residue_const_mul and TauCeti.Contour.residue_const_smul — homogeneity, in the applied and unapplied forms. These are unconditional, the junk value scaling correctly.
• TauCeti.Contour.residue_congr_nhdsNE — the residue depends only on the germ of f on a punctured neighborhood of z₀.
• TauCeti.Contour.residue_eq_zero_of_analyticAt — the residue vanishes where f is analytic.
• TauCeti.Contour.residue_eq_meromorphicTrailingCoeffAt_of_order_eq_neg_one — at a simple pole the residue is the leading Laurent (trailing) coefficient.
• TauCeti.Contour.residue_div_sub_pow_of_analyticAt — the Cauchy-kernel computation Res_{z₀} (g / (· − z₀) ^ (k + 1)) = g^{(k)}(z₀) / k ! for g analytic at z₀.

This is a Layer 0 object of the Hungerbühler–Wasem generalized residue theorem (HW Thm 3.3).

Provenance

Adapted from the AINTLIB LeanModularForms project (the residue material of ForMathlib/GeneralizedResidueTheory/Residue.lean and ForMathlib/GeneralizedResidueTheory/Residue/GeneralizedTheoremBase.lean), specialised to the raw-function design of the contour-integration roadmap and defined against Mathlib's meromorphicOrderAt / meromorphicTrailingCoeffAt API.

References

• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997.

noncomputable def TauCeti.Contour.residue (f : ℂ → ℂ) (z₀ : ℂ) : ℂ

The residue of f at z₀: the order-(−1) Laurent coefficient. When f is meromorphic at z₀ with a pole (meromorphicOrderAt f z₀ = n < 0), it is the Taylor coefficient at index −1 − n of the analytic part g (with f z = (z − z₀) ^ n • g z near z₀); it is 0 when f is analytic at z₀ (n ≥ 0) and junk (0) when f is not meromorphic at z₀. See residue_eq_of_order_lt_zero for the characteristic value from an arbitrary presentation and residue_eq_meromorphicTrailingCoeffAt_of_order_eq_neg_one for the simple-pole value.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Contour.residue_eq_of_order_lt_zero {f g : ℂ → ℂ} {z₀ : ℂ} {n : ℤ} (hlt : n < 0) (hg : AnalyticAt ℂ g z₀) (hg_ne : g z₀ ≠ 0) (hfg : f =ᶠ[nhdsWithin z₀ {z₀}ᶜ] fun (z : ℂ) => (z - z₀) ^ n • g z) : residue f z₀ = iteratedDeriv (-1 - n).toNat g z₀ / ↑(-1 - n).toNat.factorial

Characteristic value of the residue at a pole. If f z = (z − z₀) ^ n • g z near z₀ (on the punctured neighborhood) with g analytic at z₀, g z₀ ≠ 0, and n < 0, then the residue is the Taylor coefficient of g at index −1 − n. This is the standard reduced analytic presentation; the order equality meromorphicOrderAt f z₀ = n is derived from it, and the value is independent of the chosen presentation g.

@[simp]

theorem TauCeti.Contour.residue_of_not_meromorphicAt {f : ℂ → ℂ} {z₀ : ℂ} (h : ¬MeromorphicAt f z₀) : residue f z₀ = 0

If f is not meromorphic at z₀, its residue is 0 by definition.

@[simp]

theorem TauCeti.Contour.residue_eq_zero_of_meromorphicOrderAt_nonneg {f : ℂ → ℂ} {z₀ : ℂ} (h : 0 ≤ meromorphicOrderAt f z₀) : residue f z₀ = 0

The residue vanishes at a point where f has nonnegative meromorphic order (in particular where f is analytic): there is no order-(−1) Laurent coefficient.

@[simp]

theorem TauCeti.Contour.residue_eq_zero_of_analyticAt {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) : residue f z₀ = 0

The residue vanishes where f is analytic.

theorem TauCeti.Contour.residue_congr_nhdsNE {f g : ℂ → ℂ} {z₀ : ℂ} (h : f =ᶠ[nhdsWithin z₀ {z₀}ᶜ] g) : residue f z₀ = residue g z₀

The residue depends only on the germ of f on a punctured neighborhood of z₀: functions agreeing near (but not necessarily at) z₀ have the same residue.

@[simp]

theorem TauCeti.Contour.residue_eq_meromorphicTrailingCoeffAt_of_order_eq_neg_one {f : ℂ → ℂ} {z₀ : ℂ} (hord : meromorphicOrderAt f z₀ = -1) : residue f z₀ = meromorphicTrailingCoeffAt f z₀

At a simple pole (meromorphicOrderAt f z₀ = −1), the residue is the leading Laurent coefficient meromorphicTrailingCoeffAt f z₀, i.e. lim_{z→z₀} (z − z₀) · f z. The n = −1 specialization of residue_eq_of_order_lt_zero: the Taylor coefficient at index −1 − (−1) = 0 of the analytic part g is just g z₀, which is the trailing coefficient.

theorem TauCeti.Contour.residue_eq_of_eventuallyEq_zpow_smul {f g : ℂ → ℂ} {z₀ : ℂ} {n : ℤ} (hn : n ≤ -1) (hg : AnalyticAt ℂ g z₀) (hfg : f =ᶠ[nhdsWithin z₀ {z₀}ᶜ] fun (z : ℂ) => (z - z₀) ^ n • g z) : residue f z₀ = iteratedDeriv (-1 - n).toNat g z₀ / ↑(-1 - n).toNat.factorial

Generalized characteristic value of the residue. If f z = (z − z₀) ^ n • g z near z₀ (on the punctured neighborhood) with g analytic at z₀ and n ≤ −1, then the residue is the Taylor coefficient iteratedDeriv (−1 − n) g z₀ / (−1 − n)!. Unlike residue_eq_of_order_lt_zero this drops the hypothesis g z₀ ≠ 0, so the presentation exponent n need not be the meromorphic order of f: g may vanish at z₀, raising the true pole order above n; only when g's vanishing order is at least -n is f analytic (residue 0).

theorem TauCeti.Contour.exists_analyticAt_eventuallyEq_zpow_smul {f : ℂ → ℂ} {z₀ : ℂ} {m : ℤ} (hf : MeromorphicAt f z₀) (hm : ↑m ≤ meromorphicOrderAt f z₀) : ∃ (φ : ℂ → ℂ), AnalyticAt ℂ φ z₀ ∧ f =ᶠ[nhdsWithin z₀ {z₀}ᶜ] fun (z : ℂ) => (z - z₀) ^ m • φ z

Any meromorphic f admits an analytic presentation f z = (z − z₀) ^ m • φ z near z₀ at any exponent m at or below its meromorphic order (padding the reduced presentation with a nonnegative power of z − z₀). The factor φ is analytic but may vanish at z₀ when m is strictly below the order. Brings two meromorphic functions to a common exponent before adding their residues, and is the factorisation entry point for the canonical Laurent data (MeromorphicLaurent.lean).

@[simp]

theorem TauCeti.Contour.residue_add {f g : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) (hg : MeromorphicAt g z₀) : residue (f + g) z₀ = residue f z₀ + residue g z₀

Additivity of the residue. The residue is additive on functions meromorphic at z₀.

@[simp]

theorem TauCeti.Contour.residue_const_mul {f : ℂ → ℂ} {z₀ : ℂ} (c : ℂ) : residue (fun (z : ℂ) => c * f z) z₀ = c * residue f z₀

Scaling of the residue. Scaling f by a constant scales its residue by that constant.

No meromorphy hypothesis is needed: the identity holds for every f, through the junk value where f is not meromorphic at z₀. Contrast residue_add, whose hypotheses are essential — two functions that are not meromorphic can sum to one that is.

@[simp]

theorem TauCeti.Contour.residue_const_smul {f : ℂ → ℂ} {z₀ : ℂ} (c : ℂ) : residue (c • f) z₀ = c • residue f z₀

Scaling of the residue (unapplied •). The residue commutes with scalar multiplication; the Pi.smul companion to residue_const_mul.

@[deprecated "Use `residue_const_smul`, which is unconditional: drop the meromorphy argument." (since := "2026-07-30")]

theorem TauCeti.Contour.residue_smul {f : ℂ → ℂ} {z₀ : ℂ} (c : ℂ) (_hf : MeromorphicAt f z₀) : residue (c • f) z₀ = c • residue f z₀

Compatibility wrapper for the former name of residue_const_smul. Stated with the signature that name carried, so existing residue_smul c hf calls keep elaborating; the meromorphy argument is ignored, that lemma now being unconditional. Migrate to residue_const_smul, dropping that argument — which is why no automatic replacement is named here: residue_const_smul c hf would not elaborate.

@[simp]

theorem TauCeti.Contour.residue_sub {f g : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) (hg : MeromorphicAt g z₀) : residue (f - g) z₀ = residue f z₀ - residue g z₀

Subtractivity of the residue. The residue distributes over subtraction of meromorphic functions; the −1 scaling case of residue_add and residue_const_mul.

@[simp]

theorem TauCeti.Contour.residue_sum {ι : Type u_1} (s : Finset ι) {f : ι → ℂ → ℂ} {z₀ : ℂ} (hf : ∀ i ∈ s, MeromorphicAt (f i) z₀) : residue (∑ i ∈ s, f i) z₀ = ∑ i ∈ s, residue (f i) z₀

The residue of a finite sum. For a finite family of functions meromorphic at z₀, the residue of the sum is the sum of the residues — the form consumed by the residue theorem.

@[simp]

theorem TauCeti.Contour.residue_const_div_sub_pow (a z₀ : ℂ) (k : ℕ) : residue (fun (z : ℂ) => a / (z - z₀) ^ (k + 1)) z₀ = if k = 0 then a else 0

The residue of a Laurent monomial: residue (a / (z - z₀)^(k+1)) z₀ is a for k = 0 and 0 for higher-order terms.

@[simp]

theorem TauCeti.Contour.residue_div_sub_pow_of_analyticAt {g : ℂ → ℂ} {z₀ : ℂ} (hg : AnalyticAt ℂ g z₀) (k : ℕ) : residue (fun (z : ℂ) => g z / (z - z₀) ^ (k + 1)) z₀ = iteratedDeriv k g z₀ / ↑k.factorial

The residue of the Cauchy kernel. If g is analytic at z₀, then the function g z / (z - z₀) ^ (k + 1) has residue the Taylor coefficient iteratedDeriv k g z₀ / k ! at z₀: the whole Laurent principal part comes from the first k + 1 Taylor terms of g, and only the one of index k sits at order −1. This is the residue behind Cauchy's integral formula for the k-th derivative; the constant case is TauCeti.Contour.residue_const_div_sub_pow.

theorem TauCeti.Contour.residue_of_laurent_expansion {f g : ℂ → ℂ} {z₀ : ℂ} {N : ℕ} {a : Fin N → ℂ} (hg : AnalyticAt ℂ g z₀) (hf_eq : ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = g z + ∑ k : Fin N, a k / (z - z₀) ^ (↑k + 1)) : residue f z₀ = if h : 0 < N then a ⟨0, h⟩ else 0

The residue from a Laurent expansion. If f z = g z + ∑ k, a k / (z - z₀)^(k+1) near z₀ with g analytic at z₀, then residue f z₀ is the first Laurent coefficient a 0 (or 0 for an empty expansion): the analytic part and the higher-order terms contribute nothing.