Canonical Laurent data of a meromorphic function

For f meromorphic at s, this file extracts its canonical Laurent data: the polar order meromorphicPolarOrderAt — computed from meromorphicOrderAt, not chosen — together with Laurent coefficients, the finite polar part, and the analytic part, satisfying f = analytic part + ∑ k, coeff k / (z - s)^(k+1) near s. Because the tail length is the computable canonical order, downstream facts about it are provable (it is 1 at a simple pole) rather than opaque to a Classical.choose witness — which is what lets condition (A′) of the generalized residue theorem be discharged at simple poles by flatness of order one.

Main definitions

• Contour.meromorphicPolarOrderAt f s — the canonical polar order: the negative part of meromorphicOrderAt f s (0 at an analytic-or-removable point).
• Contour.meromorphicPolarCoeffAt hMero k — the k-th Laurent coefficient at s.
• Contour.meromorphicPolarPartAt hMero — the finite polar part ∑ k, coeff k / (z - s)^(k+1).
• Contour.meromorphicAnalyticPartAt hMero — the analytic part at s.

Main results

• Contour.exists_laurent_data_of_meromorphicAt — the Laurent decomposition with tail length pinned to the canonical order.
• Contour.eventuallyEq_meromorphicAnalyticPartAt_add_meromorphicPolarPartAt — f equals analytic part plus polar part near s.
• Contour.meromorphicPolarPartAt_eq_sum — the polar part as its explicit Laurent sum.
• Contour.meromorphicPolarCoeffAt_zero_eq_residue — the leading coefficient is the residue.
• Contour.meromorphicPolarOrderAt_eq_one — the canonical order at a simple pole is 1.
• Contour.laurent_coeff_unique, Contour.laurent_coeff_eq_meromorphicPolarCoeffAt — uniqueness of finite principal-part expansions: any Laurent witness of f at s has the canonical coefficients, compared through zero-padding.

Provenance

Migrated from the per-point Laurent-extraction block of HungerbuhlerWasem/LaurentExtraction.lean in the AINTLIB LeanModularForms development (meroPolarOrderAt through meroPolarCoeffAt_zero_eq_residue, here with meromorphic spelled out); the residue identification is by Contour.residue_of_laurent_expansion against the Taylor-coefficient residue. The coefficient-uniqueness block is new glue relative to the source: AINTLIB transfers condition (B)'s Laurent data through a dedicated constructor (ofMeromorphicWithCondB), while here uniqueness identifies any witness with the canonical coefficients. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

noncomputable def TauCeti.Contour.meromorphicPolarOrderAt (f : ℂ → ℂ) (s : ℂ) : ℕ

The canonical polar order of a meromorphic function at s: the negative part of meromorphicOrderAt f s. For a pole of order k this is k (in particular 1 at a simple pole, meromorphicPolarOrderAt_eq_one); at an analytic-or-removable point — including locally vanishing f — it is 0. Computed from f alone, so callers can evaluate it, unlike a Classical.choose-extracted tail length.

Equations

• TauCeti.Contour.meromorphicPolarOrderAt f s = (-(meromorphicOrderAt f s).untop₀).toNat

theorem TauCeti.Contour.meromorphicPolarOrderAt_eq_of_order_eq {f : ℂ → ℂ} {s : ℂ} {n : ℤ} (h : meromorphicOrderAt f s = ↑n) : meromorphicPolarOrderAt f s = (-n).toNat

The canonical polar order, computed from meromorphicOrderAt.

theorem TauCeti.Contour.meromorphicPolarOrderAt_eq_one {f : ℂ → ℂ} {s : ℂ} (h : meromorphicOrderAt f s = -1) : meromorphicPolarOrderAt f s = 1

At a simple pole the canonical polar order is 1. With flatness of order one (IsPwC1ImmersionOn.flatOfOrder_one), this discharges condition (A′) of the generalized residue theorem at simple poles.

theorem TauCeti.Contour.neg_meromorphicPolarOrderAt_le (f : ℂ → ℂ) (s : ℂ) : -↑↑(meromorphicPolarOrderAt f s) ≤ meromorphicOrderAt f s

