Boundedness of the real winding integrand at crossings

For a plane curve γ that is C¹ everywhere, and is C² with nonzero velocity where it meets a point w, the real winding integrand

realWindingIntegrand (γ t - w) (deriv γ t)

is bounded on every compact parameter set, even when γ passes through w. This is the smooth case of the bounded-integrand assertion in Hungerbühler--Wasem Proposition 2.3. At a crossing the displayed function is defined to be zero, while its punctured limit is half the signed curvature times speed. The proof fills in the crossing values by those finite limits, obtains a continuous auxiliary function, and then uses compactness.

The full proposition only needs C^{1,1} regularity. The result here is the direct compact-set companion to the existing pointwise C² crossing-value theorem; weakening the crossing regularity requires the corresponding almost-everywhere second-order crossing analysis.

As in the crossing-value modules, the value is written using the explicit coordinate formula because Mathlib has no signed-curvature API for plane curves.

Main result

• TauCeti.Contour.isBounded_image_realWindingIntegrand -- the real winding integrand of a C¹ curve that is C² with nonzero velocity at crossings has bounded image on a compact parameter set.

References

• N. Hungerbühler and M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997 (2018), Proposition 2.3.

theorem TauCeti.Contour.isBounded_image_realWindingIntegrand {γ : ℝ → ℂ} {w : ℂ} {K : Set ℝ} (hK : IsCompact K) (hγ1 : ∀ t ∈ K, ContDiffAt ℝ 1 γ t) (hγ2 : ∀ t ∈ K, γ t = w → ContDiffAt ℝ 2 γ t) (hvel : ∀ t ∈ K, γ t = w → deriv γ t ≠ 0) : Bornology.IsBounded ((fun (t : ℝ) => realWindingIntegrand (γ t - w) (deriv γ t)) '' K)

Hungerbühler--Wasem Proposition 2.3, bounded-integrand assertion with C² crossings. Let γ be pointwise C¹, and be pointwise C² with nonzero velocity where it meets w, on a compact parameter set K. Then the image of

t ↦ realWindingIntegrand (γ t - w) (deriv γ t)

on K is bounded. No avoidance hypothesis is imposed: at parameters where γ t = w, the real integrand is defined to be zero, and near each such parameter its finite punctured limit is the explicit half-curvature-times-speed value from tendsto_realWindingIntegrand_at_crossing_of_contDiffAt.