Contour integration and the Hungerbühler–Wasem generalized residue theorem

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe Hungerbühler–Wasem generalized residue theorem for a contour cycle (HW Thm 3.3)#

Let U be open, S ⊆ U finite, f holomorphic on U ∖ S and meromorphic at each point of S, and let C be a contour cycle in U, null-homologous in U, whose curves are piecewise-C¹ immersions rooted off S and satisfy conditions (A′) and (B). Then the Cauchy principal value of f along C exists and

PV ∮_C f = 2πi · ∑_{s ∈ S} n_s(C) · Res_s f,

each singularity weighted by the generalized winding number of C about it. The singularities are allowed to lie on C, where those weights are in general not integers and the contour integral only exists as a principal value.

Null-homology is asked of the cycle only, never of its generators, so the theorem covers the combinations that make cycles worth having: a difference of two homologous loops around a hole of U, neither of them null-homologous, is null-homologous. Its S = ∅ case is the homology Cauchy theorem for cycles (TauCeti.Contour.Cycle.homologyCauchyTheorem), and its one-generator case is the single-curve theorem TauCeti.Contour.hungerbuhlerWasem_residueTheorem. Where the trace of C avoids S the principal value is an ordinary integral and the statement is the classical residue theorem for cycles (TauCeti.Contour.Cycle.classicalResidueTheorem_nullHomologous), which needs neither immersions nor the conditions.

TauCeti.Contour.Cycle.hungerbuhlerWasem_residueTheorem {f : ℂ → ℂ} {U : Set ℂ}
  {C : TauCeti.Contour.Cycle} (hU : IsOpen U) (S : Finset ℂ) (hSU : ↑S ⊆ U)
  (hf : DifferentiableOn ℂ f (U \ ↑S)) (hmero : ∀ s ∈ S, MeromorphicAt f s) (hCU : C.IsIn U)
  (h_imm :
    ∀ γ ∈ FreeAbelianGroup.support C,
      TauCeti.Contour.IsPwC1ImmersionOn (Function.extend Subtype.val γ.toFun 0) γ.a γ.b)
  (hbase : ∀ γ ∈ FreeAbelianGroup.support C, Function.extend Subtype.val γ.toFun 0 γ.a ∉ ↑S)
  (hnull : C.IsNullHomologous U)
  (hA :
    ∀ γ ∈ FreeAbelianGroup.support C,
      TauCeti.Contour.ConditionAprime (Function.extend Subtype.val γ.toFun 0) γ.a γ.b f S)
  (hB :
    ∀ γ ∈ FreeAbelianGroup.support C,
      TauCeti.Contour.ConditionB (Function.extend Subtype.val γ.toFun 0) γ.a γ.b f) :
  C.HasCauchyPV f
    (2 * ↑Real.pi * Complex.I *
      ∑ s ∈ S, (TauCeti.Contour.Cycle.windingNumber s) C * TauCeti.Contour.residue f s)
Lean

Formalized in Tau Ceti as TauCeti.Contour.Cycle.hungerbuhlerWasem_residueTheorem.

Other forms

The Hungerbühler–Wasem generalized residue theorem (HW Thm 3.3). Formalized in Tau Ceti as TauCeti.Contour.hungerbuhlerWasem_residueTheorem.

TauCeti.Contour.hungerbuhlerWasem_residueTheorem {f : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U)
  (S : Finset ℂ) (γ : ℝ → ℂ) (a b : ℝ) (hγ_imm : TauCeti.Contour.IsPwC1ImmersionOn γ a b)
  (hSU : ↑S ⊆ U) (hclosed : γ a = γ b) (hγa : γ a ∉ ↑S) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U)
  (hf : DifferentiableOn ℂ f (U \ ↑S)) (hmero : ∀ s ∈ S, MeromorphicAt f s)
  (hnull : TauCeti.Contour.IsNullHomologous γ a b U)
  (hA : TauCeti.Contour.ConditionAprime γ a b f S) (hB : TauCeti.Contour.ConditionB γ a b f) :
  TauCeti.Contour.HasCauchyPV γ a b f
    (2 * ↑Real.pi * Complex.I *
      ∑ s ∈ S, TauCeti.Contour.windingNumber γ a b s * TauCeti.Contour.residue f s)
Sources
LeanTauCeti.Contour.Cycle.hungerbuhlerWasem_residueTheorem · TauCeti.Contour.hungerbuhlerWasem_residueTheorem
Uses 6 · Used by 2
Statement usesGeneralized winding number (HW Def 2.1) · TauCeti.Contour.Cycle
Proof usesThe canonical Laurent decomposition · First exit time at radius ε (left side) · The homology Cauchy theorem (roadmap homologyCauchyTheorem, Layer 3) · The homology Cauchy theorem for contour cycles
Used byThe generalized residue theorem on a star-shaped open set, simple-pole regime · The half-residue theorem at a simple pole

TheoremHungerbühler--Wasem Proposition 2.2 (winding decomposition)#

Let γ be a closed piecewise-C¹ immersion on [a, b], with a basepoint away from s. There is a finite ordered family of disjoint crossing windows whose circular-cap excision is again piecewise C¹, is closed, and avoids s. Its winding number accounts for the integer part of the original winding number; each crossing contributes its geometric angle divided by 2π.

The sum is indexed by the canonical finite crossing set supplied by IsPwC1ImmersionOn.finite_crossings.

TauCeti.Contour.IsPwC1ImmersionOn.exists_crossingDecomposition {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ}
  (h_imm : TauCeti.Contour.IsPwC1ImmersionOn γ a b) (hab : a < b) (hclosed : γ a = γ b)
  (hbase : γ a ≠ s) :
  ∃ windows,
    List.Pairwise (fun W V => W.upper < V.lower) windows ∧
      TauCeti.IsPiecewiseC1On (TauCeti.Contour.exciseCrossings γ s windows) a b ∧
        TauCeti.Contour.exciseCrossings γ s windows a =
            TauCeti.Contour.exciseCrossings γ s windows b ∧
          (∀ t ∈ Set.Icc a b, TauCeti.Contour.exciseCrossings γ s windows t ≠ s) ∧
            TauCeti.Contour.windingNumber γ a b s =
              TauCeti.Contour.windingNumber (TauCeti.Contour.exciseCrossings γ s windows) a b s +
                ↑(∑ t ∈ ⋯.toFinset, TauCeti.Contour.crossingAngle γ t) / (2 * ↑Real.pi)
