Change of variables for residues (residue-calculus)

RS.resAt_comp_mul_deriv — chart invariance: for a local analytic isomorphism φ at w₀ with φ w₀ = z₀, the residue of the pulled-back 1-form integrand (f ∘ φ) · φ' at w₀ equals the residue of f at z₀. This is what makes Res_p(ω) on a Riemann surface chart-independent (residue-theorem unit). Purely algebraic (route (a) of the design doc): no contour integration.

Main export: RS.resAt_comp_mul_deriv, and the =ᶠ-robust corollary RS.resAt_comp_mul_deriv_of_eventuallyEq.

theorem RS.resAt_comp_mul_deriv {f : ℂ → ℂ} {z₀ w₀ : ℂ} {φ : ℂ → ℂ} (hφ : AnalyticAt ℂ φ w₀) (hφ' : deriv φ w₀ ≠ 0) (hφ₀ : φ w₀ = z₀) (hf : MeromorphicAt f z₀) : resAt (fun (w : ℂ) => f (φ w) * deriv φ w) w₀ = resAt f z₀

Chart invariance of the residue of a 1-form integrand (Forster 9.9-flavored): for a local analytic isomorphism φ at w₀ with φ w₀ = z₀, the residue of (f ∘ φ)·φ' at w₀ equals the residue of f at z₀. Makes Res_p(ω) on a surface chart-independent (residue-theorem unit).

theorem RS.resAt_comp_mul_deriv_of_eventuallyEq {f : ℂ → ℂ} {z₀ w₀ : ℂ} {φ : ℂ → ℂ} (hφ : AnalyticAt ℂ φ w₀) (hφ' : deriv φ w₀ ≠ 0) (hφ₀ : φ w₀ = z₀) (hf : MeromorphicAt f z₀) {F : ℂ → ℂ} (hF : F =ᶠ[nhdsWithin w₀ {w₀}ᶜ] fun (w : ℂ) => f (φ w) * deriv φ w) : resAt F w₀ = resAt f z₀

Corollary (residue-theorem convenience): the chart-invariance identity survives replacing the integrand by anything =ᶠ[𝓝[≠] w₀]-equal to it.