The Cauchy principal value along a contour cycle

A contour cycle is a formal integer combination of closed piecewise-C¹ curves, and every additive invariant of curves extends to it by linearity. This file carries out that extension for the set-level Cauchy principal value, the invariant the Hungerbühler–Wasem generalized residue theorem evaluates when singularities of the integrand lie on the contour.

The direction of the definitions is opposite to the single-curve case, and deliberately so. For one curve the predicate TauCeti.Contour.HasCauchyPV comes first — it is a genuine analytic statement about symmetric excision — and the value TauCeti.Contour.cauchyPV is read off it. For a cycle the value comes first: Cycle.cauchyPV f is the additive extension of TauCeti.Contour.cauchyPV, hence an AddMonoidHom by construction, exactly like Cycle.integral and Cycle.windingNumber. The predicate Cycle.HasCauchyPV is then existence along each curve of the canonical support together with that value. Defining the predicate first, by simultaneously truncating all the generators, would not have produced an additive value: a cancelling pair of generators would have to be seen to cancel truncation by truncation, which no argument supplies before the limit is taken.

Nothing here identifies a principal value with an ordinary integral. Where the ordinary contour integrand is interval-integrable along each generator, the two agree (Cycle.hasCauchyPV_integral), which is the only bridge between them.

Main definitions

• TauCeti.Contour.Cycle.cauchyPV — the additive extension of the single-curve principal value.
• TauCeti.Contour.Cycle.CauchyPVExists — the principal value exists along every curve of the canonical support.
• TauCeti.Contour.Cycle.HasCauchyPV — existence, together with the value.

Main results

• TauCeti.Contour.Cycle.cauchyPV_eq_sum_support — the value as a coefficient-weighted sum.
• TauCeti.Contour.Cycle.cauchyPVExists_iff — existence along the canonical support.
• TauCeti.Contour.Cycle.hasCauchyPV_iff — the predicate as its two clauses.
• TauCeti.Contour.Cycle.HasCauchyPV.of_generators — a per-generator family of principal values assembles into the cycle's.
• TauCeti.Contour.Cycle.HasCauchyPV.unique — the value in the predicate is determined.
• TauCeti.Contour.Cycle.hasCauchyPV_integral — where the contour integrand is interval-integrable along each generator, the principal value is the ordinary cycle integral.

References

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

noncomputable def TauCeti.Contour.Cycle.cauchyPV (f : ℂ → ℂ) : Cycle →+ ℂ

The Cauchy principal value of f along a cycle, obtained by additively extending the single-curve principal value TauCeti.Contour.cauchyPV from generators. Like every value read off a junk-valued function, it is meaningful exactly where Cycle.CauchyPVExists holds.

Equations

• TauCeti.Contour.Cycle.cauchyPV f = FreeAbelianGroup.lift fun (γ : TauCeti.Contour.PiecewiseC1ClosedCurve) => TauCeti.Contour.cauchyPV (Function.extend Subtype.val γ.toFun 0) γ.a γ.b f

@[simp]

theorem TauCeti.Contour.Cycle.cauchyPV_of (γ : PiecewiseC1ClosedCurve) (f : ℂ → ℂ) : (cauchyPV f) (FreeAbelianGroup.of γ) = Contour.cauchyPV (Function.extend Subtype.val γ.toFun 0) γ.a γ.b f

The principal value along a one-generator cycle is the principal value along that curve.

theorem TauCeti.Contour.Cycle.cauchyPV_of_raw {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) (f : ℂ → ℂ) : (cauchyPV f) (FreeAbelianGroup.of (PiecewiseC1ClosedCurve.of γ hγ hclosed)) = Contour.cauchyPV γ a b f

The principal value along a raw closed curve bundled as a one-generator cycle is its raw principal value.

theorem TauCeti.Contour.Cycle.cauchyPV_eq_sum_support (f : ℂ → ℂ) (C : Cycle) : (cauchyPV f) C = ∑ γ ∈ FreeAbelianGroup.support C, (FreeAbelianGroup.coeff γ) C • Contour.cauchyPV (Function.extend Subtype.val γ.toFun 0) γ.a γ.b f

The principal value along a cycle is the coefficient-weighted sum of the principal values along the curves of its canonical support.

def TauCeti.Contour.Cycle.CauchyPVExists (C : Cycle) (f : ℂ → ℂ) : Prop

The Cauchy principal value of f along a cycle exists when it exists along every curve of the canonical support. Curves that cancel out of the cycle impose no condition.

Equations

• C.CauchyPVExists f = ∀ γ ∈ FreeAbelianGroup.support C, TauCeti.Contour.CauchyPVExists (Function.extend Subtype.val γ.toFun 0) γ.a γ.b f

theorem TauCeti.Contour.Cycle.cauchyPVExists_iff {f : ℂ → ℂ} {C : Cycle} : C.CauchyPVExists f ↔ ∀ γ ∈ FreeAbelianGroup.support C, Contour.CauchyPVExists (Function.extend Subtype.val γ.toFun 0) γ.a γ.b f

Characterization of Cycle.CauchyPVExists as existence along every curve of the canonical support — the eliminator/constructor interface, so downstream users need not unfold the definition.

def TauCeti.Contour.Cycle.HasCauchyPV (C : Cycle) (f : ℂ → ℂ) (v : ℂ) : Prop

The Cauchy principal value of f along the cycle C exists and equals v.

Equations

• C.HasCauchyPV f v = (C.CauchyPVExists f ∧ (TauCeti.Contour.Cycle.cauchyPV f) C = v)

