isLittleO_zpow_mul_exp — Mathlib

English

Same as above with integer exponents, using cpow for integer powers.

Русский

Та же идея для целых степеней, используя cpow для целых степеней.

LaTeX

$$$\\forall {b_1 b_2 : \\mathbb{R}},\\; hb: b_1 < b_2 \\to \\forall {m n : \\mathbb{Z}},\\; (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
integer `b₁ < b₂`, we have
`(fun z ↦ z ^ a₁ * exp (b₁ * z)) =o[l] (fun z ↦ z ^ a₂ * exp (b₂ * z))`. -/
theorem isLittleO_zpow_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_intCast] using hl.isLittleO_cpow_mul_exp hb m n

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