Equal-radius cap windows at crossings

Hungerbühler--Wasem Proposition 2.2 removes a small parameter interval about each crossing and joins its endpoints by a circular cap. The two endpoints must lie on the same circle about the crossed point: otherwise the cap does not join both of them. This file obtains those endpoints from the left and right first-exit times at a common spatial radius.

exitCapWindow packages the resulting interval and the branch-sensitive cap sweep from Crossing.CapAngle as a CircularCapWindow. Its characteristic API proves that the crossing is strictly inside the window, both endpoint chords have the prescribed norm, and the cap really joins the original curve. exitCapWindows applies the construction to the sorted members of a finite crossing set; crossings separated by more than twice the ambient half-width (2 * δ < |t - t'|) produce nonoverlapping, hence pairwise disjoint, cap windows.

This is the window construction and local analytic calculation in Proposition 2.2. exists_radius_hasCauchyPVAt_exitCapWindow evaluates the principal value on each generally asymmetric exit-time interval, and windingNumber_sub_cap_exitCapWindow_eq_crossingAngle_div_two_pi then identifies the local loop with its crossing angle.

Main definitions

• TauCeti.Contour.exitCapWindow -- the cap window determined by two first-exit times.
• TauCeti.Contour.exitCapWindows -- the corresponding list for a finite crossing set.

Main results

• TauCeti.Contour.cap_exitCapWindow_lower_eq and TauCeti.Contour.cap_exitCapWindow_upper_eq -- the cap joins the original curve at both endpoints.
• TauCeti.Contour.pairwise_disjoint_interval_exitCapWindows -- the finite windows are pairwise disjoint, in the shape Crossing.FiniteExcision consumes.
• TauCeti.Contour.exists_radius_hasCauchyPVAt_exitCapWindow -- sufficiently small exit-time windows have the boundary-argument principal value.
• TauCeti.Contour.windingNumber_sub_cap_exitCapWindow_eq_crossingAngle_div_two_pi -- the exact local angle contribution, once the principal value on the asymmetric exit-time window is supplied alongside the standing continuity, tangent, and radius hypotheses.

References

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

No external formalization is copied or adapted here. The construction composes Tau Ceti's first-exit-time, circular-cap, and crossing-angle APIs.

noncomputable def TauCeti.Contour.exitCapWindow (γ : ℝ → ℂ) (s : ℂ) (t₀ δ ε : ℝ) (L_R L_L : ℂ) : CircularCapWindow

The circular-cap window whose endpoints are the first exits from the radius-ε circle on the two sides of a crossing t₀. Those exits are searched in the ambient window [t₀ - δ, t₀ + δ], so δ is the ambient half-width. The endpoint bounds ε ≤ ‖γ (t₀ - δ) - s‖ and ε ≤ ‖γ (t₀ + δ) - s‖ certify that the defining sets are nonempty; without such witnesses, an empty defining set gives the corresponding junk value 0. The parameters L_R, L_L are the right- and left-hand tangent limits of γ at t₀, passed right before left as in crossingCapSweep; exchanging them selects a different cap. The cap starts in the direction of the left endpoint chord and sweeps by crossingCapSweep, the tangent-selected representative of the endpoint angle, which tends to -crossingAngle γ t₀ as the endpoints approach t₀ (tendsto_crossingCapSweep).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Contour.exitCapWindow_radius {γ : ℝ → ℂ} {s : ℂ} {t₀ δ ε : ℝ} {L_R L_L : ℂ} : (exitCapWindow γ s t₀ δ ε L_R L_L).radius = ε

The signed radius of an exit-time cap window is the prescribed spatial exit radius.

@[simp]

theorem TauCeti.Contour.exitCapWindow_lower {γ : ℝ → ℂ} {s : ℂ} {t₀ δ ε : ℝ} {L_R L_L : ℂ} : (exitCapWindow γ s t₀ δ ε L_R L_L).lower = firstExitTimeLeft γ t₀ δ s ε

The lower endpoint of an exit-time cap window is the left first-exit time.

@[simp]

theorem TauCeti.Contour.exitCapWindow_upper {γ : ℝ → ℂ} {s : ℂ} {t₀ δ ε : ℝ} {L_R L_L : ℂ} : (exitCapWindow γ s t₀ δ ε L_R L_L).upper = firstExitTimeRight γ t₀ δ s ε

The upper endpoint of an exit-time cap window is the right first-exit time.

@[simp]

theorem TauCeti.Contour.exitCapWindow_startAngle {γ : ℝ → ℂ} {s : ℂ} {t₀ δ ε : ℝ} {L_R L_L : ℂ} : (exitCapWindow γ s t₀ δ ε L_R L_L).startAngle = (γ (firstExitTimeLeft γ t₀ δ s ε) - s).arg

The cap starts at the argument of the left endpoint chord.

@[simp]

theorem TauCeti.Contour.exitCapWindow_endAngle {γ : ℝ → ℂ} {s : ℂ} {t₀ δ ε : ℝ} {L_R L_L : ℂ} : (exitCapWindow γ s t₀ δ ε L_R L_L).endAngle = (γ (firstExitTimeLeft γ t₀ δ s ε) - s).arg + crossingCapSweep γ t₀ L_R L_L (γ (firstExitTimeLeft γ t₀ δ s ε) - s) (γ (firstExitTimeRight γ t₀ δ s ε) - s)

The cap's terminal angle is its initial angle plus the branch-sensitive crossing sweep.

theorem TauCeti.Contour.exitCapWindow_lower_lt {γ : ℝ → ℂ} {s : ℂ} {t₀ δ ε : ℝ} {L_R L_L : ℂ} (hδ : 0 ≤ δ) (hε : 0 < ε) (h_at : γ t₀ = s) (hγ : ContinuousOn γ (Set.Icc (t₀ - δ) t₀)) (hεL : ε ≤ ‖γ (t₀ - δ) - s‖) : (exitCapWindow γ s t₀ δ ε L_R L_L).lower < t₀

The left exit time is strictly left of the crossing. If γ is continuous on the left half of the ambient window, passes through s at t₀, and the ambient left endpoint lies at distance at least ε > 0 from s, the window's lower endpoint is strictly below t₀.

theorem TauCeti.Contour.lt_exitCapWindow_upper {γ : ℝ → ℂ} {s : ℂ} {t₀ δ ε : ℝ} {L_R L_L : ℂ} (hδ : 0 ≤ δ) (hε : 0 < ε) (h_at : γ t₀ = s) (hγ : ContinuousOn γ (Set.Icc t₀ (t₀ + δ))) (hεR : ε ≤ ‖γ (t₀ + δ) - s‖) : t₀ < (exitCapWindow γ s t₀ δ ε L_R L_L).upper

The right exit time is strictly right of the crossing. The mirror image of exitCapWindow_lower_lt on the right half of the ambient window.

theorem TauCeti.Contour.norm_sub_exitCapWindow_lower_eq {γ : ℝ → ℂ} {s : ℂ} {t₀ δ ε : ℝ} {L_R L_L : ℂ} (hδ : 0 ≤ δ) (hε : 0 < ε) (h_at : γ t₀ = s) (hγ : ContinuousOn γ (Set.Icc (t₀ - δ) t₀)) (hεL : ε ≤ ‖γ (t₀ - δ) - s‖) : ‖γ (exitCapWindow γ s t₀ δ ε L_R L_L).lower - s‖ = ε

The left endpoint chord has the prescribed norm. At the left first-exit time the curve sits exactly on the circle of radius ε about s.

theorem TauCeti.Contour.norm_sub_exitCapWindow_upper_eq {γ : ℝ → ℂ} {s : ℂ} {t₀ δ ε : ℝ} {L_R L_L : ℂ} (hδ : 0 ≤ δ) (hε : 0 < ε) (h_at : γ t₀ = s) (hγ : ContinuousOn γ (Set.Icc t₀ (t₀ + δ))) (hεR : ε ≤ ‖γ (t₀ + δ) - s‖) : ‖γ (exitCapWindow γ s t₀ δ ε L_R L_L).upper - s‖ = ε

The right endpoint chord has the prescribed norm. The mirror image of norm_sub_exitCapWindow_lower_eq; together they put both endpoints on one circle about s.

theorem TauCeti.Contour.cap_exitCapWindow_eq_circleCap {γ : ℝ → ℂ} {s : ℂ} {t₀ δ ε : ℝ} {L_R L_L : ℂ} (hnorm : ‖γ (exitCapWindow γ s t₀ δ ε L_R L_L).lower - s‖ = ε) : (exitCapWindow γ s t₀ δ ε L_R L_L).cap s = circleCap s ‖γ (exitCapWindow γ s t₀ δ ε L_R L_L).lower - s‖ (exitCapWindow γ s t₀ δ ε L_R L_L).lower (exitCapWindow γ s t₀ δ ε L_R L_L).upper (γ (exitCapWindow γ s t₀ δ ε L_R L_L).lower - s).arg ((γ (exitCapWindow γ s t₀ δ ε L_R L_L).lower - s).arg + crossingCapSweep γ t₀ L_R L_L (γ (exitCapWindow γ s t₀ δ ε L_R L_L).lower - s) (γ (exitCapWindow γ s t₀ δ ε L_R L_L).upper - s))

The bundled cap of an exit-time window, spelled through the window's own endpoints: once the left endpoint chord has norm ε, it is the circular cap of that chord's radius sweeping from the chord's argument by crossingCapSweep.

theorem TauCeti.Contour.cap_exitCapWindow_lower_eq {γ : ℝ → ℂ} {s : ℂ} {t₀ δ ε : ℝ} {L_R L_L : ℂ} (hδ : 0 < δ) (hε : 0 < ε) (h_at : γ t₀ = s) (hγ : ContinuousOn γ (Set.Icc (t₀ - δ) t₀)) (hεL : ε ≤ ‖γ (t₀ - δ) - s‖) : (exitCapWindow γ s t₀ δ ε L_R L_L).cap s (exitCapWindow γ s t₀ δ ε L_R L_L).lower = γ (exitCapWindow γ s t₀ δ ε L_R L_L).lower

The cap meets the curve at the left endpoint. The cap starts in the direction of the left first-exit chord, so its initial value is γ at that exit time.

theorem TauCeti.Contour.cap_exitCapWindow_upper_eq {γ : ℝ → ℂ} {s : ℂ} {t₀ δ ε : ℝ} {L_R L_L : ℂ} (hδ : 0 < δ) (hε : 0 < ε) (h_at : γ t₀ = s) (hγ : ContinuousOn γ (Set.Icc (t₀ - δ) (t₀ + δ))) (hεL : ε ≤ ‖γ (t₀ - δ) - s‖) (hεR : ε ≤ ‖γ (t₀ + δ) - s‖) (hL_R : L_R ≠ 0) (hL_L : L_L ≠ 0) (h_R : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L_R)) (h_L : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L_L)) : (exitCapWindow γ s t₀ δ ε L_R L_L).cap s (exitCapWindow γ s t₀ δ ε L_R L_L).upper = γ (exitCapWindow γ s t₀ δ ε L_R L_L).upper

