Fourier transform

Stream: maths

[Gabriel Ebner]

I'd like to do a small project to get to know mathlib, and @Rob Lewis suggested that I could work on Fourier analysis. AFAICT this would require some basic facts about Bochner integrals (such as linearity, etc.), and single-variable derivatives would be nice too. Is anybody working on this?

[Johan Commelin]

@Kenny Lau Did you ever formalise anything in this direction?

[Patrick Massot]

You should ask @Jeremy Avigad and @Joe about the current status of integration.

[Patrick Massot]

It would be really nice to see some move in this direction.

[Joe]

@Gabriel Ebner Bochner integral is already defined in the library, though simple properties are not proved yet. But I think I’ll finish that very soon.

[Jeremy Avigad]

@Gabriel Ebner An option in the meanwhile is just to axiomatize or sorry the properties of integrals that you need. I trust Joe when he says he'll get to it soon.

[Moritz Doll]

I think after 3 years we should really define the Fourier transform. There are three bikeshedding questions that I would like to get settled before typing a single line of code:
(a) there is the very abstract definition of the Fourier transform using Pontryagin duals and whatnot. As far as I can see we don't have the tools at the moment to prove anything useful. Moreover one has to be really careful, because one might need two different FTs (additive and multiplicative). Also I don't know whether we have the tools to show that the abstract definition is equal to the usual definition of the FT on $ℝ^d$.
(b) Say we restrict our attention to the concrete definition on $ℝ^d$. Then there are at least three different conventions:
$\mathcal{F}_1 f \coloneqq \int_{ℝ^d} e^{-ixξ} f(x) dx$
$\mathcal{F}_2 f \coloneqq (2π)^{-d/2} \int_{ℝ^d} e^{-ixξ} f(x) dx$
$\mathcal{F}_3 f \coloneqq \int_{ℝ^d} e^{-2πixξ} f(x) dx$
Personally, I am a big fan of the first version, where one takes a differently scaled measure on the dual so that all powers of $2π$ disappear (I am afraid that this will not be possible in mathlib), but I think that the third variant might work better with the abstract definition. On the other hand the first two version have the advantage that you don't have to deal with the annoying powers of $2π$ every time you differentiate the phase.
(c) The last question is to whether define the "concrete" FT on a normed space with the dual being really the dual or on inner_product_space, where the dual is canonically isomorphic to the space itself. I would slightly be in favor of the later one since we will have the really abstract definition anyways and the inner_product_space version would make many theorems much clearer

[Jireh Loreaux]

Can you specify what your domain and codomain are for the Fourier transform? From what I recall of the literature, authors tend to play fast and loose with these and use whatever is convenient at the time.

[Moritz Doll]

you mean as an operator? there will be lots of variants I guess, initially it is defined for any function (mathlib can integrate every function thankfully). Then there will be a version that works for Schwartz functions (since every Schwartz function is actually integrable) and then you use duality to define it for tempered distributions. To go full circle you then show that the definition for $L^1$ coincides with the definition for $\mathcal{S}'$. If you know it for tempered distributions then you can easily restrict to $L^p$.

[Sebastien Gouezel]

(c): I'd rather define the Fourier transform on an inner product space. The general version will be the Ptryagin duality, so let's leave that just for the general version and prove the useful theorems for analysis in the useful context.
(b): I would be in favor of $\mathcal{F}_2$ because you have the same operator in both directions, and you have the same measure on the space and its dual (which is the only thing that makes sense in mathlib). And that's the one I use most of the time in papers, also :-)

[Sebastien Gouezel]

Some thought: I think that the Fourier transform should not be defined on generic functions by the integral formula. I envision things as follows:

• define fourier_transform_aux on functions by the integral formula
• restrict it to the Schwarz space, show that it is a continuous linear map there, and all the goodies.
• then define it on distributions by duality
• Finally, define it on functions as follows: if, on the corresponding distribution, it coincides with a continuous function, then use this one. Otherwise, if it coincides with a locally integrable function, use this one. Otherwise, use 0.

In this way, the definition is integrability-agnostic: it will work on L^2, on L^p, on integrable functions, and so on.

[Yaël Dillies]

Also note that combinatorics needs the discrete Fourier transform (Fourier transform on finite groups). Not sure where that fits in the greater scheme of things.

[Moritz Doll]

I can totally live with $\mathcal{F}_2$ :smiley:
Sebastien, for a function to define a tempered distribution you also need a growth estimate ($e^{x^2}$ does not define a tempered distribution). You are probably still right and the initial definition should be used not be called the Fourier transform

[Antoine Chambert-Loir]

I prefer F3...

[Thomas Browning]

My understanding of Fourier transforms is pretty limited, but my impression is that $\mathcal F_3$ best aligns with the abstract definition.

[Mauricio Collares]

Yaël Dillies said:

Also note that combinatorics needs the discrete Fourier transform (Fourier transform on finite groups). Not sure where that fits in the greater scheme of things.

In particular, https://people.maths.ox.ac.uk/greenbj/papers/addcomb2009-1.pdf (page 5) has some comments on the most convenient normalization in the discrete setting.

[Yuyang Zhao]

For the discrete setting, it may need DFT over more general rings.