The Cauchy principal value of a contour integral at a point (Hungerbühler–Wasem)

For a curve γ : ℝ → ℂ on [a, b], an integrand f : ℂ → ℂ, and a point z₀ ∈ ℂ, this file defines the Cauchy principal value of the contour integral ∮_γ f excising a symmetric ε-ball about z₀: the limit as ε → 0⁺ of the truncated integral ∫_a^b 𝟙[‖γ t − z₀‖ > ε] · f (γ t) · γ'(t) dt. This is the value one must use in place of the ordinary contour integral exactly when a singularity of f sits on the curve at z₀, where the integrand is not integrable; away from z₀ the truncation is eventually inert and the principal value collapses to the ordinary integral (HasCauchyPVAt.of_avoidance).

The predicate carries two conditions: that the truncated integrand is (eventually) genuinely IntervalIntegrable, and that the truncated integrals converge. The integrability clause is essential: without it the Tendsto clause alone is met vacuously by functions whose truncations are non-integrable, since a Bochner interval integral of a non-integrable function is 0 by convention. This keeps the principal value honest and separate from ordinary integrability of f (which fails at the on-curve singularity), never silently identifying the two.

This is the single-point companion of the roadmap's HasCauchyPV predicate: HasCauchyPVAt symmetrically excises one prescribed point z₀, the case that defines the generalized winding number n_{z₀}(γ) = (2πi)⁻¹ · PV ∮_γ dz/(z − z₀) and that feeds the on-curve residue theory (Hungerbühler–Wasem, arXiv:1808.00997). The naming mirrors Mathlib's MeromorphicAt (at a point) versus MeromorphicOn (on a set).

Main definitions

• HasCauchyPVAt γ a b f z₀ L — the truncations are eventually integrable and their integrals tend to L (the primary predicate).
• cauchyPVAt γ a b f z₀ — the value of that limit (limUnder-based; junk when it does not exist).
• CauchyPVExistsAt γ a b f z₀ — the principal value exists (∃ L, HasCauchyPVAt γ a b f z₀ L).

Main results

• hasCauchyPVAt_iff — restates the predicate as its two defining clauses, so consumers can characterize HasCauchyPVAt without unfolding its hidden body; the value cauchyPVAt is read off a witness through HasCauchyPVAt.cauchyPVAt_eq.
• HasCauchyPVAt.of_tendsto — the shared ε → 0 closing step: from a closed form F that the excised integral eventually equals, and its limit L, concludes HasCauchyPVAt at L.
• intervalIntegrable_truncated_and_integral_truncated_eq_zero_of_norm_le — where the curve stays within ε of the centre, the truncated integrand is integrable and integrates to 0.
• aestronglyMeasurable_truncated and intervalIntegrable_truncated_mul_deriv — the two halves of integrability for a truncated integrand: measurability of the truncation, and domination by M · ‖deriv γ‖ from a bound off the ball. intervalIntegrable_pow_inv_mul_deriv_truncated applies both to the order-k polar integrand c / (z - z₀) ^ k, and intervalIntegrable_inv_sub_truncated is its simple-pole case c = 1, k = 1.
• HasCauchyPVAt.intro — build the predicate from its two clauses; HasCauchyPVAt.tendsto, HasCauchyPVAt.eventually_intervalIntegrable — the clauses as named accessors; HasCauchyPVAt.cauchyPVAt_eq, HasCauchyPVAt.unique — the value and its uniqueness; cauchyPVExistsAt_iff, CauchyPVExistsAt.intro, CauchyPVExistsAt.hasCauchyPVAt_cauchyPVAt — package/unpack existence and recover the predicate at cauchyPVAt.
• HasCauchyPVAt.congr_along_curve, cauchyPVAt_congr_along_curve — the integrand only matters along γ on [a, b];
• HasCauchyPVAt.congr_curve_ae, CauchyPVExistsAt.congr_curve_ae, cauchyPVAt_congr_curve_ae — the curve only matters up to null sets: the principal value is unchanged when the curves agree almost everywhere on the integration interval and their derivatives agree almost everywhere where the curve misses z₀ (the truncation deletes the integrand at z₀); HasCauchyPVAt.congr_curve, CauchyPVExistsAt.congr_curve, cauchyPVAt_congr_curve — the pointwise corollaries, needing agreement only on the open interval Set.uIoo a b; HasCauchyPVAt.zero, HasCauchyPVAt.const_mul, HasCauchyPVAt.add, HasCauchyPVAt.sum (and the CauchyPVExistsAt forms) — the principal value is ℂ-linear in the integrand, including over finite sums.
• HasCauchyPVAt.of_dist_lower_bound — if γ stays a positive distance from z₀ on [a, b], the principal value is the ordinary integral (cauchyPVExistsAt_of_dist_lower_bound is the existence form).
• HasCauchyPVAt.of_avoidance — if γ avoids z₀ on [a, b] and the integrand is integrable there, the principal value is the ordinary integral (cauchyPVExistsAt_of_avoidance is the existence form).
• HasCauchyPVAt.translate, CauchyPVExistsAt.translate, cauchyPVAt_translate — simultaneous translation of the curve, point, and integrand preserves the principal value.
• HasCauchyPVAt.const_mul_curve, CauchyPVExistsAt.const_mul_curve, cauchyPVAt_const_mul_curve — simultaneous nonzero scaling of the curve and point, with the integrand rescaled by z ↦ c⁻¹ * f (c⁻¹ * z), preserves the principal value; the value form needs no existence hypothesis.
• HasCauchyPVAt.symm, CauchyPVExistsAt.symm, cauchyPVAt_symm — reversing the interval orientation negates the single-point principal value.
• HasCauchyPVAt.concat, HasCauchyPVAt.concat_range — principal values add over two adjacent intervals or a finite partition (CauchyPVExistsAt.concat and CauchyPVExistsAt.concat_range are the existence forms, and cauchyPVAt_concat_range computes the canonical finite value).

