8.5. ResidueCalculus.FormTracePrincipalPart🔗

Jacobians.ResidueCalculus.FormTracePrincipalPart — source

negTail

The negative-power Laurent tail at a centre c: ∑_{k=1}^{N} b k · (z − c) ^ (−k : ℤ). This is the principal part of a meromorphic coefficient at a pole of order ≤ N — a polynomial in (z − c)⁻¹, the shape of a single centre's contribution to a LaurentForm.

noncomputable def negTail (c : ℂ) (b : ℕ → ℂ) (N : ℕ) : ℂ → ℂ

exists_analyticAt_taylor_step

Single-step Taylor division. For G analytic at c, there is an analytic G₁ at c with G z = G c + (z − c) • G₁ z for all z near c.

theorem exists_analyticAt_taylor_step {G : ℂ → ℂ} {c : ℂ} (hG : AnalyticAt ℂ G c) :
    ∃ G₁ : ℂ → ℂ, AnalyticAt ℂ G₁ c ∧ ∀ᶠ z in 𝓝 c, G z = G c + (z - c) • G₁ z

exists_analyticAt_taylorPoly

Iterated Taylor division (finite Taylor expansion with analytic remainder). For G analytic at c and any N : ℕ, there are coefficients a : ℕ → ℂ and an analytic remainder R with G z = (∑_{j<N} a j · (z − c)^j) + (z − c)^N • R z for all z near c. Proved by induction on N via exists_analyticAt_taylor_step (each step peels off one Taylor coefficient).

theorem exists_analyticAt_taylorPoly {G : ℂ → ℂ} {c : ℂ} (hG : AnalyticAt ℂ G c) (N : ℕ) :
    ∃ (a : ℕ → ℂ) (R : ℂ → ℂ), AnalyticAt ℂ R c ∧
      ∀ᶠ z in 𝓝 c, G z = (∑ j ∈ Finset.range N, a j * (z - c) ^ j) + (z - c) ^ N • R z

sum_taylorHead_eq_negTail

Reindexing the Taylor head into a negative-power tail. ∑_{j<N} a j · (z − c) ^ (j − N : ℤ) = negTail c (fun k => a (N − k)) N z.

theorem sum_taylorHead_eq_negTail (c : ℂ) (a : ℕ → ℂ) (N : ℕ) (z : ℂ) :
    (∑ j ∈ Finset.range N, a j * (z - c) ^ ((j : ℤ) - N))
      = negTail c (fun k => a (N - k)) N z

exists_principalPart_meromorphicAt

Single-point principal-part extraction. For a coefficient h that is MeromorphicAt c, there are a degree N : ℕ, principal-part coefficients b : ℕ → ℂ, and an analytic remainder R (AnalyticAt ℂ R c) such that on a punctured neighbourhood of c, h z = negTail c b N z + R z. (When h has no pole at c, N = 0 and negTail ≡ 0, so h simply agrees with the analytic R off c.) This is Miranda §VIII.3 step 2 at one centre — Mathlib has no principal-part API, so it is built from meromorphicOrderAt_eq_int_iff (the (z−c)^n • g factorisation) + the iterated Taylor division exists_analyticAt_taylorPoly.

theorem exists_principalPart_meromorphicAt {h : ℂ → ℂ} {c : ℂ} (hh : MeromorphicAt h c) :
    ∃ (N : ℕ) (b : ℕ → ℂ) (R : ℂ → ℂ), AnalyticAt ℂ R c ∧
      h =ᶠ[𝓝[≠] c] fun z => negTail c b N z + R z

analyticAt_negTail_of_ne

A negTail is analytic away from its centre. negTail c' b N is AnalyticAt c for c ≠ c' (its only singularity is the pole at c').

theorem analyticAt_negTail_of_ne {c c' : ℂ} (b : ℕ → ℂ) (N : ℕ) (hne : c ≠ c') :
    AnalyticAt ℂ (negTail c' b N) c