Higher-order antiderivative asymptotics at an on-curve pole

For the higher-order pole integrand 1/(z-s)^k (k ≥ 2) with single-valued antiderivative F(z) = -1/[(k-1)(z-s)^(k-1)], this file proves the asymptotics the sector-cancellation argument of the generalized residue theorem consumes: along a branch of a curve leaving s with one-sided tangent L and perpendicular deviation o(‖γ t - s‖ ^ n) (n ≥ k), the difference F(γ t) - F(tangent target) tends to 0, where the tangent target is the point of the tangent ray at the same distance from s. Combined with the fundamental theorem of calculus on each smooth piece, this replaces the curve by its tangent rays in the excised principal value, up to a vanishing error.

Main results

• Contour.hasDerivAt_antiderivative_pow_inv — the antiderivative of 1/(z-s)^k.
• Contour.norm_antiderivative_diff_le_segment_bound — the mean-value bound for the antiderivative along a segment avoiding the pole.
• Contour.chord_to_tangent_isLittleO — the chord to the tangent target is o(‖γ t - s‖ ^ n) given the deviation bound, in the tangent hemisphere.
• Contour.antiderivative_diff_at_tangent_target_tendsto_zero — the parametrised core: the antiderivative difference to the tangent target tends to 0 for 2 ≤ k ≤ n.
• Contour.antiderivative_diff_at_tangent_target_tendsto_zero_right / _left — the one-sided forms, from a one-sided derivative and the deviation bound against the tangent (+L ray on the right, -L ray on the left).

The one-sided forms take the deviation bound ‖tangentDeviation (γ t - s) L‖ = o(‖γ t - s‖ ^ n) as a hypothesis; producing it from Contour.FlatOfOrder (whose witness directions are existential) is the tangent-forcing bridge, a separate step.

Provenance

Migrated from HungerbuhlerWasem/HigherOrderAsymptotics.lean of the AINTLIB LeanModularForms development, restated for the raw curve: the flatness hypotheses carried there by the IsFlatOfOrder structure become explicit deviation bounds against the one-sided tangent. See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3 (eq. 3.4).

theorem TauCeti.Contour.hasDerivAt_antiderivative_pow_inv {s : ℂ} {k : ℕ} (hk : 2 ≤ k) {z : ℂ} (hz : z ≠ s) : HasDerivAt (fun (w : ℂ) => -(↑(k - 1))⁻¹ * ((w - s) ^ (k - 1))⁻¹) (1 / (z - s) ^ k) z

The antiderivative of 1/(z-s)^k (k ≥ 2): the function F(z) = -1/[(k-1)(z-s)^(k-1)] has complex derivative 1/(z-s)^k at any z ≠ s.

theorem TauCeti.Contour.norm_antiderivative_diff_le_segment_bound {z₁ z₂ s : ℂ} {k : ℕ} {ε : ℝ} (hk : 2 ≤ k) (hε : 0 < ε) (h_seg_avoids : ∀ z ∈ segment ℝ z₁ z₂, ε ≤ ‖z - s‖) : ‖-(↑(k - 1))⁻¹ * ((z₂ - s) ^ (k - 1))⁻¹ - -(↑(k - 1))⁻¹ * ((z₁ - s) ^ (k - 1))⁻¹‖ ≤ 1 / ε ^ k * ‖z₂ - z₁‖

Mean-value bound for the antiderivative along a segment. When the segment from z₁ to z₂ stays at distance ≥ ε from s, the antiderivative difference satisfies ‖F(z₂) - F(z₁)‖ ≤ ‖z₂ - z₁‖ / ε^k.

theorem TauCeti.Contour.chord_to_tangent_isLittleO {γ : ℝ → ℂ} {s : ℂ} {l : Filter ℝ} {T : ℂ} {n : ℕ} (hT : T ≠ 0) (h_re : ∀ᶠ (t : ℝ) in l, 0 ≤ ((γ t - s) * (starRingEnd ℂ) T).re) (h_ne : ∀ᶠ (t : ℝ) in l, γ t ≠ s) (h_dev : (fun (t : ℝ) => ‖tangentDeviation (γ t - s) T‖) =o[l] fun (t : ℝ) => ‖γ t - s‖ ^ n) : (fun (t : ℝ) => ‖γ t - s - (‖γ t - s‖ / ‖T‖) • T‖) =o[l] fun (t : ℝ) => ‖γ t - s‖ ^ n

