Contour

Results named in Tau Ceti's TauCeti.Analysis.Contour modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe canonical Laurent decomposition#

near s, f is the analytic part plus the polar part.

TauCeti.Contour.eventuallyEq_meromorphicAnalyticPartAt_add_meromorphicPolarPartAt {f : ℂ → ℂ}
  {s : ℂ} (hMero : MeromorphicAt f s) :
  ∀ᶠ (z : ℂ) in nhdsWithin s {s}ᶜ,
    f z =
      TauCeti.Contour.meromorphicAnalyticPartAt hMero z +
        TauCeti.Contour.meromorphicPolarPartAt hMero z
Lean

Formalized in Tau Ceti as TauCeti.Contour.eventuallyEq_meromorphicAnalyticPartAt_add_meromorphicPolarPartAt.

Sources
LeanTauCeti.Contour.eventuallyEq_meromorphicAnalyticPartAt_add_meromorphicPolarPartAt
Used by 3
Used byThe converse Schwarz--Christoffel theorem from the prevertex residues · 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)

TheoremCauchy's theorem on a disc#

Cauchy's theorem on a disc — the Metric.ball case of TauCeti.Contour.cauchyTheorem_starConvex: a function holomorphic on a disc integrates to zero along every closed piecewise-C¹ curve inside it, not only along the boundary circles.

TauCeti.Contour.cauchyTheorem_ball {f : ℂ → ℂ} {γ : ℝ → ℂ} {a b : ℝ} {c : ℂ} {r : ℝ}
  (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) :
  ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = 0
Lean

Formalized in Tau Ceti as TauCeti.Contour.cauchyTheorem_ball.

Other forms

Cauchy's theorem for a cycle in a star-shaped open set. Formalized in Tau Ceti as TauCeti.Contour.Cycle.cauchyTheorem_starConvex.

TauCeti.Contour.Cycle.cauchyTheorem_starConvex {f : ℂ → ℂ} {Ω : Set ℂ} {x : ℂ}
  {C : TauCeti.Contour.Cycle} (hstar : StarConvex ℝ x Ω) (hopen : IsOpen Ω) (hCΩ : C.IsIn Ω)
  (hf : DifferentiableOn ℂ f Ω) : (TauCeti.Contour.Cycle.integral f) C = 0

Cauchy's theorem for a null-homotopic contour. Formalized in Tau Ceti as TauCeti.Contour.cauchyTheorem_of_pathHomotopy_refl.

TauCeti.Contour.cauchyTheorem_of_pathHomotopy_refl {f : ℂ → ℂ} {Ω : Set ℂ} (hΩ : IsOpen Ω) {x : ℂ}
  (p : Path x x) (hp : TauCeti.IsPiecewiseC1On (⇑p.extend) 0 1) (φ : p.Homotopy (Path.refl x))
  (hφΩ : ∀ (st : ↑unitInterval × ↑unitInterval), φ st ∈ Ω) (hf : DifferentiableOn ℂ f Ω) :
  ∫ (t : ℝ) in 0..1, deriv (⇑p.extend) t • f (p.extend t) = 0

Cauchy's theorem on a star-shaped open set. Formalized in Tau Ceti as TauCeti.Contour.cauchyTheorem_starConvex.

TauCeti.Contour.cauchyTheorem_starConvex {f : ℂ → ℂ} {Ω : Set ℂ} {γ : ℝ → ℂ} {a b : ℝ} {x : ℂ}
  (hstar : StarConvex ℝ x Ω) (hopen : IsOpen Ω) (hf : DifferentiableOn ℂ f Ω)
  (hγ : TauCeti.IsPiecewiseC1On γ a b) (hγΩ : ∀ t ∈ Set.uIcc a b, γ t ∈ Ω) (hclosed : γ a = γ b) :
  ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = 0
