12.4. MeromorphicTrace.MeromorphicTrace🔗

Jacobians.MeromorphicTrace.MeromorphicTrace — source

resAt_inv_sub_mul

Cauchy's integral formula, residue form. For h analytic at a, the residue of the simple pole z ↦ (z − a)⁻¹ · h z at a is h a.

theorem resAt_inv_sub_mul {h : ℂ → ℂ} {a : ℂ} (hh : AnalyticAt ℂ h a) :
    resAt (fun z => (z - a)⁻¹ * h z) a = h a

resAt_mul_inv_sub

Variant with the numerator on the left: Res_a (h(z) · (z − a)⁻¹) = h a.

theorem resAt_mul_inv_sub {h : ℂ → ℂ} {a : ℂ} (hh : AnalyticAt ℂ h a) :
    resAt (fun z => h z * (z - a)⁻¹) a = h a

FibreTrace

A finite fibre of an (unramified) cover over a base point of target-chart coordinate b, with the per-sheet holomorphic sections and meromorphic form coefficients. The data of Miranda's local picture for the trace Tr_F over b (off the branch locus).

structure FibreTrace where