Lean

Formalized in Tau Ceti as TauCeti.Contour.IsPwC1ImmersionOn.exists_crossingDecomposition.

Sources
LeanTauCeti.Contour.IsPwC1ImmersionOn.exists_crossingDecomposition
Uses 3
Statement usesGeneralized winding number (HW Def 2.1)
Proof usesThe exact local angle contribution of one exit-time cap window · First exit time at radius ε (left side)

TheoremThe real bounded-integrand formula, allowing crossings (Hungerbühler–Wasem Prop 2.3)#

For a closed piecewise-C¹ immersion γ on [[a, b]] that avoids s at the basepoint a (hsa, so also at b by closedness — every other crossing of s, if any, is automatically interior to [[a, b]]) and is C^{1,1} on each side of any such crossing (derivWithin γ Lipschitz on a one-sided closed piece ending or starting there, hγ_lip — the two sides need not agree, so a crossing may coincide with a breakpoint of the immersion) — in particular satisfied vacuously if γ never meets s — the generalized winding number n_s(γ) is a real number equal to its ordinary (non-principal-value) integral:

n_s(γ) = (1 / 2π) ∫_a^b (x ẏ - y ẋ) / (x² + y²) dt, x + i y = γ - s.

The two sides of a crossing need not agree: hγ_lip allows the crossing to coincide with a breakpoint of the piecewise-C¹ immersion (a corner), matching Hungerbühler–Wasem's own proof of Prop 2.3, which handles that case via the same one-sided splitting (arXiv:1808.00997, p. 9). Orientation-generic, like windingNumber and intervalIntegral themselves: no a ≤ b is needed.

TauCeti.Contour.windingNumber_eq_real_integral_of_closed_interior_crossings {γ : ℝ → ℂ} {a b : ℝ}
  {s : ℂ} (h_imm : TauCeti.Contour.IsPwC1ImmersionOn γ a b) (hclosed : γ a = γ b) (hsa : γ a ≠ s)
  (hγ_lip : ∀ t ∈ Set.uIcc a b, γ t = s → TauCeti.Contour.HasLipschitzDerivOnEachSideAt γ t) :
  TauCeti.Contour.windingNumber γ a b s =
    ↑(1 / (2 * Real.pi) *
        ∫ (t : ℝ) in a..b, TauCeti.Contour.realWindingIntegrand (γ t - s) (deriv γ t))
Lean

Formalized in Tau Ceti as TauCeti.Contour.windingNumber_eq_real_integral_of_closed_interior_crossings.

Sources
LeanTauCeti.Contour.windingNumber_eq_real_integral_of_closed_interior_crossings
Uses 2
Statement usesGeneralized winding number (HW Def 2.1)
Proof usesFirst exit time at radius ε (left side)

TheoremHungerbühler–Wasem Proposition 2.3, crossing value, under a C² hypothesis#

For a curve that is C² at the crossing parameter t₀ with nonvanishing velocity there, the real winding integrand about z₀ = γ t₀ tends to (ẋ ÿ - ẏ ẍ) / (2 (ẋ² + ẏ²)), where ẋ + i ẏ and ẍ + i ÿ are the first and second derivatives of γ at t₀.

TauCeti.Contour.tendsto_realWindingIntegrand_at_crossing_of_contDiffAt {γ : ℝ → ℂ} {t₀ : ℝ} {z₀ : ℂ}
  (hγ : ContDiffAt ℝ 2 γ t₀) (hcross : γ t₀ = z₀) (hL : deriv γ t₀ ≠ 0) :
  Filter.Tendsto (fun t => TauCeti.Contour.realWindingIntegrand (γ t - z₀) (deriv γ t))
    (nhdsWithin t₀ {t₀}ᶜ)
    (nhds
      (((deriv γ t₀).re * (deriv (deriv γ) t₀).im - (deriv γ t₀).im * (deriv (deriv γ) t₀).re) /
        (2 * ((deriv γ t₀).re ^ 2 + (deriv γ t₀).im ^ 2))))
Lean

Formalized in Tau Ceti as TauCeti.Contour.tendsto_realWindingIntegrand_at_crossing_of_contDiffAt.

Sources
LeanTauCeti.Contour.tendsto_realWindingIntegrand_at_crossing_of_contDiffAt

TheoremThe homology Cauchy theorem (roadmap homologyCauchyTheorem, Layer 3)#

Let γ be a closed piecewise-C¹ curve on [[a, b]], null-homologous in an open set Ω containing it, and let f be holomorphic on Ω. Then the contour integral of f along γ vanishes: ∫ t in a..b, deriv γ t • f (γ t) = 0.

Dixon's argument: the piecewise-C¹ regularity supplies continuity, differentiability off the finitely many breakpoints, and interval-integrability of deriv γ (the IsPiecewiseC1On API); the compact curve image cannot exhaust the open Ω, giving a base point w₀ ∈ Ω off the curve (exists_mem_off_curve); and homologyCauchyTheorem_of_point_off_curve — vanishing of the glued Dixon function by Liouville, then the Cauchy integral formula at w₀ — concludes.

TauCeti.Contour.homologyCauchyTheorem {f : ℂ → ℂ} {Ω : Set ℂ} (hΩ : IsOpen Ω) (γ : ℝ → ℂ) (a b : ℝ)
  (hγ_pc1 : TauCeti.IsPiecewiseC1On γ a b) (hγ : ∀ t ∈ Set.uIcc a b, γ t ∈ Ω) (hclosed : γ a = γ b)
  (hf : DifferentiableOn ℂ f Ω) (hnull : TauCeti.Contour.IsNullHomologous γ a b Ω) :
  ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = 0
Lean

Formalized in Tau Ceti as TauCeti.Contour.homologyCauchyTheorem.

Other forms

Homology Cauchy theorem with a supplied off-curve point. Formalized in Tau Ceti as TauCeti.Contour.homologyCauchyTheorem_of_point_off_curve.

