feat(analysis/analytic/isolated_zeros): Principle of isolated zeros (#…

…15908)

Local version: an analytic function is either locally zero, or nonzero in a punctured neighborhood.



Co-authored-by: ADedecker <anatolededecker@gmail.com>

src/analysis/analytic/basic.lean

@@ -407,12 +407,47 @@ lemma has_fpower_series_on_ball.mono
   has_fpower_series_on_ball f p x r' :=
 ⟨le_trans hr hf.1, r'_pos, λ y hy, hf.has_sum (emetric.ball_subset_ball hr hy)⟩
 
+lemma has_fpower_series_at.congr (hf : has_fpower_series_at f p x) (hg : f =ᶠ[𝓝 x] g) :
+  has_fpower_series_at g p x :=
+begin
+  rcases hf with ⟨r₁, h₁⟩,
+  rcases emetric.mem_nhds_iff.mp hg with ⟨r₂, h₂pos, h₂⟩,
+  exact ⟨min r₁ r₂, (h₁.mono (lt_min h₁.r_pos h₂pos) inf_le_left).congr
+    (λ y hy, h₂ (emetric.ball_subset_ball inf_le_right hy))⟩
+end
+
 protected lemma has_fpower_series_at.eventually (hf : has_fpower_series_at f p x) :
   ∀ᶠ r : ℝ≥0∞ in 𝓝[>] 0, has_fpower_series_on_ball f p x r :=
 let ⟨r, hr⟩ := hf in
 mem_of_superset (Ioo_mem_nhds_within_Ioi (left_mem_Ico.2 hr.r_pos)) $
   λ r' hr', hr.mono hr'.1 hr'.2.le
 
+lemma has_fpower_series_on_ball.eventually_has_sum (hf : has_fpower_series_on_ball f p x r) :
+  ∀ᶠ y in 𝓝 0, has_sum (λn:ℕ, p n (λ(i : fin n), y)) (f (x + y)) :=
+by filter_upwards [emetric.ball_mem_nhds (0 : E) hf.r_pos] using λ _, hf.has_sum
+
+lemma has_fpower_series_at.eventually_has_sum (hf : has_fpower_series_at f p x) :
+  ∀ᶠ y in 𝓝 0, has_sum (λn:ℕ, p n (λ(i : fin n), y)) (f (x + y)) :=
+let ⟨r, hr⟩ := hf in hr.eventually_has_sum
+
+lemma has_fpower_series_on_ball.eventually_has_sum_sub (hf : has_fpower_series_on_ball f p x r) :
+  ∀ᶠ y in 𝓝 x, has_sum (λn:ℕ, p n (λ(i : fin n), y - x)) (f y) :=
+by filter_upwards [emetric.ball_mem_nhds x hf.r_pos] with y using hf.has_sum_sub
+
+lemma has_fpower_series_at.eventually_has_sum_sub (hf : has_fpower_series_at f p x) :
+  ∀ᶠ y in 𝓝 x, has_sum (λn:ℕ, p n (λ(i : fin n), y - x)) (f y) :=
+let ⟨r, hr⟩ := hf in hr.eventually_has_sum_sub
+
+lemma has_fpower_series_on_ball.eventually_eq_zero
+  (hf : has_fpower_series_on_ball f (0 : formal_multilinear_series 𝕜 E F) x r) :
+  ∀ᶠ z in 𝓝 x, f z = 0 :=
+by filter_upwards [hf.eventually_has_sum_sub] with z hz using hz.unique has_sum_zero
+
+lemma has_fpower_series_at.eventually_eq_zero
+  (hf : has_fpower_series_at f (0 : formal_multilinear_series 𝕜 E F) x) :
+  ∀ᶠ z in 𝓝 x, f z = 0 :=
+let ⟨r, hr⟩ := hf in hr.eventually_eq_zero
+
 lemma has_fpower_series_on_ball.add
   (hf : has_fpower_series_on_ball f pf x r) (hg : has_fpower_series_on_ball g pg x r) :
   has_fpower_series_on_ball (f + g) (pf + pg) x r :=
@@ -840,6 +875,17 @@ theorem has_fpower_series_at.eq_formal_multilinear_series
   p₁ = p₂ :=
 sub_eq_zero.mp (has_fpower_series_at.eq_zero (by simpa only [sub_self] using h₁.sub h₂))
 