Provenance

Migrated and adapted from the AINTLIB LeanModularForms project, file ForMathlib/ClassicalCPV.lean, specialised to the raw-function (γ : ℝ → ℂ on [a, b]) design of the contour-integration roadmap, and strengthened with the truncated-integrability clause. intervalIntegrable_pow_inv_mul_deriv_truncated comes instead from the same development's cpvIntegrand_higherOrder_intervalIntegrable, in ForMathlib/HungerbuhlerWasem/MultiCrossingCPV.lean, and its simple-pole case intervalIntegrable_inv_sub_truncated from cpvIntegrand_inv_intervalIntegrable in that development's LocalCutoffs.lean.

References

• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997.

def TauCeti.Contour.HasCauchyPVAt (γ : ℝ → ℂ) (a b : ℝ) (f : ℂ → ℂ) (z₀ L : ℂ) : Prop

The Cauchy principal value at z₀ of the contour integral ∮_γ f exists with value L: the truncated integrand along γ over [a, b], excluding the symmetric ε-ball about z₀, is eventually IntervalIntegrable, and its integral tends to L as ε → 0⁺. The integrability clause prevents the Tendsto clause from being met vacuously through the convention that a Bochner integral of a non-integrable function is 0. Primary API predicate (raw γ : ℝ → ℂ, [a, b]).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Contour.hasCauchyPVAt_iff {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ L : ℂ} : HasCauchyPVAt γ a b f z₀ L ↔ (∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), IntervalIntegrable (fun (t : ℝ) => if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0) MeasureTheory.volume a b) ∧ Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds L)

Restatement of HasCauchyPVAt as the conjunction of its two defining clauses — eventual integrability of the excised integrand and convergence of the excised integrals — so consumers can characterize the predicate without unfolding its definition.

theorem TauCeti.Contour.HasCauchyPVAt.of_tendsto {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ L : ℂ} {F : ℝ → ℂ} (hF : Filter.Tendsto F (nhdsWithin 0 (Set.Ioi 0)) (nhds L)) (h : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), IntervalIntegrable (fun (t : ℝ) => if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0) MeasureTheory.volume a b ∧ (∫ (t : ℝ) in a..b, if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0) = F ε) : HasCauchyPVAt γ a b f z₀ L

The ε → 0 passage, once. A principal value is computed by exhibiting the excised integral in closed form on a punctured right-neighbourhood of 0 and taking the limit; this packages that step, so a caller supplies only the closed form F and its limit.

The excised integral is asked to equal F ε rather than a specific shape such as L - c ε, because the closed forms met in practice differ: constant in ε along a straight edge, and L minus an arcsin correction at a corner or along an arc.

noncomputable def TauCeti.Contour.cauchyPVAt (γ : ℝ → ℂ) (a b : ℝ) (f : ℂ → ℂ) (z₀ : ℂ) : ℂ

The Cauchy principal value at z₀ of ∮_γ f, excluding the symmetric ε-ball about z₀. limUnder-based; returns junk when the limit does not exist, so use HasCauchyPVAt for the predicate and HasCauchyPVAt.cauchyPVAt_eq to read the value off it.

Equations

• TauCeti.Contour.cauchyPVAt γ a b f z₀ = (nhdsWithin 0 (Set.Ioi 0)).limUnder fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0

def TauCeti.Contour.CauchyPVExistsAt (γ : ℝ → ℂ) (a b : ℝ) (f : ℂ → ℂ) (z₀ : ℂ) : Prop

