The residue functional (residue-calculus)

RS.resAt f z₀ is the (-1)-st Laurent coefficient of f at z₀ — the residue. Purely algebraic here; the circle-integral characterization is RS.circleIntegral_eq_two_pi_I_mul_resAt (IntegralBridge.lean).

Main exports:

• Inherited ℂ-linear algebra: RS.resAt_congr, RS.resAt_add/_fun_add/_const_mul/_neg/ _sub/_fun_sum;
• RS.resAt_of_analyticAt, RS.resAt_of_order_nonneg — vanishing off the pole locus;
• RS.resAt_zpow_monomial, RS.resAt_sub_inv — monomial residues;
• RS.MeromorphicAt.resAt_deriv — the residue of a derivative vanishes;
• RS.MeromorphicAt.resAt_deriv_div — the log-derivative residue is the order (argument principle atom);
• RS.resAt_tail_mul, RS.resAt_analyticAt_mul, RS.resAt_mul — Serre-pairing atoms (Miranda VI.3 Res_ω shape Σ c_n a_{−1−n}).

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

The residue of f at z₀: the (-1)-st Laurent coefficient. Purely algebraic; the circle-integral characterization is RS.circleIntegral_eq_two_pi_I_mul_resAt.

Equations

• RS.resAt f z₀ = RS.laurentCoeffAt f z₀ (-1)

theorem RS.resAt_congr {f g : ℂ → ℂ} {z₀ : ℂ} (hfg : f =ᶠ[nhdsWithin z₀ {z₀}ᶜ] g) : resAt f z₀ = resAt g z₀

theorem RS.resAt_fun_add {f g : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) (hg : MeromorphicAt g z₀) : resAt (fun (z : ℂ) => f z + g z) z₀ = resAt f z₀ + resAt g z₀

theorem RS.resAt_add {f g : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) (hg : MeromorphicAt g z₀) : resAt (f + g) z₀ = resAt f z₀ + resAt g z₀

theorem RS.resAt_const_mul {f : ℂ → ℂ} {z₀ : ℂ} (c : ℂ) : resAt (fun (z : ℂ) => c * f z) z₀ = c * resAt f z₀

theorem RS.resAt_neg {f : ℂ → ℂ} {z₀ : ℂ} : resAt (fun (z : ℂ) => -f z) z₀ = -resAt f z₀

theorem RS.resAt_sub {f g : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) (hg : MeromorphicAt g z₀) : resAt (fun (z : ℂ) => f z - g z) z₀ = resAt f z₀ - resAt g z₀

theorem RS.resAt_fun_sum {z₀ : ℂ} {ι : Type u_1} {s : Finset ι} {F : ι → ℂ → ℂ} (hF : ∀ i ∈ s, MeromorphicAt (F i) z₀) : resAt (fun (z : ℂ) => ∑ i ∈ s, F i z) z₀ = ∑ i ∈ s, resAt (F i) z₀

theorem RS.resAt_zero_fun {z₀ : ℂ} : resAt (fun (x : ℂ) => 0) z₀ = 0

@[simp]

theorem RS.resAt_of_analyticAt {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) : resAt f z₀ = 0

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

@[simp]

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

@[simp]

theorem RS.resAt_sub_inv {z₀ : ℂ} : resAt (fun (z : ℂ) => (z - z₀)⁻¹) z₀ = 1

theorem RS.deriv_sub_zpow (z₀ : ℂ) (m : ℤ) (z : ℂ) : deriv (fun (w : ℂ) => (w - z₀) ^ m) z = ↑m * (z - z₀) ^ (m - 1)

Derivative of a monomial factor, in closed form and UNCONDITIONALLY (no nonvanishing side condition needed — both sides are the mathlib deriv/zpow junk values, and they agree even at z = z₀). The workhorse for resAt_deriv.

theorem RS.MeromorphicAt.resAt_deriv {f : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) : resAt (deriv f) z₀ = 0

Residue of a derivative vanishes (Serre/Abel bookkeeping; the k ≤ -2 engine of change-of-variables).

theorem RS.MeromorphicAt.resAt_deriv_div {f : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) : resAt (fun (z : ℂ) => deriv f z / f z) z₀ = ↑(meromorphicOrderAt f z₀).untop₀

Log-derivative residue = order (THE argument-principle atom; meromorphic-trace input). Junk-robust: no order hypothesis (order ⊤ gives 0 = untop₀ ⊤).

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

Multiplying by (· - z₀) ^ m shifts the residue (special case of laurentCoeffAt_zpow_mul at k = -1).

theorem RS.resAt_tail_mul {g : ℂ → ℂ} {z₀ : ℂ} {c : ℤ → ℂ} {s : Finset ℤ} (hg : MeromorphicAt g z₀) : resAt (fun (z : ℂ) => (∑ k ∈ s, c k * (z - z₀) ^ k) * g z) z₀ = ∑ k ∈ s, c k * laurentCoeffAt g z₀ (-1 - k)

Serre-pairing atom, tail form (Miranda VI.3 eq. shape Σ c_n a_{−1−n}): residue of an explicit Laurent tail times a meromorphic germ.

theorem RS.resAt_analyticAt_mul_zpow {h : ℂ → ℂ} {z₀ : ℂ} (hh : AnalyticAt ℂ h z₀) (m : ℤ) : resAt (fun (z : ℂ) => h z * (z - z₀) ^ m) z₀ = if 0 ≤ -1 - m then taylorCoeffAt h z₀ (-1 - m).toNat else 0

Residue of h · (· - z₀) ^ m for h analytic: computed by a single Taylor coefficient of h (both cases — m ≤ -1 genuinely picks it out, m ≥ 0 gives an analytic product and 0, uniformly via the if).

theorem RS.resAt_analyticAt_mul {f h : ℂ → ℂ} {z₀ : ℂ} (hh : AnalyticAt ℂ h z₀) (hf : MeromorphicAt f z₀) {n : ℤ} (hn : ↑n ≤ meromorphicOrderAt f z₀) : resAt (fun (z : ℂ) => h z * f z) z₀ = ∑ k ∈ Finset.Icc n (-1), taylorCoeffAt h z₀ (-1 - k).toNat * laurentCoeffAt f z₀ k

Serre-pairing atom, analytic-multiplier form: residue of h·f through h's Taylor coefficients against f's principal Laurent coefficients (finite sum against the tail). n is any integer lower bound for the order that the consumer holds.

theorem RS.resAt_mul {f g : ℂ → ℂ} {z₀ : ℂ} (hf : MeromorphicAt f z₀) (hg : MeromorphicAt g z₀) {n m : ℤ} (hn : ↑n ≤ meromorphicOrderAt f z₀) (hm : ↑m ≤ meromorphicOrderAt g z₀) : resAt (fun (z : ℂ) => f z * g z) z₀ = ∑ k ∈ Finset.Icc n (-1 - m), laurentCoeffAt f z₀ k * laurentCoeffAt g z₀ (-1 - k)

General product formula (both meromorphic; subsumes the two above — provided because laurent-tails' μ_f operators multiply tails by meromorphic functions).