Isolated Zeros theorem

isolated_zeros.lean

import analysis.analytic.basic
import analysis.analytic.radius_liminf
import analysis.calculus.dslope
import analysis.calculus.fderiv_analytic
import analysis.complex.basic
import algebra.big_operators.fin

variables {f : ℂ → ℂ} {p : formal_multilinear_series ℂ ℂ ℂ}

open filter function
open_locale topological_space big_operators

/- TODO: has_sum_nat_add_iff -/

def shift (n₀ : ℕ) : ℕ ≃ set.Ici n₀ := {
  to_fun := λ n, ⟨n₀ + n, by simp only [set.Ici, set.mem_set_of_eq, le_add_iff_nonneg_right, zero_le]⟩,
  inv_fun := λ n, n - n₀,
  left_inv := λ n, by simp only [subtype.coe_mk, add_tsub_cancel_left],
  right_inv := λ ⟨n, hn⟩, by simp only [subtype.coe_mk, subtype.mk_eq_mk]; linarith }

def shift' (n₀ : ℕ) : finset ℕ ≃ finset (set.Ici n₀) := {
  to_fun := finset.map (shift n₀),
  inv_fun := finset.map (shift n₀).symm,
  left_inv := λ s, by ext b; simp only [finset.mem_map_equiv, equiv.coe_eq_to_embedding,
    equiv.symm_symm, equiv.symm_apply_apply],
  right_inv := λ s, by ext b; simp only [finset.mem_map_equiv, equiv.coe_eq_to_embedding,
    equiv.symm_symm, equiv.apply_symm_apply] }

lemma tendsto_shift'_at_top {n₀ : ℕ} : tendsto (shift' n₀) at_top at_top :=
begin
  refine filter.tendsto_at_top_finset_of_monotone (λ s1 s2, finset.map_subset_map.mpr) _,
  rintro ⟨x, hx⟩,
  refine ⟨{x - n₀}, _⟩,
  simp only [shift', shift, equiv.coe_eq_to_embedding, equiv.coe_fn_mk, finset.map_singleton,
    equiv.to_embedding_apply, finset.mem_singleton, subtype.mk_eq_mk],
  linarith
end

lemma shift_sum {n₀ : ℕ} {a : ℕ → ℂ} {s : ℂ} (ha : has_sum (a ∘ (coe : set.Ici n₀ → ℕ)) s) :
  has_sum (λ n, a (n₀ + n)) s :=
