Boundary Vanishing for Higher-Order Polar Terms

Chain rules for zpow compositions (L0), FTC for negative powers (L1), exit-time direction convergence (L2), and boundary term vanishing under angle conditions with flatness rate (L3).

Main results

• zpow_boundary_diff_tendsto_zero: boundary zpow difference → 0 under angle + flatness
• cutoff_zpow_infrastructure: full infrastructure for cutoff zpow integrals

L0: Chain rule for zpow compositions

The derivative of t ↦ (γ(t) - s)^n where n : ℤ and γ(t) ≠ s.

theorem GeneralizedResidueTheory.hasDerivAt_zpow_comp_sub {γ : ℝ → ℂ} {s : ℂ} {n : ℤ} {t : ℝ} {L : ℂ} (hγ : HasDerivAt γ L t) (hne : γ t ≠ s) : HasDerivAt (fun (t : ℝ) => (γ t - s) ^ n) (↑n * (γ t - s) ^ (n - 1) * L) t

HasDerivAt for (γ(t) - s)^n when γ is differentiable and γ(t) ≠ s. This is the chain rule applied to z ↦ z^n composed with t ↦ γ(t) - s.

theorem GeneralizedResidueTheory.continuousOn_zpow_comp_sub {γ : ℝ → ℂ} {s : ℂ} {n : ℤ} {A : Set ℝ} (hγ : ContinuousOn γ A) (hne : ∀ t ∈ A, γ t ≠ s) : ContinuousOn (fun (t : ℝ) => (γ t - s) ^ n) A

ContinuousOn for t ↦ (γ(t) - s)^n on a set where γ(t) ≠ s.

L1: FTC for negative powers on parameterized curves

When γ is differentiable and avoids s on [a, b], the integral of (γ(t) - s)^{-m} · γ'(t) equals the boundary difference of the primitive (γ(t) - s)^{1-m} / (1-m).

theorem GeneralizedResidueTheory.integral_zpow_comp_sub_mul_deriv {γ : ℝ → ℂ} {s : ℂ} {n : ℤ} (hn : n ≠ -1) {a b : ℝ} (hab : a ≤ b) (hγ_cont : ContinuousOn γ (Set.Icc a b)) (hγ_ne : ∀ t ∈ Set.Icc a b, γ t ≠ s) (E : Set ℝ) (hE : E.Countable) (_hE_sub : E ∩ Set.Ioo a b ⊆ Set.Ioo a b) (hγ_diff : ∀ t ∈ Set.Ioo a b, t ∉ E → DifferentiableAt ℝ γ t) (h_int : IntervalIntegrable (fun (t : ℝ) => (γ t - s) ^ n * deriv γ t) MeasureTheory.volume a b) : ∫ (t : ℝ) in a..b, (γ t - s) ^ n * deriv γ t = ((γ b - s) ^ (n + 1) - (γ a - s) ^ (n + 1)) / ↑(n + 1)

FTC for the integral of (γ(t) - s)^n · γ'(t) on [a, b] when γ(t) ≠ s on [a, b] and n ≠ -1. The primitive is (γ(t) - s)^{n+1} / (n+1).

L2: Exit times and direction convergence

For a piecewise C¹ immersion passing through s at parameter t₀, the curve enters and exits the ε-ball around s at unique parameters near t₀. The directions (γ(t±) - s) / ‖γ(t±) - s‖ converge to the tangent directions.

theorem GeneralizedResidueTheory.exists_unique_crossing_neighborhood (γ : PiecewiseC1Immersion) (s : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = s) : ∃ (a' : ℝ) (b' : ℝ), t₀ ∈ Set.Ioo a' b' ∧ Set.Icc a' b' ⊆ Set.Icc γ.a γ.b ∧ ∀ t ∈ Set.Icc a' b', γ.toFun t = s → t = t₀

Near a crossing point of an immersion, there exists a neighborhood such that the curve only crosses the singularity at that one point.

