isBigO_exp_neg_mul_of_le — Mathlib

English

Let c and d be real numbers with c ≤ d. Then as t grows, exp(-d t) is bounded by a constant multiple of exp(-c t); equivalently, exp(-d t) = O_atTop(exp(-c t)).

Русский

Пусть c, d ∈ ℝ и c ≤ d. Тогда при росте t экспонента exp(-d t) ограничена константой пропорционально exp(-c t); то есть exp(-d t) = O_atTop(exp(-c t)).

LaTeX

$$$\exp(-d t) = O_{\text{atTop}}(\exp(-c t)) \quad (c \le d).$$$

Lean4

theorem isBigO_exp_neg_mul_of_le {c d : ℝ} (hcd : c ≤ d) : (fun t ↦ exp (-d * t)) =O[atTop] fun t ↦ exp (-c * t) :=
  by
  apply Eventually.isBigO
  filter_upwards [eventually_gt_atTop 0] with t ht
  rw [norm_of_nonneg (exp_pos _).le]
  gcongr

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