tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact

English

For a > 0, s ∈ R, the function x -> |x|^s e^{ - a x^2 } tends to 0 along cocompact at infinity.

Русский

Для a > 0, s ∈ R функция |x|^s e^{-a x^2} стремится к 0 по кокпомпактному пути при |x| → ∞.

LaTeX

$$$$ \\lim_{\\text{cocompact } x \\to \\infty} |x|^s e^{-a x^2} = 0.$$$$

Lean4

theorem tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact {a : ℝ} (ha : 0 < a) (s : ℝ) :
    Tendsto (fun x : ℝ => |x| ^ s * rexp (-a * x ^ 2)) (cocompact ℝ) (𝓝 0) :=
  by
  conv in rexp _ => rw [← sq_abs]
  rw [cocompact_eq_atBot_atTop, ← comap_abs_atTop]
  erw [tendsto_comap'_iff (m := fun y => y ^ s * rexp (-a * y ^ 2))
      (mem_atTop_sets.mpr ⟨0, fun b hb => ⟨b, abs_of_nonneg hb⟩⟩)]
  exact
    (rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg ha s).tendsto_zero_of_tendsto
      (tendsto_exp_atBot.comp <| tendsto_id.const_mul_atTop_of_neg (neg_lt_zero.mpr one_half_pos))

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