isBigO_one_exp_comp — Mathlib

English

The constant 1 is Big-O of exp(f) along l if and only if f is bounded below along l.

Русский

Константа 1 является Big-O от exp(f) вдоль л, если и только если f ограничена снизу вдоль l.

LaTeX

$$$ 1 = O_l(\exp \circ f) \iff \operatorname{IsBoundedUnder}_{\ge}(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`. -/
@[simp]
theorem isBigO_one_exp_comp {f : α → ℝ} :
    ((fun _ => 1 : α → ℝ) =O[l] fun x => exp (f x)) ↔ IsBoundedUnder (· ≥ ·) l f := by
  simp only [← exp_zero, isBigO_exp_comp_exp_comp, Pi.sub_def, zero_sub, isBoundedUnder_le_neg]

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