The residue of a quotient at a simple zero of the denominator

For g, h analytic at z₀ with h z₀ = 0 and h' z₀ ≠ 0, the quotient g / h has at worst a simple pole at z₀ and

Res_{z₀} (g / h) = g z₀ / h' z₀.

This is the textbook recipe for the residue at a simple pole of a quotient: it applies exactly when the denominator's zero at z₀ is simple, and says nothing about higher-order zeros of h or about more general meromorphic singularities. Within that range it is the computational input to the roadmap's applications: the classical residue theorem (TauCeti.Contour.classicalResidueTheorem_circle) and the improper integrals reached by the Hungerbühler–Wasem generalized residue theorem (TauCeti.Contour.hungerbuhlerWasem_residueTheorem) both reduce an integral to a sum of residues, which then have to be computed.

The mechanism is the simple-pole limit rule TauCeti.Contour.residue_eq_of_tendsto_sub_mul: since h z₀ = 0, the difference quotient slope h z₀ z is h z / (z − z₀), so its reciprocal (z − z₀) / h z tends to (h' z₀)⁻¹ by the very definition of the derivative (hasDerivAt_iff_tendsto_slope). Multiplying by the continuous factor g gives (z − z₀) · (g z / h z) → g z₀ / h' z₀, and that limit is the residue. No Laurent expansion of h is needed: only the first-order information h z₀ = 0, h' z₀ ≠ 0.

The companion order computation is recorded alongside, because the Hungerbühler–Wasem hypotheses are stated in terms of pole orders: a simple zero of the denominator drops the order by exactly one (meromorphicOrderAt_div_of_zero_deriv_ne_zero), so g / h has an exactly simple pole as soon as g z₀ ≠ 0 (meromorphicOrderAt_div_eq_neg_one). That is precisely the shape of hypothesis that TauCeti.Contour.hasCauchyPV_half_residue_of_simple_pole and TauCeti.Contour.hungerbuhlerWasem_residueTheorem_of_simple_poles consume.

Main results

• TauCeti.Contour.residue_div_of_zero_deriv_ne_zero — residue (g / h) z₀ = g z₀ / deriv h z₀ at a simple zero z₀ of h.
• TauCeti.Contour.residue_inv_of_zero_deriv_ne_zero — the numerator-free case residue (fun z => (h z)⁻¹) z₀ = (deriv h z₀)⁻¹.
• TauCeti.Contour.meromorphicOrderAt_div_of_zero_deriv_ne_zero — a simple zero of the denominator lowers the meromorphic order by one.
• TauCeti.Contour.meromorphicOrderAt_div_eq_neg_one — the pole is exactly simple when the numerator does not vanish, the meromorphicOrderAt … = −1 hypothesis of the simple-pole residue theorems.
• TauCeti.Contour.residue_inv_pow_sub_one — the worked example residue (fun z => (z ^ n − 1)⁻¹) ζ = ζ / n at an n-th root of unity ζ, and TauCeti.Contour.residue_inv_sq_add_one_I — residue (fun z => (z ^ 2 + 1)⁻¹) I = −(I / 2), the residue behind the improper integral ∫ dx / (1 + x²).

These are Layer 2 results of the contour-integration roadmap: the residue against Mathlib's meromorphicOrderAt API, in the form the residue theorems' right-hand sides are evaluated with.

Implementation notes

The derivative hypothesis is phrased with Mathlib's deriv rather than a bundled HasDerivAt witness, so that the statement reads as the textbook formula g z₀ / h'(z₀); AnalyticAt supplies differentiability, so a HasDerivAt witness converts with HasDerivAt.deriv.

References

• L. Ahlfors, Complex Analysis, Ch. 4 (the residue at a simple pole of a quotient).
• S. Lang, Complex Analysis (GTM 103), Ch. VI.
• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997.

@[simp]

theorem TauCeti.Contour.residue_div_of_zero_deriv_ne_zero {g h : ℂ → ℂ} {z₀ : ℂ} (hg : AnalyticAt ℂ g z₀) (hh : AnalyticAt ℂ h z₀) (hh0 : h z₀ = 0) (hh' : deriv h z₀ ≠ 0) : residue (fun (z : ℂ) => g z / h z) z₀ = g z₀ / deriv h z₀

The residue of a quotient at a simple zero of the denominator. If g and h are analytic at z₀ with h z₀ = 0 and deriv h z₀ ≠ 0, then

residue (fun z => g z / h z) z₀ = g z₀ / deriv h z₀.

This is the textbook computation rule for residues of quotients; it needs only the first-order data h z₀ = 0 and deriv h z₀ ≠ 0 at the denominator's zero, no Laurent expansion.

@[simp]

theorem TauCeti.Contour.residue_inv_of_zero_deriv_ne_zero {h : ℂ → ℂ} {z₀ : ℂ} (hh : AnalyticAt ℂ h z₀) (hh0 : h z₀ = 0) (hh' : deriv h z₀ ≠ 0) : residue (fun (z : ℂ) => (h z)⁻¹) z₀ = (deriv h z₀)⁻¹

The residue of a reciprocal at a simple zero. The numerator-free case of TauCeti.Contour.residue_div_of_zero_deriv_ne_zero: at a zero of h with non-vanishing derivative, residue (fun z => (h z)⁻¹) z₀ = (deriv h z₀)⁻¹.

theorem TauCeti.Contour.meromorphicOrderAt_div_of_zero_deriv_ne_zero {g h : ℂ → ℂ} {z₀ : ℂ} (hg : MeromorphicAt g z₀) (hh : AnalyticAt ℂ h z₀) (hh0 : h z₀ = 0) (hh' : deriv h z₀ ≠ 0) : meromorphicOrderAt (fun (z : ℂ) => g z / h z) z₀ = meromorphicOrderAt g z₀ - 1

A simple zero of the denominator lowers the meromorphic order by one: if g is meromorphic at z₀ and h is analytic at z₀ with h z₀ = 0 and deriv h z₀ ≠ 0, then

meromorphicOrderAt (fun z => g z / h z) z₀ = meromorphicOrderAt g z₀ − 1.

The denominator's analytic order at a zero with non-vanishing derivative is 1 (AnalyticAt.analyticOrderAt_eq_one_of_zero_deriv_ne_zero), and orders subtract across a quotient (fun_meromorphicOrderAt_div).

theorem TauCeti.Contour.meromorphicOrderAt_div_eq_neg_one {g h : ℂ → ℂ} {z₀ : ℂ} (hg : AnalyticAt ℂ g z₀) (hgne : g z₀ ≠ 0) (hh : AnalyticAt ℂ h z₀) (hh0 : h z₀ = 0) (hh' : deriv h z₀ ≠ 0) : meromorphicOrderAt (fun (z : ℂ) => g z / h z) z₀ = -1

A non-vanishing numerator over a simple zero is an exactly simple pole. If g and h are analytic at z₀ with g z₀ ≠ 0, h z₀ = 0 and deriv h z₀ ≠ 0, then meromorphicOrderAt (fun z => g z / h z) z₀ = −1. This is the order = −1 hypothesis consumed by the simple-pole residue theorems (TauCeti.Contour.hungerbuhlerWasem_residueTheorem_of_simple_poles, TauCeti.Contour.hasCauchyPV_half_residue_of_simple_pole), whose residue is then g z₀ / deriv h z₀ by TauCeti.Contour.residue_div_of_zero_deriv_ne_zero.

Worked examples

Two concrete residues that the quotient rule reads off in a few lines, and that the classical residue theorem's right-hand side needs in order to produce a number.

@[simp]

theorem TauCeti.Contour.residue_inv_pow_sub_one {n : ℕ} {ζ : ℂ} (hζ : ζ ^ n = 1) : residue (fun (z : ℂ) => (z ^ n - 1)⁻¹) ζ = ζ / ↑n

The residue of (z ^ n − 1)⁻¹ at an n-th root of unity is ζ / n. The denominator has a simple zero at ζ with derivative n · ζ ^ (n − 1) = n · ζ⁻¹, so the residue is ζ / n; summing over the n-th roots of unity recovers the familiar partial-fraction coefficients of (z ^ n − 1)⁻¹. For n = 0 the statement degenerates: both sides are 0.

@[simp]

theorem TauCeti.Contour.residue_inv_sq_add_one_I : residue (fun (z : ℂ) => (z ^ 2 + 1)⁻¹) Complex.I = -(Complex.I / 2)

The residue of (z ^ 2 + 1)⁻¹ at I is −(I / 2): the denominator has a simple zero at I with derivative 2 I, so the residue is (2 I)⁻¹ = −(I / 2). This is the residue behind the classical evaluation of the improper integral ∫ dx / (1 + x ^ 2) = π.