The residue at a simple pole as a limit

For f : ℂ → ℂ with a simple pole at z₀ (meromorphicOrderAt f z₀ = −1), the residue TauCeti.Contour.residue f z₀ is the elementary limit lim_{z→z₀} (z − z₀) · f z — the textbook recipe for computing residues at simple poles, which the roadmap names as the defining property of the simple-pole residue. This file records that limit and its converse: the residue equals the limit whenever f is meromorphic at z₀ and the limit exists.

The order-(−1) Laurent coefficient of f at a simple pole is the trailing coefficient meromorphicTrailingCoeffAt f z₀ (via TauCeti.Contour.residue_eq_meromorphicTrailingCoeffAt_of_order_eq_neg_one), and Mathlib records that this trailing coefficient is the limit of (· − z₀) ^ (−order) • f (MeromorphicAt.tendsto_nhds_meromorphicTrailingCoeffAt). Here we phrase the statement directly on (z − z₀) · f z, valid whenever the pole order is at most 1 (−1 ≤ order, so no pole or a simple pole): at a genuine simple pole the limit is the residue, and where f is analytic (or has a higher zero) both the residue and the limit are 0.

The converse residue_eq_of_tendsto_sub_mul turns the limit into a computation rule: if (z − z₀) · f z converges as z → z₀, then the residue is exactly that limit. This is the direction one uses in practice to read off a residue.

Main results

• TauCeti.Contour.tendsto_sub_mul_nhds_residue_of_order_eq_neg_one — at a simple pole (meromorphicOrderAt f z₀ = −1), (z − z₀) · f z → residue f z₀.
• TauCeti.Contour.tendsto_sub_mul_nhds_residue — the same limit whenever −1 ≤ meromorphicOrderAt f z₀ (at most a simple pole); the analytic case gives the limit 0 = residue f z₀.
• TauCeti.Contour.residue_eq_of_tendsto_sub_mul — the converse: if f is meromorphic at z₀ and (z − z₀) · f z converges to L, then residue f z₀ = L.
• TauCeti.Contour.residue_sub_inv — residue (fun z => (z − z₀)⁻¹) z₀ = 1, and TauCeti.Contour.residue_const_mul_sub_inv — residue (fun z => c · (z − z₀)⁻¹) z₀ = c: the elementary simple-pole residues, read off from the converse rule.

Provenance

Adapted from the AINTLIB LeanModularForms project (the residue material of ForMathlib/GeneralizedResidueTheory/Residue.lean), and built on Mathlib's trailing-coefficient limit API (MeromorphicAt.tendsto_nhds_meromorphicTrailingCoeffAt) and the order/convergence dictionary in Mathlib/Analysis/Meromorphic/Order.lean.

References

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

theorem TauCeti.Contour.tendsto_sub_mul_nhds_residue_of_order_eq_neg_one {f : ℂ → ℂ} {z₀ : ℂ} (hord : meromorphicOrderAt f z₀ = -1) : Filter.Tendsto (fun (z : ℂ) => (z - z₀) * f z) (nhdsWithin z₀ {z₀}ᶜ) (nhds (residue f z₀))

The residue at a simple pole is lim_{z→z₀} (z − z₀) · f z. If f has a simple pole at z₀ (meromorphicOrderAt f z₀ = −1), then (z − z₀) · f z converges to residue f z₀ as z → z₀.

theorem TauCeti.Contour.tendsto_sub_mul_nhds_residue {f : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) (hord : -1 ≤ meromorphicOrderAt f z₀) : Filter.Tendsto (fun (z : ℂ) => (z - z₀) * f z) (nhdsWithin z₀ {z₀}ᶜ) (nhds (residue f z₀))

The residue as a limit, at most a simple pole. If f has at most a simple pole at z₀ (−1 ≤ meromorphicOrderAt f z₀), then (z − z₀) · f z → residue f z₀ as z → z₀. In the analytic case (order ≥ 0) both the residue and the limit are 0.

theorem TauCeti.Contour.residue_eq_of_tendsto_sub_mul {f : ℂ → ℂ} {z₀ L : ℂ} (hf : MeromorphicAt f z₀) (h : Filter.Tendsto (fun (z : ℂ) => (z - z₀) * f z) (nhdsWithin z₀ {z₀}ᶜ) (nhds L)) : residue f z₀ = L

Computing a residue as a limit (converse). If f is meromorphic at z₀ and the product (z − z₀) · f z converges to L as z → z₀, then residue f z₀ = L. This is the direction used in practice to read off a residue.

theorem TauCeti.Contour.meromorphicAt_sub_inv (z₀ : ℂ) : MeromorphicAt (fun (z : ℂ) => (z - z₀)⁻¹) z₀

The reciprocal (· − z₀)⁻¹ of the simple factor (· − z₀) is meromorphic at z₀.

@[simp]

theorem TauCeti.Contour.residue_sub_inv (z₀ : ℂ) : residue (fun (z : ℂ) => (z - z₀)⁻¹) z₀ = 1

The residue of the elementary simple pole (· − z₀)⁻¹ at z₀ is 1: since (z − z₀) · (z − z₀)⁻¹ → 1 as z → z₀, the simple-pole limit formula gives the residue.

@[simp]

theorem TauCeti.Contour.residue_const_mul_sub_inv (c z₀ : ℂ) : residue (fun (z : ℂ) => c * (z - z₀)⁻¹) z₀ = c

The residue of c · (· − z₀)⁻¹ at z₀ is c: scaling the elementary simple pole scales its residue.