The cap meets the curve at the right endpoint. The companion of cap_exitCapWindow_lower_eq: the same cap ends at γ of the right first-exit time, so the excised curve is continuous at both ends of the window.

noncomputable def TauCeti.Contour.exitCapWindows (γ : ℝ → ℂ) (s : ℂ) (T : Finset ℝ) (δ ε : ℝ) (L_R L_L : ℝ → ℂ) : List CircularCapWindow

The finite list of equal-radius exit-time cap windows, ordered by their crossing parameters.

Equations

• TauCeti.Contour.exitCapWindows γ s T δ ε L_R L_L = List.map (fun (t : ℝ) => TauCeti.Contour.exitCapWindow γ s t δ ε (L_R t) (L_L t)) (T.sort fun (x1 x2 : ℝ) => x1 ≤ x2)

theorem TauCeti.Contour.sum_exitCapWindows {M : Type u_1} [AddCommMonoid M] (f : CircularCapWindow → M) (γ : ℝ → ℂ) (s : ℂ) (T : Finset ℝ) (δ ε : ℝ) (L_R L_L : ℝ → ℂ) : (List.map f (exitCapWindows γ s T δ ε L_R L_L)).sum = ∑ t ∈ T, f (exitCapWindow γ s t δ ε (L_R t) (L_L t))