The Cauchy principal value at z₀ exists: shorthand for ∃ L, HasCauchyPVAt γ a b f z₀ L.

Equations

• TauCeti.Contour.CauchyPVExistsAt γ a b f z₀ = ∃ (L : ℂ), TauCeti.Contour.HasCauchyPVAt γ a b f z₀ L

theorem TauCeti.Contour.cauchyPVExistsAt_iff {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} : CauchyPVExistsAt γ a b f z₀ ↔ ∃ (L : ℂ), HasCauchyPVAt γ a b f z₀ L

Characterization of CauchyPVExistsAt as the existence of a principal value — the eliminator/constructor interface, so downstream users need not unfold the definition.

theorem TauCeti.Contour.CauchyPVExistsAt.intro {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ L : ℂ} (h : HasCauchyPVAt γ a b f z₀ L) : CauchyPVExistsAt γ a b f z₀

Constructor for CauchyPVExistsAt from a HasCauchyPVAt witness.

theorem TauCeti.Contour.aestronglyMeasurable_truncated {γ F : ℝ → ℂ} {z₀ : ℂ} {a b ε : ℝ} (hγ : AEMeasurable γ (MeasureTheory.volume.restrict (Set.uIoc a b))) (hF : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict (Set.uIoc a b))) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => if ‖γ t - z₀‖ > ε then F t else 0) (MeasureTheory.volume.restrict (Set.uIoc a b))

The ε-truncated integrand is a.e.-strongly measurable. Truncating an a.e.-strongly measurable integrand to the parameters lying at distance > ε from z₀ preserves a.e.-strong measurability: the truncation is the indicator of {t | ε < ‖γ t - z₀‖}, which is null-measurable as soon as γ is.

The hypothesis on γ is a.e.-measurability rather than continuity, which is all the statement needs and is what lets the continuous-curve and merely-measurable-curve callers share it.

theorem TauCeti.Contour.intervalIntegrable_truncated_mul_deriv {γ : ℝ → ℂ} {f : ℂ → ℂ} {z₀ : ℂ} {a b M ε : ℝ} (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume a b) (h_aesm : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0) (MeasureTheory.volume.restrict (Set.uIoc a b))) (h_bd : ∀ (t : ℝ), ε < ‖γ t - z₀‖ → ‖f (γ t)‖ ≤ M) : IntervalIntegrable (fun (t : ℝ) => if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0) MeasureTheory.volume a b

The ε-truncated integrand is interval-integrable from a bound off the ball: whenever f ∘ γ is bounded by M at distance > ε from z₀ and the truncated integrand is a.e.-strongly measurable, the truncated integrand is dominated by M · ‖deriv γ‖.

theorem TauCeti.Contour.intervalIntegrable_pow_inv_mul_deriv_truncated {γ : ℝ → ℂ} {z₀ : ℂ} {a b : ℝ} (c : ℂ) (k : ℕ) (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume a b) {ε : ℝ} (hε : 0 < ε) : IntervalIntegrable (fun (t : ℝ) => if ‖γ t - z₀‖ > ε then c / (γ t - z₀) ^ k * deriv γ t else 0) MeasureTheory.volume a b

The ε-truncated order-k polar integrand is interval-integrable: off the ε-ball it is dominated by (‖c‖ / ε ^ k) · ‖deriv γ‖.

theorem TauCeti.Contour.intervalIntegrable_inv_sub_truncated {γ : ℝ → ℂ} {z₀ : ℂ} {a b : ℝ} (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hderiv_int : IntervalIntegrable (fun (t : ℝ) => deriv γ t) MeasureTheory.volume a b) {ε : ℝ} (hε : 0 < ε) : IntervalIntegrable (fun (t : ℝ) => if ‖γ t - z₀‖ > ε then (γ t - z₀)⁻¹ * deriv γ t else 0) MeasureTheory.volume a b

The ε-truncated simple-pole integrand is interval-integrable: the simple pole is the order-1 polar term with coefficient 1, so this is intervalIntegrable_pow_inv_mul_deriv_truncated at c = 1, k = 1, where the domination bound reads (1/ε) · ‖deriv γ‖.

theorem TauCeti.Contour.ae_logDeriv_sub_eq_truncated {γ : ℝ → ℂ} {z₀ : ℂ} {a b ε : ℝ} (hab : a ≤ b) (hfar : ∀ s ∈ Set.Ioo a b, ε < ‖γ s - z₀‖) : ∀ᵐ (s : ℝ), s ∈ Set.uIoc a b → deriv (fun (r : ℝ) => γ r - z₀) s / (γ s - z₀) = if ε < ‖γ s - z₀‖ then (γ s - z₀)⁻¹ * deriv γ s else 0

