Meromorphic Laurent Principal Parts

This file connects MeromorphicAt from Mathlib with Laurent principal parts and proves that contour integrals of principal parts with zero residue vanish on closed curves.

Main Definitions

• meromorphicPrincipalPart -- the finite-rank polar part of a meromorphic function

Main Results

• meromorphicPrincipalPart_differentiableOn -- principal part is differentiable away from the pole
• meromorphicAt_sub_principalPart_eventually -- f minus its principal part is analytic at the pole
• contourIntegral_zpow_eq_zero -- contour integral of (z-s)^n dz = 0 for n <= -2 on closed curves
• contourIntegral_principalPart_eq_zero_of_residue_zero -- contour integral of pp = 0 when residue is zero

Mathematical Overview

For a function f meromorphic at s with a pole of order N, Mathlib gives a decomposition f =ae (z - s)^(-N) * g near s with g analytic and g(s) != 0. The principal part is the sum of the first N terms of the Laurent series:

pp(z) = sum_{k=1}^{N} c_k / (z - s)^k

where c_k = (1/k!) * iteratedDeriv k g s (adjusted by the order).

When Res(f, s) = 0, the (z-s)^{-1} coefficient vanishes, and each (z-s)^{-k} term for k >= 2 integrates to zero on closed curves (by FTC). So the contour integral of pp = 0.

References

• Mathlib MeromorphicAt, meromorphicOrderAt

Definition of the meromorphic principal part

For f meromorphic at s, the principal part extracts the finite Laurent tail. If meromorphicOrderAt f s = -N (pole of order N), we use the Mathlib decomposition f =ae (z - s)^(-N) * g with g analytic and g(s) != 0, then:

pp(z) = sum_{k=0}^{N-1} (g^(k)(s) / k!) * (z - s)^{k - N}

This equals sum_{j=1}^{N} c_j / (z-s)^j where c_j = g^{(N-j)}(s) / (N-j)!.

If f is analytic at s (order >= 0) or not meromorphic, the principal part is 0.

noncomputable def GeneralizedResidueTheory.meromorphicPrincipalPart (f : ℂ → ℂ) (s : ℂ) : ℂ → ℂ

The meromorphic principal part of f at s.

If f has a pole of order N at s (i.e., meromorphicOrderAt f s = -(N : ℤ) with N > 0), the principal part is a rational function that captures the singular behavior. If f is analytic at s or not meromorphic, returns 0.

Equations

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

theorem GeneralizedResidueTheory.meromorphicPrincipalPart_eq_zero_of_analyticAt (f : ℂ → ℂ) (s : ℂ) (hf : AnalyticAt ℂ f s) : meromorphicPrincipalPart f s = fun (x : ℂ) => 0

When f is analytic at s (non-negative order), the principal part is zero.

Differentiability of the principal part

theorem GeneralizedResidueTheory.meromorphicPrincipalPart_differentiableOn (f : ℂ → ℂ) (s : ℂ) (hf : MeromorphicAt f s) : DifferentiableOn ℂ (meromorphicPrincipalPart f s) {s}ᶜ

The principal part is differentiable on {s}ᶜ.

The regular part is analytic

f minus its principal part extends analytically to the pole.

theorem GeneralizedResidueTheory.meromorphicAt_sub_principalPart_eventually (f : ℂ → ℂ) (s : ℂ) (hf : MeromorphicAt f s) : ∃ (g : ℂ → ℂ), AnalyticAt ℂ g s ∧ ∀ᶠ (z : ℂ) in nhdsWithin s {s}ᶜ, f z - meromorphicPrincipalPart f s z = g z

If f is meromorphic at s, then f - meromorphicPrincipalPart f s agrees with an analytic function near s (away from s). Since the principal part captures exactly the singular behavior, the difference extends analytically.

Local reproductions of zpow FTC lemmas

These lemmas were previously imported from FlatnessTransfer.lean. They are reproved here locally to avoid a circular dependency.

Contour integral of zpow on closed curves

For n <= -2, the function z |-> (z - s)^n has a primitive (z - s)^{n+1}/(n+1), which is single-valued away from s. On a closed curve avoiding s, the boundary terms cancel.

theorem GeneralizedResidueTheory.contourIntegral_zpow_eq_zero (s : ℂ) (n : ℤ) (hn : n ≤ -2) (γ : PiecewiseC1Immersion) (hγ_closed : γ.IsClosed) (hγ_avoids : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ s) : ∫ (t : ℝ) in γ.a..γ.b, (γ.toFun t - s) ^ n * deriv γ.toFun t = 0

For n <= -2, the contour integral ∮ (z - s)^n dz = 0 along any closed piecewise C^1 immersion that avoids s. This follows from the fundamental theorem of calculus: the primitive (z-s)^{n+1}/(n+1) is well-defined since n + 1 <= -1 != -1 (i.e. n + 1 != 0), and the boundary values cancel by closedness.

theorem GeneralizedResidueTheory.contourIntegral_const_mul_zpow_eq_zero (s : ℂ) (n : ℤ) (hn : n ≤ -2) (c : ℂ) (γ : PiecewiseC1Immersion) (hγ_closed : γ.IsClosed) (hγ_avoids : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ s) : ∫ (t : ℝ) in γ.a..γ.b, c * (γ.toFun t - s) ^ n * deriv γ.toFun t = 0

Variant: contour integral of c * (z - s)^n is zero for n <= -2.

Residue of the principal part

The residue of the principal part equals the (N-1)-th coefficient c_{N-1}. This is computed directly via circle integrals: in the sum Σ c_k (z-s)^{k-N}, only the k=N-1 term (exponent -1) contributes to the residue.

Principal part integral vanishing

When the residue is zero, the principal part integral vanishes on closed curves. The principal part is a finite sum of terms c_k * (z - s)^{k - N} for k = 0..N-1. The term with k = N-1 gives exponent -1 (the residue term), which vanishes by assumption. All other terms have exponent <= -2, so they vanish by contourIntegral_zpow_eq_zero.

theorem GeneralizedResidueTheory.contourIntegral_principalPart_eq_zero_of_residue_zero (f : ℂ → ℂ) (s : ℂ) (hf : MeromorphicAt f s) (hres : residueAt f s = 0) (γ : PiecewiseC1Immersion) (hγ_closed : γ.IsClosed) (hγ_avoids : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ s) : ∫ (t : ℝ) in γ.a..γ.b, meromorphicPrincipalPart f s (γ.toFun t) * deriv γ.toFun t = 0

The contour integral of the principal part vanishes when the residue is zero.