theorem GeneralizedResidueTheory.crossing_direction_right_tendsto (γ : PiecewiseC1Immersion) (s : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = s) (L_right : ℂ) (hL : L_right ≠ 0) (hL_lim : Filter.Tendsto (deriv γ.toFun) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L_right)) : Filter.Tendsto (fun (ε : ℝ) => (γ.toFun (t₀ + ε) - s) / ↑‖γ.toFun (t₀ + ε) - s‖) (nhdsWithin 0 (Set.Ioi 0)) (nhds (L_right / ↑‖L_right‖))

As ε → 0⁺, the direction from s to the first right exit point of the ε-ball converges to the right tangent direction (normalized). Specifically, (γ(t₊(ε)) - s) / ‖γ(t₊(ε)) - s‖ → L_right / ‖L_right‖.

This follows from the first-order Taylor approximation γ(t) - s ≈ (t - t₀) · L_right and ‖γ(t) - s‖ ≈ |t - t₀| · ‖L_right‖.

theorem GeneralizedResidueTheory.crossing_direction_left_tendsto (γ : PiecewiseC1Immersion) (s : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = s) (L_left : ℂ) (hL : L_left ≠ 0) (hL_lim : Filter.Tendsto (deriv γ.toFun) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L_left)) : Filter.Tendsto (fun (ε : ℝ) => (γ.toFun (t₀ - ε) - s) / ↑‖γ.toFun (t₀ - ε) - s‖) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-L_left / ↑‖L_left‖))

Left-side analogue of crossing_direction_right_tendsto: (γ(t₋(ε)) - s) / ‖γ(t₋(ε)) - s‖ → -L_left / ‖L_left‖.

L3: Boundary term vanishing under angle condition (with flatness rate)

The FTC boundary terms at the ε-cutoff points have the form w₊^k - w₋^k where w₊, w₋ lie on the ε-sphere (‖w‖ = ε) and k ≤ -1. Writing w = ε · u with ‖u‖ = 1, the difference is ε^k · (u₊^k - u₋^k).

Since k ≤ -1, ε^k → ∞ while the angle condition gives u₊^k - u₋^k → 0. Whether the product tends to 0 depends on the rate of direction convergence:

• With flatness of order n: direction error is o(ε^{n-1}), giving u₊^k - u₋^k = o(ε^{n-1}) and the product is o(ε^{k+n-1}).
• For this to tend to 0, we need k + n - 1 ≥ 0, i.e., n + k ≥ 1.
• At a pole of order m with Laurent term (z-s)^{-(k_L+1)}, the FTC boundary exponent is k = -k_L. Flatness of order n = m ≥ k_L + 1 gives k + n - 1 = m - k_L - 1 ≥ 0.

theorem GeneralizedResidueTheory.zpow_boundary_diff_tendsto_zero (k : ℤ) (hk : k ≤ -1) (wR wL : ℝ → ℂ) (h_norm_R : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖wR ε‖ = ε) (h_norm_L : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖wL ε‖ = ε) (h_neR : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), wR ε ≠ 0) (h_neL : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), wL ε ≠ 0) (uR uL : ℂ) (huR : ‖uR‖ = 1) (huL : ‖uL‖ = 1) (h_angle : uR ^ k = uL ^ k) (n : ℕ) (hn : ↑n + k ≥ 1) (h_rate_R : (fun (ε : ℝ) => ‖wR ε / ↑‖wR ε‖ - uR‖) =o[nhdsWithin 0 (Set.Ioi 0)] fun (ε : ℝ) => ε ^ (n - 1)) (h_rate_L : (fun (ε : ℝ) => ‖wL ε / ↑‖wL ε‖ - uL‖) =o[nhdsWithin 0 (Set.Ioi 0)] fun (ε : ℝ) => ε ^ (n - 1)) : Filter.Tendsto (fun (ε : ℝ) => wR ε ^ k - wL ε ^ k) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Boundary term vanishing for zpow under angle condition with flatness rate.