The canonical polar order bounds the meromorphic order from below: -(meromorphicPolarOrderAt f s) ≤ meromorphicOrderAt f s. In particular, polar order 0 means the meromorphic order is nonnegative.

theorem TauCeti.Contour.meromorphicOrderAt_eq_neg_of_meromorphicPolarOrderAt_pos {f : ℂ → ℂ} {s : ℂ} (h_pos : 0 < meromorphicPolarOrderAt f s) : meromorphicOrderAt f s = -↑↑(meromorphicPolarOrderAt f s)

A positive canonical polar order pins the meromorphic order: meromorphicOrderAt f s = -(meromorphicPolarOrderAt f s) whenever the polar order is positive.

theorem TauCeti.Contour.meromorphicOrderAt_lt_neg_one_of_one_lt_meromorphicPolarOrderAt {f : ℂ → ℂ} {s : ℂ} (h : 1 < meromorphicPolarOrderAt f s) : meromorphicOrderAt f s < ↑(-1)

A pole of order > 1 in the canonical sense is a pole of order > 1 for meromorphicOrderAt — the guard of condition (B)'s clauses.

@[simp]

theorem TauCeti.Contour.meromorphicPolarOrderAt_le_one_iff {f : ℂ → ℂ} {s : ℂ} : meromorphicPolarOrderAt f s ≤ 1 ↔ ↑(-1) ≤ meromorphicOrderAt f s

The canonical polar order is at most one exactly when the meromorphic order is at least -1. This includes analytic and removable points (polar order zero) as well as genuine simple poles (polar order one).

theorem TauCeti.Contour.exists_laurent_data_of_meromorphicAt {f : ℂ → ℂ} {s : ℂ} (hMero : MeromorphicAt f s) : ∃ (a : Fin (meromorphicPolarOrderAt f s) → ℂ) (g : ℂ → ℂ), AnalyticAt ℂ g s ∧ ∀ᶠ (z : ℂ) in nhdsWithin s {s}ᶜ, f z = g z + ∑ k : Fin (meromorphicPolarOrderAt f s), a k / (z - s) ^ (↑k + 1)

Canonical Laurent data of a meromorphic function: near s, f = g + ∑ k, a k / (z - s)^(k+1) with g analytic at s, where the tail length is the canonical polar order meromorphicPolarOrderAt f s — pinned, not existentially chosen, so it is provable (1 at a simple pole).

noncomputable def TauCeti.Contour.meromorphicPolarCoeffAt {f : ℂ → ℂ} {s : ℂ} (hMero : MeromorphicAt f s) (k : Fin (meromorphicPolarOrderAt f s)) : ℂ

The k-th canonical Laurent coefficient of f at s.

Equations

• TauCeti.Contour.meromorphicPolarCoeffAt hMero k = ⋯.choose k

noncomputable def TauCeti.Contour.meromorphicPolarPartAt {f : ℂ → ℂ} {s : ℂ} (hMero : MeromorphicAt f s) (z : ℂ) : ℂ

The canonical finite polar part of f at s: the Laurent tail of length meromorphicPolarOrderAt f s.

Equations

• TauCeti.Contour.meromorphicPolarPartAt hMero z = ∑ k : Fin (TauCeti.Contour.meromorphicPolarOrderAt f s), TauCeti.Contour.meromorphicPolarCoeffAt hMero k / (z - s) ^ (↑k + 1)

noncomputable def TauCeti.Contour.meromorphicAnalyticPartAt {f : ℂ → ℂ} {s : ℂ} (hMero : MeromorphicAt f s) : ℂ → ℂ

The canonical analytic part of f at s.

Equations

• TauCeti.Contour.meromorphicAnalyticPartAt hMero = ⋯.choose

theorem TauCeti.Contour.meromorphicAnalyticPartAt_analyticAt {f : ℂ → ℂ} {s : ℂ} (hMero : MeromorphicAt f s) : AnalyticAt ℂ (meromorphicAnalyticPartAt hMero) s

