Boundedness of the real winding integrand at C^{1,1} crossings

Winding/BoundedIntegrand.lean proves the real winding integrand stays bounded near a crossing where the curve is C². This file weakens that regularity to merely C^{1,1} on each side of the crossing: derivWithin γ (Icc c d) Lipschitz on a one-sided closed piece [c, d] ending or starting at the crossing, with no second derivative -- pointwise or almost everywhere -- assumed to exist anywhere, and no assumption that the two sides agree. This covers a crossing that coincides with a breakpoint of a piecewise-C¹ immersion (a corner, where the two one-sided tangents may differ), not just a crossing where γ is genuinely differentiable on a full two-sided neighborhood. This is a genuinely different proof technique from the C² case, not a weakening of it: the C² proof reads the bounded limit off an explicit curvature value at the crossing (which needs a second derivative there); this file instead bounds the integrand directly from the quadratic remainder a Lipschitz derivative forces on the curve itself, via the mean value inequality applied to the affine remainder on the segment from the crossing to each nearby parameter -- entirely on one side at a time, so the two sides never need to interact. Only plain differentiability of γ is assumed (not continuity of its derivative): Lipschitz-ness of derivWithin γ (Icc c d) already gives that for free.

Main results

• TauCeti.Contour.exists_isBounded_image_realWindingIntegrand_of_lipschitzOnWith_derivWithin_right and ..._left -- the real winding integrand is bounded on a small enough one-sided window, starting (resp. ending) at a crossing where derivWithin γ is Lipschitz and non-zero there, on the one-sided piece the window lies in.
• ..._corner -- the two one-sided windows above combined into one full neighborhood of the crossing, allowing the two sides to disagree.

References

• N. Hungerbühler and M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997 (2018), Proposition 2.3 and its proof (which handles a crossing at a corner via exactly this one-sided splitting, p. 9).

theorem TauCeti.Contour.exists_isBounded_image_realWindingIntegrand_of_lipschitzOnWith_derivWithin_right {γ : ℝ → ℂ} {w : ℂ} {t₀ d : ℝ} {K : NNReal} (htd : t₀ < d) (hdiff : DifferentiableOn ℝ γ (Set.Icc t₀ d)) (hlip : LipschitzOnWith K (derivWithin γ (Set.Icc t₀ d)) (Set.Icc t₀ d)) (h_eq : γ t₀ = w) (hvel : derivWithin γ (Set.Icc t₀ d) t₀ ≠ 0) : ∃ ρ > 0, ρ < d - t₀ ∧ Bornology.IsBounded ((fun (t : ℝ) => realWindingIntegrand (γ t - w) (deriv γ t)) '' Set.Icc t₀ (t₀ + ρ))

Boundedness of the real winding integrand at a C^{1,1} crossing, from the right. If γ is differentiable on [t₀, d] and derivWithin γ (Icc t₀ d) is K-Lipschitz there and non-zero at t₀, where γ t₀ = w, then the real winding integrand (the ordinary derivative, which agrees with the within-piece one strictly inside [t₀, d]) is bounded on a small enough right-window [t₀, t₀ + ρ] -- no second derivative, pointwise or almost everywhere, is assumed to exist anywhere, and no assumption is made about γ to the left of t₀. At t₀ itself deriv γ t₀ may take any junk value (it need not equal the one-sided derivWithin): the integrand there is realWindingIntegrand 0 _, independent of the velocity argument, so the junk value is harmless. This is the corner case of Winding/BoundedIntegrand.lean's smooth-crossing result: t₀ may coincide with a breakpoint of a piecewise-C¹ immersion, where the left tangent may disagree with this one.

theorem TauCeti.Contour.exists_isBounded_image_realWindingIntegrand_of_lipschitzOnWith_derivWithin_left {γ : ℝ → ℂ} {w : ℂ} {c t₀ : ℝ} {K : NNReal} (hct : c < t₀) (hdiff : DifferentiableOn ℝ γ (Set.Icc c t₀)) (hlip : LipschitzOnWith K (derivWithin γ (Set.Icc c t₀)) (Set.Icc c t₀)) (h_eq : γ t₀ = w) (hvel : derivWithin γ (Set.Icc c t₀) t₀ ≠ 0) : ∃ ρ > 0, ρ < t₀ - c ∧ Bornology.IsBounded ((fun (t : ℝ) => realWindingIntegrand (γ t - w) (deriv γ t)) '' Set.Icc (t₀ - ρ) t₀)

Boundedness of the real winding integrand at a C^{1,1} crossing, from the left. If γ is differentiable on [c, t₀] and derivWithin γ (Icc c t₀) is K-Lipschitz there and non-zero at t₀, where γ t₀ = w, then the real winding integrand (the ordinary derivative, which agrees with the within-piece one strictly inside [c, t₀]) is bounded on a small enough left-window [t₀ - ρ, t₀] -- no second derivative, pointwise or almost everywhere, is assumed to exist anywhere, and no assumption is made about γ to the right of t₀. As in _right, deriv γ t₀'s junk value at the crossing itself is harmless: the integrand there is realWindingIntegrand 0 _, independent of the velocity argument. The mirror case of _right above.

theorem TauCeti.Contour.exists_isBounded_image_realWindingIntegrand_of_lipschitzOnWith_derivWithin_corner {γ : ℝ → ℂ} {w : ℂ} {c t₀ d : ℝ} {KR KL : NNReal} (hct : c < t₀) (htd : t₀ < d) (hdiffR : DifferentiableOn ℝ γ (Set.Icc t₀ d)) (hlipR : LipschitzOnWith KR (derivWithin γ (Set.Icc t₀ d)) (Set.Icc t₀ d)) (hdiffL : DifferentiableOn ℝ γ (Set.Icc c t₀)) (hlipL : LipschitzOnWith KL (derivWithin γ (Set.Icc c t₀)) (Set.Icc c t₀)) (h_eq : γ t₀ = w) (hvelR : derivWithin γ (Set.Icc t₀ d) t₀ ≠ 0) (hvelL : derivWithin γ (Set.Icc c t₀) t₀ ≠ 0) : ∃ ρ > 0, ρ < min (d - t₀) (t₀ - c) ∧ Bornology.IsBounded ((fun (t : ℝ) => realWindingIntegrand (γ t - w) (deriv γ t)) '' Set.Icc (t₀ - ρ) (t₀ + ρ))

Boundedness of the real winding integrand on the full neighborhood of a C^{1,1} corner crossing. Combines _right and _left above into the full two-sided window [t₀ - ρ, t₀ + ρ], allowing the two sides to have genuinely different pieces and Lipschitz constants, as at a corner where the one-sided tangents themselves may differ.