The Cauchy principal value of a contour integral on a set (Hungerbühler–Wasem)

For a curve γ : ℝ → ℂ on [a, b] and an integrand f : ℂ → ℂ, this file defines the Cauchy principal value of the contour integral ∮_γ f excising a symmetric ε-ball about each point of a finite singular set simultaneously: HasCauchyPV γ a b f v says there is a finite set S ⊆ ℂ for which the truncated integrand along γ over [a, b], zeroed within ε of any point of S, is eventually IntervalIntegrable and its integral tends to v as ε → 0⁺.

This is the set-level (…On) companion of HasCauchyPVAt (CauchyPrincipalValue.lean), which excises a single prescribed point z₀; the naming mirrors Mathlib's MeromorphicAt (at a point) versus MeromorphicOn (on a set). The finite excision set S is bound existentially, so the predicate is intrinsic to (γ, f) and stays faithful to the roadmap's S-free signature: it holds when some finite set satisfies the two clauses. A prescribed set — for instance the pole set of the generalized residue theorem, with intended value 2πi · ∑_{s ∈ S} n_γ(s) · res f s — can be used as the witness once its integrability and Tendsto clauses have been proved. Enlarging a witness leaves the limit unchanged, so the value is well-defined (HasCauchyPV.unique), named by cauchyPV; this file does not prove that any particular set satisfies the clauses.

As with HasCauchyPVAt, the predicate carries a truncated-integrability clause alongside the Tendsto clause. Without it the Tendsto clause alone would be met vacuously by integrands 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 an on-curve singularity), never silently identifying the two.

Main definitions

• HasCauchyPVWith γ a b f S v — the same with the excision set S prescribed; the form that concatenates, since adjacent subcurves must share it (PrincipalValue/Concat.lean)
• HasCauchyPV γ a b f v — some finite excision set makes the truncated integrals converge to v (the primary predicate).
• CauchyPVExists γ a b f — the principal value exists (∃ v, HasCauchyPV γ a b f v).

Main results

• hasCauchyPV_iff, cauchyPVExists_iff — restate the predicates as their defining existentials, so consumers can characterize them without unfolding the definitions.
• HasCauchyPV.intro builds the predicate from a witnessing set S and its two clauses, while CauchyPVExists.intro builds existence from a HasCauchyPV witness.
• HasCauchyPVAt.hasCauchyPV, CauchyPVExistsAt.cauchyPVExists — the single-point principal value at z₀ is the set-level principal value with S = {z₀}: the excision ‖γ t − z₀‖ > ε is exactly the S = {z₀} case of the set excision.
• HasCauchyPVWith.of_integrable_of_crossings_measure_zero and its finite-crossings wrapper HasCauchyPVWith.of_integrable_of_finite_crossings — where the integrand is integrable and the curve meets the excised points on a null set of parameters (in particular, finitely often), the principal value is the ordinary integral for any prescribed excision set
• HasCauchyPV.of_integrable — if the ordinary contour integrand is interval-integrable, the empty excision witnesses that the principal value is the ordinary integral (as when no on-curve singularity of f obstructs integrability).
• HasCauchyPV.zero, HasCauchyPV.const_mul, HasCauchyPV.congr_along_curve (and their CauchyPVExists forms) — the excision-set-preserving operations: the zero integrand, scaling by a constant, and replacing f by a function agreeing with it along γ; these need no change of the witnessing set.
• HasCauchyPV.unique, cauchyPV, HasCauchyPV.cauchyPV_eq, cauchyPV_zero, CauchyPVExists.hasCauchyPV_cauchyPV — the value is well-defined (independent of the witnessing set), so cauchyPV γ a b f names it (junk value 0 when none exists).
• HasCauchyPV.symm, CauchyPVExists.symm, cauchyPV_symm — reversing the interval orientation negates the set-level principal value.
• HasCauchyPV.add, HasCauchyPV.sum (and their CauchyPVExists forms) — additivity in f; reconciling the summands' different excision sets on their union needs the curve continuous on [[a, b]], unlike the excision-set-preserving operations above.

Provenance

Migrated and adapted from the AINTLIB LeanModularForms project (the multi-point principal value CauchyPrincipalValueExistsOn), specialised to the raw-function (γ : ℝ → ℂ on [a, b]) design of the contour-integration roadmap, with the singular set bound existentially and the truncated-integrability clause added.

