English
Let l be a filter on the complex plane. If the real part tends to +∞ along l and the imaginary part is O_l((Re z)^n) for some natural n, then l is an exponential comparison filter.
Русский
Пусть l — фильтр на комплексной плоскости. Если действительная часть z стремится к +∞ вдоль l, и мнимая часть удовлетворяет Im z =O_l((Re z)^n) для некоторого натурального n, то l является экспоненциальным сравнительным фильтром.
LaTeX
$$$\\forall l:\\,\\mathsf{Filter}\\,\\mathbb{C},\\; \\operatorname{Tendsto} (\\operatorname{re})\\, l\\, \\operatorname{atTop} \\;\\to\\; \\forall n\\in\\mathbb{N},\\; \\operatorname{Im} =O_l(z\\mapsto z.re^n)\\; \\to\\; \\IsExpCmpFilter\\ l$$$
Lean4
theorem of_isBigO_im_re_pow (hre : Tendsto re l atTop) (n : ℕ) (hr : im =O[l] fun z => z.re ^ n) : IsExpCmpFilter l :=
of_isBigO_im_re_rpow hre n <| mod_cast hr
