isLittleO_exp_neg_mul_rpow_atTop — Mathlib

English

For a > 0 and any b, exp(-a x) = o(x^b) as x → ∞.

Русский

Для a > 0 и любого b, exp(-a x) = o(x^b) при x → ∞.

LaTeX

$$$$ \exp(-a x) = o\bigl(x^b\bigr) \quad (x \to \infty) $$$$

Lean4

/-- `exp (-a * x) = o(x ^ s)` as `x → ∞`, for any positive `a` and real `s`. -/
theorem isLittleO_exp_neg_mul_rpow_atTop {a : ℝ} (ha : 0 < a) (b : ℝ) :
    IsLittleO atTop (fun x : ℝ => exp (-a * x)) fun x : ℝ => x ^ b :=
  by
  apply isLittleO_of_tendsto'
  · refine (eventually_gt_atTop 0).mono fun t ht h => ?_
    rw [rpow_eq_zero_iff_of_nonneg ht.le] at h
    exact (ht.ne' h.1).elim
  · refine (tendsto_exp_mul_div_rpow_atTop (-b) a ha).inv_tendsto_atTop.congr' ?_
    refine (eventually_ge_atTop 0).mono fun t ht => ?_
    simp [field, Real.exp_neg, rpow_neg ht]

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