TauCeti.Contour.homologyCauchyTheorem_of_point_off_curve {f : ℂ → ℂ} {U : Set ℂ} {γ : ℝ → ℂ}
  {a b : ℝ} {P : Set ℝ} {w₀ : ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U)
  (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U)
  (hderiv_int : IntervalIntegrable (fun t => deriv γ t) MeasureTheory.volume a b)
  (hclosed : γ a = γ b) (hP : P.Countable)
  (hγ_diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ t)
  (h_null : TauCeti.Contour.IsNullHomologous γ a b U) (hw₀U : w₀ ∈ U)
  (hw₀off : ∀ t ∈ Set.uIcc a b, γ t ≠ w₀) : ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = 0
Sources
LeanTauCeti.Contour.homologyCauchyTheorem · TauCeti.Contour.homologyCauchyTheorem_of_point_off_curve
Uses 2 · Used by 8
Statement usesGeneralized winding number (HW Def 2.1)
Proof usesThe pointwise homology Cauchy theorem ∮_γ f = 0
Used byA crosscut of a simply connected domain has exactly two sides · The Riemann map of a Jordan domain extends to a homeomorphism of the closures · The Schwarz--Christoffel theorem for a bounded polygonal Jordan domain · The Hungerbühler–Wasem generalized residue theorem for a contour cycle (HW Thm 3.3) · The residue theorem for a fixed polar-part decomposition · Carathéodory's theorem for the inside of a Jordan curve · Cauchy's theorem on a disc · Holomorphic functions have primitives on a star-shaped set

TheoremCauchy's integral formula for the k-th derivative, homology form#

Let f be holomorphic on an open U, let γ be a closed piecewise-C¹ curve in U that is null-homologous there, and let z ∈ U lie off the curve. Then for every k,

∫ t in a..b, γ' t • (f (γ t) / (γ t − z) ^ (k + 1)) = 2πi · n_z(γ) · f⁽ᵏ⁾(z) / k !,

the k-th Taylor coefficient of f at z weighted by the generalized winding number of γ about z. Only the residue at z contributes: the residue theorem for a null-homologous cycle applied to the Cauchy kernel w ↦ f w / (w − z) ^ (k + 1), whose only possible singularity in U is at z, leaves the single residue iteratedDeriv k f z / k !.

TauCeti.Contour.cauchyIntegralFormula_iteratedDeriv_nullHomologous {f : ℂ → ℂ} {U : Set ℂ}
  {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U)
  (hγ : TauCeti.IsPiecewiseC1On γ a b) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b)
  (hnull : TauCeti.Contour.IsNullHomologous γ a b U) (hz : z ∈ U)
  (hoff : ∀ t ∈ Set.uIcc a b, γ t ≠ z) (k : ℕ) :
  ∫ (t : ℝ) in a..b, deriv γ t • (f (γ t) / (γ t - z) ^ (k + 1)) =
    2 * ↑Real.pi * Complex.I * TauCeti.Contour.windingNumber γ a b z *
      (iteratedDeriv k f z / ↑k.factorial)
Informally uses
Lean

Formalized in Tau Ceti as TauCeti.Contour.cauchyIntegralFormula_iteratedDeriv_nullHomologous.

Other forms

Cauchy's integral formula for a cycle (roadmap Layer 3). Formalized in Tau Ceti as TauCeti.Contour.Cycle.cauchyIntegralFormula_nullHomologous.

TauCeti.Contour.Cycle.cauchyIntegralFormula_nullHomologous {f : ℂ → ℂ} {U : Set ℂ} {z : ℂ}
  (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) {C : TauCeti.Contour.Cycle} (hCU : C.IsIn U)
  (hnull : C.IsNullHomologous U) (hz : z ∈ U) (hoff : z ∉ C.trace) :
  (TauCeti.Contour.Cycle.integral fun w => f w / (w - z)) C =
    2 * ↑Real.pi * Complex.I * (TauCeti.Contour.Cycle.windingNumber z) C * f z

Cauchy's integral formula for a cycle, first derivative. Formalized in Tau Ceti as TauCeti.Contour.Cycle.cauchyIntegralFormula_deriv_nullHomologous.

TauCeti.Contour.Cycle.cauchyIntegralFormula_deriv_nullHomologous {f : ℂ → ℂ} {U : Set ℂ} {z : ℂ}
  (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) {C : TauCeti.Contour.Cycle} (hCU : C.IsIn U)
  (hnull : C.IsNullHomologous U) (hz : z ∈ U) (hoff : z ∉ C.trace) :
  (TauCeti.Contour.Cycle.integral fun w => f w / (w - z) ^ 2) C =
    2 * ↑Real.pi * Complex.I * (TauCeti.Contour.Cycle.windingNumber z) C * deriv f z

Cauchy's integral formula for a cycle, first derivative of a Banach-valued function. Formalized in Tau Ceti as TauCeti.Contour.Cycle.cauchyIntegralFormula_deriv_smul_nullHomologous.

TauCeti.Contour.Cycle.cauchyIntegralFormula_deriv_smul_nullHomologous.{u_1} {U : Set ℂ}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {z : ℂ}
  (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) {C : TauCeti.Contour.Cycle} (hCU : C.IsIn U)
  (hnull : C.IsNullHomologous U) (hz : z ∈ U) (hoff : z ∉ C.trace) :
  (TauCeti.Contour.Cycle.integral fun w => ((w - z) ^ 2)⁻¹ • f w) C =
    (2 * ↑Real.pi * Complex.I * (TauCeti.Contour.Cycle.windingNumber z) C) • deriv f z

Cauchy's integral formula for a cycle, for a Banach-valued function. Formalized in Tau Ceti as TauCeti.Contour.Cycle.cauchyIntegralFormula_smul_nullHomologous.

TauCeti.Contour.Cycle.cauchyIntegralFormula_smul_nullHomologous.{u_1} {U : Set ℂ} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {z : ℂ} (hU : IsOpen U)
  (hf : DifferentiableOn ℂ f U) {C : TauCeti.Contour.Cycle} (hCU : C.IsIn U)
  (hnull : C.IsNullHomologous U) (hz : z ∈ U) (hoff : z ∉ C.trace) :
  (TauCeti.Contour.Cycle.integral fun w => (w - z)⁻¹ • f w) C =
    (2 * ↑Real.pi * Complex.I * (TauCeti.Contour.Cycle.windingNumber z) C) • f z