Sources
LeanTauCeti.Contour.cauchyTheorem_ball · TauCeti.Contour.Cycle.cauchyTheorem_starConvex · TauCeti.Contour.cauchyTheorem_of_pathHomotopy_refl · TauCeti.Contour.cauchyTheorem_starConvex
Uses 4
Statement usesTauCeti.Contour.Cycle
Proof usesGeneralized winding number (HW Def 2.1) · The homology Cauchy theorem (roadmap homologyCauchyTheorem, Layer 3) · The homology Cauchy theorem for contour cycles

TheoremCauchy–Goursat for a pole-free meromorphic function#

If A is meromorphic on the closed disc closedBall c R (R ≥ 0) and has non-negative meromorphic order at every point of the disc, then ∮ z in C(c, R), A z = 0.

TauCeti.Contour.circleIntegral_eq_zero_of_meromorphicOrderAt_nonneg.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℂ E] {A : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R)
  (hA : MeromorphicOn A (Metric.closedBall c R))
  (hord : ∀ z ∈ Metric.closedBall c R, 0 ≤ meromorphicOrderAt A z) : circleIntegral A c R = 0
Lean

Formalized in Tau Ceti as TauCeti.Contour.circleIntegral_eq_zero_of_meromorphicOrderAt_nonneg.

Sources
LeanTauCeti.Contour.circleIntegral_eq_zero_of_meromorphicOrderAt_nonneg
Used by 3
Used byRouché's theorem for a disc, classical form · The classical residue theorem on a circle · The valence formula at general level

TheoremFubini's theorem for cycles#

For a function F continuous on the product of the traces of two cycles C and D,

∫_C (∫_D F z w dw) dz = ∫_D (∫_C F z w dz) dw.

TauCeti.Contour.Cycle.integral_integral_swap.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] {F : ℂ → ℂ → E} {C D : TauCeti.Contour.Cycle}
  (hF : ContinuousOn (Function.uncurry F) (C.trace ×ˢ D.trace)) :
  (TauCeti.Contour.Cycle.integral fun z => (TauCeti.Contour.Cycle.integral (F z)) D) C =
    (TauCeti.Contour.Cycle.integral fun w => (TauCeti.Contour.Cycle.integral fun z => F z w) C) D
Lean

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

Sources
LeanTauCeti.Contour.Cycle.integral_integral_swap
Uses 1
Statement usesTauCeti.Contour.Cycle

TheoremThe generalized residue theorem on a star-shaped open set, simple-pole regime#

Let Ω be open and star-shaped about x, S ⊆ Ω finite, f holomorphic on Ω ∖ S with at worst a simple pole at each point of S, and γ a closed piecewise-C¹ immersion in Ω based off S. Then the Cauchy principal value of the contour integral is

p.v. ∮_γ f = 2πi · ∑_{s ∈ S} n_s(γ) · Res_s f,

with the generalized, possibly non-integer, winding numbers as weights. The curve is free to pass through the singularities; conditions (A′) and (B) of Hungerbühler–Wasem are automatic in this regime, while null-homology is automatic by star-shapedness. Thus null-homology and conditions (A′) and (B) require no additional hypotheses in this regime.

