isLittleO_exp_cpow — Mathlib

English

If b<0, then exp(b z) = o_l z^a for any a.

Русский

Если b<0, то exp(b z) = o_l z^a для любого a.

LaTeX

$$$\\forall a:\\,\\mathbb{C},\\; \\forall b<0:\\; (z \\mapsto \\exp(b z)) =o_l (z \\mapsto z^a)$$$

Lean4

/-- If `l : Filter ℂ` is an "exponential comparison filter", then for any complex `a` and any
negative real `b`, we have `(fun z ↦ exp (b * z)) =o[l] (fun z ↦ z ^ a)`. -/
theorem isLittleO_exp_cpow (hl : IsExpCmpFilter l) (a : ℂ) {b : ℝ} (hb : b < 0) :
    (fun z => exp (b * z)) =o[l] fun z => z ^ a := by simpa using hl.isLittleO_cpow_mul_exp hb 0 a

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