English
If MeromorphicAt f x and 0 ≤ meromorphicOrderAt f x, then there exists a limit along nhdsWithin x.
Русский
Если f мероморфна в x и 0 ≤ порядок, то существует предел вдоль nhdsWithin x.
LaTeX
$$$MeromorphicAt\ f\ x \land 0 \le meromorphicOrderAt\ f\ x \Rightarrow \exists c, Tendsto\ f\ (nhdsWithin x) (nhds c)$$$
Lean4
/-- A meromorphic function converges to a limit iff its order is nonnegative. -/
theorem tendsto_nhds_iff_meromorphicOrderAt_nonneg (hf : MeromorphicAt f x) :
(∃ c, Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ 0 ≤ meromorphicOrderAt f x :=
by
rcases lt_or_ge (meromorphicOrderAt f x) 0 with ho | ho
· simp only [← not_lt, ho, not_true_eq_false, iff_false, not_exists]
intro c hc
apply not_tendsto_atTop_of_tendsto_nhds hc.norm
rw [tendsto_norm_atTop_iff_cobounded]
exact tendsto_cobounded_of_meromorphicOrderAt_neg ho
· simp [ho, tendsto_nhds_of_meromorphicOrderAt_nonneg hf ho]
