English
If meromorphicOrderAt f x = 0, then there exist c ≠ 0 and Tendsto f to c near x.
Русский
Если порядок равен нулю, существует c ≠ 0 и предел функции близко к c в окрестности x.
LaTeX
$$$meromorphicOrderAt\ f\ x = 0 \Rightarrow \exists c \neq 0, Tendsto\ f\ (nhdsWithin x) (nhds c)$$$
Lean4
/-- Meromorphic functions that agree in a punctured neighborhood of `z₀` have the same order at
`z₀`. -/
theorem meromorphicOrderAt_congr (hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂) : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x :=
by
by_cases hf₁ : MeromorphicAt f₁ x; swap
· have : ¬MeromorphicAt f₂ x := by
contrapose! hf₁
exact hf₁.congr hf₁₂.symm
simp [hf₁, this]
by_cases h₁f₁ : meromorphicOrderAt f₁ x = ⊤
· rw [h₁f₁, eq_comm]
rw [meromorphicOrderAt_eq_top_iff] at h₁f₁ ⊢
exact EventuallyEq.rw h₁f₁ (fun x => Eq (f₂ x)) hf₁₂.symm
· obtain ⟨n, hn : meromorphicOrderAt f₁ x = n⟩ := Option.ne_none_iff_exists'.mp h₁f₁
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff hf₁).1 hn
rw [hn, eq_comm, meromorphicOrderAt_eq_int_iff (hf₁.congr hf₁₂)]
use g, h₁g, h₂g
exact EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) hf₁₂.symm