theorem TauCeti.Contour.Cycle.hasCauchyPV_iff {f : ℂ → ℂ} {C : Cycle} {v : ℂ} : C.HasCauchyPV f v ↔ C.CauchyPVExists f ∧ (cauchyPV f) C = v

Cycle.HasCauchyPV unfolded into its two clauses — existence along every curve of the canonical support, and the value — so consumers need not unfold the definition.

Deliberately not @[simp]: it unfolds the predicate, so it would take the left-hand sides of hasCauchyPV_of_iff, hasCauchyPV_zero and hasCauchyPV_neg_iff out of simp-normal form. Those three are the normal forms simp should reach for — on a generator, on 0, and under negation — and they carry the @[simp] annotation instead.

@[simp]

theorem TauCeti.Contour.Cycle.cauchyPVExists_of_iff {f : ℂ → ℂ} (γ : PiecewiseC1ClosedCurve) : CauchyPVExists (FreeAbelianGroup.of γ) f ↔ Contour.CauchyPVExists (Function.extend Subtype.val γ.toFun 0) γ.a γ.b f

Existence of the principal value along a one-generator cycle is exactly existence along its generating curve.

@[simp]

theorem TauCeti.Contour.Cycle.hasCauchyPV_of_iff {f : ℂ → ℂ} (γ : PiecewiseC1ClosedCurve) {v : ℂ} : HasCauchyPV (FreeAbelianGroup.of γ) f v ↔ Contour.HasCauchyPV (Function.extend Subtype.val γ.toFun 0) γ.a γ.b f v

A one-generator cycle has principal value v exactly when its generating curve does.

theorem TauCeti.Contour.Cycle.HasCauchyPV.cauchyPV_eq {f : ℂ → ℂ} {C : Cycle} {v : ℂ} (h : C.HasCauchyPV f v) : (cauchyPV f) C = v

Reading the value off the predicate.

theorem TauCeti.Contour.Cycle.HasCauchyPV.cauchyPVExists {f : ℂ → ℂ} {C : Cycle} {v : ℂ} (h : C.HasCauchyPV f v) : C.CauchyPVExists f

The predicate implies existence.

theorem TauCeti.Contour.Cycle.HasCauchyPV.unique {f : ℂ → ℂ} {C : Cycle} {v₁ v₂ : ℂ} (h₁ : C.HasCauchyPV f v₁) (h₂ : C.HasCauchyPV f v₂) : v₁ = v₂

The value in the predicate is determined by the cycle and the integrand.

theorem TauCeti.Contour.Cycle.CauchyPVExists.hasCauchyPV_cauchyPV {f : ℂ → ℂ} {C : Cycle} (h : C.CauchyPVExists f) : C.HasCauchyPV f ((cauchyPV f) C)

Where the principal value exists, the predicate holds at the canonical value.

theorem TauCeti.Contour.Cycle.HasCauchyPV.of_generators {f : ℂ → ℂ} {C : Cycle} {w : PiecewiseC1ClosedCurve → ℂ} (h : ∀ γ ∈ FreeAbelianGroup.support C, Contour.HasCauchyPV (Function.extend Subtype.val γ.toFun 0) γ.a γ.b f (w γ)) : C.HasCauchyPV f (∑ γ ∈ FreeAbelianGroup.support C, (FreeAbelianGroup.coeff γ) C • w γ)

Assembling a cycle's principal value from its generators. If the principal value of f along each curve γ of the canonical support of C exists and equals w γ, then the principal value along C exists and is the coefficient-weighted sum of the w γ.

@[simp]

theorem TauCeti.Contour.Cycle.hasCauchyPV_zero (f : ℂ → ℂ) : HasCauchyPV 0 f 0

The zero cycle has principal value 0, for every integrand.

theorem TauCeti.Contour.Cycle.HasCauchyPV.add {f : ℂ → ℂ} {C D : Cycle} {v₁ v₂ : ℂ} (h₁ : C.HasCauchyPV f v₁) (h₂ : D.HasCauchyPV f v₂) : (C + D).HasCauchyPV f (v₁ + v₂)

Principal values add over a sum of cycles, provided each side has one: the value is additive by construction, and the canonical support of a sum lies in the union of the supports.

@[simp]

theorem TauCeti.Contour.Cycle.hasCauchyPV_neg_iff {f : ℂ → ℂ} {C : Cycle} {v : ℂ} : (-C).HasCauchyPV f (-v) ↔ C.HasCauchyPV f v

Negating a cycle negates its principal value.

theorem TauCeti.Contour.Cycle.HasCauchyPV.zsmul {f : ℂ → ℂ} {C : Cycle} {v : ℂ} (h : C.HasCauchyPV f v) (n : ℤ) : (n • C).HasCauchyPV f (n • v)

An integer multiple of a cycle has the correspondingly scaled principal value.

theorem TauCeti.Contour.Cycle.hasCauchyPV_integral {f : ℂ → ℂ} {C : Cycle} (h : ∀ γ ∈ FreeAbelianGroup.support C, IntervalIntegrable (fun (t : ℝ) => f (Function.extend Subtype.val γ.toFun 0 t) * deriv (Function.extend Subtype.val γ.toFun 0) t) MeasureTheory.volume γ.a γ.b) : C.HasCauchyPV f ((integral f) C)

The principal value extends the ordinary cycle integral. If the contour integrand of f is interval-integrable along every curve of the canonical support — as it is when no on-contour singularity obstructs it — then the principal value along the cycle exists and is the ordinary cycle integral.