rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg

English

A variant of the Gaussian Fourier transform in an inner product space equates the transform of a Gaussian with a shifted Gaussian in the dual variable, reflecting the standard completing-the-square mechanism in higher dimensions.

Русский

Вариант гауссова преобразования Фурье в пространстве с скалярным произведением даёт преобразование гауссиана на сдвиге в двойственном переменном.

LaTeX

$$$$\\mathcal{F}\\left(v \\mapsto e^{-b \\|v\\|^2 + 2π i ⟨x,v⟩}\\right)(w) = (\\\\pi/b)^{\\\\dim(V)/2} e^{-π^2 \\|x-w\\|^2 / b}.$$$$

Lean4

theorem rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg (s : ℝ) {b p : ℝ} (hp : 1 < p) (hb : 0 < b) :
    (fun x : ℝ => x ^ s * exp (-b * x ^ p)) =o[atTop] fun x : ℝ => exp (-(1 / 2) * x) :=
  by
  apply ((isBigO_refl (fun x : ℝ => x ^ s) atTop).mul_isLittleO (exp_neg_mul_rpow_isLittleO_exp_neg hb hp)).trans
  simpa only [mul_comm] using Real.Gamma_integrand_isLittleO s

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