isTheta_exp_comp_one — Mathlib

English

The exponential of f is Theta of 1 along l if and only if |f| is bounded above along l.

Русский

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

LaTeX

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

Lean4

/-- `Real.exp (f x)` is bounded away from zero and infinity along a filter `l` if and only if
`|f x|` is bounded from above along this filter. -/
@[simp]
theorem isTheta_exp_comp_one {f : α → ℝ} :
    (fun x => exp (f x)) =Θ[l] (fun _ => 1 : α → ℝ) ↔ IsBoundedUnder (· ≤ ·) l fun x => |f x| := by
  simp only [← exp_zero, isTheta_exp_comp_exp_comp, sub_zero]

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