isLittleO_exp_comp_exp_comp — Mathlib

English

For f,g: α → ℝ and l a filter, exp(f) = o_l exp(g) if and only if g − f tends to +∞ along l.

Русский

Пусть f,g : α → ℝ и l фильтр. Тогда exp(f) = o_l exp(g) тогда и только тогда, когда g − f стремится к +∞ вдоль l.

LaTeX

$$$ (\exp \circ f) = o_l (\exp \circ g) \iff \operatorname{Tendsto} (g - f)\ l\ \text{atTop} $$$

Lean4

@[simp]
theorem isLittleO_exp_comp_exp_comp {f g : α → ℝ} :
    ((fun x => exp (f x)) =o[l] fun x => exp (g x)) ↔ Tendsto (fun x => g x - f x) l atTop := by
  simp only [isLittleO_iff_tendsto, exp_ne_zero, ← exp_sub, ← tendsto_neg_atTop_iff, false_imp_iff, imp_true_iff,
    tendsto_exp_comp_nhds_zero, neg_sub]

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