Residue Theory

Multi-point Cauchy principal values, simple pole residues, and the generalized residue theorem for piecewise C¹ immersions.

Main Definitions

• cauchyPrincipalValueIntegrandOn — multi-point PV integrand
• cauchyPrincipalValueOn — multi-point CPV integral
• CauchyPrincipalValueExistsOn — existence of multi-point CPV
• residueSimplePole — residue at a simple pole via limit
• HasSimplePoleAt — simple pole decomposition predicate

Main Results

• integral_eq_sum_residues_of_avoids — classical residue theorem
• pv_integral_simple_pole — PV of c/(z-s) = 2πi · winding · c

noncomputable def cauchyPrincipalValueIntegrandOn (S : Finset ℂ) (f : ℂ → ℂ) (γ : ℝ → ℂ) (ε t : ℝ) : ℂ

Multi-point PV integrand: zero near any s in S, else f(γ(t))·γ'(t).

Equations

• cauchyPrincipalValueIntegrandOn S f γ ε t = if ∃ s ∈ S, ‖γ t - s‖ ≤ ε then 0 else f (γ t) * deriv γ t

noncomputable def cauchyPrincipalValueOn (S : Finset ℂ) (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) : ℂ

The multi-point Cauchy principal value.

Equations

• cauchyPrincipalValueOn S f γ a b = (nhdsWithin 0 (Set.Ioi 0)).limUnder fun (ε : ℝ) => ∫ (t : ℝ) in a..b, cauchyPrincipalValueIntegrandOn S f γ ε t

def CauchyPrincipalValueExistsOn (S : Finset ℂ) (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) : Prop

Existence of the multi-point PV.

Equations

• CauchyPrincipalValueExistsOn S f γ a b = ∃ (L : ℂ), Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, cauchyPrincipalValueIntegrandOn S f γ ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds L)

noncomputable def residueSimplePole (f : ℂ → ℂ) (z₀ : ℂ) : ℂ

Residue of f at z₀ via the limit formula lim_{z → z₀} (z - z₀) · f(z).

Equations

• residueSimplePole f z₀ = (nhdsWithin z₀ {z₀}ᶜ).limUnder fun (z : ℂ) => (z - z₀) * f z

def HasSimplePoleAt (f : ℂ → ℂ) (z₀ : ℂ) : Prop

Simple pole decomposition: f(z) = c/(z-z₀) + g(z) near z₀ with g analytic.

Equations