Chord-to-tangent-target o-bound (parametrised core). In the +T hemisphere and off s, the chord from γ t to the tangent target at the same distance is dominated by the perpendicular deviation, hence o(‖γ t - s‖ ^ n) whenever the deviation is. The right side instantiates T = L, l = 𝓝[>] t₀; the left side T = -L, l = 𝓝[<] t₀.

theorem TauCeti.Contour.antiderivative_diff_at_tangent_target_tendsto_zero {γ : ℝ → ℂ} {s : ℂ} {l : Filter ℝ} {T : ℂ} {n k : ℕ} (hT : T ≠ 0) (hk : 2 ≤ k) (hkn : k ≤ n) (h_chord : (fun (t : ℝ) => ‖γ t - s - (‖γ t - s‖ / ‖T‖) • T‖) =o[l] fun (t : ℝ) => ‖γ t - s‖ ^ n) (h_ne : ∀ᶠ (t : ℝ) in l, γ t ≠ s) (h_to : Filter.Tendsto γ l (nhds s)) : Filter.Tendsto (fun (t : ℝ) => ‖-(↑(k - 1))⁻¹ * ((γ t - s) ^ (k - 1))⁻¹ - -(↑(k - 1))⁻¹ * ((s + (‖γ t - s‖ / ‖T‖) • T - s) ^ (k - 1))⁻¹‖) l (nhds 0)

The antiderivative difference to the tangent target vanishes (parametrised core). If the chord to the +T tangent target is o(‖γ t - s‖ ^ n) along l, γ → s off s along l, and 2 ≤ k ≤ n, then F(γ t) - F(target) tends to 0 along l, for the antiderivative F of the order-k pole integrand.

theorem TauCeti.Contour.antiderivative_diff_at_tangent_target_tendsto_zero_right {γ : ℝ → ℂ} {t₀ : ℝ} {s L : ℂ} {n k : ℕ} (hL : L ≠ 0) (h_deriv : HasDerivWithinAt γ L (Set.Ioi t₀) t₀) (h_s : γ t₀ = s) (h_dev : (fun (t : ℝ) => ‖tangentDeviation (γ t - s) L‖) =o[nhdsWithin t₀ (Set.Ioi t₀)] fun (t : ℝ) => ‖γ t - s‖ ^ n) (hk : 2 ≤ k) (hkn : k ≤ n) : Filter.Tendsto (fun (t : ℝ) => ‖-(↑(k - 1))⁻¹ * ((γ t - s) ^ (k - 1))⁻¹ - -(↑(k - 1))⁻¹ * ((s + (‖γ t - s‖ / ‖L‖) • L - s) ^ (k - 1))⁻¹‖) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds 0)

The right-branch antiderivative asymptotics: with one-sided derivative L ≠ 0 from the right at t₀ and perpendicular deviation o(‖γ t - s‖ ^ n) against L, the antiderivative difference between γ t and the tangent target on the +L ray tends to 0 as t → t₀⁺ (2 ≤ k ≤ n).

theorem TauCeti.Contour.antiderivative_diff_at_tangent_target_tendsto_zero_left {γ : ℝ → ℂ} {t₀ : ℝ} {s L : ℂ} {n k : ℕ} (hL : L ≠ 0) (h_deriv : HasDerivWithinAt γ L (Set.Iio t₀) t₀) (h_s : γ t₀ = s) (h_dev : (fun (t : ℝ) => ‖tangentDeviation (γ t - s) L‖) =o[nhdsWithin t₀ (Set.Iio t₀)] fun (t : ℝ) => ‖γ t - s‖ ^ n) (hk : 2 ≤ k) (hkn : k ≤ n) : Filter.Tendsto (fun (t : ℝ) => ‖-(↑(k - 1))⁻¹ * ((γ t - s) ^ (k - 1))⁻¹ - -(↑(k - 1))⁻¹ * ((s + (‖γ t - s‖ / ‖-L‖) • -L - s) ^ (k - 1))⁻¹‖) (nhdsWithin t₀ (Set.Iio t₀)) (nhds 0)

The left-branch antiderivative asymptotics: the counterpart of antiderivative_diff_at_tangent_target_tendsto_zero_right from the left, with the tangent target on the -L ray.