Off the truncation the integrand is a logarithmic derivative. Where the curve stays further than ε from the centre z₀, the ε-truncated winding integrand agrees with the logarithmic derivative of t ↦ γ t - z₀. The equality is almost-everywhere because the far-ness hypothesis is stated on the open interval, so the right endpoint — a null set — is excluded.

theorem TauCeti.Contour.intervalIntegrable_truncated_and_integral_truncated_eq_zero_of_norm_le {γ g : ℝ → ℂ} {z₀ : ℂ} {a b ε : ℝ} (hnear : ∀ᵐ (s : ℝ), s ∈ Set.uIoc a b → ‖γ s - z₀‖ ≤ ε) : IntervalIntegrable (fun (s : ℝ) => if ε < ‖γ s - z₀‖ then g s else 0) MeasureTheory.volume a b ∧ (∫ (s : ℝ) in a..b, if ε < ‖γ s - z₀‖ then g s else 0) = 0

Inside the truncation the integrand vanishes. Where the curve stays within ε of the centre z₀, the ε-truncated integrand is almost everywhere 0, so it is integrable and integrates to 0.

Nothing is used but the falsity of the truncation condition, so the nonzero branch is an arbitrary g : ℝ → ℂ, and the hypothesis is imposed only on Set.uIoc a b — the oriented half-open interval that interval integration actually sees — and only almost everywhere on it. This is the excised corner window: the truncation is exactly what removes the corner's contribution, and the whole content is that nothing survives it.

theorem TauCeti.Contour.HasCauchyPVAt.intro {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ L : ℂ} (hint : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), IntervalIntegrable (fun (t : ℝ) => if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0) MeasureTheory.volume a b) (htendsto : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds L)) : HasCauchyPVAt γ a b f z₀ L

Constructor for HasCauchyPVAt from its two clauses — eventual integrability of the excised integrand and convergence of the excised integrals — without unfolding the definition.

theorem TauCeti.Contour.HasCauchyPVAt.of_dist_lower_bound {γ : ℝ → ℂ} {z₀ : ℂ} {f : ℂ → ℂ} {a b m : ℝ} (hm_pos : 0 < m) (h_far : ∀ t ∈ Set.uIcc a b, m ≤ ‖γ t - z₀‖) (h_int_tr : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), IntervalIntegrable (fun (t : ℝ) => if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0) MeasureTheory.volume a b) : HasCauchyPVAt γ a b f z₀ (∫ (t : ℝ) in a..b, f (γ t) * deriv γ t)

Away from the pole the principal value is the ordinary integral. On an interval where the curve keeps distance ≥ m > 0 from z₀, every small enough truncation leaves the integrand untouched, so the principal value at z₀ is the plain integral. Continuity of the curve is not needed — the distance bound and the eventual integrability carry both clauses. The endpoints are not assumed ordered; the bound is stated on uIcc a b.

theorem TauCeti.Contour.HasCauchyPVAt.tendsto {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ L : ℂ} (h : HasCauchyPVAt γ a b f z₀ L) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds L)

The convergence clause of HasCauchyPVAt: the excised integrals tend to the value.

theorem TauCeti.Contour.HasCauchyPVAt.eventually_intervalIntegrable {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ L : ℂ} (h : HasCauchyPVAt γ a b f z₀ L) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), IntervalIntegrable (fun (t : ℝ) => if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0) MeasureTheory.volume a b

The integrability clause of HasCauchyPVAt: the excised integrand is eventually integrable.

theorem TauCeti.Contour.HasCauchyPVAt.cauchyPVAt_eq {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ L : ℂ} (h : HasCauchyPVAt γ a b f z₀ L) : cauchyPVAt γ a b f z₀ = L

If HasCauchyPVAt γ a b f z₀ L, then cauchyPVAt γ a b f z₀ = L: the value function reads off the limit whenever it exists.

theorem TauCeti.Contour.HasCauchyPVAt.unique {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ L₁ L₂ : ℂ} (h₁ : HasCauchyPVAt γ a b f z₀ L₁) (h₂ : HasCauchyPVAt γ a b f z₀ L₂) : L₁ = L₂

The value of the Cauchy principal value at z₀ is unique.

theorem TauCeti.Contour.CauchyPVExistsAt.hasCauchyPVAt_cauchyPVAt {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} (h : CauchyPVExistsAt γ a b f z₀) : HasCauchyPVAt γ a b f z₀ (cauchyPVAt γ a b f z₀)

If the principal value exists, it holds at the canonical value cauchyPVAt. This recovers a HasCauchyPVAt statement from mere existence, as the winding-number value definition needs.

theorem TauCeti.Contour.HasCauchyPVAt.congr_along_curve {γ : ℝ → ℂ} {a b : ℝ} {f g : ℂ → ℂ} {z₀ L : ℂ} (h : HasCauchyPVAt γ a b f z₀ L) (h_eq : ∀ t ∈ Set.uIoo a b, f (γ t) = g (γ t)) : HasCauchyPVAt γ a b g z₀ L

