Principle of isolated zeros #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 has_fpower_series_at namespace that is useful in this setup.

Main results #

analytic_at.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₀.
analytic_on.eq_on_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.

source

theorem has_sum.has_sum_at_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] (a : ℕ → E) :

has_sum (λ (n : ℕ), 0 ^ n • a n) (a 0)

source

theorem has_sum.exists_has_sum_smul_of_apply_eq_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {s : E} {n : ℕ} {z : 𝕜} {a : ℕ → E} (hs : has_sum (λ (m : ℕ), z ^ m • a m) s) (ha : ∀ (k : ℕ), k < n → a k = 0) :

∃ (t : E), z ^ n • t = s ∧ has_sum (λ (m : ℕ), z ^ m • a (m + n)) t

source

theorem has_fpower_series_at.has_fpower_series_dslope_fslope {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {p : formal_multilinear_series 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜} (hp : has_fpower_series_at f p z₀) :

has_fpower_series_at (dslope f z₀) p.fslope z₀

source

theorem has_fpower_series_at.has_fpower_series_iterate_dslope_fslope {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {p : formal_multilinear_series 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜} (n : ℕ) (hp : has_fpower_series_at f p z₀) :

has_fpower_series_at (function.swap dslope z₀^[n] f) (formal_multilinear_series.fslope ^[n] p) z₀

source

theorem has_fpower_series_at.iterate_dslope_fslope_ne_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {p : formal_multilinear_series 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜} (hp : has_fpower_series_at f p z₀) (h : p ≠ 0) :

function.swap dslope z₀^[p.order ] f z₀ ≠ 0

source

theorem has_fpower_series_at.eq_pow_order_mul_iterate_dslope {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {p : formal_multilinear_series 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜} (hp : has_fpower_series_at f p z₀) :

∀ᶠ (z : 𝕜) in nhds z₀, f z = (z - z₀) ^ p.order • function.swap dslope z₀^[p.order ] f z

source

theorem has_fpower_series_at.locally_ne_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {p : formal_multilinear_series 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜} (hp : has_fpower_series_at f p z₀) (h : p ≠ 0) :

∀ᶠ (z : 𝕜) in nhds_within z₀ {z₀}ᶜ, f z ≠ 0

source

theorem has_fpower_series_at.locally_zero_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {p : formal_multilinear_series 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜} (hp : has_fpower_series_at f p z₀) :

(∀ᶠ (z : 𝕜) in nhds z₀, f z = 0) ↔ p = 0

source

theorem analytic_at.eventually_eq_zero_or_eventually_ne_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : analytic_at 𝕜 f z₀) :

(∀ᶠ (z : 𝕜) in nhds z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in nhds_within 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₀.

source

theorem analytic_at.eventually_eq_or_eventually_ne {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} (hf : analytic_at 𝕜 f z₀) (hg : analytic_at 𝕜 g z₀) :

(∀ᶠ (z : 𝕜) in nhds z₀, f z = g z) ∨ ∀ᶠ (z : 𝕜) in nhds_within z₀ {z₀}ᶜ, f z ≠ g z

source

theorem analytic_at.frequently_zero_iff_eventually_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {f : 𝕜 → E} {w : 𝕜} (hf : analytic_at 𝕜 f w) :

(∃ᶠ (z : 𝕜) in nhds_within w {w}ᶜ, f z = 0) ↔ ∀ᶠ (z : 𝕜) in nhds w, f z = 0

source

theorem analytic_at.frequently_eq_iff_eventually_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} (hf : analytic_at 𝕜 f z₀) (hg : analytic_at 𝕜 g z₀) :

(∃ᶠ (z : 𝕜) in nhds_within z₀ {z₀}ᶜ, f z = g z) ↔ ∀ᶠ (z : 𝕜) in nhds z₀, f z = g z

source

theorem analytic_on.eq_on_zero_of_preconnected_of_frequently_eq_zero {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} {U : set 𝕜} (hf : analytic_on 𝕜 f U) (hU : is_preconnected U) (h₀ : z₀ ∈ U) (hfw : ∃ᶠ (z : 𝕜) in nhds_within z₀ {z₀}ᶜ, f z = 0) :

set.eq_on 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 eq_on_zero_of_preconnected_of_eventually_eq_zero.

source

theorem analytic_on.eq_on_zero_of_preconnected_of_mem_closure {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} {U : set 𝕜} (hf : analytic_on 𝕜 f U) (hU : is_preconnected U) (h₀ : z₀ ∈ U) (hfz₀ : z₀ ∈ closure ({z : 𝕜 | f z = 0} \ {z₀})) :

set.eq_on f 0 U

source

theorem analytic_on.eq_on_of_preconnected_of_frequently_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} {U : set 𝕜} (hf : analytic_on 𝕜 f U) (hg : analytic_on 𝕜 g U) (hU : is_preconnected U) (h₀ : z₀ ∈ U) (hfg : ∃ᶠ (z : 𝕜) in nhds_within z₀ {z₀}ᶜ, f z = g z) :

set.eq_on 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 eq_on_of_preconnected_of_eventually_eq.

source

theorem analytic_on.eq_on_of_preconnected_of_mem_closure {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} {U : set 𝕜} (hf : analytic_on 𝕜 f U) (hg : analytic_on 𝕜 g U) (hU : is_preconnected U) (h₀ : z₀ ∈ U) (hfg : z₀ ∈ closure ({z : 𝕜 | f z = g z} \ {z₀})) :

set.eq_on f g U

source

theorem analytic_on.eq_of_frequently_eq {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} [connected_space 𝕜] (hf : analytic_on 𝕜 f set.univ) (hg : analytic_on 𝕜 g set.univ) (hfg : ∃ᶠ (z : 𝕜) in nhds_within 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 eq_of_eventually_eq.