Contour Cycles

Formal Z-linear combinations of piecewise C^1 immersions ("cycles"), with contour integration and winding numbers extended by linearity.

Main definitions

• ContourCycle -- formal Z-linear combination of PiecewiseC1Immersions.
• contourIntegralCycle f Gamma -- contour integral of f over a cycle.
• windingNumberCycle Gamma z -- winding number of a cycle around z.
• IsNullHomologousCycle Gamma U -- each component is null-homologous in U.
• cpvCycle S0 f Gamma -- CPV integral of f over a cycle.

Main results

• contourIntegralCycle_single -- single curve with multiplicity 1.
• windingNumberCycle_single -- same for winding numbers.
• contourIntegralCycle_eq_zero_of_nullHomologous -- Cauchy theorem for cycles.
• generalizedResidueTheorem_simplePoles_cycle -- residue theorem for cycles (simple poles).
• generalizedResidueTheorem_cycle -- residue theorem for cycles (higher-order, Tendsto).
• windingNumberCycle_isInt -- winding number integrality.

Definitions

@[reducible, inline]

abbrev ContourCycle : Type

A contour cycle is a formal Z-linear combination of piecewise C^1 immersions.

Equations

• ContourCycle = (PiecewiseC1Immersion →₀ ℤ)

noncomputable def contourIntegralCycle (f : ℂ → ℂ) (Γ : ContourCycle) : ℂ

Contour integral of f over a cycle Gamma, extended by linearity: sum_gamma n_gamma * integral_gamma f(z) dz.

Equations

• contourIntegralCycle f Γ = Finsupp.sum Γ fun (γ : PiecewiseC1Immersion) (n : ℤ) => ↑n * ∫ (t : ℝ) in γ.a..γ.b, f (γ.toFun t) * deriv γ.toFun t

noncomputable def windingNumberCycle (Γ : ContourCycle) (z : ℂ) : ℂ

Winding number of a cycle around z, extended by linearity: sum_gamma n_gamma * n(gamma, z).

Equations

• windingNumberCycle Γ z = Finsupp.sum Γ fun (γ : PiecewiseC1Immersion) (n : ℤ) => ↑n * generalizedWindingNumber' γ.toFun γ.a γ.b z

def IsNullHomologousCycle (Γ : ContourCycle) (U : Set ℂ) : Prop

A cycle is null-homologous in U when every component curve is null-homologous in U.

Equations

• IsNullHomologousCycle Γ U = ∀ γ ∈ Γ.support, IsNullHomologous γ U

noncomputable def cpvCycle (S0 : Finset ℂ) (f : ℂ → ℂ) (Γ : ContourCycle) : ℂ

Cauchy principal value integral of f over a cycle Gamma, extended by linearity: sum_gamma n_gamma * CPV(gamma, f).

Equations

• cpvCycle S0 f Γ = Finsupp.sum Γ fun (γ : PiecewiseC1Immersion) (n : ℤ) => ↑n * cauchyPrincipalValueOn S0 f γ.toFun γ.a γ.b

Bridge lemmas for single curves

theorem contourIntegralCycle_single (f : ℂ → ℂ) (γ : PiecewiseC1Immersion) : contourIntegralCycle f (Finsupp.single γ 1) = ∫ (t : ℝ) in γ.a..γ.b, f (γ.toFun t) * deriv γ.toFun t

Contour integral of a single curve with multiplicity 1.

theorem windingNumberCycle_single (γ : PiecewiseC1Immersion) (z : ℂ) : windingNumberCycle (Finsupp.single γ 1) z = generalizedWindingNumber' γ.toFun γ.a γ.b z

Winding number of a single curve with multiplicity 1.

theorem isNullHomologousCycle_single (γ : PiecewiseC1Immersion) (U : Set ℂ) (h : IsNullHomologous γ U) : IsNullHomologousCycle (Finsupp.single γ 1) U

A null-homologous single curve gives a null-homologous cycle.

theorem cpvCycle_single (S0 : Finset ℂ) (f : ℂ → ℂ) (γ : PiecewiseC1Immersion) : cpvCycle S0 f (Finsupp.single γ 1) = cauchyPrincipalValueOn S0 f γ.toFun γ.a γ.b

CPV integral of a single curve with multiplicity 1.

Main theorems

theorem contourIntegralCycle_eq_zero_of_nullHomologous {U : Set ℂ} (hU : IsOpen U) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (Γ : ContourCycle) (h_null : IsNullHomologousCycle Γ U) : contourIntegralCycle f Γ = 0

Cauchy theorem for cycles: if f is holomorphic on U and Gamma is null-homologous in U, then the contour integral of f over Gamma is zero.

theorem windingNumberCycle_eq_zero_outside {U : Set ℂ} (Γ : ContourCycle) (h_null : IsNullHomologousCycle Γ U) {z : ℂ} (hz : z ∉ U) : windingNumberCycle Γ z = 0

Winding number of a null-homologous cycle is zero outside U.

Residue theorem for cycles (simple poles)

