Fourier transforms of (higher order) Hermite functions

Stream: new members

[Nicholas Wilson]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.html#fourierIntegral_gaussian_pi gives the Fourier transform for the gaussian (zeroth order Hermite function)

https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Polynomial/Hermite/Gaussian.html

is the Hermite polynomials. Do we have anything on the higher order Hermite functions and their Fourier transforms?

[Josha Dekker]

From that file, it also seems we’re missing that they form an orthogonal polynomial sequence for standard normals…

[Josha Dekker]

I checked with moogle , doesn’t seem to be in Mathlib yet

[Luigi Massacci]

Yeah I was thinking along the same lines, it’s unlikely that we have what you’re looking for if we don’t even have orthogonality. Granted that one does not require the other, but it’s indicative of the fact that they haven’t been developed a lot. Anyway I found nothing with loogle, leansearch and moogle

[Luigi Massacci]

So it’s likely that if you want them you’ll need to do it yourself @Nicholas Wilson

[Nicholas Wilson]

I'll leave that as sorry then, I don't think I have the lean knowledge enough for that .

Should I add a GitHub issue for this so that it is tracked?

[Nicholas Wilson]

There seemed to be a bunch of other feature requests as issues so I added one https://github.com/leanprover-community/mathlib4/issues/18548