Documentation

Atlas.NumberTheoryI.code.GammaFunction

theorem gaussian_fourier_self :
(FourierTransform.fourier fun (x : ℝ) => Complex.exp (-↑Real.pi * ↑x ^ 2)) = fun (y : ℝ) => Complex.exp (-↑Real.pi * ↑y ^ 2)