The homology Cauchy theorem for contour cycles

This file extends the homology form of Cauchy's theorem from one parametrized closed curve to a finite formal integer cycle. If a cycle C lies in an open set U, is null-homologous there, and f is holomorphic on U, then Cycle.integral f C = 0.

The point is that null-homology belongs to the whole cycle: cancellation between different generators may make C null-homologous even when no individual generator is. Thus the result does not follow by applying the single-curve theorem termwise. Instead, Dixon's two auxiliary integrals are summed over the finite support of C. Their jump across the boundary of U is the winding number of the whole cycle, so cycle-level null-homology makes the sum entire; decay at infinity and Liouville then make it zero.

Main result

• TauCeti.Contour.Cycle.homologyCauchyTheorem — Cauchy's theorem for a null-homologous cycle.

References

• J. D. Dixon, A brief proof of Cauchy's integral theorem, Proc. Amer. Math. Soc. 29 (1971).
• N. Hungerbühler and M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997 (2018), Section 2.

Provenance

No formal implementation is vendored. The proof extends the repository's single-curve Dixon development to the cycle type by finite additivity.

theorem TauCeti.Contour.Cycle.homologyCauchyTheorem {f : ℂ → ℂ} {C : Cycle} {U : Set ℂ} (hU : IsOpen U) (hCU : C.IsIn U) (hf : DifferentiableOn ℂ f U) (hnull : C.IsNullHomologous U) : (integral f) C = 0

The homology Cauchy theorem for contour cycles. Let C be a finite formal integer combination of closed piecewise-C¹ curves whose trace lies in an open set U. If C is null-homologous in U and f is holomorphic on U, then the contour integral of f over the whole cycle vanishes.

The null-homology assumption is imposed only on C, not on each supported curve, so the theorem includes cancellations between different generators.