The per-window principal value at a higher-order pole

At a transverse crossing γ t_i = s that is flat of order n ≥ k ≥ 2 and satisfies the condition-(B) power identity, the ε-truncated window integral of the order-k polar term (c / (z - s)^k) along the curve converges as ε → 0⁺ to the boundary difference of its antiderivative F z = -(k-1)⁻¹ (z - s)^{-(k-1)}:

∫ window, truncated → c · (F (γ (t_i + r)) - F (γ (t_i - r))).

The window integral splits at the exit times (exists_exit_times_truncated_integral_split); each side integral evaluates by the fundamental theorem of calculus to a boundary difference of c · F ∘ γ, and the two inner exit-time terms cancel in the limit by the sector-even cancellation (antiderivative_diff_across_crossing_tendsto_zero) — the mechanism of Hungerbühler–Wasem condition (B) at a higher-order pole.

The fundamental theorem of calculus the window integral is built on (Contour.integral_pow_inv_mul_deriv_eq_sub) is stated here for its own sake, together with its closed-curve corollary: around a loop missing the pole the boundary difference cancels, so an order-k ≥ 2 term contributes nothing at all — the fact that leaves only the simple-pole coefficient in a residue theorem.

Main results

• Contour.perWindow_higherOrder_truncated_integral_tendsto — the truncated window integral of the order-k polar term converges, with the explicit boundary-difference value.
• Contour.integral_pow_inv_mul_deriv_eq_sub — the fundamental theorem of calculus for the order-k polar term along the curve, on an interval avoiding the pole.
• Contour.integral_pow_inv_mul_deriv_eq_zero_of_closed — the same term integrates to zero around a closed piecewise-C¹ curve missing the pole, the endpoint difference cancelling.

Provenance

Migrated from perCrossing_higherOrder_window_integral_tendsto_corner and its supporting lemmas (pow_inv_mul_deriv_intervalIntegrable, antiderivPow_FTC_on_avoiding) of MultiCrossingCPV.lean in the AINTLIB LeanModularForms development, restated for a raw curve on its crossing window. The truncated-integrability lemma migrated alongside them, cpvIntegrand_higherOrder_intervalIntegrable, lives with the rest of the truncation API in Contour.Cauchy.PrincipalValue.Basic as intervalIntegrable_pow_inv_mul_deriv_truncated. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

theorem TauCeti.Contour.integral_pow_inv_mul_deriv_eq_sub {γ : ℝ → ℂ} {s : ℂ} {k : ℕ} (hk : 2 ≤ k) (c : ℂ) {l u : ℝ} (hlu : l ≤ u) {P : Set ℝ} (hP : P.Countable) (h_ne : ∀ t ∈ Set.Icc l u, γ t ≠ s) (h_diff : ∀ t ∈ Set.Ioo l u \ P, DifferentiableAt ℝ γ t) (hγ_cont : ContinuousOn γ (Set.Icc l u)) (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume l u) : ∫ (t : ℝ) in l..u, c / (γ t - s) ^ k * deriv γ t = c * (-(↑(k - 1))⁻¹ * ((γ u - s) ^ (k - 1))⁻¹) - c * (-(↑(k - 1))⁻¹ * ((γ l - s) ^ (k - 1))⁻¹)

The fundamental theorem of calculus for the order-k polar term along the curve, on an interval avoiding the pole: the integral is the boundary difference of the antiderivative c · (-(k-1)⁻¹ (· - s)^{-(k-1)}) ∘ γ.

theorem TauCeti.Contour.integral_pow_inv_mul_deriv_eq_zero_of_closed {γ : ℝ → ℂ} {s : ℂ} {k : ℕ} (hk : 2 ≤ k) (c : ℂ) {a b : ℝ} (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) (h_ne : ∀ t ∈ Set.uIcc a b, γ t ≠ s) : ∫ (t : ℝ) in a..b, c / (γ t - s) ^ k * deriv γ t = 0

A Laurent term of order at least two integrates to zero around a closed curve. On a piecewise-C¹ curve γ with γ a = γ b that never meets s, the integrand c/(z − s)^k · γ' with k ≥ 2 is the derivative of c · (−(k−1)⁻¹ (γ · − s)^{−(k−1)}), so Contour.integral_pow_inv_mul_deriv_eq_sub returns the endpoint difference, which the closedness kills. This is why only the simple-pole coefficient of a Laurent tail survives in the residue theorem.

theorem TauCeti.Contour.perWindow_higherOrder_truncated_integral_tendsto {γ : ℝ → ℂ} {s : ℂ} {t_i r : ℝ} {L_R L_L : ℂ} {n k : ℕ} {P : Set ℝ} (hr_pos : 0 < r) (h_at : γ t_i = s) (hγ_cont : ContinuousOn γ (Set.Icc (t_i - r) (t_i + r))) (hL_R : L_R ≠ 0) (hL_L : L_L ≠ 0) (h_tendsto_R : Filter.Tendsto (deriv γ) (nhdsWithin t_i (Set.Ioi t_i)) (nhds L_R)) (h_tendsto_L : Filter.Tendsto (deriv γ) (nhdsWithin t_i (Set.Iio t_i)) (nhds L_L)) (h_diff_R : ∀ᶠ (t : ℝ) in nhdsWithin t_i (Set.Ioi t_i), DifferentiableAt ℝ γ t) (h_diff_L : ∀ᶠ (t : ℝ) in nhdsWithin t_i (Set.Iio t_i), DifferentiableAt ℝ γ t) (hP : P.Countable) (hγ_diffP : ∀ t ∈ Set.Ioo (t_i - r) (t_i + r) \ P, DifferentiableAt ℝ γ t) (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume (t_i - r) (t_i + r)) (h_unique : ∀ t ∈ Set.Icc (t_i - r) (t_i + r), γ t = s → t = t_i) (h_flat : FlatOfOrder γ t_i n) (hk : 2 ≤ k) (hkn : k ≤ n) (h_B : (L_R / ↑‖L_R‖) ^ (k - 1) = (-L_L / ↑‖L_L‖) ^ (k - 1)) (c : ℂ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in t_i - r..t_i + r, if ‖γ t - s‖ > ε then c / (γ t - s) ^ k * deriv γ t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds (c * (-(↑(k - 1))⁻¹ * ((γ (t_i + r) - s) ^ (k - 1))⁻¹) - c * (-(↑(k - 1))⁻¹ * ((γ (t_i - r) - s) ^ (k - 1))⁻¹)))

The per-window principal value at a higher-order pole: at a transverse crossing γ t_i = s, flat of order n ≥ k ≥ 2 and satisfying the condition-(B) power identity, with unique crossing on the window, the ε-truncated window integral of the order-k polar term c / (z - s)^k converges as ε → 0⁺ to the boundary difference of its antiderivative.