English
Exponential composition is Big-O of another exponential precisely when the difference f − g is bounded above along l; equivalently, IsBigO exp(f) vs exp(g) along l corresponds to boundedness of f − g.
Русский
Композиция экспоненты — выражение Big-O друг друга тогда и только тогда, когда разность f − g ограничена сверху вдоль l; эквивалентно связи exp(f) и exp(g) через ограниченность f − g вдоль l.
LaTeX
$$$((\\exp \\circ f) =O[l] (\\exp \\circ g)) \\iff IsBoundedUnder(l, \\le, f - g).$$$
Lean4
@[simp]
theorem isBigO_exp_comp_exp_comp {f g : α → ℝ} :
((fun x => exp (f x)) =O[l] fun x => exp (g x)) ↔ IsBoundedUnder (· ≤ ·) l (f - g) :=
Iff.trans (isBigO_iff_isBoundedUnder_le_div <| Eventually.of_forall fun _ => exp_ne_zero _) <| by
simp only [norm_eq_abs, abs_exp, ← exp_sub, isBoundedUnder_le_exp_comp, Pi.sub_def]
