English
In a complete space, a function meromorphic at x is analytic at all nearby points.
Русский
В полной нормированной пространстве функция, мероморфная в точке x, является аналитической во всех близких точках.
LaTeX
$$$MeromorphicAt f x \rightarrow ∀ᶠ y \in 𝓝[≠] x,\ AnalyticAt 𝕜 f y$$$
Lean4
/-- In a complete space, a function which is meromorphic at a point is analytic at all nearby
points. The completeness assumption can be dispensed with if one assumes that `f` is meromorphic
on a set around `x`, see `MeromorphicOn.eventually_analyticAt`. -/
theorem eventually_analyticAt [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜} (h : MeromorphicAt f x) :
∀ᶠ y in 𝓝[≠] x, AnalyticAt 𝕜 f y := by
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 (𝕜 := 𝕜).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]