The analytic part is analytic at s.

theorem TauCeti.Contour.eventuallyEq_meromorphicAnalyticPartAt_add_meromorphicPolarPartAt {f : ℂ → ℂ} {s : ℂ} (hMero : MeromorphicAt f s) : ∀ᶠ (z : ℂ) in nhdsWithin s {s}ᶜ, f z = meromorphicAnalyticPartAt hMero z + meromorphicPolarPartAt hMero z

The canonical Laurent decomposition: near s, f is the analytic part plus the polar part.

theorem TauCeti.Contour.meromorphicPolarPartAt_eq_sum {f : ℂ → ℂ} {s : ℂ} (hMero : MeromorphicAt f s) (z : ℂ) : meromorphicPolarPartAt hMero z = ∑ k : Fin (meromorphicPolarOrderAt f s), meromorphicPolarCoeffAt hMero k / (z - s) ^ (↑k + 1)

The polar part as its explicit Laurent sum — the characteristic unfolding of meromorphicPolarPartAt.

theorem TauCeti.Contour.meromorphicPolarPartAt_analyticAt_of_ne {f : ℂ → ℂ} {s : ℂ} (hMero : MeromorphicAt f s) {w : ℂ} (hw : w ≠ s) : AnalyticAt ℂ (meromorphicPolarPartAt hMero) w

The polar part is analytic away from its pole.

theorem TauCeti.Contour.meromorphicPolarCoeffAt_zero_eq_residue {f : ℂ → ℂ} {s : ℂ} (hMero : MeromorphicAt f s) (h_pos : 0 < meromorphicPolarOrderAt f s) : meromorphicPolarCoeffAt hMero ⟨0, h_pos⟩ = residue f s

The leading canonical Laurent coefficient is the residue.

Uniqueness of the Laurent coefficients

Any finite principal-part expansion of f at s with analytic remainder has the canonical coefficients: the sector condition (B) of the generalized residue theorem carries its own Laurent witness, and uniqueness is what lets its resonance constraints transfer to the canonical polar data. Internally the coefficients are total functions ℕ → ℂ summed over Finset.range, so expansions of different lengths compare after zero-padding.

theorem TauCeti.Contour.laurent_coeff_unique {s : ℂ} {N M : ℕ} {a : Fin N → ℂ} {b : Fin M → ℂ} {g h : ℂ → ℂ} (hg : ContinuousAt g s) (hh : ContinuousAt h s) (h_eq : ∀ᶠ (z : ℂ) in nhdsWithin s {s}ᶜ, g z + ∑ k : Fin N, a k / (z - s) ^ (↑k + 1) = h z + ∑ k : Fin M, b k / (z - s) ^ (↑k + 1)) (k : ℕ) : (if hk : k < N then a ⟨k, hk⟩ else 0) = if hk : k < M then b ⟨k, hk⟩ else 0

Uniqueness of finite principal-part expansions: two expansions of the same function near s with remainders continuous at s have the same coefficients, compared through their zero-paddings.

theorem TauCeti.Contour.laurent_coeff_eq_meromorphicPolarCoeffAt {f : ℂ → ℂ} {s : ℂ} (hMero : MeromorphicAt f s) {N : ℕ} {a : Fin N → ℂ} {g : ℂ → ℂ} (hg : ContinuousAt g s) (h_eq : ∀ᶠ (z : ℂ) in nhdsWithin s {s}ᶜ, f z = g z + ∑ k : Fin N, a k / (z - s) ^ (↑k + 1)) (k : ℕ) : (if hk : k < N then a ⟨k, hk⟩ else 0) = if hk : k < meromorphicPolarOrderAt f s then meromorphicPolarCoeffAt hMero ⟨k, hk⟩ else 0

Any Laurent witness has the canonical coefficients: an eventual finite principal-part expansion of a meromorphic f at s with remainder continuous at s agrees, coefficient by coefficient through zero-padding, with the canonical polar data. This is what transfers the sector condition (B)'s resonance constraints from its own Laurent witness to meromorphicPolarCoeffAt.