Summing a function over the ordered exit-window list is the same as summing its value on the canonical window of each crossing.

@[simp]

theorem TauCeti.Contour.mem_exitCapWindows_iff {γ : ℝ → ℂ} {s : ℂ} {T : Finset ℝ} {δ ε : ℝ} {L_R L_L : ℝ → ℂ} {W : CircularCapWindow} : W ∈ exitCapWindows γ s T δ ε L_R L_L ↔ ∃ t ∈ T, W = exitCapWindow γ s t δ ε (L_R t) (L_L t)

Membership in exitCapWindows means being the exit-time window of a listed crossing.

theorem TauCeti.Contour.radius_eq_of_mem_exitCapWindows {γ : ℝ → ℂ} {s : ℂ} {T : Finset ℝ} {δ ε : ℝ} {L_R L_L : ℝ → ℂ} {W : CircularCapWindow} (hW : W ∈ exitCapWindows γ s T δ ε L_R L_L) : W.radius = ε

Every listed window carries the common spatial radius. Thus one result depending on ε can be applied uniformly across the family; simultaneous excision itself only requires each radius to be nonzero.

theorem TauCeti.Contour.lt_lower_of_mem_exitCapWindows {γ : ℝ → ℂ} {s : ℂ} {T : Finset ℝ} {a δ ε : ℝ} {L_R L_L : ℝ → ℂ} {W : CircularCapWindow} (hδ : 0 ≤ δ) (ha : ∀ t ∈ T, a < t - δ) (hεL : ∀ t ∈ T, ε ≤ ‖γ (t - δ) - s‖) (hW : W ∈ exitCapWindows γ s T δ ε L_R L_L) : a < W.lower

