mathlib

mathlib copied to clipboard

This is another tracking issue for me, but if anyone is interested in helping out, then I would be very happy.

The goal is to get tempered distributions and the Fourier transform going and this needs several independent results:

1. An efficient characterization of continuity for Fréchet spaces Strictly speaking we don't need Fréchet spaces, but only pseudometrizable locally convex spaces.

• [x] #16550
• [x] #16595

2. Basic facts about Schwartz functions

• [x] #18649
• [x] #16756
• [ ] Multiplication of Schwartz functions as a bilinear map
• [ ] Convolution
• [x] 1-d Gaussian (would be nice to have #15566 for that)
• [ ] Compactly supported smooth functions

3. Definition of tempered distributions

• [x] #16053
• [ ] Definition of tempered distributions
• [x] #16638

4. Fourier transform

• [x] Definition
• [x] #16491
• [ ] As a continuous map on Schwartz space
• [ ] The inverse Fourier transform
• [ ] Relationship of derivatives and multiplication operators under FT