References

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

def TauCeti.Contour.HasCauchyPVWith (γ : ℝ → ℂ) (a b : ℝ) (f : ℂ → ℂ) (S : Finset ℂ) (v : ℂ) : Prop

The Cauchy principal value with a prescribed excision set. Identical to HasCauchyPV except that the finite set S of excised points is an explicit parameter rather than existentially bound, which is what makes the principal values along adjacent subcurves concatenable.

Equations

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

theorem TauCeti.Contour.hasCauchyPVWith_iff {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {S : Finset ℂ} {v : ℂ} : HasCauchyPVWith γ a b f S v ↔ (∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ S, ‖γ t - s‖ ≤ ε then 0 else f (γ t) * deriv γ t) MeasureTheory.volume a b) ∧ Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ∃ s ∈ S, ‖γ t - s‖ ≤ ε then 0 else f (γ t) * deriv γ t) (nhdsWithin 0 (Set.Ioi 0)) (nhds v)

HasCauchyPVWith unfolded into its two clauses — eventual integrability of the excised integrand and convergence of the excised integrals — so consumers need not unfold the definition.

def TauCeti.Contour.HasCauchyPV (γ : ℝ → ℂ) (a b : ℝ) (f : ℂ → ℂ) (v : ℂ) : Prop

The Cauchy principal value on a set of the contour integral ∮_γ f exists with value v: there is a finite set S ⊆ ℂ such that the truncated integrand along γ over [a, b], zeroed within a symmetric ε-ball of any point of S, is eventually IntervalIntegrable and its integral tends to v as ε → 0⁺. The set is existential so the predicate stays S-free, intrinsic to (γ, f); 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. Set-level companion of HasCauchyPVAt (raw γ : ℝ → ℂ, [a, b]).

Equations

• TauCeti.Contour.HasCauchyPV γ a b f v = ∃ (S : Finset ℂ), TauCeti.Contour.HasCauchyPVWith γ a b f S v

theorem TauCeti.Contour.hasCauchyPV_iff {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {v : ℂ} : HasCauchyPV γ a b f v ↔ ∃ (S : Finset ℂ), (∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ S, ‖γ t - s‖ ≤ ε then 0 else f (γ t) * deriv γ t) MeasureTheory.volume a b) ∧ Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ∃ s ∈ S, ‖γ t - s‖ ≤ ε then 0 else f (γ t) * deriv γ t) (nhdsWithin 0 (Set.Ioi 0)) (nhds v)

Restatement of HasCauchyPV as the existence of a finite excision set making the excised integrand eventually integrable and its integrals convergent, so consumers can characterize the predicate without unfolding its definition.

theorem TauCeti.Contour.HasCauchyPV.intro {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {v : ℂ} (S : Finset ℂ) (h_int : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), IntervalIntegrable (fun (t : ℝ) => if ∃ s ∈ S, ‖γ t - s‖ ≤ ε then 0 else f (γ t) * deriv γ t) MeasureTheory.volume a b) (h_tendsto : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ∃ s ∈ S, ‖γ t - s‖ ≤ ε then 0 else f (γ t) * deriv γ t) (nhdsWithin 0 (Set.Ioi 0)) (nhds v)) : HasCauchyPV γ a b f v

Constructor for HasCauchyPV from a witnessing finite set S and its two clauses — eventual integrability of the S-excised integrand and convergence of the excised integrals — without unfolding the definition.