+lemma has_fpower_series_at.eq_formal_multilinear_series_of_eventually
+  {p q : formal_multilinear_series 𝕜 𝕜 E} {f g : 𝕜 → E} {x : 𝕜} (hp : has_fpower_series_at f p x)
+  (hq : has_fpower_series_at g q x) (heq : ∀ᶠ z in 𝓝 x, f z = g z) :
+  p = q :=
+(hp.congr heq).eq_formal_multilinear_series hq
+
+/-- A one-dimensional formal multilinear series representing a locally zero function is zero. -/
+lemma has_fpower_series_at.eq_zero_of_eventually {p : formal_multilinear_series 𝕜 𝕜 E} {f : 𝕜 → E}
+  {x : 𝕜} (hp : has_fpower_series_at f p x) (hf : f =ᶠ[𝓝 x] 0) : p = 0 :=
+(hp.congr hf).eq_zero
+
 /-- If a function `f : 𝕜 → E` has two power series representations at `x`, then the given radii in
 which convergence is guaranteed may be interchanged. This can be useful when the formal multilinear
 series in one representation has a particularly nice form, but the other has a larger radius. -/
@@ -1180,3 +1226,46 @@ begin
 end
 
 end
+
+section
+
+open formal_multilinear_series
+
+variables {p : formal_multilinear_series 𝕜 𝕜 E} {f : 𝕜 → E} {z₀ : 𝕜}
+
+/-- A function `f : 𝕜 → E` has `p` as power series expansion at a point `z₀` iff it is the sum of
+`p` in a neighborhood of `z₀`. This makes some proofs easier by hiding the fact that
+`has_fpower_series_at` depends on `p.radius`. -/
+lemma has_fpower_series_at_iff : has_fpower_series_at f p z₀ ↔
+  ∀ᶠ z in 𝓝 0, has_sum (λ n, z ^ n • p.coeff n) (f (z₀ + z)) :=
+begin
+  refine ⟨λ ⟨r, r_le, r_pos, h⟩, eventually_of_mem (emetric.ball_mem_nhds 0 r_pos)
+    (λ _, by simpa using h), _⟩,
+  simp only [metric.eventually_nhds_iff],
+  rintro ⟨r, r_pos, h⟩,
+  refine ⟨p.radius ⊓ r.to_nnreal, by simp, _, _⟩,
+  { simp only [r_pos.lt, lt_inf_iff, ennreal.coe_pos, real.to_nnreal_pos, and_true],
+    obtain ⟨z, z_pos, le_z⟩ := normed_field.exists_norm_lt 𝕜 r_pos.lt,
+    have : (∥z∥₊ : ennreal) ≤ p.radius,
+    by { simp only [dist_zero_right] at h,
+      apply formal_multilinear_series.le_radius_of_tendsto,
+      convert tendsto_norm.comp (h le_z).summable.tendsto_at_top_zero,
+      funext; simp [norm_smul, mul_comm] },
+    refine lt_of_lt_of_le _ this,
+    simp only [ennreal.coe_pos],
+    exact zero_lt_iff.mpr (nnnorm_ne_zero_iff.mpr (norm_pos_iff.mp z_pos)) },
+  { simp only [emetric.mem_ball, lt_inf_iff, edist_lt_coe, apply_eq_pow_smul_coeff, and_imp,
+      dist_zero_right] at h ⊢,
+    refine λ y hyp hyr, h _,
+    simpa [nndist_eq_nnnorm, real.lt_to_nnreal_iff_coe_lt] using hyr }
+end
+
+lemma has_fpower_series_at_iff' : has_fpower_series_at f p z₀ ↔
+  ∀ᶠ z in 𝓝 z₀, has_sum (λ n, (z - z₀) ^ n • p.coeff n) (f z) :=
+begin
+  rw [← map_add_left_nhds_zero, eventually_map, has_fpower_series_at_iff],
+  congrm ∀ᶠ z in (𝓝 0 : filter 𝕜), has_sum (λ n, _) (f (z₀ + z)),
+  rw add_sub_cancel'
+end
+
+end

src/analysis/analytic/isolated_zeros.lean