A listed window starts strictly after a when every ambient window does.

theorem TauCeti.Contour.upper_lt_of_mem_exitCapWindows {γ : ℝ → ℂ} {s : ℂ} {T : Finset ℝ} {b δ ε : ℝ} {L_R L_L : ℝ → ℂ} {W : CircularCapWindow} (hδ : 0 ≤ δ) (hb : ∀ t ∈ T, t + δ < b) (hεR : ∀ t ∈ T, ε ≤ ‖γ (t + δ) - s‖) (hW : W ∈ exitCapWindows γ s T δ ε L_R L_L) : W.upper < b

A listed window ends strictly before b when every ambient window does.

theorem TauCeti.Contour.lower_lt_upper_of_mem_exitCapWindows {γ : ℝ → ℂ} {s : ℂ} {T : Finset ℝ} {δ ε : ℝ} {L_R L_L : ℝ → ℂ} {W : CircularCapWindow} (hδ : 0 < δ) (hε : 0 < ε) (hγ : ∀ t ∈ T, ContinuousOn γ (Set.Icc (t - δ) (t + δ))) (h_at : ∀ t ∈ T, γ t = s) (hεL : ∀ t ∈ T, ε ≤ ‖γ (t - δ) - s‖) (hεR : ∀ t ∈ T, ε ≤ ‖γ (t + δ) - s‖) (hW : W ∈ exitCapWindows γ s T δ ε L_R L_L) : W.lower < W.upper

Between the crossing's own two exit times a listed window is nondegenerate.

theorem TauCeti.Contour.norm_sub_lower_eq_of_mem_exitCapWindows {γ : ℝ → ℂ} {s : ℂ} {T : Finset ℝ} {δ ε : ℝ} {L_R L_L : ℝ → ℂ} {W : CircularCapWindow} (hδ : 0 < δ) (hε : 0 < ε) (hγ : ∀ t ∈ T, ContinuousOn γ (Set.Icc (t - δ) t)) (h_at : ∀ t ∈ T, γ t = s) (hεL : ∀ t ∈ T, ε ≤ ‖γ (t - δ) - s‖) (hW : W ∈ exitCapWindows γ s T δ ε L_R L_L) : ‖γ W.lower - s‖ = ε

Every listed window's left endpoint chord has the common radius ε.

theorem TauCeti.Contour.norm_sub_upper_eq_of_mem_exitCapWindows {γ : ℝ → ℂ} {s : ℂ} {T : Finset ℝ} {δ ε : ℝ} {L_R L_L : ℝ → ℂ} {W : CircularCapWindow} (hδ : 0 < δ) (hε : 0 < ε) (hγ : ∀ t ∈ T, ContinuousOn γ (Set.Icc t (t + δ))) (h_at : ∀ t ∈ T, γ t = s) (hεR : ∀ t ∈ T, ε ≤ ‖γ (t + δ) - s‖) (hW : W ∈ exitCapWindows γ s T δ ε L_R L_L) : ‖γ W.upper - s‖ = ε

Every listed window's right endpoint chord has the common radius ε.

theorem TauCeti.Contour.eq_circleMap_startAngle_of_mem_exitCapWindows {γ : ℝ → ℂ} {s : ℂ} {T : Finset ℝ} {δ ε : ℝ} {L_R L_L : ℝ → ℂ} {W : CircularCapWindow} (hδ : 0 < δ) (hε : 0 < ε) (hγ : ∀ t ∈ T, ContinuousOn γ (Set.Icc (t - δ) t)) (h_at : ∀ t ∈ T, γ t = s) (hεL : ∀ t ∈ T, ε ≤ ‖γ (t - δ) - s‖) (hW : W ∈ exitCapWindows γ s T δ ε L_R L_L) : γ W.lower = circleMap s W.radius W.startAngle

