English
MeromorphicAt f x is equivalent to the existence of a decomposition f(z) = (z − x)^n g(z) near x with g analytic at x.
Русский
Мероморфность f в точке x эквивалентна существованию разложения f(z) = (z − x)^n g(z) около x, где g аналитична в x.
LaTeX
$$$MeromorphicAt f x \iff \exists n \in \mathbb{Z}, \exists g:\u2061 𝕜 \to E,\ AnalyticAt 𝕜 g x \wedge \forallᶠ z \in 𝓝[≠] x,\ f z = (z - x)^n \cdot g z$$$
Lean4
theorem iff_eventuallyEq_zpow_smul_analyticAt {f : 𝕜 → E} {x : 𝕜} :
MeromorphicAt f x ↔ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ z in 𝓝[≠] x, f z = (z - x) ^ n • g z :=
by
refine ⟨fun ⟨n, hn⟩ ↦ ⟨-n, _, ⟨hn, eventually_nhdsWithin_iff.mpr ?_⟩⟩, ?_⟩
· filter_upwards with z hz
match_scalars
simp [sub_ne_zero.mpr hz]
· refine fun ⟨n, g, hg_an, hg_eq⟩ ↦ MeromorphicAt.congr ?_ (EventuallyEq.symm hg_eq)
exact (((MeromorphicAt.id x).sub (.const _ x)).zpow _).smul hg_an.meromorphicAt
