Cycles of piecewise-C¹ curves

A contour cycle is a finite formal ℤ-linear combination of closed piecewise-C¹ curves. This file packages that definition as the free abelian group on parametrized closed curves and extends the contour integral and winding number additively from curves to cycles.

Individual curves remain functions on real intervals, as elsewhere in the contour library. The small PiecewiseC1ClosedCurve bundle exists only because FreeAbelianGroup needs a type of generators; it records exactly an interval-restricted function, its oriented parameter interval, its regularity, and its closedness. Its canonical extension to ℝ lets existing raw-function contour results apply directly. In particular, it does not introduce a second notion of contour integral.

The geometric trace of a cycle is the union of the images of the generators with nonzero coefficient. Thus cancellation removes a curve from the trace, just as it removes that curve's contribution to every additive invariant.

Main definitions

• TauCeti.Contour.PiecewiseC1ClosedCurve — a closed piecewise-C¹ parametrized curve.
• TauCeti.Contour.Cycle — the free abelian group on such curves.
• TauCeti.Contour.Cycle.trace — the geometric trace of a cycle.
• TauCeti.Contour.Cycle.integral — the additive extension of the contour integral.
• TauCeti.Contour.Cycle.windingNumber — the additive extension of the winding number.
• TauCeti.Contour.Cycle.IsIn and TauCeti.Contour.Cycle.IsNullHomologous — the cycle-level domain and null-homology predicates.

References

• N. Hungerbühler and M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, Definition 2.1 and Theorem 3.3.
• L. Ahlfors, Complex Analysis, Chapter 4.

structure TauCeti.Contour.PiecewiseC1ClosedCurve : Type

A parametrized closed piecewise-C¹ curve on an oriented real interval. The parametrization is stored only on its interval, so curves cannot differ merely in irrelevant values outside it.

• a : ℝ

  The initial parameter.

• b : ℝ

  The terminal parameter.

• toFun : ↑(Set.uIcc self.a self.b) → ℂ

  The interval-restricted parametrization of the curve.

• isPiecewiseC1On : IsPiecewiseC1On (Function.extend Subtype.val self.toFun 0) self.a self.b

  Piecewise-C¹ regularity on the parameter interval.

• source_eq_target : Function.extend Subtype.val self.toFun 0 self.a = Function.extend Subtype.val self.toFun 0 self.b

  The parametrization has equal endpoints.

theorem TauCeti.Contour.PiecewiseC1ClosedCurve.ext_iff {x y : PiecewiseC1ClosedCurve} : x = y ↔ x.a = y.a ∧ x.b = y.b ∧ x.toFun ≍ y.toFun

theorem TauCeti.Contour.PiecewiseC1ClosedCurve.ext {x y : PiecewiseC1ClosedCurve} (a : x.a = y.a) (b : x.b = y.b) (toFun : x.toFun ≍ y.toFun) : x = y

@[instance_reducible]

noncomputable instance TauCeti.Contour.PiecewiseC1ClosedCurve.instCoeFunForallRealComplex : CoeFun PiecewiseC1ClosedCurve fun (x : PiecewiseC1ClosedCurve) => ℝ → ℂ

A closed curve coerces to the canonical extension of its parametrization to ℝ.

Equations

• TauCeti.Contour.PiecewiseC1ClosedCurve.instCoeFunForallRealComplex = { coe := fun (γ : TauCeti.Contour.PiecewiseC1ClosedCurve) => Function.extend Subtype.val γ.toFun 0 }

theorem TauCeti.Contour.PiecewiseC1ClosedCurve.coe_apply (γ : PiecewiseC1ClosedCurve) (t : ↑(Set.uIcc γ.a γ.b)) : Function.extend Subtype.val γ.toFun 0 ↑t = γ.toFun t

On its parameter interval, a closed curve's coercion agrees with its stored function.

def TauCeti.Contour.PiecewiseC1ClosedCurve.of {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) : PiecewiseC1ClosedCurve

Bundle a raw closed piecewise-C¹ curve by restricting it to its parameter interval.

Equations

• TauCeti.Contour.PiecewiseC1ClosedCurve.of γ hγ hclosed = { a := a, b := b, toFun := fun (t : ↑(Set.uIcc a b)) => γ ↑t, isPiecewiseC1On := ⋯, source_eq_target := ⋯ }

@[simp]

theorem TauCeti.Contour.PiecewiseC1ClosedCurve.of_a {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) : (of γ hγ hclosed).a = a

Bundling a raw curve preserves its initial parameter.

@[simp]

