Window splitting of the truncated integral at a crossing

At a transverse crossing γ t₀ = s — non-zero one-sided derivative limits, unique crossing on the window [l, u] with l < t₀ < u — there are exit-time functions τL, τR converging to t₀ from each side with exit radius exactly ε, such that for every integrand g with integrable ε-truncation the truncated integral over the window eventually splits into the two plain side integrals:

∫ l..u, truncated = ∫ l..(τL ε), g (γ v) γ'(v) + ∫ (τR ε)..u, g (γ v) γ'(v).

The middle piece [τL ε, τR ε] is annihilated — there the curve is inside the ε-ball, by strict monotonicity of the distance profile up to the exit times — and on the side pieces the truncation is inactive, by monotonicity inside the monotone radius and the positive window distance bound beyond it.

The truncated integrand if ‖γ t - s‖ > ε then g (γ t) * deriv γ t else 0 is the integrand of Contour.HasCauchyPVAt, so this is the per-window skeleton of the principal-value evaluation: consumers add the per-side fundamental-theorem evaluation and the limit of the exit-time terms.

Main results

• Contour.exists_exit_times_truncated_integral_split — the shared window-splitting core.

Provenance

Migrated from perCrossing_window_splitting of LocalCutoffs.lean in the AINTLIB LeanModularForms development, restated for a raw curve with the analytic inputs (one-sided derivative limits, eventual differentiability, continuity on the window) as hypotheses in place of the bundled ClosedPwC1Immersion, and the integrability hypothesis quantified over the window rather than [0, 1]. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

theorem TauCeti.Contour.exists_exit_times_truncated_integral_split {γ : ℝ → ℂ} {s : ℂ} {l t₀ u : ℝ} {L_R L_L : ℂ} (hlt : l < t₀) (htu : t₀ < u) (h_at : γ t₀ = s) (hγ_cont : ContinuousOn γ (Set.Icc l u)) (hL_R : L_R ≠ 0) (hL_L : L_L ≠ 0) (h_tendsto_R : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L_R)) (h_tendsto_L : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L_L)) (h_diff_R : ∀ᶠ (t : ℝ) in nhdsWithin t₀ (Set.Ioi t₀), DifferentiableAt ℝ γ t) (h_diff_L : ∀ᶠ (t : ℝ) in nhdsWithin t₀ (Set.Iio t₀), DifferentiableAt ℝ γ t) (h_unique : ∀ t ∈ Set.Icc l u, γ t = s → t = t₀) (g : ℂ → ℂ) (h_int : ∀ (ε : ℝ), 0 < ε → ∀ (a b : ℝ), l ≤ a → a ≤ b → b ≤ u → IntervalIntegrable (fun (t : ℝ) => if ‖γ t - s‖ > ε then g (γ t) * deriv γ t else 0) MeasureTheory.volume a b) : ∃ (τL : ℝ → ℝ) (τR : ℝ → ℝ), Filter.Tendsto τL (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin t₀ (Set.Iio t₀)) ∧ Filter.Tendsto τR (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin t₀ (Set.Ioi t₀)) ∧ (∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖γ (τL ε) - s‖ = ε) ∧ (∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖γ (τR ε) - s‖ = ε) ∧ (∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), τL ε ∈ Set.Ioo l t₀) ∧ (∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), τR ε ∈ Set.Ioo t₀ u) ∧ ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), (∫ (v : ℝ) in l..u, if ‖γ v - s‖ > ε then g (γ v) * deriv γ v else 0) = (∫ (v : ℝ) in l..τL ε, g (γ v) * deriv γ v) + ∫ (v : ℝ) in τR ε..u, g (γ v) * deriv γ v

Shared window-splitting core. At a transverse crossing γ t₀ = s (non-zero one-sided derivative limits L_R, L_L, unique crossing on the window [l, u]), there are exit-time functions τL, τR tending to t₀ one-sidedly with exit radius exactly ε, such that for every integrand g with interval-integrable ε-truncations on the window, the truncated integral over the window eventually equals the sum of the two plain side integrals up to the exit times.