@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2022 Vincent Beffara. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vincent Beffara
+-/
+import analysis.analytic.basic
+import analysis.calculus.dslope
+import analysis.calculus.fderiv_analytic
+import analysis.calculus.formal_multilinear_series
+import analysis.complex.basic
+import topology.algebra.infinite_sum
+
+/-!
+# 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 `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₀`.
+-/
+
+open_locale classical
+
+open filter function nat formal_multilinear_series emetric
+open_locale topological_space big_operators
+
+variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
+  {E : Type*} [normed_add_comm_group E] [normed_space 𝕜 E] {s : E}
+  {p q : formal_multilinear_series 𝕜 𝕜 E} {f g : 𝕜 → E}
+  {n : ℕ} {z z₀ : 𝕜} {y : fin n → 𝕜}
+
+namespace has_sum
+
+variables {a : ℕ → E}
+
+lemma has_sum_at_zero (a : ℕ → E) : has_sum (λ n, (0:𝕜) ^ n • a n) (a 0) :=
+by convert has_sum_single 0 (λ b h, _); simp [nat.pos_of_ne_zero h] <|> simp
+
+lemma exists_has_sum_smul_of_apply_eq_zero (hs : has_sum (λ m, z ^ m • a m) s)
+  (ha : ∀ k < n, a k = 0) :
+  ∃ t : E, z ^ n • t = s ∧ has_sum (λ m, z ^ m • a (m + n)) t :=
+begin
+  refine classical.by_cases (λ hn : n = 0, by { subst n; simpa }) (λ hn, _),
+  replace hn := nat.pos_of_ne_zero hn,
+  by_cases (z = 0),
+  { have : s = 0 := hs.unique (by simpa [ha 0 hn, h] using has_sum_at_zero a),
+    exact ⟨a n, by simp [h, hn, this], by simpa [h] using has_sum_at_zero (λ m, a (m + n))⟩ },
+  { refine ⟨(z ^ n)⁻¹ • s, by field_simp [smul_smul], _⟩,
+    have h1 : ∑ i in finset.range n, z ^ i • a i = 0,
+      from finset.sum_eq_zero (λ k hk, by simp [ha k (finset.mem_range.mp hk)]),
+    have h2 : has_sum (λ m, z ^ (m + n) • a (m + n)) s,
+      by simpa [h1] using (has_sum_nat_add_iff' n).mpr hs,
+    convert @has_sum.const_smul E ℕ 𝕜 _ _ _ _ _ _ _ (z⁻¹ ^ n) h2,
+    field_simp [pow_add, smul_smul], simp only [inv_pow] }
+end
+
+end has_sum
+
+namespace has_fpower_series_at
+
+lemma has_fpower_series_dslope_fslope (hp : has_fpower_series_at f p z₀) :
+  has_fpower_series_at (dslope f z₀) p.fslope z₀ :=
+begin
+  have hpd : deriv f z₀ = p.coeff 1 := hp.deriv,
+  have hp0 : p.coeff 0 = f z₀ := hp.coeff_zero 1,
+  simp only [has_fpower_series_at_iff, apply_eq_pow_smul_coeff, coeff_fslope] at hp ⊢,
+  refine hp.mono (λ x hx, _),
+  by_cases x = 0,
+  { convert has_sum_single 0 _; intros; simp [*] },
+  { have hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n := λ n, by field_simp [h, pow_succ'],
+    suffices : has_sum (λ n, x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀)),
+    { simpa [dslope, slope, h, smul_smul, hxx] using this },
+    { simpa [hp0] using ((has_sum_nat_add_iff' 1).mpr hx).const_smul } }
+end
+
+lemma has_fpower_series_iterate_dslope_fslope (n : ℕ) (hp : has_fpower_series_at f p z₀) :
+  has_fpower_series_at ((swap dslope z₀)^[n] f) (fslope^[n] p) z₀ :=
+begin
+  induction n with n ih generalizing f p,
+  { exact hp },
+  { simpa using ih (has_fpower_series_dslope_fslope hp) }
+end
+
+lemma iterate_dslope_fslope_ne_zero (hp : has_fpower_series_at f p z₀) (h : p ≠ 0) :
+  (swap dslope z₀)^[p.order] f z₀ ≠ 0 :=
+begin
+  rw [← coeff_zero (has_fpower_series_iterate_dslope_fslope p.order hp) 1],
+  simpa [coeff_eq_zero] using apply_order_ne_zero h
+end
+
+lemma eq_pow_order_mul_iterate_dslope (hp : has_fpower_series_at f p z₀) :
+  ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ p.order • ((swap dslope z₀)^[p.order] f z) :=
+begin
+  have hq := has_fpower_series_at_iff'.mp (has_fpower_series_iterate_dslope_fslope p.order hp),
+  filter_upwards [hq, has_fpower_series_at_iff'.mp hp] with x hx1 hx2,
+  have : ∀ k < p.order, p.coeff k = 0,
+    from λ k hk, by simpa [coeff_eq_zero] using apply_eq_zero_of_lt_order hk,
+  obtain ⟨s, hs1, hs2⟩ := has_sum.exists_has_sum_smul_of_apply_eq_zero hx2 this,
+  convert hs1.symm,
+  simp only [coeff_iterate_fslope] at hx1,
+  exact hx1.unique hs2
+end
+
+lemma locally_ne_zero (hp : has_fpower_series_at f p z₀) (h : p ≠ 0) :
+  ∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0 :=
+begin
+  rw [eventually_nhds_within_iff],
+  have h2 := (has_fpower_series_iterate_dslope_fslope p.order hp).continuous_at,
+  have h3 := h2.eventually_ne (iterate_dslope_fslope_ne_zero hp h),
+  filter_upwards [eq_pow_order_mul_iterate_dslope hp, h3] with z e1 e2 e3,
+  simpa [e1, e2, e3] using pow_ne_zero p.order (sub_ne_zero.mpr e3),
+end
+
+lemma locally_zero_iff (hp : has_fpower_series_at f p z₀) :
+  (∀ᶠ z in 𝓝 z₀, f z = 0) ↔ p = 0 :=
+⟨λ hf, hp.eq_zero_of_eventually hf, λ h, eventually_eq_zero (by rwa h at hp)⟩
+
+end has_fpower_series_at
+
+namespace analytic_at
+
+/-- 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 eventually_eq_zero_or_eventually_ne_zero (hf : analytic_at 𝕜 f z₀) :
+  (∀ᶠ z in 𝓝 z₀, f z = 0) ∨ (∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0) :=
+begin
+  rcases hf with ⟨p, hp⟩,
+  by_cases h : p = 0,
+  { exact or.inl (has_fpower_series_at.eventually_eq_zero (by rwa h at hp)) },
+  { exact or.inr (hp.locally_ne_zero h) }
+end
+
+end analytic_at

src/analysis/calculus/formal_multilinear_series.lean

@@ -67,6 +67,12 @@ end module
 
 namespace formal_multilinear_series
 
+protected lemma ext_iff {p q : formal_multilinear_series 𝕜 E F} : p = q ↔ ∀ n, p n = q n :=
+function.funext_iff
+
+protected lemma ne_iff {p q : formal_multilinear_series 𝕜 E F} : p ≠ q ↔ ∃ n, p n ≠ q n :=
+function.ne_iff
+
 /-- Killing the zeroth coefficient in a formal multilinear series -/
 def remove_zero (p : formal_multilinear_series 𝕜 E F) : formal_multilinear_series 𝕜 E F
 | 0       := 0
@@ -164,3 +170,122 @@ lemma comp_formal_multilinear_series_apply'
 rfl
 
 end continuous_linear_map
+
+namespace formal_multilinear_series
+
+section order
+
+variables [comm_ring 𝕜] {n : ℕ}
+  [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E]
+  [has_continuous_const_smul 𝕜 E]
+  [add_comm_group F] [module 𝕜 F] [topological_space F] [topological_add_group F]
+  [has_continuous_const_smul 𝕜 F]
+  {p : formal_multilinear_series 𝕜 E F}
+
+/-- The index of the first non-zero coefficient in `p` (or `0` if all coefficients are zero). This
+  is the order of the isolated zero of an analytic function `f` at a point if `p` is the Taylor
+  series of `f` at that point. -/
+noncomputable def order (p : formal_multilinear_series 𝕜 E F) : ℕ :=
+Inf { n | p n ≠ 0 }
+
+@[simp] lemma order_zero : (0 : formal_multilinear_series 𝕜 E F).order = 0 := by simp [order]
+
+lemma ne_zero_of_order_ne_zero (hp : p.order ≠ 0) : p ≠ 0 :=
+λ h, by simpa [h] using hp
+
+lemma order_eq_find [decidable_pred (λ n, p n ≠ 0)] (hp : ∃ n, p n ≠ 0) :
+  p.order = nat.find hp :=
+by simp [order, Inf, hp]
+
+lemma order_eq_find' [decidable_pred (λ n, p n ≠ 0)] (hp : p ≠ 0) :
+  p.order = nat.find (formal_multilinear_series.ne_iff.mp hp) :=
+order_eq_find _
+
+lemma order_eq_zero_iff (hp : p ≠ 0) : p.order = 0 ↔ p 0 ≠ 0 :=
+begin
+  classical,
+  have : ∃ n, p n ≠ 0 := formal_multilinear_series.ne_iff.mp hp,
+  simp [order_eq_find this, hp]
+end
+
+lemma order_eq_zero_iff' : p.order = 0 ↔ p = 0 ∨ p 0 ≠ 0 :=
+by { by_cases h : p = 0; simp [h, order_eq_zero_iff] }
+
+lemma apply_order_ne_zero (hp : p ≠ 0) : p p.order ≠ 0 :=
+begin
+  classical,
+  let h := formal_multilinear_series.ne_iff.mp hp,
+  exact (order_eq_find h).symm ▸ nat.find_spec h
+end
+
+lemma apply_order_ne_zero' (hp : p.order ≠ 0) : p p.order ≠ 0 :=
+apply_order_ne_zero (ne_zero_of_order_ne_zero hp)
+
+lemma apply_eq_zero_of_lt_order (hp : n < p.order) : p n = 0 :=
+begin
+  by_cases p = 0,
+  { simp [h] },
+  { classical,
+    rw [order_eq_find' h] at hp,
+    simpa using nat.find_min _ hp }
+end
+
+end order
+
+section coef
+
+variables [nontrivially_normed_field 𝕜]
+  [normed_add_comm_group E] [normed_space 𝕜 E] {s : E}
+  {p : formal_multilinear_series 𝕜 𝕜 E} {f : 𝕜 → E}
+  {n : ℕ} {z z₀ : 𝕜} {y : fin n → 𝕜}
+
+open_locale big_operators
+
+/-- The `n`th coefficient of `p` when seen as a power series. -/
+def coeff (p : formal_multilinear_series 𝕜 𝕜 E) (n : ℕ) : E := p n 1
+
+lemma mk_pi_field_coeff_eq (p : formal_multilinear_series 𝕜 𝕜 E) (n : ℕ) :
+  continuous_multilinear_map.mk_pi_field 𝕜 (fin n) (p.coeff n) = p n :=
+(p n).mk_pi_field_apply_one_eq_self
+
+@[simp] lemma apply_eq_prod_smul_coeff : p n y = (∏ i, y i) • p.coeff n :=
+begin
+  convert (p n).to_multilinear_map.map_smul_univ y 1,
+  funext; simp only [pi.one_apply, algebra.id.smul_eq_mul, mul_one],
+end
+
+lemma coeff_eq_zero : p.coeff n = 0 ↔ p n = 0 :=
+by rw [← mk_pi_field_coeff_eq p, continuous_multilinear_map.mk_pi_field_eq_zero_iff]
+
+@[simp] lemma apply_eq_pow_smul_coeff : p n (λ _, z) = z ^ n • p.coeff n :=
+by simp
+
+@[simp] lemma norm_apply_eq_norm_coef : ∥p n∥ = ∥coeff p n∥ :=
+by rw [← mk_pi_field_coeff_eq p, continuous_multilinear_map.norm_mk_pi_field]
+
+end coef
+
+section fslope
+
+variables [nontrivially_normed_field 𝕜]
+  [normed_add_comm_group E] [normed_space 𝕜 E]
+  {p : formal_multilinear_series 𝕜 𝕜 E} {n : ℕ}
+
+/-- The formal counterpart of `dslope`, corresponding to the expansion of `(f z - f 0) / z`. If `f`
+has `p` as a power series, then `dslope f` has `fslope p` as a power series. -/
+noncomputable def fslope (p : formal_multilinear_series 𝕜 𝕜 E) : formal_multilinear_series 𝕜 𝕜 E :=
+  λ n, (p (n + 1)).curry_left 1
+
+@[simp] lemma coeff_fslope : p.fslope.coeff n = p.coeff (n + 1) :=
+begin
+  have : @fin.cons n (λ _, 𝕜) 1 (1 : fin n → 𝕜) = 1 := fin.cons_self_tail 1,
+  simp only [fslope, coeff, continuous_multilinear_map.curry_left_apply, this],
+end
+
+@[simp] lemma coeff_iterate_fslope (k n : ℕ) :
+  (fslope^[k] p).coeff n = p.coeff (n + k) :=
+by induction k with k ih generalizing p; refl <|> simpa [ih]
+
+end fslope
+
+end formal_multilinear_series