Laurent coefficients at a point (residue-calculus)

RS.laurentCoeffAt f z₀ k is the k-th Laurent coefficient of f at z₀ (coefficient of (z - z₀) ^ k), defined through the meromorphic order presentation and the dslope-iterate Taylor extractor RS.taylorCoeffAt. Junk value 0 for non-meromorphic germs, the locally-zero germ (order ⊤), and coefficients below the order.

Main exports:

• RS.laurentCoeffAt_of_eventuallyEq — THE characterization: any presentation f =ᶠ[𝓝[≠] z₀] (· - z₀) ^ n * g with g analytic computes every Laurent coefficient (n need not be the order, g z₀ = 0 is allowed);
• RS.laurentCoeffAt_congr — invariance under =ᶠ[𝓝[≠] z₀];
• RS.laurentCoeffAt_order — compatibility with meromorphicTrailingCoeffAt;
• RS.laurentCoeffAt_fun_add / _const_mul / _sub / _fun_sum — ℂ-linearity;
• RS.laurentCoeffAt_zpow_monomial, RS.laurentCoeffAt_zpow_mul — monomials and shift;
• RS.forall_neg_laurentCoeffAt_eq_zero_iff — vanishing tail ↔ analytic-after-repair.

noncomputable def RS.laurentCoeffAt (f : ℂ → ℂ) (z₀ : ℂ) (k : ℤ) : ℂ

The k-th Laurent coefficient of f at z₀ (coefficient of (z - z₀) ^ k). Defined through the order presentation f =ᶠ[𝓝[≠] z₀] (· - z₀) ^ n • g, g analytic, g z₀ ≠ 0, n = meromorphicOrderAt f z₀: the coefficient is the (k - n)-th Taylor coefficient of g. Junk 0 if f is not meromorphic at z₀, on the locally-zero germ (order ⊤), and for k < order.

Equations

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

@[simp]

theorem RS.laurentCoeffAt_of_not_meromorphicAt {f : ℂ → ℂ} {z₀ : ℂ} (h : ¬MeromorphicAt f z₀) (k : ℤ) : laurentCoeffAt f z₀ k = 0

@[simp]

theorem RS.laurentCoeffAt_of_order_eq_top {f : ℂ → ℂ} {z₀ : ℂ} (h : meromorphicOrderAt f z₀ = ⊤) (k : ℤ) : laurentCoeffAt f z₀ k = 0

theorem RS.laurentCoeffAt_of_eventuallyEq {f g : ℂ → ℂ} {z₀ : ℂ} {n : ℤ} (hg : AnalyticAt ℂ g z₀) (hfg : f =ᶠ[nhdsWithin z₀ {z₀}ᶜ] fun (z : ℂ) => (z - z₀) ^ n * g z) (k : ℤ) : laurentCoeffAt f z₀ k = if n ≤ k then taylorCoeffAt g z₀ (k - n).toNat else 0

THE characterization (workhorse; the only lemma that unfolds the definition). Any zpow-presentation computes every Laurent coefficient — n need NOT be the order and g z₀ = 0 is allowed.

theorem RS.laurentCoeffAt_eq_zero_of_lt_order {f : ℂ → ℂ} {z₀ : ℂ} {k : ℤ} (h : ↑k < meromorphicOrderAt f z₀) : laurentCoeffAt f z₀ k = 0

theorem RS.laurentCoeffAt_congr {f g : ℂ → ℂ} {z₀ : ℂ} (hfg : f =ᶠ[nhdsWithin z₀ {z₀}ᶜ] g) (k : ℤ) : laurentCoeffAt f z₀ k = laurentCoeffAt g z₀ k

Congruence: Laurent coefficients live on the punctured germ.

theorem RS.laurentCoeffAt_order {f : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) (h : meromorphicOrderAt f z₀ ≠ ⊤) : laurentCoeffAt f z₀ (meromorphicOrderAt f z₀).untop₀ = meromorphicTrailingCoeffAt f z₀

At the order, the Laurent coefficient is mathlib's trailing coefficient.

theorem RS.laurentCoeffAt_order_ne_zero {f : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) (h : meromorphicOrderAt f z₀ ≠ ⊤) : laurentCoeffAt f z₀ (meromorphicOrderAt f z₀).untop₀ ≠ 0

theorem RS.laurentCoeffAt_of_analyticAt {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) (k : ℤ) : laurentCoeffAt f z₀ k = if 0 ≤ k then taylorCoeffAt f z₀ k.toNat else 0

For analytic f the Laurent coefficients are the Taylor coefficients.

theorem RS.laurentCoeffAt_zero_fun {z₀ : ℂ} (k : ℤ) : laurentCoeffAt (fun (x : ℂ) => 0) z₀ k = 0

theorem RS.laurentCoeffAt_fun_add {f g : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) (hg : MeromorphicAt g z₀) (k : ℤ) : laurentCoeffAt (fun (z : ℂ) => f z + g z) z₀ k = laurentCoeffAt f z₀ k + laurentCoeffAt g z₀ k

ℂ-additivity of Laurent coefficients on meromorphic germs.

theorem RS.laurentCoeffAt_add {f g : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) (hg : MeromorphicAt g z₀) (k : ℤ) : laurentCoeffAt (f + g) z₀ k = laurentCoeffAt f z₀ k + laurentCoeffAt g z₀ k

theorem RS.laurentCoeffAt_const_mul {f : ℂ → ℂ} {z₀ : ℂ} (c : ℂ) (k : ℤ) : laurentCoeffAt (fun (z : ℂ) => c * f z) z₀ k = c * laurentCoeffAt f z₀ k

theorem RS.laurentCoeffAt_neg {f : ℂ → ℂ} {z₀ : ℂ} (k : ℤ) : laurentCoeffAt (fun (z : ℂ) => -f z) z₀ k = -laurentCoeffAt f z₀ k

theorem RS.laurentCoeffAt_sub {f g : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) (hg : MeromorphicAt g z₀) (k : ℤ) : laurentCoeffAt (fun (z : ℂ) => f z - g z) z₀ k = laurentCoeffAt f z₀ k - laurentCoeffAt g z₀ k

theorem RS.laurentCoeffAt_fun_sum {z₀ : ℂ} {ι : Type u_1} {s : Finset ι} {G : ι → ℂ → ℂ} (hG : ∀ i ∈ s, MeromorphicAt (G i) z₀) (k : ℤ) : laurentCoeffAt (fun (z : ℂ) => ∑ i ∈ s, G i z) z₀ k = ∑ i ∈ s, laurentCoeffAt (G i) z₀ k

@[simp]

theorem RS.laurentCoeffAt_zpow_monomial {z₀ : ℂ} (m k : ℤ) : laurentCoeffAt (fun (z : ℂ) => (z - z₀) ^ m) z₀ k = if k = m then 1 else 0

theorem RS.laurentCoeffAt_zpow_mul {g : ℂ → ℂ} {z₀ : ℂ} (hg : MeromorphicAt g z₀) (m k : ℤ) : laurentCoeffAt (fun (z : ℂ) => (z - z₀) ^ m * g z) z₀ k = laurentCoeffAt g z₀ (k - m)

Multiplying by (· - z₀) ^ m shifts Laurent coefficients.

theorem RS.forall_neg_laurentCoeffAt_eq_zero_iff {f : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) : (∀ k < 0, laurentCoeffAt f z₀ k = 0) ↔ 0 ≤ meromorphicOrderAt f z₀

Vanishing principal tail ↔ analytic-after-repair (Mittag-Leffler-facing).