feat: preimages of codiscrete sets under analytic function in one variable

Mathlib/Analysis/Analytic/IsolatedZeros.lean

@@ -1,20 +1,21 @@
 /-
 Copyright (c) 2022 Vincent Beffara. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Vincent Beffara
+Authors: Vincent Beffara, Stefan Kebekus
 -/
 import Mathlib.Analysis.Analytic.Constructions
 import Mathlib.Analysis.Calculus.DSlope
 import Mathlib.Analysis.Calculus.FDeriv.Analytic
 import Mathlib.Analysis.Analytic.Uniqueness
+import Mathlib.Order.Filter.EventuallyConst
 import Mathlib.Topology.Perfect
 
 /-!
 # 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.
+isolated. It also introduces a little bit of API in the `HasFPowerSeriesAt` namespace that is useful
+in this setup.
 
 ## Main results
 
@@ -24,6 +25,15 @@ useful in this setup.
 * `AnalyticOnNhd.eqOn_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`.
+
+## Applications
+
+* Vanishing of products of analytic functions, `eq_zero_or_eq_zero_of_smul_eq_zero`: If `f, g` are
+  analytic on a neighbourhood of the preconnected open set `U`, and `f • g = 0` on `U`, then either
+  `f = 0` on `U` or `g = 0` on `U`.
+* Preimages of codiscrete sets, `AnalyticOnNhd.preimg_codiscrete`: if `f` is analytic on a
+  neighbourhood of `U` and not locally constant, then the preimage of any subset codiscrete within
+  `f '' U` is codiscrete within `U`.
 -/
 
 open Filter Function Nat FormalMultilinearSeries EMetric Set
@@ -297,5 +307,67 @@ lemma eq_zero_or_eq_zero_of_mul_eq_zero [NoZeroDivisors A]
   eq_zero_or_eq_zero_of_smul_eq_zero hf hg hfg hU
 
 end Mul
-
 end AnalyticOnNhd