Cauchy's integral formula for a cycle, for the k-th derivative. Formalized in Tau Ceti as TauCeti.Contour.Cycle.cauchyIntegralFormula_iteratedDeriv_nullHomologous.

TauCeti.Contour.Cycle.cauchyIntegralFormula_iteratedDeriv_nullHomologous {f : ℂ → ℂ} {U : Set ℂ}
  {z : ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) {C : TauCeti.Contour.Cycle} (hCU : C.IsIn U)
  (hnull : C.IsNullHomologous U) (hz : z ∈ U) (hoff : z ∉ C.trace) (k : ℕ) :
  (TauCeti.Contour.Cycle.integral fun w => f w / (w - z) ^ (k + 1)) C =
    2 * ↑Real.pi * Complex.I * (TauCeti.Contour.Cycle.windingNumber z) C *
      (iteratedDeriv k f z / ↑k.factorial)

Cauchy's integral formula for a cycle, for the k-th derivative of a Banach-valued function. Formalized in Tau Ceti as TauCeti.Contour.Cycle.cauchyIntegralFormula_iteratedDeriv_smul_nullHomologous.

TauCeti.Contour.Cycle.cauchyIntegralFormula_iteratedDeriv_smul_nullHomologous.{u_1} {U : Set ℂ}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {z : ℂ}
  (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) {C : TauCeti.Contour.Cycle} (hCU : C.IsIn U)
  (hnull : C.IsNullHomologous U) (hz : z ∈ U) (hoff : z ∉ C.trace) (k : ℕ) :
  (TauCeti.Contour.Cycle.integral fun w => ((w - z) ^ (k + 1))⁻¹ • f w) C =
    (2 * ↑Real.pi * Complex.I * (TauCeti.Contour.Cycle.windingNumber z) C / ↑k.factorial) •
      iteratedDeriv k f z

Cauchy's integral formula for the first derivative, homology form. Formalized in Tau Ceti as TauCeti.Contour.cauchyIntegralFormula_deriv_nullHomologous.

TauCeti.Contour.cauchyIntegralFormula_deriv_nullHomologous {f : ℂ → ℂ} {U : Set ℂ} {γ : ℝ → ℂ}
  {a b : ℝ} {z : ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U)
  (hγ : TauCeti.IsPiecewiseC1On γ a b) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b)
  (hnull : TauCeti.Contour.IsNullHomologous γ a b U) (hz : z ∈ U)
  (hoff : ∀ t ∈ Set.uIcc a b, γ t ≠ z) :
  ∫ (t : ℝ) in a..b, deriv γ t • (f (γ t) / (γ t - z) ^ 2) =
    2 * ↑Real.pi * Complex.I * TauCeti.Contour.windingNumber γ a b z * deriv f z

Cauchy's integral formula from pointwise Dixon-vanishing. Formalized in Tau Ceti as TauCeti.Contour.dixonH2_eq_windingNumber_mul_f_of_dixonFunction_eq_zero.

TauCeti.Contour.dixonH2_eq_windingNumber_mul_f_of_dixonFunction_eq_zero {f : ℂ → ℂ} {U : Set ℂ}
  {γ : ℝ → ℂ} {a b : ℝ} {w : ℂ} (h_cont : ContinuousOn γ (Set.uIcc a b)) (hw : w ∈ U)
  (hoff : ∀ t ∈ Set.uIcc a b, γ t ≠ w) (h_zero_at : TauCeti.Contour.dixonFunction f U γ a b w = 0)
  (h_cauchy_int :
    IntervalIntegrable (fun t => f (γ t) / (γ t - w) * deriv γ t) MeasureTheory.volume a b)
  (h_base_int : IntervalIntegrable (fun t => (γ t - w)⁻¹ * deriv γ t) MeasureTheory.volume a b) :
  TauCeti.Contour.dixonH2 f γ a b w =
    2 * ↑Real.pi * Complex.I * TauCeti.Contour.windingNumber γ a b w * f w

Cauchy's integral formula on a disc. Formalized in Tau Ceti as TauCeti.Contour.cauchyIntegralFormula_ball.

TauCeti.Contour.cauchyIntegralFormula_ball {f : ℂ → ℂ} {γ : ℝ → ℂ} {a b : ℝ} {c : ℂ} {r : ℝ} {z : ℂ}
  (hf : DifferentiableOn ℂ f (Metric.ball c r)) (hγ : TauCeti.IsPiecewiseC1On γ a b)
  (hγr : ∀ t ∈ Set.uIcc a b, γ t ∈ Metric.ball c r) (hclosed : γ a = γ b) (hz : z ∈ Metric.ball c r)
  (hoff : ∀ t ∈ Set.uIcc a b, γ t ≠ z) :
  ∫ (t : ℝ) in a..b, deriv γ t • (f (γ t) / (γ t - z)) =
    2 * ↑Real.pi * Complex.I * TauCeti.Contour.windingNumber γ a b z * f z

Cauchy's integral formula on a disc, for the k-th derivative. Formalized in Tau Ceti as TauCeti.Contour.cauchyIntegralFormula_iteratedDeriv_ball.

TauCeti.Contour.cauchyIntegralFormula_iteratedDeriv_ball {f : ℂ → ℂ} {γ : ℝ → ℂ} {a b : ℝ} {c : ℂ}
  {r : ℝ} {z : ℂ} (hf : DifferentiableOn ℂ f (Metric.ball c r)) (hγ : TauCeti.IsPiecewiseC1On γ a b)
  (hγr : ∀ t ∈ Set.uIcc a b, γ t ∈ Metric.ball c r) (hclosed : γ a = γ b) (hz : z ∈ Metric.ball c r)
  (hoff : ∀ t ∈ Set.uIcc a b, γ t ≠ z) (k : ℕ) :
  ∫ (t : ℝ) in a..b, deriv γ t • (f (γ t) / (γ t - z) ^ (k + 1)) =
    2 * ↑Real.pi * Complex.I * TauCeti.Contour.windingNumber γ a b z *
      (iteratedDeriv k f z / ↑k.factorial)

