feat: prove that a meromorphic function is eventually analytic (#14820)

Prove that a meromorphic function at a point is analytic on a punctured neighborhood of it, and that a meromorphic function on a set is analytic on a codiscrete subset of it.

Author: Command-Master

Mathlib/Analysis/Analytic/Meromorphic.lean

@@ -142,6 +142,23 @@ lemma zpow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℤ) : M
   | ofNat m => simpa only [Int.ofNat_eq_coe, zpow_natCast] using hf.pow m
   | negSucc m => simpa only [zpow_negSucc, inv_iff] using hf.pow (m + 1)
 
+theorem eventually_analyticAt [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜}
+    (h : MeromorphicAt f x) : ∀ᶠ y in 𝓝[≠] x, AnalyticAt 𝕜 f y := by
+  rw [MeromorphicAt] at h
+  obtain ⟨n, h⟩ := h
+  apply AnalyticAt.eventually_analyticAt at h
+  refine (h.filter_mono ?_).mp ?_
+  · simp [nhdsWithin]
+  · rw [eventually_nhdsWithin_iff]
+    apply Filter.Eventually.of_forall
+    intro y hy hf
+    rw [Set.mem_compl_iff, Set.mem_singleton_iff] at hy
+    have := (((analyticAt_id 𝕜 y).sub analyticAt_const).pow n).inv
+      (pow_ne_zero _ (sub_ne_zero_of_ne hy))
+    apply (this.smul hf).congr ∘ (eventually_ne_nhds hy).mono
+    intro z hz
+    simp [smul_smul, hz, sub_eq_zero]
+
 /-- The order of vanishing of a meromorphic function, as an element of `ℤ ∪ ∞` (to include the
 case of functions identically 0 near `x`). -/
 noncomputable def order {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : WithTop ℤ :=
@@ -281,4 +298,14 @@ lemma congr (h_eq : Set.EqOn f g U) (hu : IsOpen U) : MeromorphicOn g U := by
   refine fun x hx ↦ (hf x hx).congr (EventuallyEq.filter_mono ?_ nhdsWithin_le_nhds)
   exact eventually_of_mem (hu.mem_nhds hx) h_eq
 
+theorem eventually_codiscreteWithin_analyticAt
+    [CompleteSpace E] (f : 𝕜 → E) (h : MeromorphicOn f U) :
+    ∀ᶠ (y : 𝕜) in codiscreteWithin U, AnalyticAt 𝕜 f y := by
+  rw [eventually_iff, mem_codiscreteWithin]
+  intro x hx
+  rw [disjoint_principal_right]
+  apply Filter.mem_of_superset ((h x hx).eventually_analyticAt)
+  intro x hx
+  simp [hx]
+
 end MeromorphicOn