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.
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.