Cauchy's theorem for null-homotopic contours

A closed piecewise-C¹ path continuously homotopic to its constant path inside an open set is null-homologous there. Consequently, the homology form of Cauchy's theorem makes the contour integral of every holomorphic function vanish along such a path. This supplies the null-homotopic special case explicitly requested in Layer 3 of the Contour Integration roadmap.

The homotopy is represented by Mathlib's Path.Homotopy; no differentiability of it is required. The source path itself is assumed piecewise C¹, matching the raw-curve interface expected by homologyCauchyTheorem.

Main results

• windingNumber_eq_zero_of_pathHomotopy_refl — a piecewise-C¹ loop continuously homotopic to its constant path through a point-avoiding homotopy has winding number zero about that point.
• isNullHomologous_of_pathHomotopy_refl — a piecewise-C¹ loop continuously contracted inside Ω is null-homologous in Ω.
• cauchyTheorem_of_pathHomotopy_refl — Cauchy's theorem for such a contractible contour.

Provenance

No formalization is vendored. The proof combines Tau Ceti's homotopy invariance of the winding number with its homology Cauchy theorem. The implication “null-homotopic implies null-homologous” and the resulting Cauchy theorem are standard; see S. Lang, Complex Analysis, Chapter VI, and L. Ahlfors, Complex Analysis, Chapter 4, as cited by the Contour Integration roadmap.

theorem TauCeti.Contour.windingNumber_eq_zero_of_pathHomotopy_refl {x w : ℂ} {p : Path x x} (hp : IsPiecewiseC1On (⇑p.extend) 0 1) (φ : p.Homotopy (Path.refl x)) (havoid : ∀ (st : ↑unitInterval × ↑unitInterval), φ st ≠ w) : windingNumber (⇑p.extend) 0 1 w = 0

A piecewise-C¹ loop continuously homotopic to its constant path through points avoiding w has winding number zero about w.

theorem TauCeti.Contour.isNullHomologous_of_pathHomotopy_refl {x : ℂ} {p : Path x x} {Ω : Set ℂ} (hp : IsPiecewiseC1On (⇑p.extend) 0 1) (φ : p.Homotopy (Path.refl x)) (hφΩ : ∀ (st : ↑unitInterval × ↑unitInterval), φ st ∈ Ω) : IsNullHomologous (⇑p.extend) 0 1 Ω

Null-homotopic implies null-homologous. If a piecewise-C¹ loop admits a continuous path homotopy to its constant path whose image lies in Ω, then its generalized winding number vanishes at every point outside Ω. Thus the loop is null-homologous in Ω.

This is one direction only: a null-homologous loop need not be null-homotopic.

theorem TauCeti.Contour.cauchyTheorem_of_pathHomotopy_refl {f : ℂ → ℂ} {Ω : Set ℂ} (hΩ : IsOpen Ω) {x : ℂ} (p : Path x x) (hp : IsPiecewiseC1On (⇑p.extend) 0 1) (φ : p.Homotopy (Path.refl x)) (hφΩ : ∀ (st : ↑unitInterval × ↑unitInterval), φ st ∈ Ω) (hf : DifferentiableOn ℂ f Ω) : ∫ (t : ℝ) in 0..1, deriv (⇑p.extend) t • f (p.extend t) = 0

Cauchy's theorem for a null-homotopic contour. Let p be a piecewise-C¹ loop admitting a continuous path homotopy to its constant path inside an open set Ω. If f is holomorphic on Ω, then the contour integral of f along p vanishes.

The path regularity is exactly what homologyCauchyTheorem expects; the homotopy supplies containment of the source path in Ω and its null-homology there.