English
For a with Re(a) < 0, the function x -> exp(a x^2 + b x) is little-o of |x|^s as x → ∞, uniformly in cocompact sense.
Русский
Для a с Re(a) < 0 функция x -> exp(a x^2 + b x) = o(|x|^s) при x → ∞ равномерно по кокомпактной топологии.
LaTeX
$$$$ (\\lambda x. e^{a x^2 + b x}) = o_{\\text{cocompact}}(|x|^s). $$$$
Lean4
theorem cexp_neg_quadratic_isLittleO_abs_rpow_cocompact {a : ℂ} (ha : a.re < 0) (b : ℂ) (s : ℝ) :
(fun x : ℝ ↦ cexp (a * x ^ 2 + b * x)) =o[cocompact ℝ] (|·| ^ s) :=
by
rw [cocompact_eq_atBot_atTop, isLittleO_sup]
constructor
· refine
((cexp_neg_quadratic_isLittleO_rpow_atTop ha (-b) s).comp_tendsto Filter.tendsto_neg_atBot_atTop).congr'
(Eventually.of_forall fun x ↦ ?_) ?_
· simp only [neg_mul, Function.comp_apply, ofReal_neg, neg_sq, mul_neg, neg_neg]
· refine (eventually_lt_atBot 0).mp (Eventually.of_forall fun x hx ↦ ?_)
simp only [Function.comp_apply, abs_of_neg hx]
· refine (cexp_neg_quadratic_isLittleO_rpow_atTop ha b s).congr' EventuallyEq.rfl ?_
refine (eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx ↦ ?_)
simp_rw [abs_of_pos hx]
