The crossing value of the real winding integrand for a twice-differentiable curve

Hungerbühler–Wasem Proposition 2.3 states that the real winding integrand of a plane curve Λ = x + i y about a point it passes through stays bounded: at a crossing parameter t̃ the apparently singular quotient (x ẏ - y ẋ) / (x² + y²) converges, with limit ½ k_Λ(t̃) |Λ̇(t̃)|, half the signed curvature times the speed.

Contour.tendsto_realWindingIntegrand_at_crossing already delivers that limit from two Peano expansions with abstract coefficients L (velocity) and A (acceleration). This file discharges those expansions from the differentiability of γ alone, and so states the crossing value in the explicit second-derivative form

(ẋ ÿ - ẏ ẍ) / (2 (ẋ² + ẏ²)), ẋ + i ẏ = γ' t₀, ẍ + i ÿ = γ'' t₀.

That explicit expression is ½ k_Λ(t₀) |Λ̇(t₀)|; the roadmap prescribes stating it this way because Mathlib carries no signed-curvature API for plane curves to cite, so there is no k_Λ to name. The regularity is pinned per part, as the roadmap asks: the crossing value needs the second derivative at t₀ (the C² half of Prop 2.3), whereas the boundedness that the residue theorem consumes needs only C^{1,1}.

Main results

• Contour.tendsto_realWindingIntegrand_at_crossing_of_hasDerivAt_deriv — the crossing value for a curve that is differentiable near t₀ and whose derivative is differentiable at t₀, stated with the acceleration A supplied by HasDerivAt (deriv γ) A t₀.
• Contour.tendsto_realWindingIntegrand_at_crossing_of_contDiffAt — the same limit under the roadmap's C² hypothesis, with the acceleration read off as deriv (deriv γ) t₀.
• Contour.tendsto_realWindingIntegrand_circleMap_crossing — the value ½ at every point of a circle, the smooth-crossing check (½ · |r|⁻¹ · |r|) of the formula above.

The second-order chord expansion behind the first result is obtained from Mathlib's mean-value engine Convex.isLittleO_pow_succ_real, the same lemma Mathlib's taylor_isLittleO runs on; it is proved here for the weaker "twice differentiable at t₀" hypothesis rather than assumed from C².

References

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

theorem TauCeti.Contour.tendsto_realWindingIntegrand_at_crossing_of_hasDerivAt_deriv {γ : ℝ → ℂ} {t₀ : ℝ} {A z₀ : ℂ} (hcross : γ t₀ = z₀) (hL : deriv γ t₀ ≠ 0) (hdiff : ∀ᶠ (t : ℝ) in nhds t₀, DifferentiableAt ℝ γ t) (hA : HasDerivAt (deriv γ) A t₀) : Filter.Tendsto (fun (t : ℝ) => realWindingIntegrand (γ t - z₀) (deriv γ t)) (nhdsWithin t₀ {t₀}ᶜ) (nhds (((deriv γ t₀).re * A.im - (deriv γ t₀).im * A.re) / (2 * ((deriv γ t₀).re ^ 2 + (deriv γ t₀).im ^ 2))))

Hungerbühler–Wasem Proposition 2.3, crossing value, in second-derivative form. Let γ be differentiable near t₀, with deriv γ differentiable at t₀ with derivative A, and let the velocity deriv γ t₀ be nonzero (the immersion condition). At the crossing γ t₀ = z₀ the real winding integrand converges,

(x ẏ - y ẋ) / (x² + y²) → (ẋ ÿ - ẏ ẍ) / (2 (ẋ² + ẏ²)),

with x + i y = γ - z₀, ẋ + i ẏ = deriv γ t₀ and ẍ + i ÿ = A. The limit is ½ k_γ(t₀) |γ̇(t₀)|, half the signed curvature times the speed, written out explicitly because Mathlib has no signed-curvature API to cite.

theorem TauCeti.Contour.tendsto_realWindingIntegrand_at_crossing_of_contDiffAt {γ : ℝ → ℂ} {t₀ : ℝ} {z₀ : ℂ} (hγ : ContDiffAt ℝ 2 γ t₀) (hcross : γ t₀ = z₀) (hL : deriv γ t₀ ≠ 0) : Filter.Tendsto (fun (t : ℝ) => realWindingIntegrand (γ t - z₀) (deriv γ t)) (nhdsWithin t₀ {t₀}ᶜ) (nhds (((deriv γ t₀).re * (deriv (deriv γ) t₀).im - (deriv γ t₀).im * (deriv (deriv γ) t₀).re) / (2 * ((deriv γ t₀).re ^ 2 + (deriv γ t₀).im ^ 2))))

Hungerbühler–Wasem Proposition 2.3, crossing value, under the roadmap's C² hypothesis. For a curve that is C² at the crossing parameter t₀ with nonvanishing velocity there, the real winding integrand about z₀ = γ t₀ tends to (ẋ ÿ - ẏ ẍ) / (2 (ẋ² + ẏ²)), where ẋ + i ẏ and ẍ + i ÿ are the first and second derivatives of γ at t₀.

theorem TauCeti.Contour.tendsto_realWindingIntegrand_circleMap_crossing {c : ℂ} {r : ℝ} (hr : r ≠ 0) (t₀ : ℝ) : Filter.Tendsto (fun (t : ℝ) => realWindingIntegrand (circleMap c r t - circleMap c r t₀) (deriv (circleMap c r) t)) (nhdsWithin t₀ {t₀}ᶜ) (nhds (1 / 2))

The smooth-crossing check. At every parameter of a circle of nonzero radius, the real winding integrand about the point of the circle reached there tends to ½: the circle has signed curvature |r|⁻¹ and circleMap c r has speed |r| (a negative r traverses the circle of radius |r| counterclockwise too, only from the antipodal parameter), so ½ k |Λ̇| = ½. This is the value the roadmap's smooth crossing (opening angle π) carries, computed from tendsto_realWindingIntegrand_at_crossing_of_contDiffAt rather than assumed.