Tempered distributions

Stream: PR reviews

[Moritz Doll]

I finally got a bit of time to start PRing some of the results in #29819. I will mention below the open and review-ready PRs.
I already want to thank everyone who reviews any of these PRs. With my reviewer team hat on, I also want to mention that you don't have to be part of the reviewer or maintainer team to review PRs to mathlib.

[Moritz Doll]

#30176 (multiplication of temperate growth functions, had a some reviews, but was blocked by the file growing too much)

[Moritz Doll]

#31075 (easy clean-up)

[Moritz Doll]

#31073 (another fix)

[Moritz Doll]

#29888 (move extension of linear maps (the BLT theorem) into a new file)

[Moritz Doll]

#31079 (approximation of L^p functions by smooth compactly supported functions)

[Moritz Doll]

#31074 (the new variants of the BLT theorem). I am not sure whether LinearMap.leftInverse and friends should move somewhere

[Moritz Doll]

#31112 (temperate growth functions are closed under addition, subtraction and negation)

[Moritz Doll]

#31115 (notation type classes for Fourier transform and inverse) this might be one of the more controversial changes in this list. It introduces type classes that just carry the notation for the Fourier transform and its inverse. Currently if you use $\mathcal{F}$, then this means that you coerce to a bare function, but obviously we know that the Fourier transform of a Schwartz function is again Schwartz and the Fourier transform of an L^2 function is L^2. So to stating a lot of theorems with $\mathcal{F}$ is really bad at the moment and most uses of the Fourier transform are not with bare functions.

[Moritz Doll]

#11496 (the topology of pointwise convergence of continuous linear maps, aka the strong operator topology)

[Moritz Doll]

#31085 (fderiv of the norm squared for real inner product spaces)

[Moritz Doll]

#31114 (use notation for Fourier transform of Schwartz functions). This really shows why PR31115 was needed, it makes everything way more streamlined.

[Moritz Doll]

#31577 (the topology of pointwise convergence is locally convex)

[Moritz Doll]

#31756 (the equivalence of CLM and UniformConvergenceCLM)

[Moritz Doll]

these two are the last boring bits until we can define tempered distributions and prove the convergence criterion

[Jireh Loreaux]

I'll be having a look at these tomorrow.

[Moritz Doll]

#32566 (dense embedding)

[Moritz Doll]

#32411 (bilinear pairing of Schwartz functions)

[Moritz Doll]

#32297 (composition of temperate growth functions)

[Moritz Doll]

There is also #31757, the definition of tempered distributions, which I have changed very recently to be more similar to the definition for classical distributions (Anatole's PR).

[Laura Monk]

Hi! Just a quick message to share my enthusiasm as I have a project which requires a few basic facts about distributions :). I'll try to review if I manage to catch up ( it's been going fast!).

[Michael Rothgang]

If you like or need classical distributions, reviews there are also welcome :-)

[Moritz Doll]

Laura Monk said:

Hi! Just a quick message to share my enthusiasm as I have a project which requires a few basic facts about distributions :). I'll try to review if I manage to catch up ( it's been going fast!).

That is amazing to hear :blush: On the tempered distribution side I have quite a few of the basic results done, so if you have certain results that you need I can try to prioritize those.

[Laura Monk]

Michael Rothgang said:

If you like or need classical distributions, reviews there are also welcome :-)

Actually I appear to have sent to the wrong chat, I need classical distributions :sweat_smile: so yes definitely!

[Moritz Doll]

#32307 (the Bessel potential has temperate growth)

[Moritz Doll]

There are a couple of other PRs about embeddings and extending operations to tempered distributions, which are probably not too hard to review.