I'm not sure I entirely get the argument about renaming – the Fourier transform is given by the integral for L^1 functions, and Gaussians are about the most L^1 function you can imagine! But if you really want to rename the lemmas then go ahead, I'm not fanatically attached to the old names.

As for the inner-product space results: would it be significantly harder to treat the more general case of "ellipsoidal" rather than "spherical" Gaussians, i.e. exp(-∑ i, b i * (v i : ℂ) ^ 2 + ...) for some b : ι → ℂ, and then derive the case of constant b as a consequence? It seems to me that the proof you use would extend immediately to this case as well.

About the naming, I expect that in the not so distant future we will define the Fourier transform of a general function f : E -> ℂ, maybe as follows: if f is integrable against any Schwartz function and there exists a measurable g such that ∫ f ⬝ 𝓕 φ = ∫ g • φ for all Schwartz function, then use this g (or, better, if there is such a g which is continuous, then use the continuous version, and otherwise use the measurable one). This is what I would like to call the Fourier transform (in particular, it would work fine on L^2), and anticipating on this one I would like to use fourierTransform for lemmas about this one, and fourierIntegral for lemmas about the Fourier integral. I agree it's not essential, but planning a little bit ahead can help having a nice library.

Let me try to do the ellipsoidal Gaussian.

Ellipsoidal case done.

Looks great! We should probably change the section title

/-! ## Fourier transform of the Gaussian integral
-/

to something like "Fourier integral of the Gaussian function" for consistency with the lemma renamings (the original title is clearly a mistake anyway). Other than that I have nothing further to add.

Good remark. I've changed the section title accordingly, to Fourier integral of Gaussian functions.

🚀 Pull request has been placed on the maintainer queue by loefflerd.

bors r+

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style