Cauchy's theorem on smooth convex Jordan domains

A function differentiable in a smooth convex Jordan carrier and continuous on its closure has zero boundary contour integral. A Poincaré primitive is available only in the open carrier, so the proof first integrates along strict inward homothetic copies of the boundary. Compact-uniform convergence of their integrands then transports the zero value to the original contour.

theorem contourIntegral_eq_zero_of_diffContOnCl_smoothJordan (Omega : SmoothJordanDomain) {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f Omega.carrier) : contourIntegral f Omega.boundaryParam = 0

A scalar function continuous on the closure of a smooth convex Jordan domain and complex differentiable in its carrier has zero boundary contour integral.