Null-Homologous Curves: Definitions and Convexity Bridge

A closed piecewise C^1 immersion is null-homologous in an open set U when its winding number around every point outside U is zero. This is the topological condition required by the generalized residue theorem of Hungerbuhler-Wasem.

Main definitions

• IsNullHomologous -- null-homologous curve in an open set

Main results

• ftc_piecewise_contour -- FTC for piecewise C¹ contours
• integrand_intervalIntegrable_of_avoids -- integrability of winding integrand
• isNullHomologous_of_convex -- every closed curve in a convex open set is null-homologous (bridge lemma)

structure IsNullHomologous (γ : PiecewiseC1Immersion) (U : Set ℂ) : Prop

A closed piecewise C^1 immersion gamma is null-homologous in an open set U if:

1. gamma is a closed curve
2. gamma lies entirely in U
3. The winding number of gamma around every point outside U is zero.

This matches the definition in Hungerbuhler-Wasem (arXiv:1808.00997v2).

• closed : γ.IsClosed
• image_subset (t : ℝ) : t ∈ Set.Icc γ.a γ.b → γ.toFun t ∈ U
• winding_zero (z : ℂ) : z ∉ U → generalizedWindingNumber' γ.toFun γ.a γ.b z = 0

theorem ftc_piecewise_contour_induction {F f : ℂ → ℂ} (γ : PiecewiseC1Curve) (n : ℕ) (a' b' : ℝ) (h_int : IntervalIntegrable (fun (t : ℝ) => f (γ.toFun t) * deriv γ.toFun t) MeasureTheory.volume γ.a γ.b) (hFγ_cont : ContinuousOn (F ∘ γ.toFun) (Set.Icc γ.a γ.b)) (hFγ_deriv_off : ∀ t ∈ Set.Ioo γ.a γ.b, t ∉ ↑γ.partition → HasDerivAt (F ∘ γ.toFun) (f (γ.toFun t) * deriv γ.toFun t) t) (hcard : {t ∈ γ.partition | a' < t ∧ t < b'}.card ≤ n) (ha'b' : a' ≤ b') (hsub : Set.Icc a' b' ⊆ Set.Icc γ.a γ.b) (ha'P : a' ∈ γ.partition) (hb'P : b' ∈ γ.partition) : ∫ (t : ℝ) in a'..b', f (γ.toFun t) * deriv γ.toFun t = F (γ.toFun b') - F (γ.toFun a')

FTC for piecewise C¹ contours (induction on partition points): on any sub-interval [a', b'] whose endpoints belong to the partition and that contains at most n interior partition points, the integral of f(γ(t)) · γ'(t) equals F(γ(b')) - F(γ(a')), provided F ∘ γ is continuous, its derivative equals the integrand off the partition, and the integrand is interval-integrable.

theorem ftc_piecewise_contour {F f : ℂ → ℂ} (γ : PiecewiseC1Curve) (U : Set ℂ) (hγ_in_U : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ U) (hF_prim : ∀ z ∈ U, HasDerivAt F (f z) z) (h_int : IntervalIntegrable (fun (t : ℝ) => f (γ.toFun t) * deriv γ.toFun t) MeasureTheory.volume γ.a γ.b) : ∫ (t : ℝ) in γ.a..γ.b, f (γ.toFun t) * deriv γ.toFun t = F (γ.toFun γ.b) - F (γ.toFun γ.a)

Fundamental theorem of calculus for piecewise C¹ contours: if F is a primitive of f on U (i.e. HasDerivAt F (f z) z for every z ∈ U) and γ is a piecewise C¹ curve lying in U, then ∫_γ f(z) dz = F(γ(b)) - F(γ(a)).

theorem integrand_intervalIntegrable_of_avoids (γ : PiecewiseC1Immersion) (z : ℂ) (h_avoids : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ z) : IntervalIntegrable (fun (t : ℝ) => (γ.toFun t - z)⁻¹ * deriv γ.toFun t) MeasureTheory.volume γ.a γ.b

The integrand (γ(t) - z)⁻¹ · γ'(t) is interval-integrable whenever z is not in the image of γ. The proof uses compactness of [a, b] to bound ‖(γ(t) - z)⁻¹‖ and the piecewise C¹ bound on ‖γ'(t)‖.

theorem isNullHomologous_of_convex (U : Set ℂ) (hU : IsOpen U) (hU_convex : Convex ℝ U) (hU_ne : U.Nonempty) (γ : PiecewiseC1Immersion) (hγ_closed : γ.IsClosed) (hγ_in_U : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ U) : IsNullHomologous γ U

Every closed curve in a convex open set is null-homologous.

The proof uses:

1. generalizedWindingNumber_eq_classical_away to reduce the PV winding number to a classical contour integral (since z is not on the curve).
2. holomorphic_convex_primitive to obtain a primitive F of w |-> (w - z)^{-1} on the convex set U.
3. The fundamental theorem of calculus to evaluate the integral as F(gamma(b)) - F(gamma(a)) = 0 (since gamma is closed).