TauCeti.Contour.hungerbuhlerWasem_residueTheorem_of_simple_poles_starConvex {f : ℂ → ℂ} {Ω : Set ℂ}
  {γ : ℝ → ℂ} {a b : ℝ} {x : ℂ} {S : Finset ℂ} (hstar : StarConvex ℝ x Ω) (hopen : IsOpen Ω)
  (hγ_imm : TauCeti.Contour.IsPwC1ImmersionOn γ a b) (hSΩ : ↑S ⊆ Ω) (hclosed : γ a = γ b)
  (hγa : γ a ∉ ↑S) (hγΩ : ∀ t ∈ Set.uIcc a b, γ t ∈ Ω) (hf : DifferentiableOn ℂ f (Ω \ ↑S))
  (hmero : ∀ s ∈ S, MeromorphicAt f s) (h_simple : ∀ s ∈ S, ↑(-1) ≤ meromorphicOrderAt f s) :
  TauCeti.Contour.HasCauchyPV γ a b f
    (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.hungerbuhlerWasem_residueTheorem_of_simple_poles_starConvex.

Other forms

The generalized residue theorem for a contour cycle with simple poles — HW Thm 3.3's unconditional regime for cycles. Formalized in Tau Ceti as TauCeti.Contour.Cycle.hungerbuhlerWasem_residueTheorem_of_simple_poles.

TauCeti.Contour.Cycle.hungerbuhlerWasem_residueTheorem_of_simple_poles {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) (h_simple : ∀ s ∈ S, ↑(-1) ≤ meromorphicOrderAt f s) :
  C.HasCauchyPV f
    (2 * ↑Real.pi * Complex.I *
      ∑ s ∈ S, (TauCeti.Contour.Cycle.windingNumber s) C * TauCeti.Contour.residue f s)

The generalized residue theorem for a cycle in a star-shaped open set, simple-pole regime. Formalized in Tau Ceti as TauCeti.Contour.Cycle.hungerbuhlerWasem_residueTheorem_of_simple_poles_starConvex.

TauCeti.Contour.Cycle.hungerbuhlerWasem_residueTheorem_of_simple_poles_starConvex {f : ℂ → ℂ}
  {Ω : Set ℂ} {x : ℂ} {C : TauCeti.Contour.Cycle} {S : Finset ℂ} (hstar : StarConvex ℝ x Ω)
  (hopen : IsOpen Ω) (hSΩ : ↑S ⊆ Ω) (hf : DifferentiableOn ℂ f (Ω \ ↑S))
  (hmero : ∀ s ∈ S, MeromorphicAt f s) (hCΩ : C.IsIn Ω)
  (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)
  (h_simple : ∀ s ∈ S, ↑(-1) ≤ meromorphicOrderAt f s) :
  C.HasCauchyPV f
    (2 * ↑Real.pi * Complex.I *
      ∑ s ∈ S, (TauCeti.Contour.Cycle.windingNumber s) C * TauCeti.Contour.residue f s)

The generalized residue theorem for simple poles — HW Thm 3.3's unconditional regime. Formalized in Tau Ceti as TauCeti.Contour.hungerbuhlerWasem_residueTheorem_of_simple_poles.

TauCeti.Contour.hungerbuhlerWasem_residueTheorem_of_simple_poles {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)
  (h_simple : ∀ s ∈ S, ↑(-1) ≤ meromorphicOrderAt f s) :
  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.hungerbuhlerWasem_residueTheorem_of_simple_poles_starConvex · TauCeti.Contour.Cycle.hungerbuhlerWasem_residueTheorem_of_simple_poles · TauCeti.Contour.Cycle.hungerbuhlerWasem_residueTheorem_of_simple_poles_starConvex · TauCeti.Contour.hungerbuhlerWasem_residueTheorem_of_simple_poles
Uses 3 · Used by 2
Statement usesGeneralized winding number (HW Def 2.1) · TauCeti.Contour.Cycle
Proof usesThe Hungerbühler–Wasem generalized residue theorem for a contour cycle (HW Thm 3.3)
Used byThe half-disc residue theorem with enclosed possible singularities · The valence formula at general level

TheoremThe half-disc residue theorem with enclosed possible singularities#

Let f be holomorphic off the finite set insert 0 S, with at worst a simple singularity at each of its points, and let every point of S lie in the open upper half-disc of radius R. Then the Cauchy principal value of ∮ f along the half-disc boundary is

2π i · Σ_{s ∈ S} Res_s f + π i · Res₀ f:

each enclosed possible singularity contributes its full residue, because the generalized winding number there is 1, while the possible singularity on the contour contributes only half of its own. In the genuine simple-pole case, this is the half-residue contribution from the winding number ½ at a smooth crossing.

TauCeti.Contour.hasCauchyPV_halfDiscBoundary_of_simple_poles {R : ℝ} {S : Finset ℂ} {f : ℂ → ℂ}
  (hR : 0 < R) (hS : ∀ s ∈ S, 0 < s.im ∧ ‖s‖ < R)
  (hf : DifferentiableOn ℂ f (Set.univ \ ↑(insert 0 S)))
  (hmero : ∀ s ∈ insert 0 S, MeromorphicAt f s)
  (h_simple : ∀ s ∈ insert 0 S, ↑(-1) ≤ meromorphicOrderAt f s) :
  TauCeti.Contour.HasCauchyPV (TauCeti.Contour.halfDiscBoundary R) (-R) (R + Real.pi) f
    (2 * ↑Real.pi * Complex.I * ∑ s ∈ S, TauCeti.Contour.residue f s +
      ↑Real.pi * Complex.I * TauCeti.Contour.residue f 0)
Lean

Formalized in Tau Ceti as TauCeti.Contour.hasCauchyPV_halfDiscBoundary_of_simple_poles.

Sources
LeanTauCeti.Contour.hasCauchyPV_halfDiscBoundary_of_simple_poles
Uses 2 · Used by 1
Proof usesThe generalized residue theorem on a star-shaped open set, simple-pole regime · Generalized winding number (HW Def 2.1)
Used byThe half-residue theorem on the half-disc boundary

TheoremThe half-residue theorem at a simple pole#

the winding-½ case with the conditions discharged automatically — an on-cycle simple pole crossed by the immersion contributes πi · Res_s f. The acceptance form for the valence formula's i and ρ.

TauCeti.Contour.hasCauchyPV_half_residue_of_simple_pole {f : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U)
  (γ : ℝ → ℂ) (a b : ℝ) (s : ℂ) (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 : MeromorphicAt f s)
  (hnull : TauCeti.Contour.IsNullHomologous γ a b U) (h_simple : ↑(-1) ≤ meromorphicOrderAt f s)
  (hwind : TauCeti.Contour.windingNumber γ a b s = 1 / 2) :
  TauCeti.Contour.HasCauchyPV γ a b f (↑Real.pi * Complex.I * TauCeti.Contour.residue f s)
Lean

Formalized in Tau Ceti as TauCeti.Contour.hasCauchyPV_half_residue_of_simple_pole.

Sources
LeanTauCeti.Contour.hasCauchyPV_half_residue_of_simple_pole
Uses 2
Statement usesGeneralized winding number (HW Def 2.1)
Proof usesThe Hungerbühler–Wasem generalized residue theorem for a contour cycle (HW Thm 3.3)

TheoremThe half-residue theorem on the half-disc boundary#

If f is holomorphic off the origin and has at worst a simple pole there (the hypotheses also permit a removable singularity, or f holomorphic at 0, in which case the residue is 0), then along the half-disc boundary — which passes through the origin — the Cauchy principal value of ∫ f is π i · residue f 0: half of what the classical residue theorem would give for a pole enclosed by the contour, because the generalized winding number at a smooth crossing is ½.

This is hasCauchyPV_halfDiscBoundary_of_simple_poles with no enclosed poles.

TauCeti.Contour.hasCauchyPV_halfDiscBoundary_of_simple_pole {R : ℝ} {f : ℂ → ℂ} (hR : 0 < R)
  (hf : DifferentiableOn ℂ f (Set.univ \ {0})) (hmero : MeromorphicAt f 0)
  (h_simple : ↑(-1) ≤ meromorphicOrderAt f 0) :
  TauCeti.Contour.HasCauchyPV (TauCeti.Contour.halfDiscBoundary R) (-R) (R + Real.pi) f
    (↑Real.pi * Complex.I * TauCeti.Contour.residue f 0)
Lean

Formalized in Tau Ceti as TauCeti.Contour.hasCauchyPV_halfDiscBoundary_of_simple_pole.

Sources
LeanTauCeti.Contour.hasCauchyPV_halfDiscBoundary_of_simple_pole
Uses 1
Proof usesThe half-disc residue theorem with enclosed possible singularities

TheoremJordan index theorem (orientation sign dichotomy)#

for a simple closed absolutely continuous curve on [a, b] (a < b), jordanSign γ a b is either 1 or -1, and equals the winding number at every point of filledHull (γ '' uIcc a b) \ (γ '' uIcc a b).

AbsolutelyContinuousOnInterval.jordanSign_eq_one_or_neg_one {γ : ℝ → ℂ} {a b : ℝ} (hab : a < b)
  (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b)
  (hinj : Set.InjOn γ (Set.Ico a b)) :
  TauCeti.Contour.jordanSign γ a b = 1 ∨ TauCeti.Contour.jordanSign γ a b = -1
Lean

Formalized in Tau Ceti as AbsolutelyContinuousOnInterval.jordanSign_eq_one_or_neg_one.

Other forms

Jordan index theorem for rectifiable simple closed curves (orientation sign dichotomy). Formalized in Tau Ceti as BoundedVariationOn.jordanSign_naturalParameterization_eq_one_or_neg_one.

BoundedVariationOn.jordanSign_naturalParameterization_eq_one_or_neg_one {γ : ℝ → ℂ} {a b : ℝ}
  (hab : a < b) (hγ : BoundedVariationOn γ (Set.Icc a b)) (hcont : ContinuousOn γ (Set.Icc a b))
  (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b)) :
  TauCeti.Contour.jordanSign (naturalParameterization γ (Set.Icc a b) a) 0
        (eVariationOn γ (Set.Icc a b)).toReal =
      1 ∨
    TauCeti.Contour.jordanSign (naturalParameterization γ (Set.Icc a b) a) 0
        (eVariationOn γ (Set.Icc a b)).toReal =
      -1

