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 #

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 : โ„•), k < n โ†’ a 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} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {p : FormalMultilinearSeries ๐•œ ๐•œ E} {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} (hp : HasFPowerSeriesAt f p 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โ‚€) :
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) :
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โ‚€) ^ FormalMultilinearSeries.order p โ€ข (๐•œ โ†’ E)^[Function.swap dslope zโ‚€] (FormalMultilinearSeries.order p) 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 : ๐•œ โ†’ 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} [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 : ๐•œ โ†’ 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} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} {U : Set ๐•œ} (hf : AnalyticOn ๐•œ 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 AnalyticOn.eqOn_zero_of_preconnected_of_eventuallyEq_zero.

theorem AnalyticOn.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 : AnalyticOn ๐•œ f U) (hU : IsPreconnected U) (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} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} {U : Set ๐•œ} (hf : AnalyticOn ๐•œ f U) (hg : AnalyticOn ๐•œ 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 AnalyticOn.eqOn_of_preconnected_of_eventuallyEq.

theorem AnalyticOn.eqOn_of_preconnected_of_mem_closure {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ๐•œ โ†’ E} {g : ๐•œ โ†’ E} {zโ‚€ : ๐•œ} {U : Set ๐•œ} (hf : AnalyticOn ๐•œ f U) (hg : AnalyticOn ๐•œ g U) (hU : IsPreconnected U) (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} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [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.