The real winding integrand at a crossing

This file proves the local crossing-value calculation in Hungerbühler–Wasem Proposition 2.3. For a plane curve γ passing through s at t₀ whose chord and velocity have the stated filter expansions, the apparently singular real winding integrand

(x ẏ - y ẋ) / (x² + y²), where x + iy = γ - s,

tends to (L.re * A.im - L.im * A.re) / (2 * ‖L‖²), where L and A are the coefficients in those expansions.

The theorem is stated using two Peano expansions, independently of any particular second-derivative API.

As prescribed by the contour integration roadmap, the answer is given by an explicit coordinate formula.

Main results

• Contour.tendsto_realWindingIntegrand_at_crossing gives the crossing value for a curve.

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.tendsto_realWindingIntegrand_at_crossing {α : Type u_1} {l : Filter α} {t : α → ℝ} {t₀ : ℝ} {γ : ℝ → ℂ} {s L A : ℂ} (hL : L ≠ 0) (htend : Filter.Tendsto t l (nhds t₀)) (hcross : γ t₀ = s) (hpos₂ : Filter.Tendsto (fun (i : α) => ((γ (t i) - s) / ↑(t i - t₀) - L) / ↑(t i - t₀)) l (nhds (A / 2))) (hvel : Filter.Tendsto (fun (i : α) => (deriv γ (t i) - L) / ↑(t i - t₀)) l (nhds A)) (ht : ∀ᶠ (i : α) in l, t i ≠ t₀) : Filter.Tendsto (fun (i : α) => realWindingIntegrand (γ (t i) - s) (deriv γ (t i))) l (nhds ((L.re * A.im - L.im * A.re) / (2 * Complex.normSq L)))

Hungerbühler–Wasem Proposition 2.3, crossing value. At a crossing γ t₀ = s, a normalized second-order chord expansion with coefficients L and A, together with the matching first-order velocity expansion, implies

(x ẏ - y ẋ) / (x² + y²) → (L.re * A.im - L.im * A.re) / (2 * ‖L‖²).

The conclusion refers only to the coefficients in the assumed filter expansions.