isLittleO_exp_neg_mul_sq_cocompact

English

The function x -> exp(-a x^2) is little-o of |x|^s in cocompact sense for a.re < 0.

Русский

Функция x -> exp(-a x^2) ∈ o(|x|^s) в коккомпактном смысле, если a.re < 0.

LaTeX

$$$$ (\\exp(-a x^2)) = o_{\\text{cocompact } \\mathbb{R}} (|x|^s). $$$$

Lean4

theorem isLittleO_exp_neg_mul_sq_cocompact {a : ℂ} (ha : 0 < a.re) (s : ℝ) :
    (fun x : ℝ => Complex.exp (-a * x ^ 2)) =o[cocompact ℝ] fun x : ℝ => |x| ^ s :=
  by
  convert cexp_neg_quadratic_isLittleO_abs_rpow_cocompact (?_ : (-a).re < 0) 0 s using 1
  · simp_rw [zero_mul, add_zero]
  · rwa [neg_re, neg_lt_zero]

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