feat: principle of isolated zeros for meromorphic functions (#21083)

Establish a principle of isolated zeros and show that the set where a meromorphic function has infinite order is clopen in the domain of meromorphy.

These theorems are used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

Author: kebekus

Mathlib/Analysis/Analytic/IsolatedZeros.lean

@@ -345,6 +345,49 @@ theorem eq_of_frequently_eq [ConnectedSpace 𝕜] (hf : AnalyticOnNhd 𝕜 f uni
 @[deprecated (since := "2024-09-26")]
 alias _root_.AnalyticOn.eq_of_frequently_eq := eq_of_frequently_eq
 
+/-- The set where an analytic function has infinite order is clopen in its domain of analyticity. -/
+theorem isClopen_setOf_order_eq_top (h₁f : AnalyticOnNhd 𝕜 f U) :
+    IsClopen { u : U | (h₁f u.1 u.2).order = ⊤ } := by
+  constructor
+  · rw [← isOpen_compl_iff, isOpen_iff_forall_mem_open]
+    intro z hz
+    rcases (h₁f z.1 z.2).eventually_eq_zero_or_eventually_ne_zero with h | h
+    · -- Case: f is locally zero in a punctured neighborhood of z
+      rw [← (h₁f z.1 z.2).order_eq_top_iff] at h
+      tauto
+    · -- Case: f is locally nonzero in a punctured neighborhood of z
+      obtain ⟨t', h₁t', h₂t', h₃t'⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h)
+      use Subtype.val ⁻¹' t'
+      constructor
+      · intro w hw
+        simp only [mem_compl_iff, mem_setOf_eq]
+        by_cases h₁w : w = z
+        · rwa [h₁w]
+        · rw [(h₁f _ w.2).order_eq_zero_iff.2 ((h₁t' w hw) (Subtype.coe_ne_coe.mpr h₁w))]
+          exact ENat.zero_ne_top
+      · exact ⟨isOpen_induced h₂t', h₃t'⟩
+  · apply isOpen_iff_forall_mem_open.mpr
+    intro z hz
+    conv =>
+      arg 1; intro; left; right; arg 1; intro
+      rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff]
+    simp only [Set.mem_setOf_eq] at hz
+    rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at hz
+    obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
+    use Subtype.val ⁻¹' t'
+    simp only [Set.mem_compl_iff, Set.mem_singleton_iff, isOpen_induced h₂t', Set.mem_preimage,
+      h₃t', and_self, and_true]
+    intro w hw
+    simp only [mem_setOf_eq]
+    -- Trivial case: w = z
+    by_cases h₁w : w = z
+    · rw [h₁w]
+      tauto
+    -- Nontrivial case: w ≠ z
+    use t' \ {z.1}, fun y h₁y ↦ h₁t' y h₁y.1, h₂t'.sdiff isClosed_singleton
+    apply (Set.mem_diff w).1
+    exact ⟨hw, Set.mem_singleton_iff.not.1 (Subtype.coe_ne_coe.2 h₁w)⟩
+
 section Mul
 /-!
 ### Vanishing of products of analytic functions

Mathlib/Analysis/Analytic/Meromorphic.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 David Loeffler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: David Loeffler
+Authors: David Loeffler, Stefan Kebekus
 -/
 import Mathlib.Analysis.Analytic.IsolatedZeros
 import Mathlib.Algebra.Order.AddGroupWithTop
@@ -35,6 +35,23 @@ lemma AnalyticAt.meromorphicAt {f : 𝕜 → E} {x : 𝕜} (hf : AnalyticAt 𝕜
     MeromorphicAt f x :=
   ⟨0, by simpa only [pow_zero, one_smul]⟩
 
+/- Analogue of the principle of isolated zeros for an analytic function: if a function is
+meromorphic at `z₀`, then either it is identically zero in a punctured neighborhood of `z₀`, or it
+does not vanish there at all. -/
+theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero {f : 𝕜 → E} {z₀ : 𝕜}
+    (hf : MeromorphicAt f z₀) :
+    (∀ᶠ z in 𝓝[≠] z₀, f z = 0) ∨ (∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0) := by
+  obtain ⟨n, h⟩ := hf
+  rcases h.eventually_eq_zero_or_eventually_ne_zero with h₁ | h₂
+  · left
+    filter_upwards [nhdsWithin_le_nhds h₁, self_mem_nhdsWithin] with y h₁y h₂y
+    rcases (smul_eq_zero.1 h₁y) with h₃ | h₄
+    · exact False.elim (h₂y (sub_eq_zero.1 (pow_eq_zero_iff'.1 h₃).1))
+    · assumption
+  · right
+    filter_upwards [h₂, self_mem_nhdsWithin] with y h₁y h₂y
+    exact (smul_ne_zero_iff.1 h₁y).2
+
 namespace MeromorphicAt
 
 lemma id (x : 𝕜) : MeromorphicAt id x := analyticAt_id.meromorphicAt
@@ -334,6 +351,82 @@ lemma id {U : Set 𝕜} : MeromorphicOn id U := fun x _ ↦ .id x
 lemma const (e : E) {U : Set 𝕜} : MeromorphicOn (fun _ ↦ e) U :=
   fun x _ ↦ .const e x
 
+/-- The set where a meromorphic function has infinite order is clopen in its domain of meromorphy.
+-/
+theorem isClopen_setOf_order_eq_top {U : Set 𝕜} (hf : MeromorphicOn f U) :
+    IsClopen { u : U | (hf u.1 u.2).order = ⊤ } := by
+  constructor
+  · rw [← isOpen_compl_iff, isOpen_iff_forall_mem_open]
+    intro z hz
+    rcases (hf z.1 z.2).eventually_eq_zero_or_eventually_ne_zero with h | h
+    · -- Case: f is locally zero in a punctured neighborhood of z
+      rw [← (hf z.1 z.2).order_eq_top_iff] at h
+      tauto
+    · -- Case: f is locally nonzero in a punctured neighborhood of z
+      obtain ⟨t', h₁t', h₂t', h₃t'⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h)
+      use Subtype.val ⁻¹' t'
+      constructor
+      · intro w hw
+        simp only [Set.mem_compl_iff, Set.mem_setOf_eq]
+        by_cases h₁w : w = z
+        · rwa [h₁w]
+        · rw [MeromorphicAt.order_eq_top_iff, not_eventually]
+          apply Filter.Eventually.frequently
+          rw [eventually_nhdsWithin_iff, eventually_nhds_iff]
+          use t' \ {z.1}, fun y h₁y h₂y ↦ h₁t' y h₁y.1 h₁y.2, h₂t'.sdiff isClosed_singleton, hw,
+            Set.mem_singleton_iff.not.2 (Subtype.coe_ne_coe.mpr h₁w)
+      · exact ⟨isOpen_induced h₂t', h₃t'⟩
+  · apply isOpen_iff_forall_mem_open.mpr
+    intro z hz
+    conv =>
+      arg 1; intro; left; right; arg 1; intro
+      rw [MeromorphicAt.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff]
+    simp only [Set.mem_setOf_eq] at hz
+    rw [MeromorphicAt.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at hz
+    obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
+    use Subtype.val ⁻¹' t'
+    simp only [Set.mem_compl_iff, Set.mem_singleton_iff, isOpen_induced h₂t', Set.mem_preimage,
+      h₃t', and_self, and_true]
+    intro w hw
+    simp only [Set.mem_setOf_eq]
+    -- Trivial case: w = z
+    by_cases h₁w : w = z
+    · rw [h₁w]
+      tauto
+    -- Nontrivial case: w ≠ z
+    use t' \ {z.1}, fun y h₁y _ ↦ h₁t' y (Set.mem_of_mem_diff h₁y) (Set.mem_of_mem_inter_right h₁y)
+    constructor
+    · exact h₂t'.sdiff isClosed_singleton
+    · apply (Set.mem_diff w).1
+      exact ⟨hw, Set.mem_singleton_iff.not.1 (Subtype.coe_ne_coe.2 h₁w)⟩
+
+/-- On a connected set, there exists a point where a meromorphic function `f` has finite order iff
+`f` has finite order at every point. -/
+theorem exists_order_ne_top_iff_forall {U : Set 𝕜} (hf : MeromorphicOn f U) (hU : IsConnected U) :
+    (∃ u : U, (hf u u.2).order ≠ ⊤) ↔ (∀ u : U, (hf u u.2).order ≠ ⊤) := by
+  constructor
+  · intro h₂f
+    have := isPreconnected_iff_preconnectedSpace.1 hU.isPreconnected
+    rcases isClopen_iff.1 hf.isClopen_setOf_order_eq_top with h | h
+    · intro u
+      have : u ∉ (∅ : Set U) := by exact fun a => a
+      rw [← h] at this
+      tauto
+    · obtain ⟨u, hU⟩ := h₂f
+      have : u ∈ Set.univ := by trivial
+      rw [← h] at this
+      tauto
+  · intro h₂f
+    obtain ⟨v, hv⟩ := hU.nonempty
+    use ⟨v, hv⟩, h₂f ⟨v, hv⟩
+
+/-- On a preconnected set, a meromorphic function has finite order at one point if it has finite
+order at another point. -/
+theorem order_ne_top_of_isPreconnected {U : Set 𝕜} {x y : 𝕜} (hf : MeromorphicOn f U)
+    (hU : IsPreconnected U) (h₁x : x ∈ U) (hy : y ∈ U) (h₂x : (hf x h₁x).order ≠ ⊤) :
+    (hf y hy).order ≠ ⊤ :=
+  (hf.exists_order_ne_top_iff_forall ⟨Set.nonempty_of_mem h₁x, hU⟩).1 (by use ⟨x, h₁x⟩) ⟨y, hy⟩
+
 section arithmetic
 
 include hf in