When w_R, w_L lie on the ε-sphere (‖w‖ = ε), directions converge to unit vectors uR, uL at rate o(ε^{n-1}) (from flatness of order n), and the angle condition ensures uR^k = uL^k, the zpow boundary difference tends to 0 provided n + k ≥ 1.

Bridge: tangent deviation → direction norm difference

For unit vectors u, v with ‖u - v‖ ≤ 1: ‖u - v‖ ≤ 2 * ‖tangentDeviation u v‖.

This bridges IsFlatOfOrder (stated in terms of tangent deviation) to the direction rate condition in zpow_boundary_diff_tendsto_zero (L3).

theorem GeneralizedResidueTheory.norm_sub_le_tangentDeviation_of_unit (u v : ℂ) (hu : ‖u‖ = 1) (hv : ‖v‖ = 1) (h_close : ‖u - v‖ ≤ 1) : ‖u - v‖ ≤ 2 * ‖tangentDeviation u v‖

For unit vectors u, v with ‖u - v‖ ≤ 1: ‖u - v‖ ≤ 2 * ‖tangentDeviation u v‖.

theorem GeneralizedResidueTheory.unit_zpow_eq_of_angle_multiple (z₁ z₂ : ℂ) (k : ℤ) (hz₁ : ‖z₁‖ = 1) (hz₂ : ‖z₂‖ = 1) (h : ∃ (n : ℤ), ↑k * (z₁.arg - z₂.arg) = ↑n * (2 * Real.pi)) : z₁ ^ k = z₂ ^ k

For unit vectors z₁, z₂ and integer exponent k, if k · (arg z₁ - arg z₂) ∈ 2πℤ, then z₁^k = z₂^k.

theorem GeneralizedResidueTheory.tangentDeviation_real_smul_left (c : ℝ) (w L : ℂ) : tangentDeviation (c • w) L = c • tangentDeviation w L

theorem GeneralizedResidueTheory.tangentDeviation_real_smul_right (c : ℝ) (hc : c ≠ 0) (w L : ℂ) : tangentDeviation w (c • L) = tangentDeviation w L

theorem GeneralizedResidueTheory.direction_rate_final_calc (m : ℕ) (c ε : ℝ) (hε_pos : 0 < ε) (hm : 2 ≤ m) (w L u v₀ : ℂ) (hu : ‖u‖ = 1) (hv₀ : ‖v₀‖ = 1) (hR_pos : 0 < (u * (starRingEnd ℂ) v₀).re) (h_td_scale : ‖tangentDeviation u v₀‖ = ‖tangentDeviation w L‖ / ‖w‖) (hε_norm : ‖w‖ = ε) (h_td_bound' : ‖tangentDeviation w L‖ ≤ c / √2 * ε ^ m) : ‖u - v₀‖ ≤ c * ‖ε ^ (m - 1)‖

theorem GeneralizedResidueTheory.re_pos_right_of_slope (γ : PiecewiseC1Immersion) (s : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = s) (L_R : ℂ) (hL_R_ne : L_R ≠ 0) (htend_R : Filter.Tendsto (deriv γ.toFun) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L_R)) : ∀ᶠ (t : ℝ) in nhdsWithin t₀ (Set.Ioi t₀), 0 < ((γ.toFun t - s) * (starRingEnd ℂ) L_R).re

theorem GeneralizedResidueTheory.re_pos_left_of_slope (γ : PiecewiseC1Immersion) (s : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = s) (L_L : ℂ) (hL_L_ne : L_L ≠ 0) (htend_L : Filter.Tendsto (deriv γ.toFun) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L_L)) : ∀ᶠ (t : ℝ) in nhdsWithin t₀ (Set.Iio t₀), 0 < ((γ.toFun t - s) * (starRingEnd ℂ) (-L_L)).re

theorem GeneralizedResidueTheory.tangentDeviation_scale_eq (w L : ℂ) (_hw_ne : ‖w‖ ≠ 0) (hL_ne : ‖L‖ ≠ 0) : ‖tangentDeviation (w / ↑‖w‖) (L / ↑‖L‖)‖ = ‖tangentDeviation w L‖ / ‖w‖