Documentation

LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.MeromorphicPrincipalPart

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 #

Main Results #

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 #

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.

source
noncomputable def GeneralizedResidueTheory.poleOrderNat (f : ℂ → ℂ) (s : ℂ) :
ℕ

Helper: extract the pole order as a natural number from meromorphic data.

Equations
Instances For
    source
    noncomputable def GeneralizedResidueTheory.meromorphicFactor (f : ℂ → ℂ) (s : ℂ) (hf : MeromorphicAt f s) (hne : meromorphicOrderAt f s ≠ ⊤) :
    ℂ → ℂ

    Helper: extract the analytic factor g from the meromorphic decomposition.

    Equations
    Instances For
      source
      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.
      Instances For
        source
        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 #

        source
        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.

        source
        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.

        source
        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.

        source
        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.

        source
        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.