English
A variant of the Gaussian FT identity specialized to a real inner product space expresses the transform in terms of the dimension and the inner product structure.
Русский
Уточнение гауссова преобразования Фурье для вещественно-пространства с скалярным произведением в терминах размерности и внутреннего произведения.
LaTeX
$$$$\\mathcal{F}(v \\mapsto e^{-b \\|v\\|^2})(w) = (\\\\pi/b)^{\\\\dim V / 2} e^{-π^2 \\|w\\|^2 / b}.$$$$
Lean4
theorem integrableOn_rpow_mul_exp_neg_mul_rpow {p s b : ℝ} (hs : -1 < s) (hp : 1 ≤ p) (hb : 0 < b) :
IntegrableOn (fun x : ℝ => x ^ s * exp (-b * x ^ p)) (Ioi 0) :=
by
have hib : 0 < b ^ (-p⁻¹) := rpow_pos_of_pos hb _
suffices IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * exp (-x ^ p))) (Ioi 0)
by
rw [show 0 = b ^ (-p⁻¹) * 0 by rw [mul_zero], ← integrableOn_Ioi_comp_mul_left_iff _ _ hib]
refine this.congr_fun (fun _ hx => ?_) measurableSet_Ioi
rw [← mul_assoc, mul_rpow, mul_rpow, ← rpow_mul (z := p), neg_mul, neg_mul, inv_mul_cancel₀, rpow_neg_one,
mul_inv_cancel_left₀]
all_goals linarith [mem_Ioi.mp hx]
refine Integrable.const_mul ?_ _
rw [← IntegrableOn]
exact integrableOn_rpow_mul_exp_neg_rpow hs hp