theorem generalizedResidueTheorem_simplePoles_cycle (U : Set ℂ) (hU : IsOpen U) (S : Set ℂ) (hS_in_U : ∀ s ∈ S, s ∈ U) (hS_discrete : ∀ s ∈ S, ∃ ε > 0, ∀ s' ∈ S, s' ≠ s → ε ≤ ‖s' - s‖) (hS_closed : IsClosed S) (S0 : Finset ℂ) (hS0_subset : ∀ s ∈ S0, s ∈ S) (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f (U \ ↑S0)) (Γ : ContourCycle) (h_null : IsNullHomologousCycle Γ U) (hS_on_curve : ∀ γ ∈ Γ.support, ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ S → γ.toFun t ∈ S0) (hSimplePoles : ∀ s ∈ S0, HasSimplePoleAt f s) (hf_ext : ∀ s ∈ S0, ContinuousAt (fun (z : ℂ) => f z - residueSimplePole f s / (z - s)) s) (hγ_meas : ∀ γ ∈ Γ.support, Measurable γ.toFun) (h_no_endpt : ∀ γ ∈ Γ.support, ∀ s ∈ S0, γ.toFun γ.a ≠ s ∧ γ.toFun γ.b ≠ s) (h_unique : ∀ γ ∈ Γ.support, ∀ s ∈ S0, ∀ t₁ ∈ Set.Icc γ.a γ.b, ∀ t₂ ∈ Set.Icc γ.a γ.b, γ.toFun t₁ = s → γ.toFun t₂ = s → t₁ = t₂) : cpvCycle S0 f Γ = 2 * ↑Real.pi * Complex.I * ∑ s ∈ S0, windingNumberCycle Γ s * residueAt f s

Generalized Residue Theorem for simple poles on a cycle.

Extends generalizedResidueTheorem_simplePoles from a single curve to a formal Z-linear combination of curves.

Higher-order residue theorem for cycles (Tendsto version)

theorem generalizedResidueTheorem_cycle (U : Set ℂ) (hU : IsOpen U) (S : Set ℂ) (hS_in_U : ∀ s ∈ S, s ∈ U) (hS_discrete : ∀ s ∈ S, ∃ ε > 0, ∀ s' ∈ S, s' ≠ s → ε ≤ ‖s' - s‖) (hS_closed : IsClosed S) (S0 : Finset ℂ) (hS0_subset : ∀ s ∈ S0, s ∈ S) (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f (U \ ↑S0)) (Γ : ContourCycle) (h_null : IsNullHomologousCycle Γ U) (hS_on_curve : ∀ γ ∈ Γ.support, ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ S → γ.toFun t ∈ S0) (hMero : ∀ s ∈ S0, MeromorphicAt f s) (hCondA : ∀ γ ∈ Γ.support, SatisfiesConditionA' γ S0 fun (s : ℂ) => poleOrderAt f s) (hCondB : ∀ γ ∈ Γ.support, SatisfiesConditionB γ f S0) (hγ_meas : ∀ γ ∈ Γ.support, Measurable γ.toFun) (h_no_endpt : ∀ γ ∈ Γ.support, ∀ s ∈ S0, γ.toFun γ.a ≠ s ∧ γ.toFun γ.b ≠ s) (h_unique : ∀ γ ∈ Γ.support, ∀ s ∈ S0, ∀ t₁ ∈ Set.Icc γ.a γ.b, ∀ t₂ ∈ Set.Icc γ.a γ.b, γ.toFun t₁ = s → γ.toFun t₂ = s → t₁ = t₂) : Filter.Tendsto (fun (ε : ℝ) => Finsupp.sum Γ fun (γ : PiecewiseC1Immersion) (n : ℤ) => ↑n * ∫ (t : ℝ) in γ.a..γ.b, cauchyPrincipalValueIntegrandOn S0 f γ.toFun ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (2 * ↑Real.pi * Complex.I * ∑ s ∈ S0, windingNumberCycle Γ s * residueAt f s))

Generalized Residue Theorem for cycles (higher-order poles, Tendsto).

Extends generalizedResidueTheorem from a single curve to a formal Z-linear combination of curves. Each component must satisfy conditions (A') and (B).

Winding number integrality

theorem windingNumber_isInt_of_immersion_closed_avoiding (γ : PiecewiseC1Immersion) (z : ℂ) (hγ_closed : γ.IsClosed) (h_avoids : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ z) : ∃ (n : ℤ), generalizedWindingNumber' γ.toFun γ.a γ.b z = ↑n

The generalized winding number of a closed piecewise C^1 immersion around a point it avoids is an integer.

theorem windingNumberCycle_isInt (Γ : ContourCycle) (h_closed : ∀ γ ∈ Γ.support, γ.IsClosed) (z : ℂ) (h_avoids : ∀ γ ∈ Γ.support, ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ z) : ∃ (n : ℤ), windingNumberCycle Γ z = ↑n

Winding number of a cycle around a point avoided by all component curves is an integer, provided each component curve is closed.