Documentation

TauCeti.Analysis.Contour.Argument.Cycle

The argument principle for an arbitrary null-homologous cycle #

For f whose zeros and poles in an open set U all lie in a finite set S, and a closed piecewise-C¹ curve γ that is null-homologous in U and avoids S,

∫ t in a..b, γ' t • logDeriv f (γ t) = 2πi · ∑_{z ∈ S} n_z(γ) · ord z,

where n_z(γ) is the generalized winding number of γ about z and ord is a caller-supplied integer-valued function required to agree with meromorphicOrderAt f only at the points of S that lie in U — positive at a zero, negative at a pole. Nothing is asked of f or of ord at a point of S outside U: null-homology forces the winding number there to vanish, so its term drops out whatever ord says. This is the arbitrary-cycle form of the argument principle: the roadmap's Layer-2 statement TauCeti.Contour.argumentPrinciple fixes the contour to be a round circle with every special point strictly inside, so each order is counted exactly once; here the contour is any piecewise-C¹ loop and each order is counted with the multiplicity with which the loop winds around it.

The proof is the classical one-liner over the two pieces the repository already has: the residue theorem for a null-homologous cycle (TauCeti.Contour.classicalResidueTheorem_nullHomologous) applied to logDeriv f, whose residue at each point is the order of f there (TauCeti.Contour.residue_logDeriv_eq_meromorphicOrderAt). What has to be supplied is the input regularity of logDeriv f rather than of f: on U ∖ S the logarithmic derivative is holomorphic because f is analytic and non-vanishing there (a zero of f is a pole of logDeriv f, which is exactly why the hypothesis asks S to collect the zeros as well as the poles), and at each point of S lying in U it is meromorphic because f is.

Null-homology is load-bearing, as it already is for the residue theorem: on a domain with a hole a loop that merely avoids the zeros and poles can still see the function's behaviour in the hole, and n_w(γ) = 0 for every w ∉ U is exactly the hypothesis that rules this out.

Unlike the circle statement, the hypotheses ask for genuine analyticity and non-vanishing of f at every point of U ∖ S, so no pointwise "wrong value" there is tolerated. Nothing pointwise is asked at the points of S lying in U, where only meromorphy is required, nor anywhere outside U. The circle proof may instead replace f by its meromorphic normal form, because a circle integral is unchanged by a change of integrand on a set codiscrete within the sphere (circleIntegral.circleIntegral_congr_codiscreteWithin); no such congruence is available for a general piecewise-C¹ contour, and the null-homologous residue theorem used here asks for honest differentiability of logDeriv f on U ∖ S.

Main results #

This is the arbitrary-cycle upgrade of a Layer-2 target of the contour-integration roadmap; like the residue theorem it rests on it, it is a Layer-3 statement, since its hypotheses and its proof go through the homology Cauchy theorem.

Provenance #

No formal source is vendored: the statement is assembled here from the repository's residue theorem for a null-homologous cycle and the local residue-form of the argument principle, which are themselves migrated from the AINTLIB LeanModularForms development (where the residue theorem is applied to logDeriv f).

References #

source
theorem TauCeti.Contour.argumentPrinciple_nullHomologous {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} {ord : ℂ → ℤ} (hU : IsOpen U) (hoff : ∀ z ∈ U, z ∉ S → AnalyticAt ℂ f z ∧ f z ≠ 0) (hmero : ∀ s ∈ S, s ∈ U → MeromorphicAt f s) (hord : ∀ s ∈ S, s ∈ U → meromorphicOrderAt f s = ↑(ord s)) {γ : ℝ → ℂ} {a b : ℝ} (hγ : IsPiecewiseC1On γ a b) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b) (hγoff : ∀ t ∈ Set.uIcc a b, γ t ∉ ↑S) (hnull : IsNullHomologous γ a b U) :
∫ (t : ℝ) in a..b, deriv γ t • logDeriv f (γ t) = 2 * ↑Real.pi * Complex.I * ∑ z ∈ S, windingNumber γ a b z * ↑(ord z)

The argument principle for an arbitrary null-homologous cycle. Let U be open, S a finite set collecting every zero and pole of f in U: f is analytic and non-vanishing at each point of U ∖ S, and meromorphic of order ord s at each s ∈ S lying in U. Let γ be a closed piecewise-C¹ curve in U, null-homologous in U, that avoids S. Then the contour integral of the logarithmic derivative counts the orders, each weighted by the winding number of γ about it:

∫ t in a..b, γ' t • logDeriv f (γ t) = 2πi · ∑_{z ∈ S} n_z(γ) · ord z.

