isBigO_exp_comp_one — Mathlib

English

The exponential of f is Big-O of 1 if and only if |f| is bounded above along l.

Русский

Экспонента f ограничена сверху по отношению к константе 1 вдоль l тогда и только тогда, как |f| ограничено сверху вдоль l.

LaTeX

$$$ (\exp \circ f) = O_l 1 \iff \operatorname{IsBoundedUnder}_{\le}(l |f|) $$$

Lean4

/-- `Real.exp (f x)` is bounded away from zero along a filter if and only if this filter is bounded
from below under `f`. -/
theorem isBigO_exp_comp_one {f : α → ℝ} :
    (fun x => exp (f x)) =O[l] (fun _ => 1 : α → ℝ) ↔ IsBoundedUnder (· ≤ ·) l f := by
  simp only [isBigO_one_iff, norm_eq_abs, abs_exp, isBoundedUnder_le_exp_comp]

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