theorem TauCeti.Contour.PiecewiseC1ClosedCurve.of_b {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) : (of γ hγ hclosed).b = b

Bundling a raw curve preserves its terminal parameter.

@[simp]

theorem TauCeti.Contour.PiecewiseC1ClosedCurve.of_apply {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) {t : ℝ} (ht : t ∈ Set.uIcc a b) : Function.extend Subtype.val (of γ hγ hclosed).toFun 0 t = γ t

Bundling a raw curve preserves its values on the parameter interval.

@[simp]

theorem TauCeti.Contour.PiecewiseC1ClosedCurve.image_of {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) : Function.extend Subtype.val (of γ hγ hclosed).toFun 0 '' Set.uIcc a b = γ '' Set.uIcc a b

Bundling a raw curve preserves its interval image.

@[simp]

theorem TauCeti.Contour.PiecewiseC1ClosedCurve.mapsTo_of_iff {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) (Ω : Set ℂ) : Set.MapsTo (Function.extend Subtype.val (of γ hγ hclosed).toFun 0) (Set.uIcc a b) Ω ↔ Set.MapsTo γ (Set.uIcc a b) Ω

Bundling a raw curve preserves the set into which it maps its parameter interval.

@[simp]

theorem TauCeti.Contour.PiecewiseC1ClosedCurve.integral_of {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) : ∫ (t : ℝ) in a..b, deriv (Function.extend Subtype.val (of γ hγ hclosed).toFun 0) t • f (Function.extend Subtype.val (of γ hγ hclosed).toFun 0 t) = ∫ (t : ℝ) in a..b, deriv γ t • f (γ t)

Bundling a raw curve preserves its contour integral.

@[simp]

theorem TauCeti.Contour.PiecewiseC1ClosedCurve.windingNumber_of {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) (z₀ : ℂ) : windingNumber (Function.extend Subtype.val (of γ hγ hclosed).toFun 0) a b z₀ = windingNumber γ a b z₀

Bundling a raw curve preserves its winding number.

@[simp]

theorem TauCeti.Contour.PiecewiseC1ClosedCurve.isNullHomologous_of_iff {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) (Ω : Set ℂ) : IsNullHomologous (Function.extend Subtype.val (of γ hγ hclosed).toFun 0) a b Ω ↔ IsNullHomologous γ a b Ω

Bundling a raw curve preserves null-homology.

theorem TauCeti.Contour.PiecewiseC1ClosedCurve.continuousOn (γ : PiecewiseC1ClosedCurve) : ContinuousOn (Function.extend Subtype.val γ.toFun 0) (Set.uIcc γ.a γ.b)

The underlying parametrization is continuous on its parameter interval.

theorem TauCeti.Contour.PiecewiseC1ClosedCurve.intervalIntegrable_deriv (γ : PiecewiseC1ClosedCurve) : IntervalIntegrable (fun (t : ℝ) => deriv (Function.extend Subtype.val γ.toFun 0) t) MeasureTheory.volume γ.a γ.b

The derivative of a closed piecewise-C¹ curve is interval-integrable.

@[reducible, inline]

abbrev TauCeti.Contour.Cycle : Type

A contour cycle is a finite formal ℤ-linear combination of closed piecewise-C¹ curves.

Equations

• TauCeti.Contour.Cycle = FreeAbelianGroup TauCeti.Contour.PiecewiseC1ClosedCurve

def TauCeti.Contour.Cycle.trace (C : Cycle) : Set ℂ

The geometric trace of a cycle: the union of the images of the curves occurring with nonzero coefficient.

Equations

• C.trace = ⋃ γ ∈ FreeAbelianGroup.support C, Function.extend Subtype.val γ.toFun 0 '' Set.uIcc γ.a γ.b

@[simp]

theorem TauCeti.Contour.Cycle.mem_trace_iff {C : Cycle} {z : ℂ} : z ∈ C.trace ↔ ∃ γ ∈ FreeAbelianGroup.support C, z ∈ Function.extend Subtype.val γ.toFun 0 '' Set.uIcc γ.a γ.b

Membership in the trace means membership in the image of a generator with nonzero coefficient.

theorem TauCeti.Contour.Cycle.avoids_of_mem_support {C : Cycle} {z : ℂ} (hz : z ∉ C.trace) {γ : PiecewiseC1ClosedCurve} (hγ : γ ∈ FreeAbelianGroup.support C) (t : ℝ) : t ∈ Set.uIcc γ.a γ.b → Function.extend Subtype.val γ.toFun 0 t ≠ z

