English
For a complex number a with Re(a) < 0, the function x -> exp(a x^2 + b x) is little-o of |x|^s along cocompact at infinity, for any s.
Русский
Для комплексного a с Re(a) < 0 функция x -> exp(a x^2 + b x) = o(|x|^s) при скачке cocompact к бесконечности, для любого s.
LaTeX
$$$$ (\\text{fun } x \\mapsto e^{a x^2 + b x}) =_o_{\\text{cocompact } \\mathbb{R}} |x|^s. $$$$
Lean4
theorem rexp_neg_quadratic_isLittleO_rpow_atTop {a : ℝ} (ha : a < 0) (b s : ℝ) :
(fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] (· ^ s) :=
by
suffices (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] (fun x ↦ rexp (-x))
by
refine this.trans ?_
simpa only [neg_one_mul] using isLittleO_exp_neg_mul_rpow_atTop zero_lt_one s
rw [isLittleO_exp_comp_exp_comp]
have : (fun x ↦ -x - (a * x ^ 2 + b * x)) = fun x ↦ x * (-a * x - (b + 1)) := by ext1 x; ring_nf
rw [this]
exact tendsto_id.atTop_mul_atTop₀ <| tendsto_atTop_add_const_right _ _ <| tendsto_id.const_mul_atTop (neg_pos.mpr ha)