The principal value depends on the integrand only through its values along γ on the open interval between a and b: if f = g on the image of γ restricted to Set.uIoo a b, their principal values agree (endpoint values are invisible to the interval integral).

theorem TauCeti.Contour.cauchyPVAt_congr_along_curve {γ : ℝ → ℂ} {a b : ℝ} {f g : ℂ → ℂ} {z₀ : ℂ} (h_eq : ∀ t ∈ Set.uIoo a b, f (γ t) = g (γ t)) : cauchyPVAt γ a b f z₀ = cauchyPVAt γ a b g z₀

Value form of HasCauchyPVAt.congr_along_curve: the raw cauchyPVAt value only depends on the integrand along γ on the open interval between a and b.

theorem TauCeti.Contour.HasCauchyPVAt.congr_curve_ae {γ₁ γ₂ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ L : ℂ} (h : HasCauchyPVAt γ₁ a b f z₀ L) (h_eq : γ₁ =ᵐ[MeasureTheory.volume.restrict (Set.uIoc a b)] γ₂) (h_deriv : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.uIoc a b), γ₁ t ≠ z₀ → deriv γ₁ t = deriv γ₂ t) : HasCauchyPVAt γ₂ a b f z₀ L

The principal value depends on the curve only up to null sets. If γ₁ and γ₂ agree almost everywhere on the integration interval, and their derivatives agree almost everywhere where the curve misses z₀, their contour principal values agree.

Derivative agreement is only needed off z₀: the ε-truncation deletes the integrand wherever ‖γ t - z₀‖ ≤ ε, so for the positive ε the principal value ranges over, a point with γ₁ t = z₀ contributes 0 whatever the derivative there is. Curve agreement alone is still not enough — the integrand contains deriv γ.

theorem TauCeti.Contour.HasCauchyPVAt.congr_curve {γ₁ γ₂ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ L : ℂ} (h : HasCauchyPVAt γ₁ a b f z₀ L) (h_eq : Set.EqOn γ₁ γ₂ (Set.uIoo a b)) : HasCauchyPVAt γ₂ a b f z₀ L

The principal value depends on the curve only through its values on the open interval between a and b. Agreement on the open interval is enough even though the integrand involves deriv γ, because an open set is a neighbourhood of each of its points (Set.EqOn.deriv), and the endpoints are invisible to the interval integral.

theorem TauCeti.Contour.CauchyPVExistsAt.congr_curve_ae {γ₁ γ₂ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} (h : CauchyPVExistsAt γ₁ a b f z₀) (h_eq : γ₁ =ᵐ[MeasureTheory.volume.restrict (Set.uIoc a b)] γ₂) (h_deriv : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.uIoc a b), γ₁ t ≠ z₀ → deriv γ₁ t = deriv γ₂ t) : CauchyPVExistsAt γ₂ a b f z₀

Existence form of HasCauchyPVAt.congr_curve_ae.

theorem TauCeti.Contour.CauchyPVExistsAt.congr_curve {γ₁ γ₂ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} (h : CauchyPVExistsAt γ₁ a b f z₀) (h_eq : Set.EqOn γ₁ γ₂ (Set.uIoo a b)) : CauchyPVExistsAt γ₂ a b f z₀

Existence form of HasCauchyPVAt.congr_curve.

theorem TauCeti.Contour.cauchyPVAt_congr_curve_ae {γ₁ γ₂ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} (h_eq : γ₁ =ᵐ[MeasureTheory.volume.restrict (Set.uIoc a b)] γ₂) (h_deriv : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.uIoc a b), γ₁ t ≠ z₀ → deriv γ₁ t = deriv γ₂ t) : cauchyPVAt γ₁ a b f z₀ = cauchyPVAt γ₂ a b f z₀

Value form of HasCauchyPVAt.congr_curve_ae: the raw cauchyPVAt value is unchanged when the curves agree almost everywhere on the integration interval and their derivatives agree almost everywhere where the curve misses z₀. Curve equality alone does not suffice — the integrand contains deriv γ.

theorem TauCeti.Contour.cauchyPVAt_congr_curve {γ₁ γ₂ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} (h_eq : Set.EqOn γ₁ γ₂ (Set.uIoo a b)) : cauchyPVAt γ₁ a b f z₀ = cauchyPVAt γ₂ a b f z₀

Value form of HasCauchyPVAt.congr_curve.

theorem TauCeti.Contour.HasCauchyPVAt.const_mul {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ L : ℂ} (h : HasCauchyPVAt γ a b f z₀ L) (c : ℂ) : HasCauchyPVAt γ a b (fun (z : ℂ) => c * f z) z₀ (c * L)

