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_zero
is 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โ
.AnalyticOn.eqOn_of_preconnected_of_frequently_eq
is the identity theorem for analytic functions: if a functionf
is analytic on a connected setU
and is zero on a set with an accumulation point inU
thenf
is identically0
onU
.
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โ
.
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 AnalyticOn.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 AnalyticOn.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 AnalyticOn.eq_of_eventuallyEq
.