• HasSimplePoleAt f z₀ = ∃ (c : ℂ) (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = c / (z - z₀) + g z

theorem piecewiseC1Immersion_deriv_bounded (γ : PiecewiseC1Immersion) : ∃ (M : ℝ), ∀ t ∈ Set.Icc γ.a γ.b, ‖deriv γ.toFun t‖ ≤ M

The derivative of a piecewise C¹ immersion is bounded on [a,b].

theorem piecewiseC1_deriv_intervalIntegrable (γ : PiecewiseC1Curve) (h_bdd : ∃ (M : ℝ), ∀ t ∈ Set.Icc γ.a γ.b, ‖deriv γ.toFun t‖ ≤ M) : IntervalIntegrable (deriv γ.toFun) MeasureTheory.volume γ.a γ.b

The derivative of a piecewise C¹ curve is interval integrable when bounded.

theorem singular_term_intervalIntegrable (f : ℂ → ℂ) (s : ℂ) (γ : PiecewiseC1Curve) (hγ_avoids_s : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ s) (hγ'_bdd : ∃ (M : ℝ), ∀ t ∈ Set.Icc γ.a γ.b, ‖deriv γ.toFun t‖ ≤ M) : IntervalIntegrable (fun (t : ℝ) => residueSimplePole f s / (γ.toFun t - s) * deriv γ.toFun t) MeasureTheory.volume γ.a γ.b

A single singular term is interval integrable when γ avoids s.

theorem singular_sum_intervalIntegrable (f : ℂ → ℂ) (S0 : Finset ℂ) (γ : PiecewiseC1Curve) (hγ_avoids : ∀ s ∈ S0, ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ s) (hγ'_bdd : ∃ (M : ℝ), ∀ t ∈ Set.Icc γ.a γ.b, ‖deriv γ.toFun t‖ ≤ M) : IntervalIntegrable (fun (t : ℝ) => ∑ s ∈ S0, residueSimplePole f s / (γ.toFun t - s) * deriv γ.toFun t) MeasureTheory.volume γ.a γ.b

The singular sum is interval integrable when curve avoids all poles.

theorem residue_simple_pole_eq_laurent (f : ℂ → ℂ) (z₀ c : ℂ) (g : ℂ → ℂ) (hg : AnalyticAt ℂ g z₀) (hf : ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = c / (z - z₀) + g z) : residueSimplePole f z₀ = c

For simple poles, the residue equals the Laurent coefficient.

theorem integral_singular_term_eq_winding_times_coeff (γ : PiecewiseC1Curve) (s c : ℂ) (h_avoids : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ s) : ∫ (t : ℝ) in γ.a..γ.b, c / (γ.toFun t - s) * deriv γ.toFun t = 2 * ↑Real.pi * Complex.I * generalizedWindingNumber' γ.toFun γ.a γ.b s * c

The integral of a singular term equals the winding number times the coefficient.

theorem simple_poles_decomposition (U : Set ℂ) (hU : IsOpen U) (S0 : Finset ℂ) (_hS0_in_U : ∀ s ∈ S0, s ∈ U) (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f (U \ ↑S0)) (_hSimplePoles : ∀ s ∈ S0, HasSimplePoleAt f s) (hf_ext : ∀ s ∈ S0, ContinuousAt (fun (z : ℂ) => f z - residueSimplePole f s / (z - s)) s) : have g := fun (z : ℂ) => f z - ∑ s ∈ S0, residueSimplePole f s / (z - s); DifferentiableOn ℂ g U ∧ ∀ z ∈ U \ ↑S0, f z = ∑ s ∈ S0, residueSimplePole f s / (z - s) + g z

theorem integral_eq_sum_residues_of_avoids (U : Set ℂ) (hU : IsOpen U) (hU_convex : Convex ℝ U) (S0 : Finset ℂ) (hS0_in_U : ∀ s ∈ S0, s ∈ U) (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f (U \ ↑S0)) (γ : PiecewiseC1Curve) (hγ_closed : γ.IsClosed) (hγ_in_U : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ U) (hγ_avoids : ∀ s ∈ S0, ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ s) (hSimplePoles : ∀ s ∈ S0, HasSimplePoleAt f s) (hf_ext : ∀ s ∈ S0, ContinuousAt (fun (z : ℂ) => f z - residueSimplePole f s / (z - s)) s) (hγ'_bdd : ∃ (M : ℝ), ∀ t ∈ Set.Icc γ.a γ.b, ‖deriv γ.toFun t‖ ≤ M) : ∫ (t : ℝ) in γ.a..γ.b, f (γ.toFun t) * deriv γ.toFun t = 2 * ↑Real.pi * Complex.I * ∑ s ∈ S0, generalizedWindingNumber' γ.toFun γ.a γ.b s * residueSimplePole f s

Classical residue theorem: when γ avoids all poles, the contour integral equals 2πi · Σ winding · residue.

theorem cauchyPrincipalValueIntegrandOn_eq_of_far (S0 : Finset ℂ) (f : ℂ → ℂ) (γ : ℝ → ℂ) (ε t : ℝ) (h_far : ∀ s ∈ S0, ε < ‖γ t - s‖) : cauchyPrincipalValueIntegrandOn S0 f γ ε t = f (γ t) * deriv γ t

theorem cauchyPrincipalValueIntegrandOn_empty (f : ℂ → ℂ) (γ : ℝ → ℂ) (ε t : ℝ) : cauchyPrincipalValueIntegrandOn ∅ f γ ε t = f (γ t) * deriv γ t

theorem cauchyPrincipalValueIntegrandOn_singleton (f : ℂ → ℂ) (γ : ℝ → ℂ) (z₀ : ℂ) (ε t : ℝ) : cauchyPrincipalValueIntegrandOn {z₀} f γ ε t = if ‖γ t - z₀‖ > ε then f (γ t) * deriv γ t else 0

theorem cauchyPrincipalValueOn_empty (f : ℂ → ℂ) (γ : ℝ → ℂ) (a b : ℝ) : cauchyPrincipalValueOn ∅ f γ a b = ∫ (t : ℝ) in a..b, f (γ t) * deriv γ t

theorem cauchyPrincipalValueExistsOn_avoids (S0 : Finset ℂ) (f : ℂ → ℂ) (γ : PiecewiseC1Curve) (h_avoids : ∀ s ∈ S0, ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ s) : CauchyPrincipalValueExistsOn S0 f γ.toFun γ.a γ.b

PV exists when curve avoids all singularities.

theorem cauchyPrincipalValueOn_avoids (S0 : Finset ℂ) (f : ℂ → ℂ) (γ : PiecewiseC1Curve) (h_avoids : ∀ s ∈ S0, ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ s) : cauchyPrincipalValueOn S0 f γ.toFun γ.a γ.b = ∫ (t : ℝ) in γ.a..γ.b, f (γ.toFun t) * deriv γ.toFun t

PV value equals classical integral when avoiding.

theorem pv_integral_inverse (γ : PiecewiseC1Curve) (z₀ : ℂ) : cauchyPrincipalValue' (fun (x : ℂ) => x⁻¹) (fun (t : ℝ) => γ.toFun t - z₀) γ.a γ.b 0 = 2 * ↑Real.pi * Complex.I * generalizedWindingNumber' γ.toFun γ.a γ.b z₀

PV of 1/z equals 2πi times winding number.

theorem pv_integral_simple_pole (γ : PiecewiseC1Curve) (z₀ c : ℂ) (hPV : ∃ (L : ℂ), Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in γ.a..γ.b, if ‖(fun (s : ℝ) => γ.toFun s - z₀) t - 0‖ > ε then (fun (x : ℂ) => x⁻¹) ((fun (s : ℝ) => γ.toFun s - z₀) t) * deriv (fun (s : ℝ) => γ.toFun s - z₀) t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds L)) : cauchyPrincipalValue' (fun (z : ℂ) => c / (z - z₀)) γ.toFun γ.a γ.b z₀ = 2 * ↑Real.pi * Complex.I * generalizedWindingNumber' γ.toFun γ.a γ.b z₀ * c

Single-point PV formula for simple pole.