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 < 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 : ๐•œ โ†’ 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 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โ‚€.

noncomputable def AnalyticAt.order {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [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} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [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} [NontriviallyNormedField ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [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 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 : ๐•œ โ†’ E} {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 : ๐•œ โ†’ E} {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 : ๐•œ โ†’ E} {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 : ๐•œ โ†’ E} {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.

    @[deprecated AnalyticOnNhd.eq_of_frequently_eq]
    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 : AnalyticOnNhd ๐•œ f Set.univ) (hg : AnalyticOnNhd ๐•œ g Set.univ) (hfg : โˆƒแถ  (z : ๐•œ) in nhdsWithin zโ‚€ {zโ‚€}แถœ, f z = g z) :
    f = g

    Alias of AnalyticOnNhd.eq_of_frequently_eq.


    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.