The curve meets the cap's initial point at a listed window's lower endpoint, in the shape IsPiecewiseC1On.exciseCrossings consumes.

theorem TauCeti.Contour.eq_circleMap_endAngle_of_mem_exitCapWindows {γ : ℝ → ℂ} {s : ℂ} {T : Finset ℝ} {δ ε : ℝ} {L_R L_L : ℝ → ℂ} {W : CircularCapWindow} (hδ : 0 < δ) (hε : 0 < ε) (hγ : ∀ t ∈ T, ContinuousOn γ (Set.Icc (t - δ) (t + δ))) (h_at : ∀ t ∈ T, γ t = s) (hεL : ∀ t ∈ T, ε ≤ ‖γ (t - δ) - s‖) (hεR : ∀ t ∈ T, ε ≤ ‖γ (t + δ) - s‖) (hL_R : ∀ t ∈ T, L_R t ≠ 0) (hL_L : ∀ t ∈ T, L_L t ≠ 0) (h_R : ∀ t ∈ T, Filter.Tendsto (deriv γ) (nhdsWithin t (Set.Ioi t)) (nhds (L_R t))) (h_L : ∀ t ∈ T, Filter.Tendsto (deriv γ) (nhdsWithin t (Set.Iio t)) (nhds (L_L t))) (hW : W ∈ exitCapWindows γ s T δ ε L_R L_L) : γ W.upper = circleMap s W.radius W.endAngle

The curve meets the cap's terminal point at a listed window's upper endpoint, in the shape IsPiecewiseC1On.exciseCrossings consumes.

theorem TauCeti.Contour.pairwise_upper_lt_lower_exitCapWindows {γ : ℝ → ℂ} {s : ℂ} {T : Finset ℝ} {δ ε : ℝ} {L_R L_L : ℝ → ℂ} (hδ : 0 ≤ δ) (hεL : ∀ t ∈ T, ε ≤ ‖γ (t - δ) - s‖) (hεR : ∀ t ∈ T, ε ≤ ‖γ (t + δ) - s‖) (hsep : ∀ t ∈ T, ∀ t' ∈ T, t ≠ t' → 2 * δ < |t - t'|) : List.Pairwise (fun (W V : CircularCapWindow) => W.upper < V.lower) (exitCapWindows γ s T δ ε L_R L_L)

Exit-time cap windows inherit strict left-to-right ordering from separated symmetric windows.

theorem TauCeti.Contour.pairwise_disjoint_interval_exitCapWindows {γ : ℝ → ℂ} {s : ℂ} {T : Finset ℝ} {δ ε : ℝ} {L_R L_L : ℝ → ℂ} (hδ : 0 ≤ δ) (hεL : ∀ t ∈ T, ε ≤ ‖γ (t - δ) - s‖) (hεR : ∀ t ∈ T, ε ≤ ‖γ (t + δ) - s‖) (hsep : ∀ t ∈ T, ∀ t' ∈ T, t ≠ t' → 2 * δ < |t - t'|) : List.Pairwise (fun (W V : CircularCapWindow) => Disjoint W.interval V.interval) (exitCapWindows γ s T δ ε L_R L_L)

Strictly ordered exit-time cap windows are pairwise disjoint, the hypothesis shape of the simultaneous excision in Crossing.FiniteExcision.

theorem TauCeti.Contour.exists_common_exitCapWindows_radius {γ : ℝ → ℂ} {s : ℂ} {T : Finset ℝ} {δ : ℝ} {L_R L_L : ℝ → ℂ} (hδ : 0 < δ) (hγ : ∀ t ∈ T, ContinuousOn γ (Set.Icc (t - δ) (t + δ))) (h_at : ∀ t ∈ T, γ t = s) (hendpoint : ∀ t ∈ T, γ (t - δ) ≠ s ∧ γ (t + δ) ≠ s) : ∃ ε > 0, (∀ t ∈ T, ε ≤ ‖γ (t - δ) - s‖ ∧ ε ≤ ‖γ (t + δ) - s‖) ∧ ∀ t ∈ T, t ∈ Set.Ioo (exitCapWindow γ s t δ ε (L_R t) (L_L t)).lower (exitCapWindow γ s t δ ε (L_R t) (L_L t)).upper

A common spatial exit radius for a finite crossing family. If both ambient endpoints stay away from the crossed point, one positive radius works on both sides of every crossing. For this radius, continuity places every crossing strictly inside its generated exit-time window. The empty family is included.

theorem TauCeti.Contour.exists_radius_hasCauchyPVAt_exitCapWindow {γ : ℝ → ℂ} {s : ℂ} {a b t₀ : ℝ} (h_imm : IsPwC1ImmersionOn γ a b) (ht₀ : t₀ ∈ Set.Ioo a b) (h_at : γ t₀ = s) : ∃ R > 0, ∃ (L_R : ℂ) (L_L : ℂ), L_R ≠ 0 ∧ L_L ≠ 0 ∧ Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L_R) ∧ Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L_L) ∧ ∀ (δ : ℝ), 0 < δ → δ ≤ R → a < t₀ - δ → t₀ + δ ≤ b → (∀ t ∈ Set.Icc (t₀ - δ) (t₀ + δ), γ t = s → t = t₀) → ∀ (ε : ℝ), 0 < ε → ε ≤ ‖γ (t₀ - δ) - s‖ → ε ≤ ‖γ (t₀ + δ) - s‖ → HasCauchyPVAt γ (exitCapWindow γ s t₀ δ ε L_R L_L).lower (exitCapWindow γ s t₀ δ ε L_R L_L).upper (fun (z : ℂ) => (z - s)⁻¹) s (↑((-L_L / (γ (exitCapWindow γ s t₀ δ ε L_R L_L).lower - s)).arg + ((γ (exitCapWindow γ s t₀ δ ε L_R L_L).upper - s) / L_R).arg) * Complex.I)