A point outside the trace of a cycle is avoided by every curve in its canonical support.

theorem TauCeti.Contour.Cycle.isCompact_trace (C : Cycle) : IsCompact C.trace

The trace of a contour cycle is compact.

@[simp]

theorem TauCeti.Contour.Cycle.trace_zero : trace 0 = ∅

The zero cycle has empty trace.

@[simp]

theorem TauCeti.Contour.Cycle.trace_of (γ : PiecewiseC1ClosedCurve) : trace (FreeAbelianGroup.of γ) = Function.extend Subtype.val γ.toFun 0 '' Set.uIcc γ.a γ.b

The trace of a single generator is its image on its parameter interval.

theorem TauCeti.Contour.Cycle.trace_of_raw {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) : trace (FreeAbelianGroup.of (PiecewiseC1ClosedCurve.of γ hγ hclosed)) = γ '' Set.uIcc a b

The trace of a raw curve bundled as a one-generator cycle is its raw interval image.

@[simp]

theorem TauCeti.Contour.Cycle.trace_neg (C : Cycle) : (-C).trace = C.trace

Negating every coefficient does not change the trace.

theorem TauCeti.Contour.Cycle.trace_add_subset (C D : Cycle) : (C + D).trace ⊆ C.trace ∪ D.trace

The trace of a sum is contained in the union of the traces. Equality can fail when a generator occurs with opposite coefficients and cancels.

theorem TauCeti.Contour.Cycle.trace_zsmul (C : Cycle) {n : ℤ} (hn : n ≠ 0) : (n • C).trace = C.trace

A nonzero integer multiple has the same trace as the original cycle.

def TauCeti.Contour.Cycle.IsIn (C : Cycle) (Ω : Set ℂ) : Prop

A cycle lies in Ω when its geometric trace is contained in Ω.

Equations

• C.IsIn Ω = (C.trace ⊆ Ω)

theorem TauCeti.Contour.Cycle.isIn_iff {C : Cycle} {Ω : Set ℂ} : C.IsIn Ω ↔ C.trace ⊆ Ω

Restatement of cycle containment in terms of its trace.

theorem TauCeti.Contour.Cycle.isIn_of_raw_iff {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) (Ω : Set ℂ) : IsIn (FreeAbelianGroup.of (PiecewiseC1ClosedCurve.of γ hγ hclosed)) Ω ↔ Set.MapsTo γ (Set.uIcc a b) Ω

A raw curve bundled as a one-generator cycle lies in Ω exactly when it maps its interval into Ω.

@[simp]

theorem TauCeti.Contour.Cycle.isIn_of_iff {γ : PiecewiseC1ClosedCurve} {Ω : Set ℂ} : IsIn (FreeAbelianGroup.of γ) Ω ↔ Set.MapsTo (Function.extend Subtype.val γ.toFun 0) (Set.uIcc γ.a γ.b) Ω

A one-generator cycle lies in Ω exactly when its parametrization maps its interval into Ω.

@[simp]

theorem TauCeti.Contour.Cycle.IsIn.zero (Ω : Set ℂ) : IsIn 0 Ω

The zero cycle lies in every set.

theorem TauCeti.Contour.Cycle.IsIn.add {C D : Cycle} {Ω : Set ℂ} (hC : C.IsIn Ω) (hD : D.IsIn Ω) : (C + D).IsIn Ω

A sum of two cycles in Ω is in Ω.

@[simp]

theorem TauCeti.Contour.Cycle.isIn_neg_iff {C : Cycle} {Ω : Set ℂ} : (-C).IsIn Ω ↔ C.IsIn Ω

Negation preserves containment in a set.

theorem TauCeti.Contour.Cycle.IsIn.zsmul {C : Cycle} {Ω : Set ℂ} (hC : C.IsIn Ω) (n : ℤ) : (n • C).IsIn Ω

Every integer multiple of a cycle in Ω is in Ω.

noncomputable def TauCeti.Contour.Cycle.integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) : Cycle →+ E

The integral of f over a cycle, obtained by additively extending the raw contour integral ∫ t in γ.a..γ.b, deriv γ t • f (γ t) from generators.

Equations

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

theorem TauCeti.Contour.Cycle.integral_of_raw {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) : (integral f) (FreeAbelianGroup.of (PiecewiseC1ClosedCurve.of γ hγ hclosed)) = ∫ (t : ℝ) in a..b, deriv γ t • f (γ t)

Integrating over a raw curve bundled as a one-generator cycle gives its raw contour integral.

@[simp]