Cauchy's integral formula on a star-shaped open set. Formalized in Tau Ceti as TauCeti.Contour.cauchyIntegralFormula_starConvex.

TauCeti.Contour.cauchyIntegralFormula_starConvex {f : ℂ → ℂ} {Ω : Set ℂ} {γ : ℝ → ℂ} {a b : ℝ}
  {x z : ℂ} (hstar : StarConvex ℝ x Ω) (hopen : IsOpen Ω) (hf : DifferentiableOn ℂ f Ω)
  (hγ : TauCeti.IsPiecewiseC1On γ a b) (hγΩ : ∀ t ∈ Set.uIcc a b, γ t ∈ Ω) (hclosed : γ a = γ b)
  (hz : z ∈ Ω) (hoff : ∀ t ∈ Set.uIcc a b, γ t ≠ z) :
  ∫ (t : ℝ) in a..b, deriv γ t • (f (γ t) / (γ t - z)) =
    2 * ↑Real.pi * Complex.I * TauCeti.Contour.windingNumber γ a b z * f z

Cauchy's integral formula on a star-shaped open set, for the k-th derivative. Formalized in Tau Ceti as TauCeti.Contour.cauchyIntegralFormula_iteratedDeriv_starConvex.

TauCeti.Contour.cauchyIntegralFormula_iteratedDeriv_starConvex {f : ℂ → ℂ} {Ω : Set ℂ} {γ : ℝ → ℂ}
  {a b : ℝ} {x z : ℂ} (hstar : StarConvex ℝ x Ω) (hopen : IsOpen Ω) (hf : DifferentiableOn ℂ f Ω)
  (hγ : TauCeti.IsPiecewiseC1On γ a b) (hγΩ : ∀ t ∈ Set.uIcc a b, γ t ∈ Ω) (hclosed : γ a = γ b)
  (hz : z ∈ Ω) (hoff : ∀ t ∈ Set.uIcc a b, γ t ≠ z) (k : ℕ) :
  ∫ (t : ℝ) in a..b, deriv γ t • (f (γ t) / (γ t - z) ^ (k + 1)) =
    2 * ↑Real.pi * Complex.I * TauCeti.Contour.windingNumber γ a b z *
      (iteratedDeriv k f z / ↑k.factorial)

Cauchy's integral formula, homology form. Formalized in Tau Ceti as TauCeti.Contour.cauchyIntegralFormula_nullHomologous.

TauCeti.Contour.cauchyIntegralFormula_nullHomologous {f : ℂ → ℂ} {U : Set ℂ} {γ : ℝ → ℂ} {a b : ℝ}
  {z : ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) (hγ : TauCeti.IsPiecewiseC1On γ a b)
  (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b)
  (hnull : TauCeti.Contour.IsNullHomologous γ a b U) (hz : z ∈ U)
  (hoff : ∀ t ∈ Set.uIcc a b, γ t ≠ z) :
  ∫ (t : ℝ) in a..b, deriv γ t • (f (γ t) / (γ t - z)) =
    2 * ↑Real.pi * Complex.I * TauCeti.Contour.windingNumber γ a b z * f z
Sources
LeanTauCeti.Contour.cauchyIntegralFormula_iteratedDeriv_nullHomologous · TauCeti.Contour.Cycle.cauchyIntegralFormula_nullHomologous · TauCeti.Contour.Cycle.cauchyIntegralFormula_deriv_nullHomologous · TauCeti.Contour.Cycle.cauchyIntegralFormula_deriv_smul_nullHomologous · TauCeti.Contour.Cycle.cauchyIntegralFormula_smul_nullHomologous · TauCeti.Contour.Cycle.cauchyIntegralFormula_iteratedDeriv_nullHomologous · TauCeti.Contour.Cycle.cauchyIntegralFormula_iteratedDeriv_smul_nullHomologous · TauCeti.Contour.cauchyIntegralFormula_deriv_nullHomologous · TauCeti.Contour.dixonH2_eq_windingNumber_mul_f_of_dixonFunction_eq_zero · TauCeti.Contour.cauchyIntegralFormula_ball · TauCeti.Contour.cauchyIntegralFormula_iteratedDeriv_ball · TauCeti.Contour.cauchyIntegralFormula_starConvex · TauCeti.Contour.cauchyIntegralFormula_iteratedDeriv_starConvex · TauCeti.Contour.cauchyIntegralFormula_nullHomologous
Uses 3 · Used by 2
Statement usesGeneralized winding number (HW Def 2.1) · TauCeti.Contour.Cycle
Proof usesThe residue of the Cauchy kernel
Used byNull-homologous Cauchy integral formula at an off-curve point · The pointwise homology Cauchy theorem ∮_γ f = 0

TheoremThe classical residue theorem for a null-homologous contour cycle#

Let U be open, S a finite set, f differentiable on U ∖ S and meromorphic at each point of S lying in U, and let C be a contour cycle in U, null-homologous in U, whose trace avoids S. Then

Cycle.integral f C = 2πi · ∑_{s ∈ S} n_s(C) · Res_s f,

each pole weighted by the generalized winding number of C about it.

Null-homology is asked of the cycle only, never of its generators, so the theorem covers the combinations that make cycles worth having: a difference of two loops around a hole of U, neither of them null-homologous, is. Points of S outside U are harmless rather than excluded, their winding number vanishing by null-homology, and S may list regular points of f, whose residues are 0.

Its S = ∅ case is the homology Cauchy theorem for cycles (TauCeti.Contour.Cycle.homologyCauchyTheorem), and its one-generator case is the single-curve theorem TauCeti.Contour.classicalResidueTheorem_nullHomologous.

