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.

[Moritz Doll]

#33633 (split FourierModule into FourierAdd and FourierSMul, because otherwise fourier_add needs to find a ring)

[Moritz Doll]

#33636 (the Laplacian on Schwartz functions, uses the sum of second derivatives as a definition to avoid proving more continuity statements. We show that that it is independent of the choice of basis)

[Moritz Doll]

#33858 (convolution on Schwartz functions, uses the Fourier transform and multiplication for the definition, yet again to avoid tedious calculations for the well-definedness and continuity)

[Moritz Doll]

#33741 (additional lemmas for smulLeftCLM, show be relatively straightforward)

[Moritz Doll]

#33751 (self-adjointness for the inverse Fourier transform, almost copied from the same fact about the FT)

[Moritz Doll]

#33752 (line derivative of Fourier transform for Schwartz functions)

[Moritz Doll]

#33776 (bounded continuous functions are $L^\infty$ - I am surprised that this does not seem to exist)

[Moritz Doll]

#33859 (coercion Lp to temperd distribution and multiplication, just one lemma relating Hölder and smulLeftCLM)

[Moritz Doll]

I know this is a lot of PRs, but I've tried to get them in a very reviewable size. Except for the convolution (which I did just for fun) these are all needed for defining Sobolev spaces..

[Jireh Loreaux]

I'll have a look at these today.

[Jireh Loreaux]

@Moritz Doll can you say a bit more about why you're using the sum of second derivatives definition in #33636 ? I know you alluded to it above, but details would be helpful.

[Moritz Doll]

#34294 (derivatives of Fourier transform for tempered distribution), should be easy

[Moritz Doll]

#34099 (Fourier multiplier)

[Moritz Doll]

#34637 (support), a bit lengthy, I am happy to split if desired