theorem TauCeti.Contour.Cycle.integral_of {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (γ : PiecewiseC1ClosedCurve) (f : ℂ → E) : (integral f) (FreeAbelianGroup.of γ) = ∫ (t : ℝ) in γ.a..γ.b, deriv (Function.extend Subtype.val γ.toFun 0) t • f (Function.extend Subtype.val γ.toFun 0 t)

Integrating over a one-generator cycle gives the raw contour integral over that curve.

theorem TauCeti.Contour.Cycle.integral_eq_sum_support {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (C : Cycle) : (integral f) C = ∑ γ ∈ FreeAbelianGroup.support C, (FreeAbelianGroup.coeff γ) C • ∫ (t : ℝ) in γ.a..γ.b, deriv (Function.extend Subtype.val γ.toFun 0) t • f (Function.extend Subtype.val γ.toFun 0 t)

The integral over a cycle is the coefficient-weighted sum of the integrals over the curves in its canonical support.

noncomputable def TauCeti.Contour.Cycle.windingNumber (z₀ : ℂ) : Cycle →+ ℂ

The winding number of a cycle, obtained by additively extending the generalized winding number of its generators.

Equations

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

theorem TauCeti.Contour.Cycle.windingNumber_of_raw {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) (z₀ : ℂ) : (windingNumber z₀) (FreeAbelianGroup.of (PiecewiseC1ClosedCurve.of γ hγ hclosed)) = Contour.windingNumber γ a b z₀

The winding number of a raw curve bundled as a one-generator cycle is its raw winding number.

@[simp]

theorem TauCeti.Contour.Cycle.windingNumber_of (γ : PiecewiseC1ClosedCurve) (z₀ : ℂ) : (windingNumber z₀) (FreeAbelianGroup.of γ) = Contour.windingNumber (Function.extend Subtype.val γ.toFun 0) γ.a γ.b z₀

The winding number of a one-generator cycle is the winding number of that curve.

def TauCeti.Contour.Cycle.IsNullHomologous (C : Cycle) (Ω : Set ℂ) : Prop

A cycle is null-homologous in Ω when its winding number vanishes at every point outside Ω.

Equations

• C.IsNullHomologous Ω = ∀ z ∉ Ω, (TauCeti.Contour.Cycle.windingNumber z) C = 0

theorem TauCeti.Contour.Cycle.isNullHomologous_iff {C : Cycle} {Ω : Set ℂ} : C.IsNullHomologous Ω ↔ ∀ z ∉ Ω, (windingNumber z) C = 0

Restatement of null-homology as vanishing of the cycle winding number outside the domain.

theorem TauCeti.Contour.Cycle.isNullHomologous_of_raw_iff {a b : ℝ} (γ : ℝ → ℂ) (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) (Ω : Set ℂ) : IsNullHomologous (FreeAbelianGroup.of (PiecewiseC1ClosedCurve.of γ hγ hclosed)) Ω ↔ Contour.IsNullHomologous γ a b Ω

Null-homology of a raw curve bundled as a one-generator cycle is the raw-curve predicate.

@[simp]

theorem TauCeti.Contour.Cycle.isNullHomologous_of_iff {γ : PiecewiseC1ClosedCurve} {Ω : Set ℂ} : IsNullHomologous (FreeAbelianGroup.of γ) Ω ↔ Contour.IsNullHomologous (Function.extend Subtype.val γ.toFun 0) γ.a γ.b Ω

Cycle null-homology specializes on a generator to the raw-curve predicate.

@[simp]

theorem TauCeti.Contour.Cycle.IsNullHomologous.zero (Ω : Set ℂ) : IsNullHomologous 0 Ω

The zero cycle is null-homologous in every set.

theorem TauCeti.Contour.Cycle.IsNullHomologous.add {C D : Cycle} {Ω : Set ℂ} (hC : C.IsNullHomologous Ω) (hD : D.IsNullHomologous Ω) : (C + D).IsNullHomologous Ω

A sum of null-homologous cycles is null-homologous.

@[simp]

theorem TauCeti.Contour.Cycle.isNullHomologous_neg_iff {C : Cycle} {Ω : Set ℂ} : (-C).IsNullHomologous Ω ↔ C.IsNullHomologous Ω

Negation preserves null-homology.

theorem TauCeti.Contour.Cycle.IsNullHomologous.zsmul {C : Cycle} {Ω : Set ℂ} (hC : C.IsNullHomologous Ω) (n : ℤ) : (n • C).IsNullHomologous Ω

Every integer multiple of a null-homologous cycle is null-homologous.