4 Facts from Fourier analysis

Recall the definition of a Fourier transform.

Definition 4.1

✓

The Fourier transform of an \(L^1\)-function \(f:\mathbb {R}^d\to \mathbb {C}\) is defined as

\[ \mathcal{F}(f)(y) = \widehat{f}(y) := \int _{\mathbb {R}^d} f(x)e^{-2\pi i \langle x, y \rangle } \, \mathrm{d}x, \quad y \in \mathbb {R}^d \]

where \(\langle x, y \rangle = \frac12\| x\| ^2 + \frac12\| y\| ^2 - \frac12\| x - y\| ^2\) is the standard scalar product in \(\mathbb {R}^d\).

The following computational result will be of use later on.

Lemma 4.2

\begin{equation} \mathcal{F}(e^{\pi i \| x\| ^2 z})(y) = z^{-4}\, e^{\pi i \| y\| ^2 \, (\frac{-1}{z}) }. \end{equation}

Proof ▶

redFill in proof.

Of great interest to us will be a specific family of functions, known as Schwartz Functions. The Fourier transform behaves particularly well when acting on Schwartz functions. We elaborate in the following subsections.

4.1 On Schwartz Functions

Definition 4.3

✓

A \(C^\infty \) function \(f:\mathbb {R}^d\to \mathbb {C}\) is called a Schwartz function if it decays to zero as \(\| x\| \to \infty \) faster then any inverse power of \(\| x\| \), and the same holds for all partial derivatives of \(f\), ie, if for all \(k, n \in \mathbb {N}\), there exists a constant \(C \in \mathbb {R}\) such that for all \(x \in \mathbb {R}^d\), \(\left\lVert x \right\rVert ^k \cdot \left\lVert f^{(n)}(x) \right\rVert \leq C\), where \(f^{(n)}\) denotes the \(n\)-th derivative of \(f\) considered along with the appropriate operator norm. The set of all Schwartz functions from \(\mathbb {R}^d\) to \(\mathbb {C}\) is called the Schwartz space. It is an \(\mathbb {R}\)-vector space.

Lemma 4.4

✓

The Fourier transform is a continuous, linear automorphism of the space of Schwartz functions.

Proof ▶

We do not elaborate here as the result already exists in Mathlib. We do, however, mention that the Lean implementation defines a continuous linear equivalence on the Schwartz space using the Fourier transform (see SchwartzMap.fourierTransformCLM). The ‘proof’ that for any Schwartz function \(f\), its Fourier transform and its image under this continuous linear equivalence are, indeed, the same \(\mathbb {R}^d \to \mathbb {R}\) function, is stated in Mathlib solely for the purpose of rw and simp tactics, and is proven simply by rfl.

Another reason we are interested in Schwartz Functions is that they behave well under infinite sums. This will be useful to us when proving the Cohn-Elkies linear programming bound.

4.2 On the Summability of Schwartz Functions

We begin by stating a general summability result over specific subsets of \(\mathbb {R}^d\).

Lemma 4.5

Let \(X \subset \mathbb {R}^d\) be a set of sphere packing centres of separation \(1\) that is periodic with some lattice \(\Lambda \subset \mathbb {R}^d\). Then, there exists \(k \in \mathbb {N}\) sufficiently large such that

\[ \sum _{x \in X} \frac{1}{\left\lVert x \right\rVert ^{k}} {\lt} \infty . \]

Proof ▶

First, note that it does not matter how we number the (countably many) elements of the discrete set \(X\): if we prove absolute convergence for one numbering, we prove absolute convergence for any numbering. The idea will be to bound the sequence of partial sums by considering the volumes of concentric \(d\)-spheres of the appropriate radii (or scaled versions of a \(0\)-centred fundamental domain).

redFinish!

The decaying property of Schwartz functions means that they can be compared to the absolutely convergent power series above.

Lemma 4.6

Let \(f : \mathbb {R}^d \to \mathbb {C}\) be a Schwartz function and let \(X \subset \mathbb {R}^d\) be periodic with respect to some lattice \(\Lambda \subset \mathbb {R}^d\). Then,

\[ \sum _{x \in X} |f(x)| {\lt} \infty . \]

Proof ▶

Without loss of generality, assume that \(0 \notin X\): if \(0 \in X\), then we can add the \(f(0)\) term to the sum over nonzero elements of \(X\), which, if the sum over the nonzero elements converges absolutely, will be equal to the sum over all of \(X\). Now, we know that for all \(k \in \mathbb {N}\), there exists some constant \(C\) such that \(|f(x)| \leq C\left\lVert x \right\rVert ^{-k}\) for all \(x \in \mathbb {R}^d\). Choosing \(k\) to be sufficiently large, we see that

\[ \sum _{x \in X} |f(x)| \leq \sum _{x \in X} \frac{C}{\left\lVert x \right\rVert ^{k}} = C \sum _{x \in X} \frac{1}{\left\lVert x \right\rVert ^k} {\lt} \infty . \]

We end with a crucial result on Schwartz functions, the statement of which only makes sense because of the above result.

Theorem 4.7 Poisson summation formula

Let \(\Lambda \) be a lattice in \(\mathbb {R}^d\), and let \(f:\mathbb {R}^d\to \mathbb {R}\) be a Schwartz function. Then, for all \(v \in \mathbb {R}^d\),

\[ \sum _{\ell \in \Lambda }f(\ell + v) = \frac{1}{\operatorname {Vol}\! \left(\mathbb {R}^d/\Lambda \right)} \sum _{m\in \Lambda ^*}\widehat{f}(m) e^{-2\pi i \left\langle v, m \right\rangle }. \]

Proof ▶

redFill in proof.

While the Poisson Summation Formula over lattices can be stated in greater generality (and probably should be formalised as such in Mathlib due to the many applications it admits), we stick with Schwartz functions because that should be sufficient for our purposes.