The Jordan index theorem for simple closed absolutely continuous curves. Formalized in Tau Ceti as AbsolutelyContinuousOnInterval.windingNumber_eq_jordanSign_of_mem_filledHull_sdiff.

AbsolutelyContinuousOnInterval.windingNumber_eq_jordanSign_of_mem_filledHull_sdiff {γ : ℝ → ℂ}
  {a b : ℝ} {z : ℂ} (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b)
  (hinj : Set.InjOn γ (Set.Ico a b))
  (hz : z ∈ TauCeti.filledHull (γ '' Set.uIcc a b) \ γ '' Set.uIcc a b) :
  TauCeti.Contour.windingNumber γ a b z = ↑(TauCeti.Contour.jordanSign γ a b)

The Jordan index theorem for the arclength parametrization of a rectifiable simple closed curve. Formalized in Tau Ceti as BoundedVariationOn.windingNumber_naturalParameterization_eq_jordanSign.

BoundedVariationOn.windingNumber_naturalParameterization_eq_jordanSign {γ : ℝ → ℂ} {a b : ℝ} {z : ℂ}
  (hab : a < b) (hγ : BoundedVariationOn γ (Set.Icc a b)) (hcont : ContinuousOn γ (Set.Icc a b))
  (hclosed : γ a = γ b) (hinj : Set.InjOn γ (Set.Ico a b))
  (hz : z ∈ TauCeti.filledHull (γ '' Set.Icc a b) \ γ '' Set.Icc a b) :
  TauCeti.Contour.windingNumber (naturalParameterization γ (Set.Icc a b) a) 0
      (eVariationOn γ (Set.Icc a b)).toReal z =
    ↑(TauCeti.Contour.jordanSign (naturalParameterization γ (Set.Icc a b) a) 0
        (eVariationOn γ (Set.Icc a b)).toReal)
