English
If f1 and f2 coincide in a punctured neighborhood of x, then their orders at x are equal.
Русский
Если f1 и f2 совпадают в пунктированной окрестности x, то их порядки в x равны.
LaTeX
$$meromorphicOrderAt f1 x = meromorphicOrderAt f2 x при f1 =^{{\mathcal{N}_{≠} x}} f2$$
Lean4
/-- If the order of a meromorphic function is positive, then this function converges to zero
at this point. See also the iff version `tendsto_zero_iff_meromorphicOrderAt_pos`. -/
theorem tendsto_zero_of_meromorphicOrderAt_pos (ho : 0 < meromorphicOrderAt f x) : Tendsto f (𝓝[≠] x) (𝓝 0) :=
by
have hf : MeromorphicAt f x := meromorphicAt_of_meromorphicOrderAt_ne_zero ho.ne'
cases h'o : meromorphicOrderAt f x with
| top =>
apply tendsto_const_nhds.congr'
filter_upwards [meromorphicOrderAt_eq_top_iff.1 h'o] with y hy using hy.symm
| coe n =>
rcases (meromorphicOrderAt_eq_int_iff hf).1 h'o with ⟨g, g_an, gx, hg⟩
lift n to ℕ using by simpa [h'o] using ho.le
have : (0 : E) = (x - x) ^ n • g x := by
have : 0 < n := by simpa [h'o] using ho
simp [zero_pow_eq_zero.2 this.ne']
rw [this]
have : ContinuousAt (fun z ↦ (z - x) ^ n • g z) x := by fun_prop
apply this.continuousWithinAt.tendsto.congr'
filter_upwards [hg] with y hy using by simp [hy]
