Principle of isolated zeros #
This file proves the fact that the zeros of a non-constant analytic function of one variable are
isolated. It also introduces a little bit of API in the HasFPowerSeriesAt namespace that is useful
in this setup.
Main results #
AnalyticAt.eventually_eq_zero_or_eventually_ne_zerois the main statement that if a function is analytic atzβ, then either it is identically zero in a neighborhood ofzβ, or it does not vanish in a punctured neighborhood ofzβ.AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eqis the identity theorem for analytic functions: if a functionfis analytic on a connected setUand is zero on a set with an accumulation point inUthenfis identically0onU.
Applications #
- Vanishing of products of analytic functions,
eq_zero_or_eq_zero_of_smul_eq_zero: Iff, gare analytic on a neighbourhood of the preconnected open setU, andf β’ g = 0onU, then eitherf = 0onUorg = 0onU. - Preimages of codiscrete sets,
AnalyticOnNhd.preimage_mem_codiscreteWithin: iffis analytic on a neighbourhood ofUand not locally constant, then the preimage of any subset codiscrete withinf '' Uis codiscrete withinU.
The principle of isolated zeros for an analytic function, local version: if a function is
analytic at zβ, then either it is identically zero in a neighborhood of zβ, or it does not
vanish in a punctured neighborhood of zβ.
For a function f on π, and zβ β π, there exists at most one n such that on a punctured
neighbourhood of zβ we have f z = (z - zβ) ^ n β’ g z, with g analytic and nonvanishing at
zβ. We formulate this with n : β€, and deduce the case n : β later, for applications to
meromorphic functions.
For a function f on π, and zβ β π, there exists at most one n such that on a
neighbourhood of zβ we have f z = (z - zβ) ^ n β’ g z, with g analytic and nonvanishing at
zβ.
If f is analytic at zβ, then exactly one of the following two possibilities occurs: either
f vanishes identically near zβ, or locally around zβ it has the form z β¦ (z - zβ) ^ n β’ g z
for some n and some g which is analytic and non-vanishing at zβ.
The principle of isolated zeros for an analytic function, global version: if a function is
analytic on a connected set U and vanishes in arbitrary neighborhoods of a point zβ β U, then
it is identically zero in U.
For higher-dimensional versions requiring that the function vanishes in a neighborhood of zβ,
see AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero.
The identity principle for analytic functions, global version: if two functions are
analytic on a connected set U and coincide at points which accumulate to a point zβ β U, then
they coincide globally in U.
For higher-dimensional versions requiring that the functions coincide in a neighborhood of zβ,
see AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq.
The identity principle for analytic functions, global version: if two functions on a normed
field π are analytic everywhere and coincide at points which accumulate to a point zβ, then
they coincide globally.
For higher-dimensional versions requiring that the functions coincide in a neighborhood of zβ,
see AnalyticOnNhd.eq_of_eventuallyEq.
Alias of AnalyticOnNhd.eq_of_frequently_eq.
The identity principle for analytic functions, global version: if two functions on a normed
field π are analytic everywhere and coincide at points which accumulate to a point zβ, then
they coincide globally.
For higher-dimensional versions requiring that the functions coincide in a neighborhood of zβ,
see AnalyticOnNhd.eq_of_eventuallyEq.
###Β Vanishing of products of analytic functions
If f, g are analytic on a neighbourhood of the preconnected open set U, and f β’ g = 0
on U, then either f = 0 on U or g = 0 on U.
If f, g are analytic on a neighbourhood of the preconnected open set U, and f * g = 0
on U, then either f = 0 on U or g = 0 on U.
###Β Preimages of codiscrete sets
Preimages of codiscrete sets, local version: if f is analytic at x and not locally constant,
then the preimage of any punctured neighbourhood of f x is a punctured neighbourhood of x.
Preimages of codiscrete sets, local filter version: if f is analytic at x and not locally
constant, then the push-forward of the punctured neighbourhood filter π[β ] x is less than or
equal to the punctured neighbourhood filter π[β ] f x.
Preimages of codiscrete sets: if f is analytic on a neighbourhood of U and not locally
constant, then the preimage of any subset codiscrete within f '' U is codiscrete within U.
Applications might want to use the theorem Filter.codiscreteWithin.mono.
Preimages of codiscrete sets, filter version: if f is analytic on a neighbourhood of U and
not locally constant, then the push-forward of the filter of sets codiscrete within U is less
than or equal to the filter of sets codiscrete within f '' U.
Applications might want to use the theorem Filter.codiscreteWithin.mono.