Scalar multiplication: if the principal value of f is L, that of c • f is c • L.

theorem TauCeti.Contour.HasCauchyPVAt.add {γ : ℝ → ℂ} {a b : ℝ} {f g : ℂ → ℂ} {z₀ L₁ L₂ : ℂ} (hf : HasCauchyPVAt γ a b f z₀ L₁) (hg : HasCauchyPVAt γ a b g z₀ L₂) : HasCauchyPVAt γ a b (fun (z : ℂ) => f z + g z) z₀ (L₁ + L₂)

Additivity: the principal values of f and g add to that of f + g. Together with HasCauchyPVAt.const_mul this is the ℂ-linearity of the principal value in the integrand.

theorem TauCeti.Contour.HasCauchyPVAt.zero {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} : HasCauchyPVAt γ a b (fun (x : ℂ) => 0) z₀ 0

The principal value of the zero integrand is 0 — the additive identity for HasCauchyPVAt.add.

@[simp]

theorem TauCeti.Contour.cauchyPVAt_zero {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} : cauchyPVAt γ a b (fun (x : ℂ) => 0) z₀ = 0

The value form of HasCauchyPVAt.zero: the principal value of the zero integrand is 0.

theorem TauCeti.Contour.HasCauchyPVAt.refl (γ : ℝ → ℂ) (a : ℝ) (f : ℂ → ℂ) (z₀ : ℂ) : HasCauchyPVAt γ a a f z₀ 0

The Cauchy principal value at a single point over a zero-length interval is 0.

theorem TauCeti.Contour.HasCauchyPVAt.of_eq (γ : ℝ → ℂ) {a b : ℝ} (hab : a = b) (f : ℂ → ℂ) (z₀ : ℂ) : HasCauchyPVAt γ a b f z₀ 0

If the two endpoints are equal, the single-point Cauchy principal value is 0.

theorem TauCeti.Contour.CauchyPVExistsAt.refl (γ : ℝ → ℂ) (a : ℝ) (f : ℂ → ℂ) (z₀ : ℂ) : CauchyPVExistsAt γ a a f z₀

Existence form of HasCauchyPVAt.refl: a zero-length interval always has a single-point Cauchy principal value.

theorem TauCeti.Contour.CauchyPVExistsAt.of_eq (γ : ℝ → ℂ) {a b : ℝ} (hab : a = b) (f : ℂ → ℂ) (z₀ : ℂ) : CauchyPVExistsAt γ a b f z₀

Existence form of HasCauchyPVAt.of_eq.

@[simp]

theorem TauCeti.Contour.cauchyPVAt_same (γ : ℝ → ℂ) (a : ℝ) (f : ℂ → ℂ) (z₀ : ℂ) : cauchyPVAt γ a a f z₀ = 0

Value form of HasCauchyPVAt.refl: the single-point Cauchy principal value on [a, a] is 0.

theorem TauCeti.Contour.cauchyPVAt_eq_zero_of_eq (γ : ℝ → ℂ) {a b : ℝ} (hab : a = b) (f : ℂ → ℂ) (z₀ : ℂ) : cauchyPVAt γ a b f z₀ = 0

Value form of HasCauchyPVAt.of_eq.

theorem TauCeti.Contour.HasCauchyPVAt.sum {ι : Type u_1} {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} {f : ι → ℂ → ℂ} {L : ι → ℂ} {s : Finset ι} (h : ∀ i ∈ s, HasCauchyPVAt γ a b (f i) z₀ (L i)) : HasCauchyPVAt γ a b (fun (z : ℂ) => ∑ i ∈ s, f i z) z₀ (∑ i ∈ s, L i)

Finite additivity. The principal value of a finite sum of integrands is the sum of their principal values. With HasCauchyPVAt.zero and HasCauchyPVAt.add this extends the ℂ-linearity of the principal value to finite sums, as the generalized residue theorem's residue sum needs.

theorem TauCeti.Contour.HasCauchyPVAt.of_avoidance {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} (h_cont : ContinuousOn γ (Set.uIcc a b)) (h_avoid : ∀ t ∈ Set.uIcc a b, γ t ≠ z₀) (hf_int : IntervalIntegrable (fun (t : ℝ) => f (γ t) * deriv γ t) MeasureTheory.volume a b) : HasCauchyPVAt γ a b f z₀ (∫ (t : ℝ) in a..b, f (γ t) * deriv γ t)

Avoidance. If γ stays away from z₀ throughout [a, b] and the ordinary contour integrand is integrable there, the symmetric excision is eventually inert, so the principal value exists and equals the ordinary contour integral.

