English
Let f be a function with meromorphic order at x. Then the meromorphic order of f at x coincides with the natural image of its analytic order at x under the embedding of natural numbers into the extended natural numbers.
Русский
Пусть f имеет мероморфный порядок в точке x. Тогда мероморфный порядок f в x совпадает с образом через встроение (из натурального порядка) порядка аналитического f в x в дальшее множество ℕ ∪ {∞}.
LaTeX
$$$\\operatorname{meromorphicOrderAt} f x = \\operatorname{ENat}.map (Nat.cast) (\\operatorname{analyticOrderAt} f x)$$$
Lean4
/-- Compatibility of notions of `order` for analytic and meromorphic functions. -/
theorem meromorphicOrderAt_eq (hf : AnalyticAt 𝕜 f x) : meromorphicOrderAt f x = (analyticOrderAt f x).map (↑) :=
by
cases hn : analyticOrderAt f x
· rw [ENat.map_top, meromorphicOrderAt_eq_top_iff]
exact (analyticOrderAt_eq_top.mp hn).filter_mono nhdsWithin_le_nhds
· simp_rw [ENat.map_coe, meromorphicOrderAt_eq_int_iff hf.meromorphicAt, zpow_natCast]
rcases hf.analyticOrderAt_eq_natCast.mp hn with ⟨g, h1, h2, h3⟩
exact ⟨g, h1, h2, h3.filter_mono nhdsWithin_le_nhds⟩