theorem TauCeti.Contour.HasCauchyPVWith.hasCauchyPV {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {S : Finset ℂ} {v : ℂ} (h : HasCauchyPVWith γ a b f S v) : HasCauchyPV γ a b f v

Forgetting the witness recovers the existentially-bound form.

theorem TauCeti.Contour.hasCauchyPV_iff_exists_hasCauchyPVWith {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {v : ℂ} : HasCauchyPV γ a b f v ↔ ∃ (S : Finset ℂ), HasCauchyPVWith γ a b f S v

HasCauchyPV is exactly HasCauchyPVWith with the excision set existentially quantified.

This is the abstraction-preserving bridge between the two forms, and is not redundant with the definition: under the module system HasCauchyPV's body is not exposed outside this file, so Iff.rfl proves this only here and consumers elsewhere cannot unfold their way across. The sibling hasCauchyPV_iff expands the truncation body instead, which loses the abstraction.

def TauCeti.Contour.CauchyPVExists (γ : ℝ → ℂ) (a b : ℝ) (f : ℂ → ℂ) : Prop

The Cauchy principal value on a set exists: shorthand for ∃ v, HasCauchyPV γ a b f v.

Equations

• TauCeti.Contour.CauchyPVExists γ a b f = ∃ (v : ℂ), TauCeti.Contour.HasCauchyPV γ a b f v

theorem TauCeti.Contour.cauchyPVExists_iff {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} : CauchyPVExists γ a b f ↔ ∃ (v : ℂ), HasCauchyPV γ a b f v

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

theorem TauCeti.Contour.CauchyPVExists.intro {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {v : ℂ} (h : HasCauchyPV γ a b f v) : CauchyPVExists γ a b f

Constructor for CauchyPVExists from a HasCauchyPV witness.

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

From a point to a set. The single-point principal value at z₀ is the set-level principal value with S = {z₀}: the single-point excision ‖γ t − z₀‖ > ε (keep) is exactly the negation of the set excision ∃ s ∈ {z₀}, ‖γ t − s‖ ≤ ε (zero).

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

Existence form of HasCauchyPVAt.hasCauchyPV: if the single-point principal value at z₀ exists, so does the set-level principal value.

theorem TauCeti.Contour.HasCauchyPV.of_integrable {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} (hf_int : IntervalIntegrable (fun (t : ℝ) => f (γ t) * deriv γ t) MeasureTheory.volume a b) : HasCauchyPV γ a b f (∫ (t : ℝ) in a..b, f (γ t) * deriv γ t)

Integrable integrand. If the ordinary contour integrand t ↦ f (γ t) · γ'(t) is IntervalIntegrable on [a, b], then the empty excision (S = ∅) is inert, so the principal value exists and equals the ordinary contour integral ∫_a^b f (γ t) · γ'(t) dt.

theorem TauCeti.Contour.HasCauchyPVWith.of_integrable_of_crossings_measure_zero {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} (S : Finset ℂ) (hγ : AEMeasurable γ (MeasureTheory.volume.restrict (Set.uIoc a b))) (h_int : IntervalIntegrable (fun (t : ℝ) => f (γ t) * deriv γ t) MeasureTheory.volume a b) (h_null : MeasureTheory.volume (⋃ s ∈ S, Set.uIoc a b ∩ γ ⁻¹' {s}) = 0) : HasCauchyPVWith γ a b f S (∫ (t : ℝ) in a..b, f (γ t) * deriv γ t)

An integrable integrand has principal value the ordinary integral, for any prescribed excision set. Where the contour integrand is interval-integrable and the curve meets the excised points only on a null set of parameters, shrinking the excised neighbourhoods recovers the ordinary integral: for each fixed ε the excision may perturb the integrand on a set of positive measure, but as ε → 0⁺ the excised integrands converge almost everywhere to the original one, since the limiting crossing set is null.

The strength here is that S is arbitrary: the conclusion holds for whatever excision set another principal value happens to be witnessed by, which is what lets an arc carrying no singularity be subtracted off via HasCauchyPVWith.sub_right without knowing that witness. Compare HasCauchyPV.of_integrable, which proves the weaker existential form by exhibiting S = ∅.

theorem TauCeti.Contour.HasCauchyPVWith.of_integrable_of_finite_crossings {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} (S : Finset ℂ) (hγ : AEMeasurable γ (MeasureTheory.volume.restrict (Set.uIoc a b))) (h_int : IntervalIntegrable (fun (t : ℝ) => f (γ t) * deriv γ t) MeasureTheory.volume a b) (h_fin : ∀ s ∈ S, (Set.uIoc a b ∩ γ ⁻¹' {s}).Finite) : HasCauchyPVWith γ a b f S (∫ (t : ℝ) in a..b, f (γ t) * deriv γ t)

Finite-crossings form of HasCauchyPVWith.of_integrable_of_crossings_measure_zero: a curve meeting each excised point only finitely often meets them on a null set of parameters. This is the form contour arguments consume: IsPwC1ImmersionOn.finite_crossings (HW Prop 2.2) supplies finiteness on the closed interval, from which this follows by Set.Finite.subset along Set.uIoc_subset_uIcc.

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

Zero integrand. The principal value of the zero integrand is 0, witnessed by the empty excision: the truncated integrand is identically 0, hence integrable with vanishing integral.

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

Scaling by a constant. Scaling the integrand by c : ℂ scales the principal value by c, reusing the same excision set: the truncation and the integral both commute with multiplication by the constant c.

theorem TauCeti.Contour.HasCauchyPVWith.congr_curve {γ₁ γ₂ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {S : Finset ℂ} {v : ℂ} (h : HasCauchyPVWith γ₁ a b f S v) (h_eq : Set.EqOn γ₁ γ₂ (Set.uIoo a b)) : HasCauchyPVWith γ₂ a b f S v

Changing the curve. Two curves that agree on the open parameter interval have the same principal value: both the excision test ‖γ t - s‖ ≤ ε and the integrand f (γ t) * deriv γ t are computed pointwise from the curve, the derivatives agree automatically because the interval is open, and the endpoints do not affect an interval integral.

This is what lets a contour identity be restated along a more convenient parametrization — for instance replacing a piece of a closed contour by the straight line it traces.

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

Curve congruence for the primary predicate: HasCauchyPVWith.congr_curve with the excision set re-hidden, so consumers need not name it.

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

Existence form of HasCauchyPV.congr_curve.

theorem TauCeti.Contour.HasCauchyPV.congr_along_curve {γ : ℝ → ℂ} {a b : ℝ} {f g : ℂ → ℂ} {v : ℂ} (h : HasCauchyPV γ a b f v) (hfg : ∀ t ∈ Set.uIoo a b, f (γ t) = g (γ t)) : HasCauchyPV γ a b g v

Congruence along the curve. If f and g agree along γ on the open interval Set.uIoo a b, they share the same principal value there, with the same excision set (the endpoints are invisible to the interval integral; the excised integrand reads f only through f (γ t)).

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

Existence form of HasCauchyPV.zero: the principal value of the zero integrand exists.

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

Existence form of HasCauchyPV.const_mul: if the principal value of f exists, so does that of fun z => c * f z.

theorem TauCeti.Contour.CauchyPVExists.congr_along_curve {γ : ℝ → ℂ} {a b : ℝ} {f g : ℂ → ℂ} (h : CauchyPVExists γ a b f) (hfg : ∀ t ∈ Set.uIoo a b, f (γ t) = g (γ t)) : CauchyPVExists γ a b g

Existence form of HasCauchyPV.congr_along_curve: agreement along γ on Set.uIoo a b transports existence of the principal value from f to g.

theorem TauCeti.Contour.HasCauchyPV.unique {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {v₁ v₂ : ℂ} (h₁ : HasCauchyPV γ a b f v₁) (h₂ : HasCauchyPV γ a b f v₂) : v₁ = v₂

Uniqueness of the set-level principal value. Any two values of the Cauchy principal value on a set coincide. Unlike the single-point case, the two witnesses may use different finite excision sets; enlargement inertness (tendsto_integral_truncatedIntegrand_sub) shows the difference of their truncated integrals vanishes in the limit, so the two limits agree.

noncomputable def TauCeti.Contour.cauchyPV (γ : ℝ → ℂ) (a b : ℝ) (f : ℂ → ℂ) : ℂ

The value of the set-level Cauchy principal value: the common limit when it exists, and the junk value 0 otherwise. Read it off a HasCauchyPV witness via HasCauchyPV.cauchyPV_eq.

Equations

• TauCeti.Contour.cauchyPV γ a b f = if h : ∃ (v : ℂ), TauCeti.Contour.HasCauchyPV γ a b f v then h.choose else 0

theorem TauCeti.Contour.HasCauchyPV.cauchyPV_eq {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {v : ℂ} (h : HasCauchyPV γ a b f v) : cauchyPV γ a b f = v

If HasCauchyPV γ a b f v, then cauchyPV γ a b f = v: the value function reads off the principal value whenever it exists, by uniqueness.

theorem TauCeti.Contour.cauchyPV_congr_curve {γ₁ γ₂ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} (h_eq : Set.EqOn γ₁ γ₂ (Set.uIoo a b)) : cauchyPV γ₁ a b f = cauchyPV γ₂ a b f

Value form of HasCauchyPV.congr_curve: curves agreeing on the open parameter interval have the same principal value, whether or not it exists (both sides are 0 when it does not).

@[simp]

theorem TauCeti.Contour.cauchyPV_zero {γ : ℝ → ℂ} {a b : ℝ} : (cauchyPV γ a b fun (x : ℂ) => 0) = 0

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

theorem TauCeti.Contour.HasCauchyPV.refl (γ : ℝ → ℂ) (a : ℝ) (f : ℂ → ℂ) : HasCauchyPV γ a a f 0

The set-level Cauchy principal value over a zero-length interval is 0.

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

If the two endpoints are equal, the set-level Cauchy principal value is 0.

theorem TauCeti.Contour.CauchyPVExists.refl (γ : ℝ → ℂ) (a : ℝ) (f : ℂ → ℂ) : CauchyPVExists γ a a f

Existence form of HasCauchyPV.refl: a zero-length interval always has a set-level Cauchy principal value.

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

Existence form of HasCauchyPV.of_eq.

@[simp]

theorem TauCeti.Contour.cauchyPV_same (γ : ℝ → ℂ) (a : ℝ) (f : ℂ → ℂ) : cauchyPV γ a a f = 0

Value form of HasCauchyPV.refl: the set-level Cauchy principal value on [a, a] is 0.

theorem TauCeti.Contour.cauchyPV_eq_zero_of_eq (γ : ℝ → ℂ) {a b : ℝ} (hab : a = b) (f : ℂ → ℂ) : cauchyPV γ a b f = 0

Value form of HasCauchyPV.of_eq.

theorem TauCeti.Contour.CauchyPVExists.hasCauchyPV_cauchyPV {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} (h : CauchyPVExists γ a b f) : HasCauchyPV γ a b f (cauchyPV γ a b f)

If the set-level principal value exists, it holds at the canonical value cauchyPV. This recovers a HasCauchyPV statement from mere existence.

theorem TauCeti.Contour.HasCauchyPV.symm {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} {v : ℂ} (h : HasCauchyPV γ a b f v) : HasCauchyPV γ b a f (-v)

Reversing the interval orientation negates a set-level Cauchy principal value.

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

Existence of a set-level Cauchy principal value is invariant under reversing the interval orientation.

theorem TauCeti.Contour.cauchyPV_symm {γ : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ} (h : CauchyPVExists γ a b f) : cauchyPV γ b a f = -cauchyPV γ a b f

Value form of HasCauchyPV.symm: if the set-level principal value exists on [a, b], then the value on [b, a] is its negative.

theorem TauCeti.Contour.HasCauchyPV.add {γ : ℝ → ℂ} {a b : ℝ} {f₁ f₂ : ℂ → ℂ} {v₁ v₂ : ℂ} (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (h₁ : HasCauchyPV γ a b f₁ v₁) (h₂ : HasCauchyPV γ a b f₂ v₂) : HasCauchyPV γ a b (fun (z : ℂ) => f₁ z + f₂ z) (v₁ + v₂)

Additivity. The set-level principal value is additive: if f₁ and f₂ each have a principal value along γ, so does f₁ + f₂, with the sum as value. The summands may excise different finite sets, reconciled on the union S₁ ∪ S₂; this needs the curve continuous on [[a, b]], unlike const_mul, which reuses a single excision set.

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

Finite additivity. A finite sum of set-level principal values is the principal value of the summed integrand — the additive companion to HasCauchyPV.const_mul, built from zero and add (hence the curve-continuity hypothesis).

theorem TauCeti.Contour.HasCauchyPV.congr_along_curve_off {γ : ℝ → ℂ} {a b : ℝ} {f g : ℂ → ℂ} {v : ℂ} (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (P : Finset ℂ) (h : HasCauchyPV γ a b f v) (h_eq : ∀ t ∈ Set.uIoo a b, γ t ∉ ↑P → f (γ t) = g (γ t)) : HasCauchyPV γ a b g v

Congruence along the curve off excised points: if f and g agree along γ at every parameter where γ avoids the finite set P, a principal value of f is one of g — the witnessing excision enlarges to include P, and off the enlarged excision the curve avoids P. Needs the curve continuous on [[a, b]] for the enlargement.

theorem TauCeti.Contour.CauchyPVExists.add {γ : ℝ → ℂ} {a b : ℝ} {f g : ℂ → ℂ} (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hf : CauchyPVExists γ a b f) (hg : CauchyPVExists γ a b g) : CauchyPVExists γ a b fun (z : ℂ) => f z + g z

Existence form of HasCauchyPV.add.

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

Existence form of HasCauchyPV.sum.