+
+section PreimgCodiscrete
+/-!
+### Preimages of codiscrete sets
+-/
+
+/-- Preimages of codiscrete sets, local version: if `f` is analytic at `x` and not locally constant,
+then the preimage of any punctured neighbourhood of `f x` is a punctured neighbourhood of `x`. -/
+theorem AnalyticAt.preimg_of_puncNhd {x : 𝕜} {f : 𝕜 → E} {s : Set E} (hfx : AnalyticAt 𝕜 f x)
+    (h₂f : ¬Filter.EventuallyConst f (𝓝 x)) (hs : s ∈ 𝓝[≠] f x) :
+    f ⁻¹' s ∈ 𝓝[≠] x := by
+  have : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s := by
+    filter_upwards [hfx.continuousAt.preimage_mem_nhds (insert_mem_nhds_iff.2 hs)]
+    tauto
+  by_contra h
+  have : Filter.EventuallyConst f (𝓝 x) := by
+    rw [Filter.eventuallyConst_iff_exists_eventuallyEq]
+    use f x
+    rw [Filter.EventuallyEq, ← hfx.frequently_eq_iff_eventually_eq analyticAt_const]
+    apply ((frequently_imp_distrib_right.2 h).and_eventually
+      (eventually_nhdsWithin_of_eventually_nhds this)).mono
+    intro z ⟨h₁z, h₂z⟩
+    rw [Set.mem_insert_iff] at h₂z
+    tauto
+  tauto
+
+/-- Preimages of codiscrete sets, local filter version: if `f` is analytic at `x` and not locally
+constant, then the push-forward of the punctured neighbourhood filter `𝓝[≠] x` is less than or
+equal to the punctured neighbourhood filter `𝓝[≠] f x`. -/
+theorem AnalyticAt.map_of_puncNhdFilter {x : 𝕜} {f : 𝕜 → E} (hfx : AnalyticAt 𝕜 f x)
+    (h₂f : ¬Filter.EventuallyConst f (𝓝 x)) :
+    (𝓝[≠] x).map f ≤ (𝓝[≠] f x) := fun _ hs ↦ mem_map.1 (preimg_of_puncNhd hfx h₂f hs)
+
+/-- Preimages of codiscrete sets: if `f` is analytic on a neighbourhood of `U` and not locally
+constant, then the preimage of any subset codiscrete within `f '' U` is codiscrete within `U`.
+
+Applications might want to use the theorem `Filter.codiscreteWithin.mono`.
+-/
+theorem AnalyticOnNhd.preimg_codiscrete {U : Set 𝕜} {s : Set E} {f : 𝕜 → E}
+    (hfU : AnalyticOnNhd 𝕜 f U) (h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x))
+    (hs : s ∈ codiscreteWithin (f '' U)) :
+    f ⁻¹' s ∈ codiscreteWithin U := by
+  simp_rw [mem_codiscreteWithin, disjoint_principal_right, Set.compl_diff] at *
+  intro x hx
+  apply mem_of_superset ((hfU x hx).preimg_of_puncNhd (h₂f x hx) (hs (f x) (by tauto)))
+  rw [preimage_union, preimage_compl]
+  apply union_subset_union_right (f ⁻¹' s)
+  intro x hx
+  simp only [mem_compl_iff, mem_preimage, mem_image, not_exists, not_and] at hx ⊢
+  tauto
+
+/-- Preimages of codiscrete sets, filter version: if `f` is analytic on a neighbourhood of `U` and
+not locally constant, then the push-forward of the filter of sets codiscrete within `U` is less
+than or equal to the filter of sets codiscrete within `f '' U`.
+
+Applications might want to use the theorem `Filter.codiscreteWithin.mono`.
+-/
+theorem AnalyticOnNhd.map_of_codiscreteWithinFilter {U : Set 𝕜} {f : 𝕜 → E}
+    (hfU : AnalyticOnNhd 𝕜 f U) (h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x)) :
+    Filter.map f (Filter.codiscreteWithin U) ≤ (Filter.codiscreteWithin (f '' U)) :=
+  fun _ hs ↦ mem_map.1 (preimg_codiscrete hfU h₂f hs)
+
+end PreimgCodiscrete

Mathlib/Data/Set/Basic.lean

@@ -1260,6 +1260,11 @@ theorem diff_inter_diff {s t u : Set α} : s \ t ∩ (s \ u) = s \ (t ∪ u) :=
 theorem diff_compl : s \ tᶜ = s ∩ t :=
   sdiff_compl
 
+theorem compl_diff {α : Type u} {s t : Set α} : (t \ s)ᶜ = s ∪ tᶜ := by
+  ext z
+  rw [mem_compl_iff, mem_diff, not_and, not_not, mem_union]
+  tauto
+
 theorem diff_diff_right {s t u : Set α} : s \ (t \ u) = s \ t ∪ s ∩ u :=
   sdiff_sdiff_right'
 

Mathlib/Topology/DiscreteSubset.lean

@@ -145,4 +145,13 @@ lemma mem_codiscrete_subtype_iff_mem_codiscreteWithin {S : Set X} {U : Set S} :
     exact tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
       continuous_subtype_val.continuousWithinAt <| eventually_mem_nhdsWithin.mono (by simp)
 
+/-- If a set is codiscrete within `U`, then it is codiscrete within any subset of `U`. -/
+lemma Filter.codiscreteWithin.mono {X : Type u_1} [TopologicalSpace X] {U₁ U₂ : Set X}
+    (hU : U₁ ⊆ U₂) :
+    Filter.codiscreteWithin U₁ ≤ Filter.codiscreteWithin U₂ := by
+  intro s hs
+  simp_rw [mem_codiscreteWithin, disjoint_principal_right] at hs ⊢
+  exact fun x hx ↦ mem_of_superset (hs x (hU hx)) (Set.compl_subset_compl.2
+    (fun y hy ↦ ⟨hU hy.1, hy.2⟩))
+
 end codiscrete_filter