feat(Analysis/Fourier/Derivative): Fréchet derivative of the Fourier transform

[AlexKontorovich]

We evaluate the Fréchet derivative of the Fourier transform, expressing it itself as a Fourier transform. The latter will allow one to iterate differentiation, eventually showing that the Fourier transform of a Schwartz function is also Schwartz.

Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com

---

[loefflerd]

This should probably go in Fourier.FourierTransform rather than here.

[loefflerd]

I had a draft for a mathlib3 PR doing much the same thing, but it got overtaken by the lean4 port and I never got around to forward-porting it. I'll dig it up and compare with what you wrote. (It's not unlikely that your work supersedes it entirely, but we may as well check.)

[loefflerd]

Comparing with the Lean3 code I had lying around, there is indeed a difference.

You impose the condition [InnerProductSpace ℝ E], in order to interpret the Fourier transform of a function on E as a function on E. However, requiring an inner-product space structure (i.e. a symmetric positive-definite pairing) seems a bit limiting. For instance, in automorphic forms theory it's conventional to define the Fourier transform of functions on ℝ² by
$$\hat{\Phi}(x, y) = \int \Phi(u, v) e^{2\pi i (yu - xv)}\ \mathrm{d}u \mathrm{d}v,$$
i.e. with a symplectic bilinear form rather than a symmetric one; this has the advantage that $\hat{\hat{\Phi}} = \Phi$ (the annoying minus sign goes away).

I'd be in favour of a formulation where we don't privilege any choice of bilinear form, but instead takes as a parameter an arbitrary pairing L : V × W → ℝ, and sends functions on V to functions on W. This is what I coded up in Lean3: if v ↦ ‖v‖ * ‖f v‖ is integrable, then the derivative of the Fourier transform of f : V → E is the Fourier transform of v ↦ L(v, ⬝) • f v regarded as a function valued in Hom(W, E) [note my E is your F, and my V is your E].

Of course, one could potentially derive the more general bilinear-maps-space formulation from the inner-product-space formulation that you prove, by picking an arbitrary inner-product-space structure on V, and then pulling back along the unique map W → V determined by L. (There is an argument of the same type in mathlib already, in the proof of the Riemann-Lebesgue lemma.)

[loefflerd]

So, I dug up my old code and ported it to mathlib4. See this branch: https://github.com/leanprover-community/mathlib4/tree/DL_fourier_deriv

(CI is reporting some errors on it at the moment, but that's just code-style glitches picked up by the linter; it does compile.) (edit: now fixed)

[loefflerd]

I've tried to merge together your approach and mine, by adding to my git branch a lemma which (up to relabelling the variables) is the main result from your branch, derived as a special case of the more general one for arbitrary pairings. I've also added the special case of scalar-valued functions (which is surprisingly hard to deduce from the general theory!)

How should we proceed from here? May I suggest we make a new PR with my branch, and credit all three of us as coauthors on it?