Since ord is positive at a zero and negative at a pole, this is 2πi times the number of zeros minus poles counted with multiplicity and with winding multiplicity — for a simple loop enclosing them once, the classical zero-minus-pole count.

As in TauCeti.Contour.classicalResidueTheorem_nullHomologous, points of S outside U are harmless rather than excluded: null-homology forces their winding number, hence their contribution, to vanish, so nothing is asked of f there. Likewise S may list regular non-vanishing points of f, whose order is 0.

The round-circle case, which asks nothing pointwise of f because it may pass to the meromorphic normal form, is TauCeti.Contour.argumentPrinciple.

source
theorem TauCeti.Contour.argumentPrinciple_nullHomologous_local {f : ℂ → ℂ} {U : Set ℂ} {z₀ : ℂ} {n : ℤ} (hU : IsOpen U) (hmero : z₀ ∈ U → MeromorphicAt f z₀) (hn : z₀ ∈ U → meromorphicOrderAt f z₀ = ↑n) (hoff : ∀ z ∈ U, z ≠ z₀ → AnalyticAt ℂ f z ∧ f z ≠ 0) {γ : ℝ → ℂ} {a b : ℝ} (hγ : IsPiecewiseC1On γ a b) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b) (hγoff : ∀ t ∈ Set.uIcc a b, γ t ≠ z₀) (hnull : IsNullHomologous γ a b U) :
∫ (t : ℝ) in a..b, deriv γ t • logDeriv f (γ t) = 2 * ↑Real.pi * Complex.I * (windingNumber γ a b z₀ * ↑n)

The argument principle for a cycle around a single zero or pole. If z₀ is the only point of an open U at which f fails to be analytic and non-vanishing, of order n there, and γ is a closed piecewise-C¹ curve in U, null-homologous in U, missing z₀, then

∫ t in a..b, γ' t • logDeriv f (γ t) = 2πi · n_{z₀}(γ) · n.

This is the S = {z₀} case of TauCeti.Contour.argumentPrinciple_nullHomologous, and the arbitrary-cycle counterpart of TauCeti.Contour.argumentPrinciple_local: a loop winding k times around a zero of order n integrates f'/f to 2πi · k · n.

Membership z₀ ∈ U is not required, and nothing at all is asked of f at z₀ unless it holds: if z₀ lies outside U then f is analytic and non-vanishing on all of U, and null-homology makes n_{z₀}(γ) vanish, so both sides are 0 for any n. Accordingly the meromorphy and the order hypotheses are conditional on z₀ ∈ U, exactly as they are in TauCeti.Contour.argumentPrinciple_nullHomologous.

source
theorem TauCeti.Contour.argumentPrinciple_nullHomologous_of_analyticOnNhd {f : ℂ → ℂ} {S : Finset ℂ} {U : Set ℂ} (hU : IsOpen U) (hf : AnalyticOnNhd ℂ f U) (hzeros : ∀ z ∈ U, f z = 0 → z ∈ S) {γ : ℝ → ℂ} {a b : ℝ} (hγ : IsPiecewiseC1On γ a b) (hγU : ∀ t ∈ Set.uIcc a b, γ t ∈ U) (hclosed : γ a = γ b) (hγoff : ∀ t ∈ Set.uIcc a b, f (γ t) ≠ 0) (hnull : IsNullHomologous γ a b U) :
∫ (t : ℝ) in a..b, deriv γ t • logDeriv f (γ t) = 2 * ↑Real.pi * Complex.I * ∑ z ∈ S, windingNumber γ a b z * ↑(analyticOrderNatAt f z)

Winding-weighted zero counting. Let f be analytic on an open U with all its zeros in a finite set S, and let γ be a closed piecewise-C¹ curve in U, null-homologous in U, along which f does not vanish. Then

∫ t in a..b, γ' t • logDeriv f (γ t) = 2πi · ∑_{z ∈ S} n_z(γ) · analyticOrderNatAt f z:

the contour integral of f'/f counts the zeros of f with multiplicity, each weighted by the winding number of γ about it. This is the pole-free specialisation of TauCeti.Contour.argumentPrinciple_nullHomologous, with the orders read off by analyticOrderNatAt instead of by a caller-supplied ord.

Only the zeros need be avoided, not all of S: S may list points where f does not vanish, and γ is free to run through them, since logDeriv f is holomorphic there and their order — and so their term in the sum — is 0.

The zeros are automatically of finite order (TauCeti.analyticOrderAt_ne_top_of_zeros_subset): confining them to a finite set already rules out f vanishing identically near a point of U.