The principal value of a higher-order polar term along an immersed curve

For a piecewise-C¹ immersed curve γ on [a, b] whose value-s parameters are interior, flat of order n ≥ k, and sector-compatible, the single-point Cauchy principal value of the order-k ≥ 2 polar term t ↦ c / (γ t - s) ^ k * deriv γ t exists on [a, b] and equals the boundary difference of the antiderivative c · (-(k-1)⁻¹ (· - s)^{-(k-1)}) ∘ γ — in particular it vanishes around a closed curve, which is why only the simple-pole part of a polar decomposition contributes to the generalized residue theorem. The crossings are finitely many (Contour.IsPwC1ImmersionOn.finite_crossings), a common window radius separates them (Contour.exists_common_window_radius), each window integral converges to the boundary difference (Contour.perWindow_higherOrder_truncated_integral_tendsto), and the pieces telescope (Contour.hasCauchyPVAt_of_perWindow_boundary_tendsto_of_interiorDisjoint).

The flatness and sector hypotheses are the raw per-crossing forms of the Hungerbühler–Wasem conditions (A′) and (B) at s (Contour.FlatOfOrder; the tangent-direction power equation, stated for the one-sided derivative limits, which are unique).

Main results

• Contour.IsPwC1ImmersionOn.hasCauchyPVAt_pow_inv — the single-point principal value of the order-k ≥ 2 polar term along a piecewise-C¹ immersion is the boundary difference of its antiderivative.

Provenance

Migrated from the higher-order content of hasCauchyPVOn_multiCrossing_higherOrder_corner of MultiCrossingCPV.lean in the AINTLIB LeanModularForms development (there stated for the bundled ClosedPwC1Immersion). See N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997, §3.

theorem TauCeti.Contour.IsPwC1ImmersionOn.hasCauchyPVAt_pow_inv {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} {k n : ℕ} (h_imm : IsPwC1ImmersionOn γ a b) (hab : a ≤ b) (h_interior : ∀ t ∈ Set.Icc a b, γ t = s → t ∈ Set.Ioo a b) (hk : 2 ≤ k) (hkn : k ≤ n) (h_flat : ∀ t ∈ Set.Icc a b, γ t = s → FlatOfOrder γ t n) (h_B : ∀ t ∈ Set.Icc a b, γ t = s → ∀ (L_R L_L : ℂ), Filter.Tendsto (deriv γ) (nhdsWithin t (Set.Ioi t)) (nhds L_R) → Filter.Tendsto (deriv γ) (nhdsWithin t (Set.Iio t)) (nhds L_L) → (L_R / ↑‖L_R‖) ^ (k - 1) = (-L_L / ↑‖L_L‖) ^ (k - 1)) (c : ℂ) : HasCauchyPVAt γ a b (fun (z : ℂ) => c / (z - s) ^ k) s (c * (-(↑(k - 1))⁻¹ * ((γ b - s) ^ (k - 1))⁻¹) - c * (-(↑(k - 1))⁻¹ * ((γ a - s) ^ (k - 1))⁻¹))

The principal value of a higher-order polar term along a piecewise-C¹ immersion is the boundary difference of its antiderivative: if every parameter of [a, b] where γ meets s is interior, flat of order n ≥ k, and sector-compatible in the tangent-direction power sense, then for k ≥ 2 the single-point Cauchy principal value of t ↦ c / (γ t - s) ^ k * deriv γ t at s exists on [a, b] with value c · (-(k-1)⁻¹ (· - s)^{-(k-1)}) ∘ γ differenced at the endpoints — zero around a closed curve. Endpoint crossings are excluded by h_interior; for a closed curve this is the choice of a basepoint off s.