begin
  simp only [has_sum] at ha ⊢,
  suffices : tendsto (((λ (s : finset ℕ), ∑ b in s, a (n₀ + b)) ∘ (shift' n₀).symm) ∘ (shift' n₀))
    at_top (𝓝 s),
  simpa only [comp.assoc _ (shift' n₀).symm (shift' n₀), equiv.symm_comp_self] using this,
  refine tendsto.comp _ tendsto_shift'_at_top,
  change tendsto (λ s, ∑ b in ((shift' n₀).symm s), a (n₀ + b)) at_top (𝓝 s),
  convert ha,
  funext s,
  simp only [shift', shift, equiv.coe_eq_to_embedding, equiv.coe_fn_symm_mk, finset.sum_map,
    equiv.to_embedding_apply, comp_app],
  congr,
  funext,
  congr,
  cases x,
  linarith
end

noncomputable def coef : formal_multilinear_series ℂ ℂ ℂ ≃ (ℕ → ℂ) := {
  to_fun := λ p n, p n (λ i, 1),
  inv_fun := λ q n, continuous_multilinear_map.mk_pi_field _ _ (q n),
  left_inv := λ p, funext (λ n, continuous_multilinear_map.mk_pi_field_apply_one_eq_self (p n)),
  right_inv := λ q, by simp only [continuous_multilinear_map.mk_pi_field_apply,
    finset.prod_const_one, algebra.id.smul_eq_mul, one_mul]
}

lemma foo₁ {𝕜 ι E : Type*} [fintype ι] [decidable_eq ι] [comm_semiring 𝕜] [add_comm_monoid E]
  [module 𝕜 E] (f : multilinear_map 𝕜 (λ i : ι, 𝕜) E) (x : ι → 𝕜) :
  f x = (∏ i, x i) • (f 1) :=
begin
  rw ← multilinear_map.map_smul_univ,
  exact congr_arg f (funext $ λ i, by simp)
end

lemma to_coef {p : formal_multilinear_series ℂ ℂ ℂ} {n : ℕ} {y : ℂ} :
  p n (λ i, y) = (coef p n) * y^n :=
by simpa [coef, mul_comm (y^n)] using foo₁ (p n).to_multilinear_map (λ i, y)

lemma to_coef' {p : formal_multilinear_series ℂ ℂ ℂ} {n : ℕ} {y : fin n → ℂ} :
  p n y = (coef p n) * finset.univ.prod y :=
begin
  simpa only [mul_comm _ (p n 1), continuous_multilinear_map.coe_coe,
    algebra.id.smul_eq_mul] using foo₁ (p n).to_multilinear_map y
end

lemma sum_coef {y z : ℂ} :
  has_sum (λ n, p n (λ i, y)) z ↔ has_sum (λ n, coef p n * y^n) z :=
by simp [to_coef]

noncomputable def order (p : formal_multilinear_series ℂ ℂ ℂ) : with_top ℕ :=
by classical; exact dite (∀ n, coef p n = 0) (λ _, ⊤) (λ h, nat.find (not_forall.mp h))

lemma coef_zero (hp : has_fpower_series_at f p 0) : coef p 0 = f 0 :=
hp.coeff_zero (λ _, 1)

lemma order_eq_top_iff : order p = ⊤ ↔ ∀ n, coef p n = 0 :=
by { by_cases (∀ n, coef p n = 0); simp [h, order] }

lemma locally_zero_of_order_eq_top (hp : has_fpower_series_at f p 0) (h : order p = ⊤) :
  ∀ᶠ z in 𝓝 0, f z = 0 :=
begin
  obtain ⟨r, le_r, r_pos, is_sum⟩ := hp,
  simp only [to_coef, order_eq_top_iff.mp h, emetric.mem_ball, zero_mul, zero_add] at is_sum,
  exact eventually_of_mem (emetric.ball_mem_nhds 0 r_pos) (λ x hx, (is_sum hx).unique has_sum_zero)
end

lemma order_eq_zero_iff (hp : has_fpower_series_at f p 0) : order p = 0 ↔ f 0 ≠ 0 :=
by { by_cases (∀ n, coef p n = 0); simp [h, order, ← coef_zero hp] }

def sderiv' (q : ℕ → ℂ) (n : ℕ) : ℂ := q (n + 1)

noncomputable def sderiv (p : formal_multilinear_series ℂ ℂ ℂ) : formal_multilinear_series ℂ ℂ ℂ :=
  coef.symm (sderiv' (coef p))

@[simp] lemma coef_sderiv (n : ℕ) : coef (sderiv p) n = coef p (n + 1) :=
by simp [sderiv, sderiv']

noncomputable def sderiv'' (p : formal_multilinear_series ℂ ℂ ℂ) : formal_multilinear_series ℂ ℂ ℂ :=
  λ n, @continuous_multilinear_map.curry_left ℂ n (λ _, ℂ) ℂ _ _ _ _ _ (p (n + 1)) 1

lemma sderiv_eq_sderiv'' : sderiv = sderiv'' :=
begin
  ext1 p; ext1 n; ext1 z,
  simp only [sderiv, coef, equiv.coe_fn_mk, equiv.coe_fn_symm_mk,
    continuous_multilinear_map.mk_pi_field_apply, algebra.id.smul_eq_mul],
  simp only [sderiv', sderiv'', continuous_multilinear_map.curry_left_apply],
  simp only [to_coef', mul_comm (coef _ _), fin.prod_cons, finset.prod_const_one, one_mul,
    complex.mul_re],
end

lemma order_sderiv (ho : order p ≠ 0) : order (sderiv p) = order p - 1 :=
begin
  by_cases (order p = ⊤),
  { have := order_eq_top_iff.mp h,
    have : ∀ n, coef (sderiv p) n = 0 := by simp [this],
    simpa only [h, order_eq_top_iff.mpr this]},
  { have h1 : ¬∀ (n : ℕ), coef p n = 0 := by simpa only [order_eq_top_iff] using h,
    simp only [order, h1, not_false_iff, coef_sderiv, dif_neg] at ho,
    norm_cast at ho,
    have h2 : ¬∀ (n : ℕ), coef p (n + 1) = 0 := by {
      push_neg at h1,
      obtain ⟨n, hn⟩ := h1,
      have := not_not.mp ((nat.find_eq_zero _).not.mp ho),
      have : n ≠ 0 := by { intro h, rw [h] at hn, exact hn this },
      push_neg,
      use n.pred,
      rwa [nat.add_one, nat.succ_pred_eq_of_pos (nat.pos_of_ne_zero this)] },
    simp only [order, h1, h2, not_false_iff, coef_sderiv, dif_neg] at ho ⊢,
    norm_cast at ho ⊢,
    rw ← nat.succ_inj',
    rw nat.sub_one,
    rw nat.succ_pred_eq_of_pos (nat.pos_of_ne_zero ho),
    rw ← nat.add_one,
    symmetry,
    exact nat.find_comp_succ _ _ ((nat.find_eq_zero _).not.mp ho) }
end

lemma sderiv_radius : p.radius ≤ (sderiv p).radius :=
begin
  have h0 : ∀ n, ∥sderiv p n∥ ≤ ∥p (n+1)∥ := λ n, by {
    simpa only [sderiv_eq_sderiv'', continuous_multilinear_map.curry_left_norm, complex.norm_eq_abs,
      complex.abs_one, mul_one] using continuous_linear_map.le_of_op_norm_le
      (@continuous_multilinear_map.curry_left ℂ n (λ _, ℂ) ℂ _ _ _ _ _ (p (n + 1))) rfl.le 1 },
  apply ennreal.le_of_forall_nnreal_lt,
  intros c hc,
  obtain ⟨a, ha, p_is_o⟩ := formal_multilinear_series.is_o_of_lt_radius _ hc,
  have h4 := p_is_o.comp_tendsto (tendsto_add_at_top_nat 1),
  change asymptotics.is_o (λ n, ∥p (n + 1)∥ * c ^ (n + 1)) (pow a ∘ λ n, n + 1) at_top at h4,
  replace h4 := h4.is_O,
  have h5 : asymptotics.is_O (λ n, ∥sderiv p n∥ * c ^ (n + 1)) (pow a ∘ λ n, n + 1) at_top := by {
    refine asymptotics.is_O.trans _ h4,
    refine asymptotics.is_O_of_le _ (λ n, _),
    simp only [norm_mul, norm_norm, norm_pow, nnreal.norm_eq],
    exact mul_le_mul (h0 n) rfl.le (pow_nonneg c.coe_nonneg _) (norm_nonneg _) },
  have h6 : asymptotics.is_O (λ n, ∥sderiv p n∥ * c ^ (n + 1)) (λ n, (1:ℝ)) at_top := by {
    apply h5.trans,
    refine asymptotics.is_O_of_le _ (λ n, _),
    simp only [real.norm_eq_abs, abs_pow, abs_one],
    refine pow_le_one _ (abs_nonneg _) _,
    rw abs_le,
    simp at ha; split; linarith },
  have h7 : asymptotics.is_O (λ n, ∥sderiv p n∥ * c ^ n) (λ n, (1:ℝ)) at_top := by {
    by_cases c = 0,
    { subst c,
      refine asymptotics.is_O.of_bound (∥sderiv p 0∥) _,
      simp only [nonneg.coe_zero, norm_mul, norm_norm, norm_pow, norm_zero, cstar_ring.norm_one,
        mul_one, eventually_at_top, ge_iff_le],
      exact ⟨1, λ b hb, by simp only [zero_pow (nat.succ_le_iff.mp hb), mul_zero, norm_nonneg]⟩ },
    { refine asymptotics.is_O.trans _ h6,
      refine @asymptotics.is_O_of_le' _ _ _ _ _ c⁻¹ _ _ _ (λ n, _),
      field_simp [h, pow_succ],
      ring_nf,
      simp [h] } },
  exact formal_multilinear_series.le_radius_of_is_O _ h7
end

lemma has_fpower_series_at.dslope (hf : f 0 = 0) (hp : has_fpower_series_at f p 0) :
  has_fpower_series_at (dslope f 0) (sderiv p) 0 :=
begin
  have hpd := hp.deriv,
  have hp0 : coef p 0 = 0 := hf ▸ coef_zero hp,
  obtain ⟨r, r_le, r_pos, is_sum⟩ := hp,
  refine ⟨r, r_le.trans sderiv_radius, r_pos, λ y hy, _⟩,
  by_cases y = 0,
  { simp only [h, sderiv, coef, sderiv', hpd, equiv.coe_fn_mk, equiv.coe_fn_symm_mk,
      continuous_multilinear_map.mk_pi_field_apply, finset.prod_const, finset.card_fin,
      algebra.id.smul_eq_mul, add_zero, dslope_same],
    convert has_sum_single 0 _,
    { simp only [pow_zero, one_mul] },
    { rintro b hb; simp only [hb, zero_pow', ne.def, not_false_iff, zero_mul]} },
  { simp only [sderiv, sderiv', coef, dslope, h, slope, hf, equiv.coe_fn_mk, equiv.coe_fn_symm_mk,
      continuous_multilinear_map.mk_pi_field_apply, finset.prod_const, finset.card_fin,
      algebra.id.smul_eq_mul, zero_add, update_noteq, ne.def, not_false_iff, sub_zero, vsub_eq_sub],
    have h1 : has_sum (λ n, y⁻¹ • p n (λ i, y)) (y⁻¹ • f y) := by {
      apply has_sum.const_smul,
      simpa only [zero_add] using is_sum hy },
    simp only [algebra.id.smul_eq_mul] at h1,
    have h2 : support (λ n, y⁻¹ * p n (λ i, y)) ⊆ set.Ici 1 := by {
      intro n,
      contrapose,
      intro hn,
      simp only [set.mem_Ici, not_le, nat.lt_one_iff] at hn,
      simpa only [h, hn, to_coef, support_mul, support_inv, set.mem_inter_eq, mem_support, ne.def,
        not_false_iff, pow_zero, one_ne_zero, and_true, true_and] },
    convert (shift_sum ((has_sum_subtype_iff_of_support_subset h2).mpr h1)),
    ext1 n,
    field_simp [to_coef, h, add_comm 1 n, pow_succ]; ring }
end

lemma locally_ne_zero_aux (hp : has_fpower_series_at f p 0) {n : ℕ} (h : order p = n) :
  ∀ᶠ z in 𝓝[≠] 0, f z ≠ 0 :=
begin
  induction n generalizing f p,
  { apply eventually_nhds_within_of_eventually_nhds,
    have f0_ne_0 := (order_eq_zero_iff hp).mp h,
    convert hp.continuous_at.eventually (is_open_compl_singleton.eventually_mem f0_ne_0) },
  { have order_ne_0 : order p ≠ 0 := by { by_contra h'; rw h' at h; norm_cast at h },
    have f0_eq_0 : f 0 = 0 := not_not.mp ((order_eq_zero_iff hp).not.mp order_ne_0),
    have hpdslope := hp.dslope f0_eq_0,
    have osderiv : order (sderiv p) = ↑n_n := by {
      have := order_sderiv order_ne_0,
      rw [order_sderiv order_ne_0, h]; norm_cast
    },
    simp only [eventually_nhds_within_iff] at n_ih ⊢,
    refine (n_ih hpdslope osderiv).mono (λ z hs hz hf, _),
    change z ≠ 0 at hz,
    specialize hs hz,
    simp [hz, dslope, slope, hf, f0_eq_0] at hs,
    exact hs hf }
end

theorem analytic_at.isolated_zero (hf : analytic_at ℂ f 0) :
  (∀ᶠ z in 𝓝 0, f z = 0) ∨ (∀ᶠ z in 𝓝[≠] 0, f z ≠ 0) :=
begin
  rcases hf with ⟨p, hp⟩,
  by_cases (order p = ⊤),
  { exact or.inl (locally_zero_of_order_eq_top hp h) },
  { let o := with_top.untop _ h,
    have : order p = o := by simp only [with_top.coe_untop],
    exact or.inr (locally_ne_zero_aux hp this) }
end