TauCeti.Contour.Cycle.classicalResidueTheorem_nullHomologous {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ}
  (hU : IsOpen U) (hf : DifferentiableOn ℂ f (U \ ↑S)) (hmero : ∀ s ∈ S, s ∈ U → MeromorphicAt f s)
  {C : TauCeti.Contour.Cycle} (hCU : C.IsIn U) (hoff : ∀ s ∈ S, s ∉ C.trace)
  (hnull : C.IsNullHomologous U) :
  (TauCeti.Contour.Cycle.integral f) C =
    2 * ↑Real.pi * Complex.I *
      ∑ s ∈ S, (TauCeti.Contour.Cycle.windingNumber s) C * TauCeti.Contour.residue f s
Lean

Formalized in Tau Ceti as TauCeti.Contour.Cycle.classicalResidueTheorem_nullHomologous.

Other forms

The classical residue theorem for a cycle in a star-shaped open set. Formalized in Tau Ceti as TauCeti.Contour.Cycle.classicalResidueTheorem_starConvex.

TauCeti.Contour.Cycle.classicalResidueTheorem_starConvex {f : ℂ → ℂ} {Ω : Set ℂ} {x : ℂ}
  {C : TauCeti.Contour.Cycle} {S : Finset ℂ} (hstar : StarConvex ℝ x Ω) (hopen : IsOpen Ω)
  (hf : DifferentiableOn ℂ f (Ω \ ↑S)) (hmero : ∀ s ∈ S, s ∈ Ω → MeromorphicAt f s) (hCΩ : C.IsIn Ω)
  (hoff : ∀ s ∈ S, s ∉ C.trace) :
  (TauCeti.Contour.Cycle.integral f) C =
    2 * ↑Real.pi * Complex.I *
      ∑ s ∈ S, (TauCeti.Contour.Cycle.windingNumber s) C * TauCeti.Contour.residue f s

The classical residue theorem for an arbitrary null-homologous cycle. Formalized in Tau Ceti as TauCeti.Contour.classicalResidueTheorem_nullHomologous.

TauCeti.Contour.classicalResidueTheorem_nullHomologous {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ}
  (hU : IsOpen U) (hf : DifferentiableOn ℂ f (U \ ↑S)) (hmero : ∀ s ∈ S, s ∈ U → MeromorphicAt f s)
  {γ : ℝ → ℂ} {a b : ℝ} (hγ : TauCeti.IsPiecewiseC1On γ a b) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U)
  (hclosed : γ a = γ b) (hoff : ∀ t ∈ Set.uIcc a b, γ t ∉ ↑S)
  (hnull : TauCeti.Contour.IsNullHomologous γ a b U) :
  ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) =
    2 * ↑Real.pi * Complex.I *
      ∑ s ∈ S, TauCeti.Contour.windingNumber γ a b s * TauCeti.Contour.residue f s
Sources
LeanTauCeti.Contour.Cycle.classicalResidueTheorem_nullHomologous · TauCeti.Contour.Cycle.classicalResidueTheorem_starConvex · TauCeti.Contour.classicalResidueTheorem_nullHomologous
Uses 5 · Used by 2
Statement usesGeneralized winding number (HW Def 2.1) · TauCeti.Contour.Cycle
Proof usesThe canonical Laurent decomposition · The homology Cauchy theorem for contour cycles · The residue theorem for a fixed polar-part decomposition
Used byRouché's theorem for a disc, classical form · The classical residue theorem on a circle

TheoremThe classical residue theorem on a circle#

If f is meromorphic on the closed disc C(c, R) (R > 0) and every point of nonzero meromorphic order lies in a finite set S inside the open disc, then ∮_{C(c,R)} f = 2πi · ∑_{s ∈ S} residue f s. Since residues at non-poles vanish, classicalResidueTheorem_circle_of_meromorphicOrderAt_neg proves the same conclusion asking only the poles (points of negative order) to lie in S.

TauCeti.Contour.classicalResidueTheorem_circle {f : ℂ → ℂ} {c : ℂ} {R : ℝ} (hR : 0 < R)
  (S : Finset ℂ) (hf : MeromorphicOn f (Metric.closedBall c R)) (hS : ↑S ⊆ Metric.ball c R)
  (hsupp : ∀ z ∈ Metric.closedBall c R, meromorphicOrderAt f z ≠ 0 → z ∈ S) :
  circleIntegral f c R = 2 * ↑Real.pi * Complex.I * ∑ s ∈ S, TauCeti.Contour.residue f s
Lean

Formalized in Tau Ceti as TauCeti.Contour.classicalResidueTheorem_circle.

Other forms

The classical residue theorem on a circle (sharp support form). Formalized in Tau Ceti as TauCeti.Contour.classicalResidueTheorem_circle_of_meromorphicOrderAt_neg.

TauCeti.Contour.classicalResidueTheorem_circle_of_meromorphicOrderAt_neg {f : ℂ → ℂ} {c : ℂ} {R : ℝ}
  (hR : 0 < R) (S : Finset ℂ) (hf : MeromorphicOn f (Metric.closedBall c R))
  (hS : ↑S ⊆ Metric.ball c R)
  (hsupp : ∀ z ∈ Metric.closedBall c R, meromorphicOrderAt f z < 0 → z ∈ S) :
  circleIntegral f c R = 2 * ↑Real.pi * Complex.I * ∑ s ∈ S, TauCeti.Contour.residue f s

The classical residue theorem on a star-shaped open set. Formalized in Tau Ceti as TauCeti.Contour.classicalResidueTheorem_starConvex.

TauCeti.Contour.classicalResidueTheorem_starConvex {f : ℂ → ℂ} {Ω : Set ℂ} {γ : ℝ → ℂ} {a b : ℝ}
  {x : ℂ} {S : Finset ℂ} (hstar : StarConvex ℝ x Ω) (hopen : IsOpen Ω)
  (hf : DifferentiableOn ℂ f (Ω \ ↑S)) (hmero : ∀ s ∈ S, s ∈ Ω → MeromorphicAt f s)
  (hγ : TauCeti.IsPiecewiseC1On γ a b) (hγΩ : ∀ t ∈ Set.uIcc a b, γ t ∈ Ω) (hclosed : γ a = γ b)
  (hoff : ∀ t ∈ Set.uIcc a b, γ t ∉ ↑S) :
  ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) =
    2 * ↑Real.pi * Complex.I *
      ∑ s ∈ S, TauCeti.Contour.windingNumber γ a b s * TauCeti.Contour.residue f s
