rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg

English

For real parameters p > 1 and b > 0, the function x^s e^{-b x^p} is little-o of e^{-x/2} as x → ∞, i.e., it decays faster than e^{-x/2}. This is a refinement of the standard comparison with a Gaussian tail.

Русский

При p > 1 и b > 0 функция x^s e^{-b x^p} затухает быстрее, чем e^{-x/2} при x → ∞.

LaTeX

$$$$\\lim_{x \\to \\infty} \\frac{x^s e^{-b x^p}}{e^{-x/2}} = 0.$$$$

Lean4

theorem rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg {b : ℝ} (hb : 0 < b) (s : ℝ) :
    (fun x : ℝ => x ^ s * exp (-b * x ^ 2)) =o[atTop] fun x : ℝ => exp (-(1 / 2) * x) :=
  by
  simp_rw [← rpow_two]
  exact rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg s one_lt_two hb

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