isLittleO_pow_mul_exp — Mathlib

English

For natural m<n and b1<b2, (z^m e^{b1 z}) = o_l (z^n e^{b2 z}).

Русский

Если m<n и b1<b2, то z^m e^{b1 z} = o_l z^n e^{b2 z}.

LaTeX

$$$\\forall {b_1 b_2 : \\mathbb{R}},\\; (hb: b_1 < b_2)\\to \\forall {m n : \\mathbb{N}},\\; (z \\mapsto z^m e^{b_1 z}) =o_l (z \\mapsto z^n e^{b_2 z})$$$

Lean4

/-- If `l : Filter ℂ` is an "exponential comparison filter", then for any complex `a₁`, `a₂` and any
natural `b₁ < b₂`, we have
`(fun z ↦ z ^ a₁ * exp (b₁ * z)) =o[l] (fun z ↦ z ^ a₂ * exp (b₂ * z))`. -/
theorem isLittleO_pow_mul_exp {b₁ b₂ : ℝ} (hl : IsExpCmpFilter l) (hb : b₁ < b₂) (m n : ℕ) :
    (fun z => z ^ m * exp (b₁ * z)) =o[l] fun z => z ^ n * exp (b₂ * z) := by
  simpa only [cpow_natCast] using hl.isLittleO_cpow_mul_exp hb m n

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