Sources
LeanAbsolutelyContinuousOnInterval.jordanSign_eq_one_or_neg_one · BoundedVariationOn.jordanSign_naturalParameterization_eq_one_or_neg_one · AbsolutelyContinuousOnInterval.windingNumber_eq_jordanSign_of_mem_filledHull_sdiff · BoundedVariationOn.windingNumber_naturalParameterization_eq_jordanSign
Uses 4 · Used by 1
Statement usesGeneralized winding number (HW Def 2.1)
Proof usesFundamental theorem for absolutely continuous curves, integrability · The Jordan curve theorem · The Jordan separation theorem
Used byGreen's theorem for a simple closed absolutely continuous curve

TheoremJordan's lemma#

If ‖f‖ ≤ M on the upper semicircle of radius R, then for a > 0 the arc contribution of f z · e^{iaz} is at most π M / a in norm — a bound independent of R, obtained without assuming any decay of f.

No integrability hypothesis is imposed on the integrand, matching the Mathlib norm-of-integral idiom (intervalIntegral.norm_integral_le_of_norm_le constrains only the dominating function). When the parameterized integrand fails to be integrable the interval integral totalizes to 0 and the bound reads 0 ≤ π M / a, which holds since 0 ≤ M; the content of the lemma is therefore unchanged, and callers are not obliged to discharge integrability.