The Cauchy principal value on an exit-time window. Around an interior crossing of a piecewise-C¹ immersion, there is an ambient radius R and nonzero one-sided tangent limits such that every smaller ambient window containing no other crossing has the following property. For each positive spatial exit radius reached on both sides, the Cauchy-kernel principal value on the generally asymmetric interval between the two first exits is

i * (arg (-L_L / (γ(lower) - s)) + arg ((γ(upper) - s) / L_R)).

The real logarithmic term vanishes because both exit chords have the same norm. This is the analytic input that windingNumber_sub_cap_exitCapWindow_eq_crossingAngle_div_two_pi consumes in Hungerbühler--Wasem Proposition 2.2.

theorem TauCeti.Contour.windingNumber_sub_cap_exitCapWindow_eq_crossingAngle_div_two_pi {γ : ℝ → ℂ} {s : ℂ} {t₀ δ ε : ℝ} {L_R L_L : ℂ} (hδ : 0 < δ) (hε : 0 < ε) (h_at : γ t₀ = s) (hγ : ContinuousOn γ (Set.Icc (t₀ - δ) (t₀ + δ))) (hεL : ε ≤ ‖γ (t₀ - δ) - s‖) (hεR : ε ≤ ‖γ (t₀ + δ) - s‖) (hL_R : L_R ≠ 0) (hL_L : L_L ≠ 0) (h_R : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L_R)) (h_L : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L_L)) (hpv : HasCauchyPVAt γ (exitCapWindow γ s t₀ δ ε L_R L_L).lower (exitCapWindow γ s t₀ δ ε L_R L_L).upper (fun (z : ℂ) => (z - s)⁻¹) s (↑((-L_L / (γ (exitCapWindow γ s t₀ δ ε L_R L_L).lower - s)).arg + ((γ (exitCapWindow γ s t₀ δ ε L_R L_L).upper - s) / L_R).arg) * Complex.I)) : windingNumber γ (exitCapWindow γ s t₀ δ ε L_R L_L).lower (exitCapWindow γ s t₀ δ ε L_R L_L).upper s - windingNumber ((exitCapWindow γ s t₀ δ ε L_R L_L).cap s) (exitCapWindow γ s t₀ δ ε L_R L_L).lower (exitCapWindow γ s t₀ δ ε L_R L_L).upper s = ↑(crossingAngle γ t₀) / (2 * ↑Real.pi)

The exact local angle contribution of one exit-time cap window. The winding number of the curve over the window minus that of its cap is crossingAngle γ t₀ / 2π. Beyond the standing continuity, tangent, and radius hypotheses -- which already give equal endpoint radii and endpoint matching -- the only extra input is the principal value of (z - s)⁻¹ along the generally asymmetric exit-time interval.