21.6. LaurentTail.LaurentCoeff🔗

Jacobians.LaurentTail.LaurentCoeff — source

laurentCoeff

The n-th Laurent coefficient of g : ℂ → ℂ at c: the residue at c of g(z)·(z − c)^{−n−1} (for g = ∑ aₖ (z−c)^k the only term surviving the contour integral is k = n, giving aₙ).

noncomputable def laurentCoeff (g : ℂ → ℂ) (c : ℂ) (n : ℤ) : ℂ

laurentCoeff_def

theorem laurentCoeff_def (g : ℂ → ℂ) (c : ℂ) (n : ℤ) :
    laurentCoeff g c n = resAt (fun z => g z * (z - c) ^ (-n - 1)) c

meromorphicAt_monomial

The Laurent monomial (· − c)^k is meromorphic at c.

theorem meromorphicAt_monomial (c : ℂ) (k : ℤ) : MeromorphicAt ((· - c) ^ k) c

holoPunctured_mul_monomial

g·(· − c)^k has an isolated singularity at c whenever g is meromorphic at c.

theorem holoPunctured_mul_monomial {g : ℂ → ℂ} {c : ℂ} (hg : MeromorphicAt g c) (k : ℤ) :
    HoloPunctured (g * (· - c) ^ k) c

laurentCoeff_congr

Laurent coefficients are germ invariants: functions agreeing on a punctured neighbourhood of c have the same coefficients.

theorem laurentCoeff_congr {g₁ g₂ : ℂ → ℂ} {c : ℂ} (h : g₁ =ᶠ[𝓝[≠] c] g₂) (n : ℤ) :
    laurentCoeff g₁ c n = laurentCoeff g₂ c n

laurentCoeff_zero

@[simp] theorem laurentCoeff_zero (c : ℂ) (n : ℤ) : laurentCoeff (0 : ℂ → ℂ) c n = 0

laurentCoeff_add

ℂ-additivity of the Laurent coefficients (on meromorphic germs).

theorem laurentCoeff_add {g₁ g₂ : ℂ → ℂ} {c : ℂ} (h₁ : MeromorphicAt g₁ c)
    (h₂ : MeromorphicAt g₂ c) (n : ℤ) :
    laurentCoeff (g₁ + g₂) c n = laurentCoeff g₁ c n + laurentCoeff g₂ c n

laurentCoeff_smul

ℂ-homogeneity of the Laurent coefficients (on meromorphic germs).

theorem laurentCoeff_smul {g : ℂ → ℂ} {c : ℂ} (a : ℂ) (hg : MeromorphicAt g c) (n : ℤ) :
    laurentCoeff (a • g) c n = a * laurentCoeff g c n

resAt_eq_zero_of_nonneg_order

Residues of nonnegative-order germs vanish. If F is meromorphic at c with meromorphicOrderAt F c ≥ 0, then resAt F c = 0: either F vanishes near c, or it agrees on a punctured neighbourhood with the analytic function (· − c)^m • G (m ≥ 0, G analytic).

theorem resAt_eq_zero_of_nonneg_order {F : ℂ → ℂ} {c : ℂ} (hF : MeromorphicAt F c)
    (h : 0 ≤ meromorphicOrderAt F c) : resAt F c = 0

laurentCoeff_eq_zero_of_lt_order

Anchor (a): coefficients below the order vanish.

theorem laurentCoeff_eq_zero_of_lt_order {g : ℂ → ℂ} {c : ℂ} {n : ℤ} (hg : MeromorphicAt g c)
    (hn : (n : WithTop ℤ) < meromorphicOrderAt g c) : laurentCoeff g c n = 0

laurentCoeff_order_ne_zero

Anchor (a′): the leading coefficient is nonzero. If g has finite order m at c, its m-th Laurent coefficient does not vanish (Cauchy's integral formula on the analytic factor).

theorem laurentCoeff_order_ne_zero {g : ℂ → ℂ} {c : ℂ} {m : ℤ} (hg : MeromorphicAt g c)
    (h : meromorphicOrderAt g c = (m : WithTop ℤ)) : laurentCoeff g c m ≠ 0

le_order_iff_laurentCoeff_eq_zero

Anchor (b): order via coefficients. A meromorphic germ has order ≥ k iff all its Laurent coefficients of degree < k vanish.

theorem le_order_iff_laurentCoeff_eq_zero {g : ℂ → ℂ} {c : ℂ} (hg : MeromorphicAt g c) (k : ℤ) :
    (k : WithTop ℤ) ≤ meromorphicOrderAt g c ↔ ∀ n : ℤ, n < k → laurentCoeff g c n = 0