English
In a finite index setting, the Fourier transform of the product of Gaussian exponentials equals the product of their individual Fourier transforms, consistent with separability over the index set.
Русский
В конечном наборе индексов преобразование Фурье произведения гауссовых экспонент равно произведению их индивидуальных преобразований Фурье.
LaTeX
$$$$\\\\mathcal{F}\\left(\\\\prod_i e^{-b_i x_i^2} e^{c_i x_i} \\right) = \\\\prod_i \\,\\\\mathcal{F}\\left(e^{-b_i x_i^2} e^{c_i x_i}\\right).$$$$
Lean4
theorem integral_cexp_neg_mul_sum_add {ι : Type*} [Fintype ι] (hb : 0 < b.re) (c : ι → ℂ) :
∫ v : ι → ℝ, cexp (-b * ∑ i, (v i : ℂ) ^ 2 + ∑ i, c i * v i) =
(π / b) ^ (Fintype.card ι / 2 : ℂ) * cexp ((∑ i, c i ^ 2) / (4 * b)) :=
by
simp_rw [neg_mul, Finset.mul_sum, integral_cexp_neg_sum_mul_add (fun _ ↦ hb) c, one_div, Finset.prod_mul_distrib,
Finset.prod_const, ← cpow_nat_mul, ← Complex.exp_sum, Fintype.card, Finset.sum_div, div_eq_mul_inv]
