English
Let f,g be functions from an index set to the real numbers, and l be a filter on the index set. Then the exponential-of-f and exponential-of-g are Θ-equivalent along l if and only if the difference f − g is bounded above along l.
Русский
Пусть f,g : α → ℝ и l — фильтр на α. Тогда exp∘f и exp∘g ведут себя как Θ вдоль l тогда и только тогда, когда разность f − g ограничена сверху вдоль l.
LaTeX
$$$ (\exp \circ f) =_{\Theta}^{l} (\exp \circ g) \iff \exists M \in \mathbb{R}, \{x \mid |f(x) - g(x)| \le M\} \in l $$$
Lean4
@[simp]
theorem isTheta_exp_comp_exp_comp {f g : α → ℝ} :
((fun x => exp (f x)) =Θ[l] fun x => exp (g x)) ↔ IsBoundedUnder (· ≤ ·) l fun x => |f x - g x| := by
simp only [isBoundedUnder_le_abs, ← isBoundedUnder_le_neg, neg_sub, IsTheta, isBigO_exp_comp_exp_comp, Pi.sub_def]
