# 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 at zโ, then either it is identically zero in a neighborhood of zโ, or it does not vanish in a punctured neighborhood of zโ.
• AnalyticOn.eqOn_of_preconnected_of_frequently_eq is the identity theorem for analytic functions: if a function f is analytic on a connected set U and is zero on a set with an accumulation point in U then f is identically 0 on U.
theorem HasSum.hasSum_at_zero {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] (a : โ โ E) :
HasSum (fun (n : โ) => 0 ^ n โข a n) (a 0)
theorem HasSum.exists_hasSum_smul_of_apply_eq_zero {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {s : E} {n : โ} {z : ๐} {a : โ โ E} (hs : HasSum (fun (m : โ) => z ^ m โข a m) s) (ha : โ k < n, a k = 0) :
โ (t : E), z ^ n โข t = s โง HasSum (fun (m : โ) => z ^ m โข a (m + n)) t
theorem HasFPowerSeriesAt.has_fpower_series_dslope_fslope {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {p : FormalMultilinearSeries ๐ ๐ E} {f : ๐ โ E} {zโ : ๐} (hp : HasFPowerSeriesAt f p zโ) :
HasFPowerSeriesAt (dslope f zโ) p.fslope zโ
theorem HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {p : FormalMultilinearSeries ๐ ๐ E} {f : ๐ โ E} {zโ : ๐} (n : โ) (hp : HasFPowerSeriesAt f p zโ) :
HasFPowerSeriesAt ((Function.swap dslope zโ)^[n] f) (FormalMultilinearSeries.fslope^[n] p) zโ
theorem HasFPowerSeriesAt.iterate_dslope_fslope_ne_zero {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {p : FormalMultilinearSeries ๐ ๐ E} {f : ๐ โ E} {zโ : ๐} (hp : HasFPowerSeriesAt f p zโ) (h : p โ  0) :
(Function.swap dslope zโ)^[p.order] f zโ โ  0
theorem HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {p : FormalMultilinearSeries ๐ ๐ E} {f : ๐ โ E} {zโ : ๐} (hp : HasFPowerSeriesAt f p zโ) :
โแถ  (z : ๐) in nhds zโ, f z = (z - zโ) ^ p.order โข (Function.swap dslope zโ)^[p.order] f z
theorem HasFPowerSeriesAt.locally_ne_zero {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {p : FormalMultilinearSeries ๐ ๐ E} {f : ๐ โ E} {zโ : ๐} (hp : HasFPowerSeriesAt f p zโ) (h : p โ  0) :
โแถ  (z : ๐) in nhdsWithin zโ {zโ}แถ, f z โ  0
theorem HasFPowerSeriesAt.locally_zero_iff {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {p : FormalMultilinearSeries ๐ ๐ E} {f : ๐ โ E} {zโ : ๐} (hp : HasFPowerSeriesAt f p zโ) :
(โแถ  (z : ๐) in nhds zโ, f z = 0) โ p = 0
theorem AnalyticAt.eventually_eq_zero_or_eventually_ne_zero {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {zโ : ๐} (hf : AnalyticAt ๐ f zโ) :
(โแถ  (z : ๐) in nhds zโ, f z = 0) โจ โแถ  (z : ๐) in nhdsWithin zโ {zโ}แถ, f z โ  0

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โ.

theorem AnalyticAt.eventually_eq_or_eventually_ne {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {g : ๐ โ E} {zโ : ๐} (hf : AnalyticAt ๐ f zโ) (hg : AnalyticAt ๐ g zโ) :
(โแถ  (z : ๐) in nhds zโ, f z = g z) โจ โแถ  (z : ๐) in nhdsWithin zโ {zโ}แถ, f z โ  g z
theorem AnalyticAt.frequently_zero_iff_eventually_zero {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {w : ๐} (hf : AnalyticAt ๐ f w) :
(โแถ  (z : ๐) in nhdsWithin w {w}แถ, f z = 0) โ โแถ  (z : ๐) in nhds w, f z = 0
theorem AnalyticAt.frequently_eq_iff_eventually_eq {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {g : ๐ โ E} {zโ : ๐} (hf : AnalyticAt ๐ f zโ) (hg : AnalyticAt ๐ g zโ) :
(โแถ  (z : ๐) in nhdsWithin zโ {zโ}แถ, f z = g z) โ โแถ  (z : ๐) in nhds zโ, f z = g z
theorem AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {zโ : ๐} {m : โค} {n : โค} (hm : โ (g : ๐ โ E), AnalyticAt ๐ g zโ โง g zโ โ  0 โง โแถ  (z : ๐) in nhdsWithin zโ {zโ}แถ, f z = (z - zโ) ^ m โข g z) (hn : โ (g : ๐ โ E), AnalyticAt ๐ g zโ โง g zโ โ  0 โง โแถ  (z : ๐) in nhdsWithin zโ {zโ}แถ, f z = (z - zโ) ^ n โข g z) :
m = n

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.

theorem AnalyticAt.unique_eventuallyEq_pow_smul_nonzero {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {zโ : ๐} {m : โ} {n : โ} (hm : โ (g : ๐ โ E), AnalyticAt ๐ g zโ โง g zโ โ  0 โง โแถ  (z : ๐) in nhds zโ, f z = (z - zโ) ^ m โข g z) (hn : โ (g : ๐ โ E), AnalyticAt ๐ g zโ โง g zโ โ  0 โง โแถ  (z : ๐) in nhds zโ, f z = (z - zโ) ^ n โข g z) :
m = n

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โ.

theorem AnalyticAt.exists_eventuallyEq_pow_smul_nonzero_iff {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {zโ : ๐} (hf : AnalyticAt ๐ f zโ) :
(โ (n : โ) (g : ๐ โ E), AnalyticAt ๐ g zโ โง g zโ โ  0 โง โแถ  (z : ๐) in nhds zโ, f z = (z - zโ) ^ n โข g z) โ ยฌโแถ  (z : ๐) in nhds zโ, f z = 0

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โ.

noncomputable def AnalyticAt.order {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {zโ : ๐} (hf : AnalyticAt ๐ f zโ) :

The order of vanishing of f at zโ, as an element of โโ.

This is defined to be โ if f is identically 0 on a neighbourhood of zโ, and otherwise the unique n such that f z = (z - zโ) ^ n โข g z with g analytic and non-vanishing at zโ. See AnalyticAt.order_eq_top_iff and AnalyticAt.order_eq_nat_iff for these equivalences.

Equations
• hf.order = if h : โแถ  (z : ๐) in nhds zโ, f z = 0 then โค else โโฏ.choose
Instances For
theorem AnalyticAt.order_eq_top_iff {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {zโ : ๐} (hf : AnalyticAt ๐ f zโ) :
hf.order = โค โ โแถ  (z : ๐) in nhds zโ, f z = 0
theorem AnalyticAt.order_eq_nat_iff {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {zโ : ๐} (hf : AnalyticAt ๐ f zโ) (n : โ) :
hf.order = โn โ โ (g : ๐ โ E), AnalyticAt ๐ g zโ โง g zโ โ  0 โง โแถ  (z : ๐) in nhds zโ, f z = (z - zโ) ^ n โข g z
theorem AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {zโ : ๐} {U : Set ๐} (hf : AnalyticOn ๐ f U) (hU : ) (hโ : zโ โ U) (hfw : โแถ  (z : ๐) in nhdsWithin zโ {zโ}แถ, f z = 0) :
Set.EqOn f 0 U

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.

theorem AnalyticOn.eqOn_zero_of_preconnected_of_mem_closure {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {zโ : ๐} {U : Set ๐} (hf : AnalyticOn ๐ f U) (hU : ) (hโ : zโ โ U) (hfzโ : zโ โ closure ({z : ๐ | f z = 0} \ {zโ})) :
Set.EqOn f 0 U
theorem AnalyticOn.eqOn_of_preconnected_of_frequently_eq {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {g : ๐ โ E} {zโ : ๐} {U : Set ๐} (hf : AnalyticOn ๐ f U) (hg : AnalyticOn ๐ g U) (hU : ) (hโ : zโ โ U) (hfg : โแถ  (z : ๐) in nhdsWithin zโ {zโ}แถ, f z = g z) :
Set.EqOn f g U

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.

theorem AnalyticOn.eqOn_of_preconnected_of_mem_closure {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {g : ๐ โ E} {zโ : ๐} {U : Set ๐} (hf : AnalyticOn ๐ f U) (hg : AnalyticOn ๐ g U) (hU : ) (hโ : zโ โ U) (hfg : zโ โ closure ({z : ๐ | f z = g z} \ {zโ})) :
Set.EqOn f g U
theorem AnalyticOn.eq_of_frequently_eq {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {f : ๐ โ E} {g : ๐ โ E} {zโ : ๐} [ConnectedSpace ๐] (hf : AnalyticOn ๐ f Set.univ) (hg : AnalyticOn ๐ g Set.univ) (hfg : โแถ  (z : ๐) in nhdsWithin zโ {zโ}แถ, f z = g z) :
f = g

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.