feat(analysis/analytic/isolated_zeros): the uniqueness theorem for an…

…alytic fns (#16489)

src/analysis/analytic/basic.lean

@@ -151,6 +151,11 @@ lemma radius_eq_top_of_forall_image_add_eq_zero (n : ℕ) (hn : ∀ m, p (m + n)
 p.radius_eq_top_of_eventually_eq_zero $ mem_at_top_sets.2
   ⟨n, λ k hk, tsub_add_cancel_of_le hk ▸ hn _⟩
 
+@[simp] lemma const_formal_multilinear_series_radius {v : F} :
+  (const_formal_multilinear_series 𝕜 E v).radius = ⊤ :=
+(const_formal_multilinear_series 𝕜 E v).radius_eq_top_of_forall_image_add_eq_zero 1
+  (by simp [const_formal_multilinear_series])
+
 /-- For `r` strictly smaller than the radius of `p`, then `∥pₙ∥ rⁿ` tends to zero exponentially:
 for some `0 < a < 1`, `∥p n∥ rⁿ = o(aⁿ)`. -/
 lemma is_o_of_lt_radius (h : ↑r < p.radius) :
@@ -448,6 +453,23 @@ lemma has_fpower_series_at.eventually_eq_zero
   ∀ᶠ z in 𝓝 x, f z = 0 :=
 let ⟨r, hr⟩ := hf in hr.eventually_eq_zero
 
+lemma has_fpower_series_on_ball_const {c : F} {e : E} :
+  has_fpower_series_on_ball (λ _, c) (const_formal_multilinear_series 𝕜 E c) e ⊤ :=
+begin
+  refine ⟨by simp, with_top.zero_lt_top, λ y hy, has_sum_single 0 (λ n hn, _)⟩,
+  simp [const_formal_multilinear_series_apply hn]
+end
+
+lemma has_fpower_series_at_const {c : F} {e : E} :
+  has_fpower_series_at (λ _, c) (const_formal_multilinear_series 𝕜 E c) e :=
+⟨⊤, has_fpower_series_on_ball_const⟩
+
+lemma analytic_at_const {v : F} : analytic_at 𝕜 (λ _, v) x :=
+⟨const_formal_multilinear_series 𝕜 E v, has_fpower_series_at_const⟩
+
+lemma analytic_on_const {v : F} {s : set E} : analytic_on 𝕜 (λ _, v) s :=
+λ z _, analytic_at_const
+
 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 :=
@@ -494,6 +516,14 @@ lemma analytic_at.sub (hf : analytic_at 𝕜 f x) (hg : analytic_at 𝕜 g x) :
   analytic_at 𝕜 (f - g) x :=
 by simpa only [sub_eq_add_neg] using hf.add hg.neg
 
+lemma analytic_on.add {s : set E} (hf : analytic_on 𝕜 f s) (hg : analytic_on 𝕜 g s) :
+  analytic_on 𝕜 (f + g) s :=
+λ z hz, (hf z hz).add (hg z hz)
+
+lemma analytic_on.sub {s : set E} (hf : analytic_on 𝕜 f s) (hg : analytic_on 𝕜 g s) :
+  analytic_on 𝕜 (f - g) s :=
+λ z hz, (hf z hz).sub (hg z hz)
+
 lemma has_fpower_series_on_ball.coeff_zero (hf : has_fpower_series_on_ball f pf x r)
   (v : fin 0 → E) : pf 0 v = f x :=
 begin

src/analysis/analytic/isolated_zeros.lean

@@ -14,19 +14,22 @@ 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.
+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`.
 -/
 
 open_locale classical
 
-open filter function nat formal_multilinear_series emetric
+open filter function nat formal_multilinear_series emetric set
 open_locale topological_space big_operators
 
 variables {𝕜 : Type*} [nontrivially_normed_field 𝕜]
@@ -137,4 +140,55 @@ begin
   { exact or.inr (hp.locally_ne_zero h) }
 end
 
+lemma frequently_zero_iff_eventually_zero {f : 𝕜 → E} {w : 𝕜} (hf : analytic_at 𝕜 f w) :
+  (∃ᶠ z in 𝓝[≠] w, f z = 0) ↔ (∀ᶠ z in 𝓝 w, f z = 0) :=
+⟨hf.eventually_eq_zero_or_eventually_ne_zero.resolve_right,
+  λ h, (h.filter_mono nhds_within_le_nhds).frequently⟩
+
 end analytic_at
+
+namespace analytic_on
+
+variables {U : set 𝕜} {w : 𝕜}
+
+theorem eq_on_of_preconnected_of_frequently_eq (hf : analytic_on 𝕜 f U) (hU : is_preconnected U)
+  (hw : w ∈ U) (hfw : ∃ᶠ z in 𝓝[≠] w, f z = 0) :
+  eq_on f 0 U :=
+begin
+  by_contra,
+  simp only [eq_on, not_forall] at h,
+  obtain ⟨x, hx1, hx2⟩ := h,
+  let u := {z | f =ᶠ[𝓝 z] 0},
+  have hu : is_open u := is_open_set_of_eventually_nhds,
+  have hu' : (U ∩ u).nonempty := ⟨w, hw, (hf w hw).frequently_zero_iff_eventually_zero.mp hfw⟩,
+  let v := {z | ∀ᶠ w in 𝓝[≠] z, f w ≠ 0},
+  have hv : is_open v := by apply is_open_set_of_eventually_nhds_within,
+  have hv' : (U ∩ v).nonempty,
+    from ⟨x, hx1, ((hf x hx1).continuous_at.eventually_ne hx2).filter_mono nhds_within_le_nhds⟩,
+  have huv : U ⊆ u ∪ v := λ z hz, (hf z hz).eventually_eq_zero_or_eventually_ne_zero,
+  have huv' : u ∩ v = ∅,
+    by { ext z,
+      simp only [mem_inter_iff, mem_empty_iff_false, iff_false, not_and],
+      exact λ h, (h.filter_mono nhds_within_le_nhds).frequently },
+  simpa [huv'] using hU u v hu hv huv hu' hv'
+end
+
+theorem eq_on_of_preconnected_of_mem_closure (hf : analytic_on 𝕜 f U) (hU : is_preconnected U)
+  (hw : w ∈ U) (hfw : w ∈ closure ({z | f z = 0} \ {w})) :
+  eq_on f 0 U :=
+hf.eq_on_of_preconnected_of_frequently_eq hU hw (mem_closure_ne_iff_frequently_within.mp hfw)
+
+theorem eq_on_of_preconnected_of_frequently_eq' (hf : analytic_on 𝕜 f U) (hg : analytic_on 𝕜 g U)
+  (hU : is_preconnected U) (hw : w ∈ U) (hfg : ∃ᶠ z in 𝓝[≠] w, f z = g z) :
+  eq_on f g U :=
+begin
+  have hfg' : ∃ᶠ z in 𝓝[≠] w, (f - g) z = 0 := hfg.mono (λ z h, by rw [pi.sub_apply, h, sub_self]),
+  simpa [sub_eq_zero] using λ z hz, (hf.sub hg).eq_on_of_preconnected_of_frequently_eq hU hw hfg' hz
+end
+
+theorem eq_on_of_preconnected_of_mem_closure' (hf : analytic_on 𝕜 f U) (hg : analytic_on 𝕜 g U)
+  (hU : is_preconnected U) (hw : w ∈ U) (hfw : w ∈ closure ({z | f z = g z} \ {w})) :
+  eq_on f g U :=
+hf.eq_on_of_preconnected_of_frequently_eq' hg hU hw (mem_closure_ne_iff_frequently_within.mp hfw)
+
+end analytic_on

src/analysis/calculus/formal_multilinear_series.lean

@@ -289,3 +289,23 @@ by induction k with k ih generalizing p; refl <|> simpa [ih]
 end fslope
 
 end formal_multilinear_series
+
+section const
+
+/-- The formal multilinear series where all terms of positive degree are equal to zero, and the term
+of degree zero is `c`. It is the power series expansion of the constant function equal to `c`
+everywhere. -/
+def const_formal_multilinear_series (𝕜 : Type*) [nontrivially_normed_field 𝕜]
+  (E : Type*) [normed_add_comm_group E] [normed_space 𝕜 E] [has_continuous_const_smul 𝕜 E]
+  [topological_add_group E] {F : Type*} [normed_add_comm_group F] [topological_add_group F]
+  [normed_space 𝕜 F]  [has_continuous_const_smul 𝕜 F] (c : F) : formal_multilinear_series 𝕜 E F
+| 0 := continuous_multilinear_map.curry0 _ _ c
+| _ := 0
+
+@[simp] lemma const_formal_multilinear_series_apply [nontrivially_normed_field 𝕜]
+  [normed_add_comm_group E] [normed_add_comm_group F] [normed_space 𝕜 E] [normed_space 𝕜 F]
+  {c : F} {n : ℕ} (hn : n ≠ 0) :
+  const_formal_multilinear_series 𝕜 E c n = 0 :=
+nat.cases_on n (λ hn, (hn rfl).elim) (λ _ _, rfl) hn
+
+end const

src/topology/continuous_on.lean

@@ -44,6 +44,14 @@ lemma eventually_nhds_within_iff {a : α} {s : set α} {p : α → Prop} :
   (∀ᶠ x in 𝓝[s] a, p x) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → p x :=
 eventually_inf_principal
 
+lemma frequently_nhds_within_iff {z : α} {p : α → Prop} :
+  (∃ᶠ x in 𝓝[≠] z, p x) ↔ (∃ᶠ x in 𝓝 z, p x ∧ x ≠ z) :=
+iff.not (by simp [eventually_nhds_within_iff, not_imp_not])
+
+lemma mem_closure_ne_iff_frequently_within {z : α} {s : set α} :
+  z ∈ closure (s \ {z}) ↔ ∃ᶠ x in 𝓝[≠] z, x ∈ s :=
+by simp [mem_closure_iff_frequently, frequently_nhds_within_iff]
+
 @[simp] lemma eventually_nhds_within_nhds_within {a : α} {s : set α} {p : α → Prop} :
   (∀ᶠ y in 𝓝[s] a, ∀ᶠ x in 𝓝[s] y, p x) ↔ ∀ᶠ x in 𝓝[s] a, p x :=
 begin

src/topology/separation.lean

@@ -333,6 +333,17 @@ begin
   exact mem_nhds_within_of_mem_nhds (is_open_ne.mem_nhds h)
 end
 
+lemma is_open_set_of_eventually_nhds_within [t1_space α] {p : α → Prop} :
+  is_open {x | ∀ᶠ y in 𝓝[≠] x, p y} :=
+begin
+  refine is_open_iff_mem_nhds.mpr (λ a ha, _),
+  filter_upwards [eventually_nhds_nhds_within.mpr ha] with b hb,
+  by_cases a = b,
+  { subst h, exact hb },
+  { rw (ne.symm h).nhds_within_compl_singleton at hb,
+    exact hb.filter_mono nhds_within_le_nhds }
+end
+
 protected lemma set.finite.is_closed [t1_space α] {s : set α} (hs : set.finite s) :
   is_closed s :=
 begin