# Documentation

Mathlib.Analysis.Analytic.IsolatedZeros

# 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} [] (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} [] {s : E} {n : } {z : 𝕜} {a : E} (hs : HasSum (fun m => z ^ m a m) s) (ha : ∀ (k : ), k < na k = 0) :
t, 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} [] {p : } {f : 𝕜E} {z₀ : 𝕜} (hp : ) :
HasFPowerSeriesAt (dslope f z₀) () z₀
theorem HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope {𝕜 : Type u_1} {E : Type u_2} [] {p : } {f : 𝕜E} {z₀ : 𝕜} (n : ) (hp : ) :
HasFPowerSeriesAt ((Function.swap dslope z₀)^[n] f) () z₀
theorem HasFPowerSeriesAt.iterate_dslope_fslope_ne_zero {𝕜 : Type u_1} {E : Type u_2} [] {p : } {f : 𝕜E} {z₀ : 𝕜} (hp : ) (h : p 0) :
(𝕜E)^[Function.swap dslope z₀] () f z₀ 0
theorem HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope {𝕜 : Type u_1} {E : Type u_2} [] {p : } {f : 𝕜E} {z₀ : 𝕜} (hp : ) :
∀ᶠ (z : 𝕜) in nhds z₀, f z = (z - z₀) ^ (𝕜E)^[Function.swap dslope z₀] () f z
theorem HasFPowerSeriesAt.locally_ne_zero {𝕜 : Type u_1} {E : Type u_2} [] {p : } {f : 𝕜E} {z₀ : 𝕜} (hp : ) (h : p 0) :
∀ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}, f z 0
theorem HasFPowerSeriesAt.locally_zero_iff {𝕜 : Type u_1} {E : Type u_2} [] {p : } {f : 𝕜E} {z₀ : 𝕜} (hp : ) :
(∀ᶠ (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} [] {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} [] {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} [] {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} [] {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 AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero {𝕜 : Type u_1} {E : Type u_2} [] {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} [] {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} [] {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} [] {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} [] {f : 𝕜E} {g : 𝕜E} {z₀ : 𝕜} [] (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.