theorem TauCeti.Contour.HasCauchyPVAt.concat {γ : ℝ → ℂ} {a b c : ℝ} {f : ℂ → ℂ} {z₀ L₁ L₂ : ℂ} (h_ab : HasCauchyPVAt γ a b f z₀ L₁) (h_bc : HasCauchyPVAt γ b c f z₀ L₂) : HasCauchyPVAt γ a c f z₀ (L₁ + L₂)

Concatenation. The principal values along adjacent subcurves [a, b] and [b, c] add to the principal value along [a, c]. The integrability of the excised integrand across [a, c] and the additivity of the integral both follow from the two given principal values, so no ordering or separate integrability hypothesis is needed.

theorem TauCeti.Contour.HasCauchyPVAt.concat_range {γ : ℝ → ℂ} {f : ℂ → ℂ} {z₀ : ℂ} {n : ℕ} {t : ℕ → ℝ} {L : ℕ → ℂ} (h : ∀ k < n, HasCauchyPVAt γ (t k) (t (k + 1)) f z₀ (L k)) : HasCauchyPVAt γ (t 0) (t n) f z₀ (∑ k ∈ Finset.range n, L k)

Finite concatenation. If the principal value on every adjacent interval [t k, t (k + 1)] is L k, then the principal value on [t 0, t n] is their sum. The endpoints need not be ordered.

theorem TauCeti.Contour.cauchyPVExistsAt_of_dist_lower_bound {γ : ℝ → ℂ} {z₀ : ℂ} {f : ℂ → ℂ} {a b m : ℝ} (hm_pos : 0 < m) (h_far : ∀ t ∈ Set.uIcc a b, m ≤ ‖γ t - z₀‖) (h_int_tr : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), IntervalIntegrable (fun (t : ℝ) => if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0) MeasureTheory.volume a b) : CauchyPVExistsAt γ a b f z₀

Existence form of HasCauchyPVAt.of_dist_lower_bound.

theorem TauCeti.Contour.cauchyPVExistsAt_of_avoidance {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} (h_cont : ContinuousOn γ (Set.uIcc a b)) (h_avoid : ∀ t ∈ Set.uIcc a b, γ t ≠ z₀) (hf_int : IntervalIntegrable (fun (t : ℝ) => f (γ t) * deriv γ t) MeasureTheory.volume a b) : CauchyPVExistsAt γ a b f z₀

Existence form of HasCauchyPVAt.of_avoidance.

theorem TauCeti.Contour.CauchyPVExistsAt.const_mul {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} (h : CauchyPVExistsAt γ a b f z₀) (c : ℂ) : CauchyPVExistsAt γ a b (fun (z : ℂ) => c * f z) z₀

Existence-level scalar multiplication: scaling preserves existence of the principal value.

theorem TauCeti.Contour.CauchyPVExistsAt.add {γ : ℝ → ℂ} {a b : ℝ} {f g : ℂ → ℂ} {z₀ : ℂ} (hf : CauchyPVExistsAt γ a b f z₀) (hg : CauchyPVExistsAt γ a b g z₀) : CauchyPVExistsAt γ a b (fun (z : ℂ) => f z + g z) z₀

Existence-level additivity: existence of the principal values of f and g gives that of f + g.

theorem TauCeti.Contour.CauchyPVExistsAt.zero {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} : CauchyPVExistsAt γ a b (fun (x : ℂ) => 0) z₀

Existence-level: the zero integrand has a principal value.

theorem TauCeti.Contour.CauchyPVExistsAt.sum {ι : Type u_1} {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} {f : ι → ℂ → ℂ} {s : Finset ι} (h : ∀ i ∈ s, CauchyPVExistsAt γ a b (f i) z₀) : CauchyPVExistsAt γ a b (fun (z : ℂ) => ∑ i ∈ s, f i z) z₀

Existence-level finite additivity: if each summand has a principal value, so does the finite sum of integrands.

theorem TauCeti.Contour.HasCauchyPVAt.translate {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ L : ℂ} (h : HasCauchyPVAt γ a b f z₀ L) (c : ℂ) : HasCauchyPVAt (fun (t : ℝ) => γ t + c) a b (fun (z : ℂ) => f (z - c)) (z₀ + c) L

Simultaneously translating the curve and the excision point preserves a single-point Cauchy principal value, provided the integrand is translated back by the same amount.

theorem TauCeti.Contour.CauchyPVExistsAt.translate {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} (h : CauchyPVExistsAt γ a b f z₀) (c : ℂ) : CauchyPVExistsAt (fun (t : ℝ) => γ t + c) a b (fun (z : ℂ) => f (z - c)) (z₀ + c)

Existence form of HasCauchyPVAt.translate: simultaneous translation preserves existence of a single-point Cauchy principal value.

