Principal parts at a point (residue-calculus)

RS.principalPartAt f z₀ is the finite sum of the negative-exponent Laurent terms of f at z₀ — an honest function ℂ → ℂ, analytic away from z₀ and meromorphic at z₀; it is 0 (empty sum) when f is analytic-after-repair at z₀, not meromorphic there, or locally 0.

Main exports:

• RS.MeromorphicAt.exists_principalPart_add_analyticAt — THE decomposition f =ᶠ[𝓝[≠] z₀] principalPartAt f z₀ + h with h analytic whose Taylor coefficients are the nonnegative Laurent coefficients of f;
• RS.MeromorphicAt.orderAt_sub_principalPartAt_nonneg — repair form;
• RS.laurentCoeffAt_principalPartAt — the principal part has exactly the negative tail;
• RS.eq_principalPart_of_eventuallyEq — uniqueness of tail + analytic decompositions.

noncomputable def RS.principalPartAt (f : ℂ → ℂ) (z₀ : ℂ) : ℂ → ℂ

The principal part of f at z₀: the finite sum of the negative-exponent Laurent terms. An honest function ℂ → ℂ, analytic on ℂ \ {z₀}, meromorphic at z₀. Zero (empty sum) when f is analytic-after-repair at z₀, not meromorphic there, or locally 0.

Equations

• RS.principalPartAt f z₀ z = ∑ k ∈ Finset.Icc (meromorphicOrderAt f z₀).untop₀ (-1), RS.laurentCoeffAt f z₀ k * (z - z₀) ^ k

theorem RS.meromorphicAt_principalPartAt {f : ℂ → ℂ} {z₀ : ℂ} : MeromorphicAt (principalPartAt f z₀) z₀

theorem RS.analyticOnNhd_principalPartAt {f : ℂ → ℂ} {z₀ : ℂ} : AnalyticOnNhd ℂ (principalPartAt f z₀) {z₀}ᶜ

theorem RS.principalPartAt_eq_zero_of_order_nonneg {f : ℂ → ℂ} {z₀ : ℂ} (h : 0 ≤ meromorphicOrderAt f z₀) : principalPartAt f z₀ = 0

theorem RS.principalPartAt_of_not_meromorphicAt {f : ℂ → ℂ} {z₀ : ℂ} (h : ¬MeromorphicAt f z₀) : principalPartAt f z₀ = 0

theorem RS.principalPartAt_of_order_eq_top {f : ℂ → ℂ} {z₀ : ℂ} (h : meromorphicOrderAt f z₀ = ⊤) : principalPartAt f z₀ = 0

theorem RS.laurentCoeffAt_principalPartAt {f : ℂ → ℂ} {z₀ : ℂ} (_hf : MeromorphicAt f z₀) (k : ℤ) : laurentCoeffAt (principalPartAt f z₀) z₀ k = if k < 0 then laurentCoeffAt f z₀ k else 0

The Laurent coefficients of the principal part: exactly the negative tail of f.

theorem RS.MeromorphicAt.exists_principalPart_add_analyticAt {f : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) : ∃ (h : ℂ → ℂ), AnalyticAt ℂ h z₀ ∧ (∀ (j : ℕ), taylorCoeffAt h z₀ j = laurentCoeffAt f z₀ ↑j) ∧ f =ᶠ[nhdsWithin z₀ {z₀}ᶜ] fun (z : ℂ) => principalPartAt f z₀ z + h z

THE decomposition: f = (principal part) + (analytic) on a punctured neighborhood. The analytic part's Taylor coefficients are the nonnegative Laurent coefficients of f.

theorem RS.MeromorphicAt.orderAt_sub_principalPartAt_nonneg {f : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) : 0 ≤ meromorphicOrderAt (fun (z : ℂ) => f z - principalPartAt f z₀ z) z₀

Repair form (MeromorphicNFAt-compatible corollary): subtracting the principal part leaves a germ of nonnegative order.

theorem RS.eq_principalPart_of_eventuallyEq {f h : ℂ → ℂ} {z₀ : ℂ} {c : ℤ → ℂ} {s : Finset ℤ} (hs : ∀ k ∈ s, k < 0) (hh : AnalyticAt ℂ h z₀) (hfg : f =ᶠ[nhdsWithin z₀ {z₀}ᶜ] fun (z : ℂ) => ∑ k ∈ s, c k * (z - z₀) ^ k + h z) : (∀ k ∈ s, c k = laurentCoeffAt f z₀ k) ∧ (∀ k < 0, k ∉ s → laurentCoeffAt f z₀ k = 0) ∧ ∀ (j : ℕ), taylorCoeffAt h z₀ j = laurentCoeffAt f z₀ ↑j

Uniqueness: any Laurent-tail + analytic decomposition IS the canonical one.