Sources
LeanTauCeti.Contour.classicalResidueTheorem_circle · TauCeti.Contour.classicalResidueTheorem_circle_of_meromorphicOrderAt_neg · TauCeti.Contour.classicalResidueTheorem_starConvex
Uses 3 · Used by 1
Statement usesGeneralized winding number (HW Def 2.1)
Proof usesCauchy–Goursat for a pole-free meromorphic function · The classical residue theorem for a null-homologous contour cycle
Used byComplex analytic Weierstrass preparation theorem

AbbreviationTauCeti.Contour.Cycle#

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

TauCeti.Contour.Cycle : Type
Lean

Formalized in Tau Ceti as TauCeti.Contour.Cycle.

Sources
LeanTauCeti.Contour.Cycle
Used by 7
Used byThe homology Cauchy theorem for contour cycles · Cauchy's integral formula for the k-th derivative, homology form · The classical residue theorem for a null-homologous contour cycle · The Hungerbühler–Wasem generalized residue theorem for a contour cycle (HW Thm 3.3) · Cauchy's theorem on a disc · Fubini's theorem for cycles · The generalized residue theorem on a star-shaped open set, simple-pole regime

DefinitionGeneralized winding number (HW Def 2.1)#

n_{z₀}(γ) = (2πi)⁻¹ · PV ∮_γ dz/(z − z₀), the principal-value normalization of the index integral for a curve γ : ℝ → ℂ on [a, b] and any point z₀. See windingNumber_eq_integral_of_avoidance for its reduction to the ordinary index integral; as a limUnder-based value it is junk when the principal value does not exist.

TauCeti.Contour.windingNumber (γ : ℝ → ℂ) (a b : ℝ) (z₀ : ℂ) : ℂ
Lean

Formalized in Tau Ceti as TauCeti.Contour.windingNumber.

Sources
LeanTauCeti.Contour.windingNumber
Used by 28
Used byThe homology Cauchy theorem for contour cycles · A crosscut of a simply connected domain has exactly two sides · Carathéodory's continuity theorem, as a characterization · The Riemann map of a Jordan domain extends to a homeomorphism of the closures · The Schwarz--Christoffel theorem for a bounded polygonal Jordan domain · Rouché's theorem for a disc, classical form · Cauchy's integral formula for the k-th derivative, homology form · Hungerbühler--Wasem Proposition 2.2 (winding decomposition) · Null-homologous Cauchy integral formula at an off-curve point · The classical residue theorem for a null-homologous contour cycle · The classical residue theorem on a circle · The exact local angle contribution of one exit-time cap window · The homology Cauchy theorem (roadmap homologyCauchyTheorem, Layer 3) · The Hungerbühler–Wasem generalized residue theorem for a contour cycle (HW Thm 3.3) · The real bounded-integrand formula, allowing crossings (Hungerbühler–Wasem Prop 2.3) · The residue theorem for a fixed polar-part decomposition · Carathéodory's theorem for the inside of a Jordan curve · Cauchy's theorem on a disc · Jordan index theorem (orientation sign dichotomy) · The generalized residue theorem on a star-shaped open set, simple-pole regime · The half-disc residue theorem with enclosed possible singularities · The half-residue theorem at a simple pole · The pointwise homology Cauchy theorem ∮_γ f = 0 · Flux-divergence form of Green's theorem for a simple closed absolutely continuous curve · Green's theorem for a simple closed absolutely continuous curve · TauCeti.Green.green_ac_winding · Holomorphic functions have primitives on a star-shaped set · The valence formula at general level

DefinitionFirst exit time at radius ε (left side)#

the sSup of the times t ∈ [t₀ - δ, t₀] with ε ≤ ‖γ t - s‖ — the latest outside-the-ball time before t₀, which is the first exit when moving left from t₀. The junk value is sSup ∅ when the defining set is empty.

TauCeti.Contour.firstExitTimeLeft.{u_1} {E : Type u_1} [Sub E] [Norm E] (γ : ℝ → E) (t₀ δ : ℝ)
  (s : E) (ε : ℝ) : ℝ
Lean

Formalized in Tau Ceti as TauCeti.Contour.firstExitTimeLeft.

Sources
LeanTauCeti.Contour.firstExitTimeLeft
Used by 4
Used byHungerbühler--Wasem Proposition 2.2 (winding decomposition) · The exact local angle contribution of one exit-time cap window · The Hungerbühler–Wasem generalized residue theorem for a contour cycle (HW Thm 3.3) · The real bounded-integrand formula, allowing crossings (Hungerbühler–Wasem Prop 2.3)

TheoremThe exact local angle contribution of one exit-time cap window#

The winding number of the curve over the window minus that of its cap is crossingAngle γ t₀ / 2π. Beyond the standing continuity, tangent, and radius hypotheses -- which already give equal endpoint radii and endpoint matching -- the only extra input is the principal value of (z - s)⁻¹ along the generally asymmetric exit-time interval.

TauCeti.Contour.windingNumber_sub_cap_exitCapWindow_eq_crossingAngle_div_two_pi {γ : ℝ → ℂ} {s : ℂ}
  {t₀ δ ε : ℝ} {L_R L_L : ℂ} (hδ : 0 < δ) (hε : 0 < ε) (h_at : γ t₀ = s)
  (hγ : ContinuousOn γ (Set.Icc (t₀ - δ) (t₀ + δ))) (hεL : ε ≤ ‖γ (t₀ - δ) - s‖)
  (hεR : ε ≤ ‖γ (t₀ + δ) - s‖) (hL_R : L_R ≠ 0) (hL_L : L_L ≠ 0)
  (h_R : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L_R))
  (h_L : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L_L))
  (hpv :
    TauCeti.Contour.HasCauchyPVAt γ (TauCeti.Contour.exitCapWindow γ s t₀ δ ε L_R L_L).lower
      (TauCeti.Contour.exitCapWindow γ s t₀ δ ε L_R L_L).upper (fun z => (z - s)⁻¹) s
      (↑((-L_L / (γ (TauCeti.Contour.exitCapWindow γ s t₀ δ ε L_R L_L).lower - s)).arg +
            ((γ (TauCeti.Contour.exitCapWindow γ s t₀ δ ε L_R L_L).upper - s) / L_R).arg) *
        Complex.I)) :
  TauCeti.Contour.windingNumber γ (TauCeti.Contour.exitCapWindow γ s t₀ δ ε L_R L_L).lower
        (TauCeti.Contour.exitCapWindow γ s t₀ δ ε L_R L_L).upper s -
      TauCeti.Contour.windingNumber ((TauCeti.Contour.exitCapWindow γ s t₀ δ ε L_R L_L).cap s)
        (TauCeti.Contour.exitCapWindow γ s t₀ δ ε L_R L_L).lower
        (TauCeti.Contour.exitCapWindow γ s t₀ δ ε L_R L_L).upper s =
    ↑(TauCeti.Contour.crossingAngle γ t₀) / (2 * ↑Real.pi)