TauCeti.Contour.norm_integral_semicircle_exp_mul_le.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] {f : ℂ → E} {a R M : ℝ} (ha : 0 < a) (hR : 0 ≤ R)
  (hM : ∀ θ ∈ Set.Icc 0 Real.pi, ‖f (circleMap 0 R θ)‖ ≤ M) :
  ‖∫ (θ : ℝ) in 0..Real.pi,
        (Complex.exp (Complex.I * ↑a * circleMap 0 R θ) * deriv (circleMap 0 R) θ) •
          f (circleMap 0 R θ)‖ ≤
    Real.pi * M / a
Lean

Formalized in Tau Ceti as TauCeti.Contour.norm_integral_semicircle_exp_mul_le.

Sources
LeanTauCeti.Contour.norm_integral_semicircle_exp_mul_le
Uses 1
Proof usesJordan's integral bound

TheoremThe pointwise homology Cauchy theorem ∮_γ f = 0#

Applying the Cauchy integral formula to the twist g z = (z - w₀) · f z, which satisfies g w₀ = 0, forces dixonH2 g γ a b w₀ = 0; and since g (γ t) / (γ t - w₀) = f (γ t) for γ off w₀, that Cauchy-type integral is the contour integral of f. Hence ∫ t in a..b, deriv γ t • f (γ t) = 0, given the pointwise vanishing dixonFunction (fun z ↦ (z - w₀) * f z) U γ a b w₀ = 0, interval-integrability of the contour integrand deriv γ • f ∘ γ, and of the index integrand. Discharging the vanishing via dixonFunction_eq_zero yields the roadmap homologyCauchyTheorem.

TauCeti.Contour.intervalIntegral_deriv_smul_eq_zero_of_dixonFunction_eq_zero {f : ℂ → ℂ} {U : Set ℂ}
  {γ : ℝ → ℂ} {a b : ℝ} (h_cont : ContinuousOn γ (Set.uIcc a b)) (w₀ : ℂ) (hw₀_in_U : w₀ ∈ U)
  (hw₀_off : ∀ t ∈ Set.uIcc a b, γ t ≠ w₀)
  (h_zero_at : TauCeti.Contour.dixonFunction (fun z => (z - w₀) * f z) U γ a b w₀ = 0)
  (h_int : IntervalIntegrable (fun t => deriv γ t • f (γ t)) MeasureTheory.volume a b)
  (h_base_int : IntervalIntegrable (fun t => (γ t - w₀)⁻¹ * deriv γ t) MeasureTheory.volume a b) :
  ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = 0
Lean

Formalized in Tau Ceti as TauCeti.Contour.intervalIntegral_deriv_smul_eq_zero_of_dixonFunction_eq_zero.

Sources
LeanTauCeti.Contour.intervalIntegral_deriv_smul_eq_zero_of_dixonFunction_eq_zero
Uses 2 · Used by 1
Proof usesCauchy's integral formula for the k-th derivative, homology form · Generalized winding number (HW Def 2.1)
Used byThe homology Cauchy theorem (roadmap homologyCauchyTheorem, Layer 3)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.