Multi-variable Fourier analysis

Stream: maths

[David Loeffler]

I see that @Junyan Xu posted on #18477 (relaxing a hypothesis in the Poisson summation formula), shortly before it got merged, asking about generalisations to the multi-variable case; but the PR got merged and closed before anyone had time to reply. So I'd like to continue the discussion here.

Is anyone currently working on multi-variable Fourier analysis (either Fourier series or Fourier transforms or both)? And, what versions of these theories would people in this community like to see formalised in the future?

FWIW, I have a (rather old) git branch somewhere which generalises the theorems about Fourier series from Analysis/Fourier/AddCircle.lean from functions on $\mathbb{R} / \mathbb{Z}$ to functions on $\mathbb{R}^n / \mathbb{Z}^n$. I didn't attempt to PR it yet, because I wasn't 100% convinced it was the right approach – should one work with $\mathbb{R}^n / \mathbb{Z}^n$ and deduce results about general finite-dimensional spaces from this, or maybe $\prod_i \mathbb{R} / t_i \mathbb{Z}$ for some vector of positive reals $(t_1, \dots, t_n)$, or should one rather work from the start with $V / \Lambda$, where V is a finite-diml' real vector space and $\Lambda$ a full-rank lattice in V? Anyway, this is the sort of question I think it would be good to discuss.

[Michael Stoll]

I would say we want the general lattice version eventually. Whether it is easier to get there via products of circles or directly is perhaps a more technical question.

[Junyan Xu]

I think I've seen this thread (Poisson summation on lattices) a while ago, but had forgotten about it when I posted; this new thread could probably be merged with it.
D-dimensional Fourier analysis is another relevant thread

[Kevin Buzzard]

$\mathbb{A}_K/K$ ;-)

[Thomas Browning]

Eventually, this will all be covered by the Pontryagin dual, but that's still a long way off.

[David Loeffler]

@Thomas Browning What are the general statement about Pontryagin duality you are aiming for which would imply the main theorems of Fourier analysis for $\mathbb{R}$ and $\mathbb{R} / \mathbb{Z}$?

In my head Pontryagin duality is the statement that for an LCA group $G \stackrel{\sim}{\to} \widehat{\widehat{G}}$. But that doesn't tell us much for $G = \mathbb{R} / \mathbb{Z}$. I guess you are referring to some statement beyond that – maybe that the Fourier transform is a bijection between suitable function spaces on $G$ and $\widehat{G}$, perhaps for L^2 functions, or Schwartz functions?

How would you recover e.g. Poisson summation from this general theory?

[Thomas Browning]

My memory is that if you have a short exact sequence of locally compact Hausdorff abelian topological groups
$0\to A\to B\to C\to 0$
with compatible Haar measures
$\int_Bf(b)\,db=\int_C\int_Af(ac)\,da\,dc,$
then you get a Poisson summation formula
$\int_Af(a)\,da=\int_{\widehat{C}}\widehat{f}(\hat{c})\,d\hat{c}.$
The proof is the same as the usual one: Apply the Fourier inversion theorem to
$F(c)=\int_Af(ac)\,da.$

[Thomas Browning]

Here's an old note of mine that I dug up:
PoissonSummation.pdf

[Thomas Browning]

David Loeffler said:

Thomas Browning What are the general statement about Pontryagin duality you are aiming for which would imply the main theorems of Fourier analysis for $\mathbb{R}$ and $\mathbb{R} / \mathbb{Z}$?

It's more that all of the main theorems of Fourier analysis generalize to the Pontryagin dual (the Fourier inversion theorem, the Poisson summation formula, Plancherel's theorem).

[Antoine Chambert-Loir]

All of the above is fine, except that in concrete cases, one wishes to have a specific model of the Pontryagin dual. For example in the case of the exact sequence that leads to the general version of Poisson, one often wishes to view $\widehat C$ has the orthogonal of $A$ in $\widehat B$. Analogously, characters of $V/\Lambda$ are usually seen as some sublattice of $V^\vee$ (those for which the duality pairing with all elements of $\Lambda$ is integral).

[Antoine Chambert-Loir]

It is probably useful to have some “duality” typeclass here.