English
Two meromorphic functions in normal form at x agree in a punctured neighborhood of x if and only if they agree in a neighborhood of x, provided both are meromorphic in normal form at x.
Русский
Две функции мероморфны в нормальной форме в точке x совпадают в окрестности точке x без самой точки тогда и только тогда, когда совпадают в полной окрестности, при условии, что обе функции мероморфны в нормальной форме в x.
LaTeX
$$$MeromorphicNFAt\ f\ x \wedge MeromorphicNFAt\ g\ x \Rightarrow (f =^{nhds[\neq]} g \iff f =^{nhds} g)$$$
Lean4
/-- **Local identity theorem**: two meromorphic functions in normal form agree in a
neighborhood iff they agree in a pointed neighborhood.
See `ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE` for the analogous
statement for continuous functions.
-/
theorem eventuallyEq_nhdsNE_iff_eventuallyEq_nhds {g : 𝕜 → E} (hf : MeromorphicNFAt f x) (hg : MeromorphicNFAt g x) :
f =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g := by
constructor
· intro h
have t₀ := meromorphicOrderAt_congr h
by_cases cs : meromorphicOrderAt f x = 0
· rw [cs] at t₀
have Z := (hf.meromorphicOrderAt_nonneg_iff_analyticAt.1 (le_of_eq cs.symm)).continuousAt
have W := (hg.meromorphicOrderAt_nonneg_iff_analyticAt.1 (le_of_eq t₀)).continuousAt
exact (Z.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE W).1 h
· apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE h
let h₁f := cs
rw [hf.meromorphicOrderAt_eq_zero_iff] at h₁f
let h₁g := cs
rw [t₀, hg.meromorphicOrderAt_eq_zero_iff] at h₁g
simp only [not_not] at *
rw [h₁f, h₁g]
· exact (Filter.EventuallyEq.filter_mono · nhdsWithin_le_nhds)
