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₀.
• AnalyticOnNhd.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.

Applications

• Vanishing of products of analytic functions, eq_zero_or_eq_zero_of_smul_eq_zero: 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, AnalyticOnNhd.preimage_mem_codiscreteWithin: 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.

theorem HasSum.hasSum_at_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f 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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f 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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [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} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [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₀.

theorem AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) (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 AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero.

theorem AnalyticOnNhd.eqOn_zero_or_eventually_ne_zero_of_preconnected {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) : Set.EqOn f 0 U ∨ ∀ᶠ (x : 𝕜) in Filter.codiscreteWithin U, f x ≠ 0

theorem AnalyticOnNhd.eqOn_zero_of_preconnected_of_mem_closure {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfz₀ : z₀ ∈ closure ({z : 𝕜 | f z = 0} \ {z₀})) : Set.EqOn f 0 U

theorem AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) (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 AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq.

theorem AnalyticOnNhd.eqOn_or_eventually_ne_of_preconnected {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) : Set.EqOn f g U ∨ ∀ᶠ (x : 𝕜) in Filter.codiscreteWithin U, f x ≠ g x

theorem AnalyticOnNhd.eqOn_of_preconnected_of_mem_closure {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : z₀ ∈ closure ({z : 𝕜 | f z = g z} \ {z₀})) : Set.EqOn f g U

theorem AnalyticOnNhd.eq_of_frequently_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} [ConnectedSpace 𝕜] (hf : AnalyticOnNhd 𝕜 f Set.univ) (hg : AnalyticOnNhd 𝕜 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 AnalyticOnNhd.eq_of_eventuallyEq.

### Vanishing of products of analytic functions

theorem AnalyticOnNhd.eq_zero_or_eq_zero_of_smul_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {A : Type u_3} [NormedRing A] [NormedAlgebra 𝕜 A] {B : Type u_4} [NormedAddCommGroup B] [NormedSpace 𝕜 B] [Module A B] [NoZeroSMulDivisors A B] {f : 𝕜 → A} {g : 𝕜 → B} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hfg : ∀ z ∈ U, f z • g z = 0) (hU : IsPreconnected U) : (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

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.

theorem AnalyticOnNhd.eq_zero_or_eq_zero_of_mul_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {A : Type u_3} [NormedRing A] [NormedAlgebra 𝕜 A] [NoZeroDivisors A] {f g : 𝕜 → A} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hfg : ∀ z ∈ U, f z * g z = 0) (hU : IsPreconnected U) : (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

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

theorem AnalyticAt.preimage_of_nhdsNE {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} {s : Set E} (hfx : AnalyticAt 𝕜 f x) (h₂f : ¬Filter.EventuallyConst f (nhds x)) (hs : s ∈ nhdsWithin (f x) {f x}ᶜ) : f ⁻¹' s ∈ nhdsWithin x {x}ᶜ

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.

theorem AnalyticAt.map_nhdsNE {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} (hfx : AnalyticAt 𝕜 f x) (h₂f : ¬Filter.EventuallyConst f (nhds x)) : Filter.map f (nhdsWithin x {x}ᶜ) ≤ nhdsWithin (f x) {f 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.

theorem AnalyticOnNhd.preimage_mem_codiscreteWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {s : Set E} {f : 𝕜 → E} (hfU : AnalyticOnNhd 𝕜 f U) (h₂f : ∀ x ∈ U, ¬Filter.EventuallyConst f (nhds x)) (hs : s ∈ Filter.codiscreteWithin (f '' U)) : f ⁻¹' s ∈ Filter.codiscreteWithin U

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.

See AnalyticOnNhd.preimage_zero_mem_codiscreteWithin for the special case that s is the complement of zero. Applications might want to use the theorem Filter.codiscreteWithin.mono.

theorem AnalyticOnNhd.map_codiscreteWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E} (hfU : AnalyticOnNhd 𝕜 f U) (h₂f : ∀ x ∈ U, ¬Filter.EventuallyConst f (nhds x)) : Filter.map f (Filter.codiscreteWithin U) ≤ Filter.codiscreteWithin (f '' U)

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.