abs_im_pow_eventuallyLE_exp_re — Mathlib

English

There exists eventual domination of |Im z|^n by exp(Re z).

Русский

Существует асимптотическое доминирование |Im z|^n над exp(Re z).

LaTeX

$$$\\forall n:\\;\\mathbb{N},\\; (|\\operatorname{im} z|)^n \\leq^?_l \\exp(\\operatorname{re} z)$$$

Lean4

theorem abs_im_pow_eventuallyLE_exp_re (hl : IsExpCmpFilter l) (n : ℕ) :
    (fun z : ℂ => |z.im| ^ n) ≤ᶠ[l] fun z => Real.exp z.re := by
  simpa using (hl.isLittleO_im_pow_exp_re n).bound zero_lt_one

Похожие утверждения