English
A meromorphic function tends to infinity at x if and only if its order at x is top.
Русский
Функция стремится к бесконечности в точке x тогда и только тогда, когда порядок в x равен верхнему элементу.
LaTeX
$$$meromorphicOrderAt\ f\ x = \top \iff Tendsto\ f\ (nhdsWithin x)\ (cobounded E)$$$$
Lean4
/-- A meromorphic function converges to zero iff its order is positive. -/
theorem tendsto_zero_iff_meromorphicOrderAt_pos (hf : MeromorphicAt f x) :
(Tendsto f (𝓝[≠] x) (𝓝 0)) ↔ 0 < meromorphicOrderAt f x :=
by
rcases lt_or_ge 0 (meromorphicOrderAt f x) with ho | ho
· simp [ho, tendsto_zero_of_meromorphicOrderAt_pos ho]
simp only [← not_le, ho, not_true_eq_false, iff_false]
intro hc
rcases ho.eq_or_lt with ho | ho
· obtain ⟨c, c_ne, h'c⟩ := tendsto_ne_zero_of_meromorphicOrderAt_eq_zero hf ho
apply c_ne
exact tendsto_nhds_unique h'c hc
· apply not_tendsto_atTop_of_tendsto_nhds hc.norm
rw [tendsto_norm_atTop_iff_cobounded]
exact tendsto_cobounded_of_meromorphicOrderAt_neg ho
