tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero

English

Let s ∈ ℝ and b > 0. Then x^s e^{−b x} → 0 as x → ∞.

Русский

Пусть s ∈ ℝ и b > 0. Тогда x^{s} e^{−b x} сходится к 0 при x → ∞.

LaTeX

$$$$\displaystyle \lim_{x \to +\infty} x^{s} e^{-b x} = 0\qquad (s \in \mathbb{R},\ b>0).$$$$

Lean4

/-- The function `x ^ s * exp (-b * x)` tends to `0` at `+∞`, for any real `s` and `b > 0`. -/
theorem tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (s : ℝ) (b : ℝ) (hb : 0 < b) :
    Tendsto (fun x : ℝ => x ^ s * exp (-b * x)) atTop (𝓝 0) :=
  by
  refine (tendsto_exp_mul_div_rpow_atTop s b hb).inv_tendsto_atTop.congr' ?_
  filter_upwards with x using by simp [exp_neg, inv_div, div_eq_mul_inv _ (exp _)]

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