theorem TauCeti.Contour.cauchyPVAt_translate {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} (c : ℂ) : cauchyPVAt (fun (t : ℝ) => γ t + c) a b (fun (z : ℂ) => f (z - c)) (z₀ + c) = cauchyPVAt γ a b f z₀

Value form of HasCauchyPVAt.translate: simultaneous translation preserves the single-point Cauchy principal value.

theorem TauCeti.Contour.HasCauchyPVAt.const_mul_curve {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ L : ℂ} (h : HasCauchyPVAt γ a b f z₀ L) {c : ℂ} (hc : c ≠ 0) : HasCauchyPVAt (fun (t : ℝ) => c * γ t) a b (fun (z : ℂ) => c⁻¹ * f (c⁻¹ * z)) (c * z₀) L

Simultaneously scaling the curve and the excision point by a nonzero complex number c preserves a single-point Cauchy principal value, provided the integrand is rescaled by z ↦ c⁻¹ * f (c⁻¹ * z): the excision radius rescales by ‖c‖ and, after this rescaling, the two truncated integrands agree along the scaled curve.

theorem TauCeti.Contour.CauchyPVExistsAt.const_mul_curve {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} (h : CauchyPVExistsAt γ a b f z₀) {c : ℂ} (hc : c ≠ 0) : CauchyPVExistsAt (fun (t : ℝ) => c * γ t) a b (fun (z : ℂ) => c⁻¹ * f (c⁻¹ * z)) (c * z₀)

Existence form of HasCauchyPVAt.const_mul_curve: nonzero scaling of the curve and excision point preserves existence of a single-point Cauchy principal value.

theorem TauCeti.Contour.cauchyPVAt_const_mul_curve {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ c : ℂ} (hc : c ≠ 0) : cauchyPVAt (fun (t : ℝ) => c * γ t) a b (fun (z : ℂ) => c⁻¹ * f (c⁻¹ * z)) (c * z₀) = cauchyPVAt γ a b f z₀

Value form of HasCauchyPVAt.const_mul_curve: simultaneous nonzero scaling of the curve and the excision point preserves the raw single-point Cauchy principal value, with no existence hypothesis. Scaling only reindexes the excision radius by the order-isomorphism ε ↦ ε / ‖c‖, which fixes the filter 𝓝[>] 0, so the underlying limUnder is unchanged even when it does not converge.

theorem TauCeti.Contour.HasCauchyPVAt.symm {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ L : ℂ} (h : HasCauchyPVAt γ a b f z₀ L) : HasCauchyPVAt γ b a f z₀ (-L)

Reversing the interval orientation negates a single-point Cauchy principal value.

theorem TauCeti.Contour.CauchyPVExistsAt.symm {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} (h : CauchyPVExistsAt γ a b f z₀) : CauchyPVExistsAt γ b a f z₀

Existence of a single-point Cauchy principal value is invariant under reversing the interval orientation.

theorem TauCeti.Contour.cauchyPVAt_symm {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} (h : CauchyPVExistsAt γ a b f z₀) : cauchyPVAt γ b a f z₀ = -cauchyPVAt γ a b f z₀

Value form of HasCauchyPVAt.symm: if the single-point principal value exists on [a, b], then the value on [b, a] is its negative.

theorem TauCeti.Contour.CauchyPVExistsAt.concat {γ : ℝ → ℂ} {a b c : ℝ} {f : ℂ → ℂ} {z₀ : ℂ} (h_ab : CauchyPVExistsAt γ a b f z₀) (h_bc : CauchyPVExistsAt γ b c f z₀) : CauchyPVExistsAt γ a c f z₀

Existence form of HasCauchyPVAt.concat.

theorem TauCeti.Contour.CauchyPVExistsAt.concat_range {γ : ℝ → ℂ} {f : ℂ → ℂ} {z₀ : ℂ} {n : ℕ} {t : ℕ → ℝ} (h : ∀ k < n, CauchyPVExistsAt γ (t k) (t (k + 1)) f z₀) : CauchyPVExistsAt γ (t 0) (t n) f z₀

Existence form of HasCauchyPVAt.concat_range: existence on every adjacent interval of a finite partition gives existence on the whole interval.

theorem TauCeti.Contour.cauchyPVAt_concat_range {γ : ℝ → ℂ} {f : ℂ → ℂ} {z₀ : ℂ} {n : ℕ} {t : ℕ → ℝ} (h : ∀ k < n, CauchyPVExistsAt γ (t k) (t (k + 1)) f z₀) : cauchyPVAt γ (t 0) (t n) f z₀ = ∑ k ∈ Finset.range n, cauchyPVAt γ (t k) (t (k + 1)) f z₀

Value form of HasCauchyPVAt.concat_range: the canonical principal value on a finite partition is the sum of its canonical values on the adjacent intervals.