noncomputable def FourierAnalysis.bookFourierTransform {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (f : V → ℂ) (w : V) : ℂ

The Fourier transform as defined in Melrose's book: (Ff)(w) = ∫ e^{-i⟨v,w⟩} f(v) dv, on a real finite-dimensional inner product space V.

theorem FourierAnalysis.fourier_transform_gaussian {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (w : V) : bookFourierTransform (fun (v : V) => Complex.exp (-(1 / 2) * ↑‖v‖ ^ 2)) w = ↑((2 * Real.pi) ^ (↑(Module.finrank ℝ V) / 2)) * Complex.exp (-(1 / 2) * ↑‖w‖ ^ 2)

Lemma 8.12 (Gaussian Fourier transform): the Fourier transform of the standard Gaussian v ↦ exp(-‖v‖²/2) on a finite-dimensional real inner product space V equals (2π)^{dim V / 2} · exp(-‖w‖²/2).