Tempered distributions

Stream: Is there code for X?

[Michael Rothgang]

mathlib#16386 was a tracking issue (by the way, is there any reason not to move/re-create this at mathlib4? I would find this useful). The checklist seems a bit outdated; IIRC, mathlib has compactly supported smooth functions now and @David Loeffler did some work on Fourier transforms.

@Moritz Doll @Anatole Dedecker You were working on this back in mathlib3 -- was there anything else I did not find?

My understanding is that the Sobolev project of @Floris van Doorn and @Heather Macbeth does not define distributions or Sobolev spaces, but rather shows the Sobolev inequality for C¹ functions (which, by density, will imply the same for Sobolev functions).

[David Loeffler]

The Fourier-transforms code I added was somewhat orthogonal to this – I was concentrating on defining Fourier transforms directly on $L^1(\mathbb{R})$ using the obvious integral, rather than defining it on Schwartz functions and extending by density etc. But it is clearly related. I think @rtertr (Sonia) also added some related code (showing that the Gaussian is a Schwartz function – possibly only in one dimension though).