Bridge: Project residueAt and Mathlib MeromorphicAt

As of Mathlib v4.29, there is no MeromorphicAt.residue definition in Mathlib. Mathlib provides:

• MeromorphicAt f z₀ -- existence of a meromorphic decomposition
• meromorphicOrderAt f z₀ -- the order (pole/zero multiplicity) as WithTop ℤ
• meromorphicOrderAt_eq_int_iff -- factorization: f =ᶠ (z - z₀)^n • g with g analytic, g(z₀) ≠ 0

This file bridges the project's residue definitions to Mathlib's meromorphic API:

Main Results

• residueAt_eq_zero_of_analyticAt -- residueAt f z₀ = 0 when f is analytic at z₀
• residueSimplePole_eq_zero_of_nonneg_order -- residueSimplePole f z₀ = 0 when the order is non-negative

For higher-order poles, the project's residueAt_eq_laurent_head_coeff (in FlatnessTransfer/PerTermVanishing.lean) provides the general connection to the a₋₁ Laurent coefficient.

Analytic / non-negative order bridge

theorem GeneralizedResidueTheory.residueAt_eq_zero_of_analyticAt (f : ℂ → ℂ) (z₀ : ℂ) (hf : AnalyticAt ℂ f z₀) : residueAt f z₀ = 0

If f is analytic at z₀, then residueAt f z₀ = 0. The contour integral of an analytic function on a small circle vanishes by Cauchy's theorem.

theorem GeneralizedResidueTheory.residueSimplePole_eq_zero_of_nonneg_order (f : ℂ → ℂ) (z₀ : ℂ) (hf : MeromorphicAt f z₀) (hord : 0 ≤ meromorphicOrderAt f z₀) : residueSimplePole f z₀ = 0

If f is meromorphic at z₀ with non-negative order (i.e., analytic or removable singularity), then residueSimplePole f z₀ = 0.