Lean

Formalized in Tau Ceti as TauCeti.Contour.windingNumber_sub_cap_exitCapWindow_eq_crossingAngle_div_two_pi.

Sources
LeanTauCeti.Contour.windingNumber_sub_cap_exitCapWindow_eq_crossingAngle_div_two_pi
Uses 2 · Used by 1
Statement usesFirst exit time at radius ε (left side) · Generalized winding number (HW Def 2.1)
Used byHungerbühler--Wasem Proposition 2.2 (winding decomposition)

TheoremThe residue of the Cauchy kernel#

If g is analytic at z₀, then the function g z / (z - z₀) ^ (k + 1) has residue the Taylor coefficient iteratedDeriv k g z₀ / k ! at z₀: the whole Laurent principal part comes from the first k + 1 Taylor terms of g, and only the one of index k sits at order −1. This is the residue behind Cauchy's integral formula for the k-th derivative; the constant case is TauCeti.Contour.residue_const_div_sub_pow.

TauCeti.Contour.residue_div_sub_pow_of_analyticAt {g : ℂ → ℂ} {z₀ : ℂ} (hg : AnalyticAt ℂ g z₀)
  (k : ℕ) :
  TauCeti.Contour.residue (fun z => g z / (z - z₀) ^ (k + 1)) z₀ =
    iteratedDeriv k g z₀ / ↑k.factorial
Lean

Formalized in Tau Ceti as TauCeti.Contour.residue_div_sub_pow_of_analyticAt.

Sources
LeanTauCeti.Contour.residue_div_sub_pow_of_analyticAt
Used by 1
Used byCauchy's integral formula for the k-th derivative, homology form

TheoremNull-homologous Cauchy integral formula at an off-curve point#

Let γ be a closed curve in an open set U, continuous on uIcc a b, differentiable off a countable set, with interval-integrable derivative, and null-homologous in U. If f is holomorphic on U and w ∈ U is not on the curve, then the Cauchy-type integral evaluates to 2πi · windingNumber γ a b w · f w.

This is the Cauchy-integral-formula output of Dixon's vanishing theorem. The off-curve point is kept as an explicit hypothesis; proving that such a point exists in the ambient domain is a separate geometric prerequisite for the full global homology Cauchy theorem.

TauCeti.Contour.dixonH2_eq_windingNumber_mul_f_of_nullHomologous {f : ℂ → ℂ} {U : Set ℂ} {γ : ℝ → ℂ}
  {a b : ℝ} {P : Set ℝ} {w : ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U)
  (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U)
  (hderiv_int : IntervalIntegrable (fun t => deriv γ t) MeasureTheory.volume a b)
  (hclosed : γ a = γ b) (hP : P.Countable)
  (hγ_diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ t)
  (h_null : TauCeti.Contour.IsNullHomologous γ a b U) (hwU : w ∈ U)
  (hoff : ∀ t ∈ Set.uIcc a b, γ t ≠ w) :
  TauCeti.Contour.dixonH2 f γ a b w =
    2 * ↑Real.pi * Complex.I * TauCeti.Contour.windingNumber γ a b w * f w
Lean

Formalized in Tau Ceti as TauCeti.Contour.dixonH2_eq_windingNumber_mul_f_of_nullHomologous.

Sources
LeanTauCeti.Contour.dixonH2_eq_windingNumber_mul_f_of_nullHomologous
Uses 2
Statement usesGeneralized winding number (HW Def 2.1)
Proof usesCauchy's integral formula for the k-th derivative, homology form

TheoremThe residue theorem for a fixed polar-part decomposition#

Once f is presented on U as an analytic remainder plus finite Laurent tails at the points of S, a closed null-homologous piecewise-C¹ curve in U avoiding S integrates to the winding-weighted residue sum. This is the sum of the two preceding facts: the remainder contributes nothing (intervalIntegral_deriv_smul_analyticRemainder_eq_zero) and the tails contribute the residue sum (intervalIntegral_deriv_smul_eq_analyticRemainder_add_sum).

TauCeti.Contour.PolarPartDecomposition.intervalIntegral_deriv_smul_eq_sum_windingNumber_mul_residue
  {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (decomp : TauCeti.Contour.PolarPartDecomposition f S U)
  (hU : IsOpen U) {γ : ℝ → ℂ} {a b : ℝ} (hγ : TauCeti.IsPiecewiseC1On γ a b)
  (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b) (hoff : ∀ t ∈ Set.uIcc a b, γ t ∉ ↑S)
  (hnull : TauCeti.Contour.IsNullHomologous γ a b U) :
  ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) =
    2 * ↑Real.pi * Complex.I *
      ∑ s ∈ S, TauCeti.Contour.windingNumber γ a b s * TauCeti.Contour.residue f s
Lean

Formalized in Tau Ceti as TauCeti.Contour.PolarPartDecomposition.intervalIntegral_deriv_smul_eq_sum_windingNumber_mul_residue.

Sources
LeanTauCeti.Contour.PolarPartDecomposition.intervalIntegral_deriv_smul_eq_sum_windingNumber_mul_residue
Uses 2 · Used by 1
Statement usesGeneralized winding number (HW Def 2.1)
Proof usesThe homology Cauchy theorem (roadmap homologyCauchyTheorem, Layer 3)
Used byThe classical residue theorem for a null-homologous contour cycle

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.