English
If f is meromorphic at x, then meromorphicOrderAt f x = n for some integer n if and only if there exists a nonvanishing analytic g near x such that f(z) = (z−x)^n g(z) for z near x, z ≠ x.
Русский
Если f мероморфна в точке x, то порядок имеет целочисленное значение n тогда и только тогда существует аналитическая функция g, ненуловая вблизи x, такая что f(z) = (z−x)^n g(z) для z близко к x, z ≠ x.
LaTeX
$$$meromorphicOrderAt\ f\ x = n \iff \exists\ g:\ 𝕜 \to E,\ AnalyticAt\ 𝕜\ g\ x \land g\ x \neq 0 \land\forall\ᶠ z\ in\ 𝓝[≠]\ x,\ f\ z = (z - x)^n \cdot g\ z$$$
Lean4
/-- The order of a meromorphic function `f` at `z₀`, as an element of `ℤ ∪ {∞}`.
The order is defined to be `∞` if `f` is identically 0 on a neighbourhood of `z₀`, and otherwise the
unique `n` such that `f` can locally be written as `f z = (z - z₀) ^ n • g z`, where `g` is analytic
and does not vanish at `z₀`. See `MeromorphicAt.meromorphicOrderAt_eq_top_iff` and
`MeromorphicAt.meromorphicOrderAt_eq_int_iff` for these equivalences.
If the function is not meromorphic at `x`, we use the junk value `0`. -/
noncomputable def meromorphicOrderAt (f : 𝕜 → E) (x : 𝕜) : WithTop ℤ :=
if hf : MeromorphicAt f x then ((analyticOrderAt (fun z ↦ (z - x) ^ hf.choose • f z) x).map (↑· : ℕ → ℤ)) - hf.choose
else 0
