Rouché's theorem #
If f and g are holomorphic on a closed disc and ‖f - g‖ < ‖f‖ + ‖g‖ everywhere on the
bounding circle, then f and g have the same number of zeros inside, counted with multiplicity.
This symmetric hypothesis — Estermann's form of Rouché's theorem — is the one proved here; the
familiar asymmetric hypothesis ‖f - g‖ < ‖f‖ implies it, so the classical statement is a
corollary. Rouché is the first target of layer L0 (the local-mapping engine) of the
conformal-mapping roadmap.
The proof is the classical argument-principle one. On the circle the hypothesis forces both f ≠ 0
and g ≠ 0, so the quotient h = g / f is defined and nonzero there; moreover h avoids the
closed ray (-∞, 0], since at a nonpositive real value t of h the hypothesis would read
(1 - t)‖f‖ < (1 - t)‖f‖. Avoiding that ray is exactly membership in Complex.slitPlane, where
Complex.log is holomorphic — so Complex.log ∘ h is a primitive of logDeriv h at every point
of the circle and ∮ logDeriv h = 0 by
circleIntegral.integral_eq_zero_of_hasDerivWithinAt. Splitting logDeriv h as
logDeriv g - logDeriv f (logDeriv_div, valid pointwise on the circle since neither function
vanishes there) turns that into ∮ logDeriv g = ∮ logDeriv f, and the argument principle
(TauCeti.Contour.argumentPrinciple_divisor) converts each side into a sum of zero orders.
It is the passage to the slit plane, rather than to the disc ball 1 1, that buys the symmetric
hypothesis: ‖h - 1‖ < 1 says h lies in a disc that happens to miss the ray, whereas
‖1 - h‖ < 1 + ‖h‖ says precisely that h misses the ray, and nothing more.
Note that the primitive is only ever needed on the circle: the lemma consuming it asks for a
HasDerivWithinAt there, not on a neighbourhood of the disc. That is what keeps the proof free of
any simply-connectedness or branch-construction machinery — h may well have zeros and poles
inside the disc, and indeed the theorem is about exactly those.
The count is expressed with Mathlib's analyticOrderNatAt, summed over the open disc. Care is
needed about infinite order: analyticOrderNatAt sends a locally identically-zero function to 0,
and such a point is likewise absent from the support of MeromorphicOn.divisor, so in general the
divisor support is the set of zeros of finite order rather than the zero set outright. Under the
Rouché hypotheses that distinction is vacuous: the hypothesis forces f to be zero-free on the
circle, and closedBall c R is convex hence preconnected, so
MeromorphicOn.meromorphicOrderAt_ne_top_of_isPreconnected propagates finite order from a boundary
point to the whole disc — neither f nor g vanishes identically near any point of it.
The circle is not essential to the argument, only convenient: the second half of the file replays
it along an arbitrary closed piecewise-C¹ curve that is null-homologous in an open set carrying
both functions, weighting each zero by the winding number of the curve about it — and there the
functions may be meromorphic, the preserved quantity becoming zeros minus poles. The homological
argument principle TauCeti.Contour.argumentPrinciple_nullHomologous replaces the circle one, and
the slit-plane primitive is pushed across the corners of the curve by
TauCeti.Contour.integral_deriv_smul_logDeriv_eq_zero_of_mem_slitPlane, the curve form of the
countable-exception logarithmic-derivative FTC.
That equality of logarithmic-derivative integrals also has a purely geometric reading, obtained by
running it through TauCeti.Contour.windingNumber_comp_eq_integral_logDeriv: the two image curves
f ∘ γ and g ∘ γ wind equally often about the origin. That is the classical "dog on a leash"
form, and it is stronger than the counting statement, needing only analyticity at each point of the
curve — no single ambient open set, no finite S, no null-homology — because the vanishing of the
slit-plane integral already holds there.
That same observation is what makes the count detect zeros rather than merely count them:
TauCeti.finsum_analyticOrderNatAt_ball_eq_zero_iff, from TauCeti.Analysis.Complex.ZeroCount,
says the count vanishes exactly when the function has no zero in the open disc, so Rouché transfers
the existence of a zero from one function to the other. That transfer, not the numerical
equality, is how Rouché is normally used.
Main results #
TauCeti.rouche_symm— the symmetric (Estermann) form: if‖f z - g z‖ < ‖f z‖ + ‖g z‖onsphere c R, thenfandghave equal zero counts inball c R.TauCeti.rouche— if‖f z - g z‖ < ‖f z‖onsphere c R, thenfandghave equal zero counts inball c R, each counted with multiplicity.TauCeti.rouche_add— the classical additive phrasing: if‖g z‖ < ‖f z‖onsphere c R, thenfandf + ghave equal zero counts inball c R.TauCeti.exists_mem_closedBall_ne_zero_of_forall_mem_sphere_ne_zero— the witness those transfers need: a function that is zero-free on the bounding circle does not vanish identically on the closed disc.TauCeti.rouche_symm_exists_eq_zero_iff,TauCeti.rouche_exists_eq_zero_iff,TauCeti.rouche_add_exists_eq_zero_iff— under the respective hypotheses,fhas a zero inball c Rif and only if the function compared to it does.TauCeti.rouche_symm_nullHomologous— the homology form, for meromorphicfandg: across an arbitrary closed piecewise-C¹curve, null-homologous in an open set carrying both functions, the enclosed zeros minus poles agree, counted by multiplicity and by the winding number of the curve about them.TauCeti.rouche_symm_nullHomologous_of_analyticOnNhd,TauCeti.rouche_nullHomologous,TauCeti.rouche_add_nullHomologous— its holomorphic specialization in the same three phrasings as the disc statements.TauCeti.rouche_symm_windingNumber_comp,TauCeti.rouche_windingNumber_comp,TauCeti.rouche_add_windingNumber_comp— the "dog on a leash" form, in the same three phrasings: under the symmetric, the classical, respectively the additive hypothesis along the curve, the image curves wind equally often about the origin.
Coordination with upstream Mathlib #
Mathlib has no Rouché theorem. However, per the Coordination with upstream Mathlib section of
ConformalMapping/README.md, this layer overlaps
mathlib4#33505, the in-progress
human-curated Riemann-mapping-theorem effort, which proves L0-level material (an argument
principle, Hurwitz) internally as private lemmas. This file is therefore a temporary shim: once
the corresponding Mathlib lemmas land, this statement should be backed by them — or deleted and its
consumers refactored — rather than maintained as an independent re-proof. What Tau Ceti adds at L0
is named, discoverable API, not first proof.
References #
- L. Ahlfors, Complex Analysis, Ch. 4.
- S. Lang, Complex Analysis (GTM 103), Ch. VI.
Rouché's theorem, symmetric form (Estermann). If f and g are holomorphic on the closed
disc closedBall c R and ‖f z - g z‖ < ‖f z‖ + ‖g z‖ at every point z of the bounding circle,
then f and g have the same number of zeros in ball c R, each counted with multiplicity. The
hypothesis forces both functions to be zero-free on the circle, hence of finite order throughout
the disc, so every zero is genuinely counted.
The hypothesis is the strict form of the triangle inequality ‖f z - g z‖ ≤ ‖f z‖ + ‖g z‖, so it
says exactly that f z and g z never point in opposite directions on the circle. It is
symmetric in f and g and strictly weaker than the classical ‖f z - g z‖ < ‖f z‖ of
TauCeti.rouche.
The counts are the canonical finitely supported sums ∑ᶠ z ∈ ball c R, analyticOrderNatAt · z;
no finiteness witness appears in the statement.
Rouché's theorem for a disc, classical form. If f and g are holomorphic on the closed
disc closedBall c R and ‖f z - g z‖ < ‖f z‖ at every point z of the bounding circle, then f
and g have the same number of zeros in ball c R, each counted with multiplicity.
This is the special case of TauCeti.rouche_symm obtained by discarding the nonnegative summand
‖g z‖ from the symmetric hypothesis.
Rouché's theorem, in the additive phrasing of most textbooks: a holomorphic perturbation
g that is dominated by f on the bounding circle does not change the number of zeros inside.
Detecting zeros #
Rouché is usually applied not to compare two counts but to transfer the existence of a zero. The
bridge is TauCeti.finsum_analyticOrderNatAt_ball_eq_zero_iff: the count vanishes exactly when
there is no zero, provided the function is nonzero somewhere on the closed disc. The Rouché
hypothesis supplies that witness on the bounding circle.
A function that is zero-free on the bounding circle of a disc does not vanish identically on
the closed disc — the boundary point c + R witnesses it. The radius may be 0, where both discs
degenerate to {c}. This is the shape in which
TauCeti.finsum_analyticOrderNatAt_ball_eq_zero_iff wants the Rouché hypothesis, and it is the
same shape every zero-detection argument on a disc needs.
Rouché's theorem as a zero-detection principle, symmetric form. Under the hypothesis
‖f z - g z‖ < ‖f z‖ + ‖g z‖ on the bounding circle, f has a zero in the open disc if and only
if g does. This is how Rouché is normally used: to import a zero of a comparison function.
Rouché's theorem as a zero-detection principle, classical form: under
‖f z - g z‖ < ‖f z‖ on the bounding circle, f has a zero in the open disc if and only if g
does.
Rouché's theorem as a zero-detection principle, additive form: a holomorphic perturbation
g dominated by f on the bounding circle neither creates nor destroys zeros inside, so f has a
zero in the open disc if and only if f + g does. This is the phrasing that reads a zero of a
perturbed function off the unperturbed one, the existence counterpart of TauCeti.rouche_add.
Rouché's theorem for a null-homologous cycle #
The disc statements above compare the zeros enclosed by a circle. The homology forms below
replace the circle by an arbitrary closed piecewise-C¹ curve γ, null-homologous in an open set
U carrying both functions: they compare the winding-weighted counts ∑_{z ∈ S} n_z(γ) · ord z
over a finite set S carrying the exceptional points. That is the form Rouché takes on a domain
that is not a disc, and the form in which the multiplicity of enclosure is visible.
At this generality the functions may be meromorphic, exactly as in the argument principle the
proof runs through: the quantity that is preserved is then zeros minus poles, each counted with
multiplicity and with winding number. TauCeti.rouche_symm_nullHomologous is that statement, with
the orders supplied by the caller; TauCeti.rouche_symm_nullHomologous_of_analyticOnNhd is the
holomorphic specialization, whose orders are read off by analyticOrderNatAt.
The proof is the disc one, run through TauCeti.Contour.argumentPrinciple_nullHomologous instead
of the circle argument principle. What changes is the vanishing step. On a circle the integral of
logDeriv (g / f) was killed by circleIntegral.integral_eq_zero_of_hasDerivWithinAt; along a
piecewise-C¹ curve the primitive has to be pushed through the finitely many corners, which is
exactly what the countable exceptional set of TauCeti.Contour.integral_deriv_div_eq_log_sub_log
allows; that step is contour theory rather than Rouché, and lives with the FTC it specializes, as
TauCeti.Contour.integral_deriv_smul_logDeriv_eq_zero_of_mem_slitPlane. The geometry is unchanged:
the symmetric hypothesis confines g / f to Complex.slitPlane, where the principal Complex.log
is a single-valued primitive of the logarithmic derivative, so the integral is an endpoint
difference and the curve is closed.
The two are stated and proved separately because their interfaces differ, not because the disc case
is out of reach from here. It is reachable: analyticity on a neighbourhood of closedBall c R
gives, by compactness, analyticity on a slightly larger open ball U, in which every closed curve
is null-homologous; the zeros in closedBall c R are finite in number, so they can be collected
into an S; and the winding number of the bounding circle is 1 at each of them. What that route
costs is exactly that bookkeeping — producing S, evaluating the winding numbers, and converting
the resulting weighted Finset sum back into the ∑ᶠ count of TauCeti.rouche_symm, which ranges
over the whole open disc with no finiteness hypothesis. In the other direction there is no route at
all: on a general open set the zeros may accumulate at the boundary, so no finite S exists and
the cycle form has nothing to say.
Unlike on a circle there is no zero-detection corollary here, and that is not an omission: what
fails for a general cycle is the equivalence, not detection outright. With winding numbers of
both signs the weighted counts can cancel, so a vanishing count no longer means the function is
zero-free — TauCeti.finsum_analyticOrderNatAt_ball_eq_zero_iff, which the disc forms use, has no
cycle analogue. The converse direction survives and needs no corollary: if the weighted count of
f is nonzero then by the theorem so is that of g, so some z ∈ S has nonzero winding number
and analyticOrderNatAt g z ≠ 0; null-homology places such a z in U, where a nonzero order
means g z = 0. It is the iff that requires a sign hypothesis on the cycle, which the disc case
supplies by winding once.
Rouché's theorem for a null-homologous cycle, symmetric form (Estermann). Let f and g
be meromorphic on an open set U, analytic and non-vanishing off a finite set S, of orders
ordf and ordg on S, and let γ be a closed piecewise-C¹ curve in U, null-homologous in
U, missing S, and satisfying ‖f (γ t) - g (γ t)‖ < ‖f (γ t)‖ + ‖g (γ t)‖ along its length.
Then f and g enclose the same number of zeros minus poles, each counted with its multiplicity
and with the winding number of γ about it.
The hypothesis is the strict form of the triangle inequality ‖f z - g z‖ ≤ ‖f z‖ + ‖g z‖, so it
says exactly that f and g never point in opposite directions along the curve; it is symmetric
in the two functions and strictly weaker than the classical ‖f (γ t) - g (γ t)‖ < ‖f (γ t)‖.
Exactly as in TauCeti.Contour.argumentPrinciple_nullHomologous, points of S outside U are
harmless rather than excluded — null-homology makes their winding number, hence their contribution
on either side, vanish — so the meromorphy and order hypotheses are conditional on membership in
U, and S may list ordinary points, of order 0.
TauCeti.rouche_symm is the circle case, proved separately: see the section introduction for how
the two interfaces differ and what recovering the disc statement from this one would take.
Rouché's theorem for a null-homologous cycle, holomorphic form. Let f and g be analytic
on an open set U with all their zeros in a finite set S, and let γ be a closed piecewise-C¹
curve in U, null-homologous in U, along which ‖f (γ t) - g (γ t)‖ < ‖f (γ t)‖ + ‖g (γ t)‖.
Then f and g have the same zero count enclosed by γ, each zero counted with its multiplicity
and with the winding number of γ about it.
The curve is not required to miss S: the hypothesis already forces both functions to be zero-free
along it, so it may run through the non-zeros that S happens to list. This is the holomorphic
specialization of TauCeti.rouche_symm_nullHomologous, with the orders read off by
analyticOrderNatAt instead of supplied by the caller.
Rouché's theorem for a null-homologous cycle, classical form. Under
‖f (γ t) - g (γ t)‖ < ‖f (γ t)‖ along the curve, f and g enclose the same winding-weighted
number of zeros. This is the special case of
TauCeti.rouche_symm_nullHomologous_of_analyticOnNhd obtained by discarding the nonnegative
summand ‖g (γ t)‖.
Rouché's theorem for a null-homologous cycle, additive form: a holomorphic perturbation g
dominated by f along the curve does not change the winding-weighted number of zeros enclosed.
This is the phrasing of most textbooks, and the one that reads the zeros of a perturbed function
off the unperturbed one.
Rouché's theorem as an equality of image winding numbers, symmetric form — the "dog on a
leash" statement. If f and g are analytic along a closed piecewise-C¹ curve γ and never
point in opposite directions there, the image curves f ∘ γ and g ∘ γ wind equally often about
the origin.
Read through TauCeti.argumentPrinciple_windingNumber_of_analyticOnNhd, this is the geometric face
of TauCeti.rouche_symm_nullHomologous_of_analyticOnNhd; on its own it is stronger, since apart
from analyticity at each point of the curve — AnalyticAt, hence on some neighbourhood of that
point — only the behaviour of the two functions along the curve enters: no single ambient open
set carrying both, no confinement of the zeros to a finite set, and no null-homology. That is
because the equality of the two logarithmic-derivative integrals is already forced by the
hypothesis: it
puts g / f in Complex.slitPlane, where Complex.log is a single-valued primitive. It is only
in counting the winding that those extra hypotheses are needed.
Rouché's theorem as an equality of image winding numbers, classical form. Under
‖f (γ t) - g (γ t)‖ < ‖f (γ t)‖ along a closed piecewise-C¹ curve, the image curves f ∘ γ
and g ∘ γ wind equally often about the origin. This is the special case of
TauCeti.rouche_symm_windingNumber_comp obtained by discarding the nonnegative summand
‖g (γ t)‖.
Rouché's theorem as an equality of image winding numbers, additive form. A holomorphic
perturbation g dominated by f along a closed piecewise-C¹ curve does not change how often the
image winds about the origin. This is the phrasing that names the "dog on a leash" picture: the
walker f ∘ γ and the dog (f + g) ∘ γ, on a leash shorter than the walker's distance from the
lamppost at the origin, circle it the same number of times.
It is the special case of TauCeti.rouche_windingNumber_comp for the pair f, f + g.