Blueprint for the collaborative Formalization Seminar

2 Plancherel’s Theorem

2.1 Basic Properties of the Fourier Transform

In this section we record, mostly without proofs, basic statements about the Fourier transform on \(L^1\) functions. Most of these are already formalized in mathlib.

Let \((V,\mu ),(W,\nu )\) be vector spaces over \(\mathbb {R}\) with a \(\sigma \)-finite measure, \(E,F\) be normed spaces over \(\mathbb {C}\) and let \(L:V\times W\to \mathbb {R}\), \(M:E\times F\to \mathbb {C}\) be bilinear maps.

Let \(f\in L^1(V,E)\). Its Fourier transform (w.r.t. \(L\)) is the function \(\mathcal Ff=\widehat f:W\to E\) given by

\[ \mathcal Ff(w):=\widehat f(w):=\int _V e^{-2\pi i L(v,w)}f(v)\, d\mu . \]

The inverse Fourier transform (w.r.t. \(L\)) is similarly defined as

\[ \mathcal F^{-1}f(w)=\check f(w):=\int _Ve^{2\pi iL(v,w)}f(v)\, d\mu . \]

Let \(f\in L^1(V,E)\). Then its Fourier transform \(\widehat f\) is well-defined and bounded. In particular, the Fourier transform defines a map \(\mathcal F:L^1(V,E)\to L^\infty (V,E)\).

Proof

Omitted.

From now on assume that \(V\) and \(W\) are equipped with second-countable topologies such that \(L\) is continuous.

Lemma 2.3

Let \(f\in L^1(V,E)\). Then \(\widehat f\) is continuous.

Proof

Omitted.

Lemma 2.4 Multiplication formula

Let \(f,g\in L^1(V,E)\). Then

\[ \int _WM(\widehat f(w),g(w))\, d\nu (w)=\int _VM(f(v),\widehat g(v))\, d\mu (v). \]
Proof

Omitted.

Lef \(f,g\in L^1(V,E)\), \(t\in \mathbb {R}\) and \(a,b\in \mathbb {C}\). The Fourier transform satisfies the following elementary properties:

  1. \(\mathcal F(af+bg)=a\mathcal Ff+b\mathcal Fg\)(Linearity)

  2. \(\mathcal F(f(x-t)) = e^{-2\pi i ty}\mathcal F f(y)\)(Shifting)

  3. \(\mathcal F(f(tx)) = \frac1{|t|}\mathcal F f(\frac yt)\)(Scaling)

  4. If \(E\) admits a conjugation, then \(\mathcal F(\overline{f(x)}) = \overline{\mathcal Ff(-y)}\)(Conjugation)

  5. Define the convolution of \(f\) and \(g\) w.r.t. a bilinear map \(M:E\times E\to F\) as

    \[ (f\ast _Mg)(w):=\int _VM(f(v),g(w-v))\, d\mu (v). \]

    Then \(\mathcal F(f\ast _M g) =M(\mathcal Ff,\mathcal Fg)\) (Convolution)

Proof

Omitted.

From now on, let \(V\) be a finite-dimensional inner product space. We denote this product as ordinary multiplication, and the induced norm as \(|\cdot |.\)

We now study a family of functions which is useful for later proofs.

Lemma 2.6

Let \(x\in V\) and \(\delta {\gt}0\). Define the modulated Gaussian

\[ u_{x,\delta }(y):V\to \mathbb {C},\quad y\mapsto e^{-\delta \pi |y|^2}e^{2\pi i x y}. \]

Its Fourier transform (w.r.t. the inner product) is given by

\[ \widehat{u_{x,\delta }}(z)=\delta ^{-n/2}e^{-\pi |x-y|^2/\delta }=:K_\delta (x-z). \]
Proof

By choosing an orthonormal basis, wlog we may assume \(V=\mathbb {R}^n\). First note \(\widehat{u_{x,\delta }}(z-x)=\widehat{u_{0,\delta }}(z)\), so it is enough to consider \(x=0\). Next,

\[ \widehat{u_{0,\delta }}(z)=\int _{\mathbb {R}^n}e^{-\pi \delta |y|^2-2\pi iyz}\, dy= \prod _{i=1}^n\int _{\mathbb {R}}e^{-\pi \delta y_i^2-2\pi iy_iz_i}dy_i\quad \text{and}\quad K_\delta (-z)=\prod _{i=1}^n\delta ^{-1/2}e^{-\pi y_i^2/\delta }, \]

hence we may assume \(n=1\). The change of variables \(w=\delta ^{1/2}y+iz/\delta ^{1/2}\) results in

\[ \widehat{u_{0,\delta }}(z)=\int _{\mathbb {R}} e^{-\pi \delta y^2-2\pi i y z}\, dy= \delta ^{-1/2}e^{-\pi z^2/\delta }\int _{Im(w)=z/\delta ^{1/2}}e^{-\pi w^2}\, dw. \]

Contour integration along the rectangle with vertices \((\pm R,0),(\pm R,iz/\delta ^{1/2})\), together with the bound

\[ \left|\int _{\pm R}^{\pm R+iz/\delta ^{1/2}}e^{-\pi w^2}\, dw\right|\leq \frac{|z|}{\delta ^{1/2}}\sup _{w\in [R,R+iz/\delta ^{1/2}]}|e^{-\pi w^2}|= \frac{|z|}{\delta ^{1/2}}e^{-\pi R^2}\xrightarrow {R\to \infty }0 \]

yields

\[ \int _{Im(w)=-z/\delta ^{1/2}}e^{-\pi w^2}\, dw= \int _{\mathbb {R}} e^{-\pi w^2}\, dw=1, \]

finishing the proof.

Lemma 2.7

Let \(K_\delta (v)=\delta ^{-n/2}e^{-\pi |v|^2/\delta }\) as in Lemma 2.6. This is a good kernel, called the Weierstrass kernel, satisfying

\[ \int _{V}K_\delta (x)\, dx= 1\quad \text{and}\quad \int _{|x|{\gt}\eta }K_\delta (x)\, dx\xrightarrow {\delta \to 0}0\quad \text{for all }\eta {\gt}0. \]

Furthermore, it satisfies the stronger bounds

\[ K_\delta (x)\leq \delta ^{-n/2}\quad \text{and}\quad K_\delta (x)\leq B\delta ^{1/2}|x|^{-n-1} \]

for some constant \(B\) independent of \(\delta \).

Proof

By choosing an orthonormal basis, wlog we may assume \(V=\mathbb {R}^n\). Then these are all straight-forward calculations:

\[ \int _{\mathbb {R}^n}e^{-\pi |x|^2/\delta }\, dx=\delta ^{n/2}\int _{\mathbb {R}^n}e^{-\pi |x|^2}\, dx=\delta ^{n/2}. \]
\[ \int _{|x|{\gt}\eta }\delta ^{-n/2}e^{-\pi |x|^2/\delta }\, dx=\int _{|x|{\gt}\eta /\delta ^{1/2}}e^{-\pi |x|^2}\xrightarrow {\delta \to 0}0. \]

The first upper bound is trivial. For the second one, consider for \(r,z\geq 0\) the inequality

\[ \Gamma (r+1)=\int _0^\infty e^{-y}y^r\, dy\geq \int _z^\infty e^{-y}y^r\, dy\geq z^r\int _z^\infty e^{-y}\, dy=z^re^{-z}. \]

Applied to \(z=\pi |x|^2/\delta \) and \(r=(n+1)/2\), this gives

\[ |x|^{n+1}=\delta ^{(n+1)/2}\frac{|x|^{n+1}}{\delta ^{(n+1)/2}}\leq \underbrace{\frac{\Gamma ((n+3)/2)}{\pi ^{(n+1)/2}}}_{=:B}\delta ^{(n+1)/2}e^{\pi |x|^2/\delta }, \]

which is equivalent to the second upper bound of the lemma.

The following technical theorem is used in the proofs of both the inversion formula and Plancherel’s theorem.

Theorem 2.8
#

Let \(f:V\to E\) be integrable. Let \(K_\delta \) be the Weierstrass kernel from Lemma 2.7, or indeed any family of functions satisfying the conditions of Lemma 2.7. Then

\[ (K_\delta \ast f)(x):=\int _V K_\delta (y)f(x-y)\, d\mu (y)\xrightarrow {\delta \to 0}f(x) \]

in the \(L^1\)-norm. If \(f\) is continuous, the convergence also holds pointwise.

Proof

Again we may assume \(V=\mathbb {R}^n\). Consider the difference

\[ \Delta _\delta (x):=(K_\delta \ast f)(x)-f(x)= \int _{\mathbb {R}^n}(f(x-y)-f(x))K_\delta (y)\, dy. \]

We prove \(L^1\)-convergence first: Take \(L^1\)-norms and use Fubini’s theorem to conclude

\[ \| \Delta _\delta \| _1\leq \int _{\mathbb {R}^n}\| f(x-y)-f(x)\| _1K_\delta (y)\, dy. \]

For \(\varepsilon {\gt}0\) find \(\eta {\gt}0\) small enough so that \(\| f(x-y)-f(x)\| _1{\lt}\varepsilon \) when \(|y|\eta \). Thus

\[ \| \Delta _\delta \| _1\leq \varepsilon +\int _{|y|{\gt}\eta }\| f(x-y)-f(x)\| K_\delta (y)\, dy\leq \varepsilon +2\| f\| _1\int _{\| y\| {\gt}\eta }K_\delta (y)\, dy. \]

By one of the properties in Lemma 2.7, we can choose \(\delta \) small enough so that the second integral is less than \(\varepsilon \), which finishes the proof in this case.

Now assume that \(f\) is continuous. Let \(d=\delta ^{1/2}\) and shorten \(g_\delta (x,y)=|f(x-y)-f(x)|K_\delta (y)\).Then

\[ |\Delta _\delta (x)|\leq \int _{0{\lt}|y|{\lt}d}g_\delta (x,y)\, dy+\sum _{k\in \mathbb N}\int _{2^kd{\lt}|y|{\lt}2^{k+1}d}g_\delta (x,y)\, dy. \]

To bound these integrals, consider

\[ \varphi (r)=\frac1{r^n}\int _{|y|{\lt}r}|f(x-y)-f(x)|\, dy. \]

It is easy to see that \(\varphi \) is continuous, bounded, and approaches \(0\) for \(r\to 0\), by continuity of \(f\). Now

\[ \int _{0{\lt}|y|{\lt}d}g_\delta (x,y)\, dy\overset {(\ast )}\leq d^{-n}\int _{0{\lt}|y|{\lt}d}|f(x-y)-f(x)|\, dy=\varphi (d) \]

and

\[ \int _{2^kd{\lt}|y|{\lt}2^{k+1}d}g\, dy\overset {(\ast )}\leq \frac{Bd}{(2^kd)^{n+1}}\int _{2^kd{\lt}|y|{\lt}2^{k+1}d}|f(x-y)-f(x)|\, dy\leq 2^{n-k}B\varphi (2^{k+1}d), \]

where for the inequalities labeled \((\ast )\) we used the upper bounds from Lemma 2.7. Together, we find

\[ |\Delta _\delta (x)|\leq \varphi (d)+C\sum _{k\in \mathbb N}2^{-k}\varphi (2^{k+1}d) \]

for \(C=\frac{2^n\Gamma ((n+3)/2)}{\pi ^{(n+1)/2}}\). Say \(\varphi \) is bounded by \(M\in \mathbb {R}\) and let \(\varepsilon {\gt}0\). Take \(N\) large enough such that \(\sum _{k\geq N}2^{-k}{\lt}\varepsilon \). Choose \(\delta \) small enough that \(A(2^kd){\lt}\varepsilon /N\) for all \(k{\lt}N\). Then

\[ |\Delta _\delta (x)|\leq \varepsilon /N+(N-1)C\varepsilon /N+C\varepsilon M\leq \varepsilon C(M+1). \]
Remark 2.9
#

One can drop the continuity assumption and still get pointwise convergence almost everywhere. The proof stays the same, but one focuses on Lebesgue points of \(f\). It takes slightly more work to argue that \(\varphi \) behaves nicely, but the rest of the proof stays the same.

Theorem 2.10 Inversion formula

Let \(f:V\to E\) be integrable and continuous. Assume \(\widehat f\) is integrable as well. Then

\[ \mathcal F^{-1}\mathcal F f=f. \]
Proof

Apply the multiplication formula Lemma 2.4 to \(u_{x,\delta }\) and \(f\), and conclude with Theorem 2.8.

Remark 2.11
#

Note that both assumptions are necessary, since \(\mathcal F^{-1}\mathcal Ff\) is continuous, and only defined if \(\mathcal Ff\) is integrable.

Theorem 2.12 Inversion formula, \(L^1\)-version

Let \(f\in L^1(V,E)\). If \(\widehat f\in L^1(V,E)\), then \(\mathcal F^{-1}\mathcal Ff=f\).

Proof

Similar to Theorem 2.10.

2.2 Plancherel’s Theorem and the Fourier Transform on \(L^2\)

Let \((V,\cdot )\) be a finite-dimensional inner product space over \(\mathbb {R}\) and let \((E,\langle \cdot ,\cdot \rangle )\) be an inner product space over \(\mathbb {C}\).

Theorem 2.13 Plancherel’s Theorem

Suppose that \(f : V \to E\) is in \(L^1(V,E)\cap L^2(V,E)\) and let \(\widehat{f}\) be the Fourier transform of \(f\). Then \(\widehat{f},\check{f}\in L^2(V,E)\) and

\[ \| \widehat{f}\| _{L^2} = \| f\| _{L^2}=\| \check f\| _{L^2}. \]

Suppose that \(f : V \to E\) is in \(L^1(V,E)\cap L^2(V,E)\) and let \(\widehat{f}\) be the Fourier transform of \(f\). Then \(\widehat{f},\check{f}\in L^2(V,E)\) and

\[ \| \widehat{f}\| _{L^2} = \| f\| _{L^2}=\| \check f\| _{L^2}. \]
Proof

Let \(g(x)=f(-x)\) and apply the multiplication formula Lemma 2.4 to \(f\ast g\) and \(u_{0,\delta }\):

\[ \int _V\widehat{f\ast g}\cdot u_{0,\delta }(x)\, dx=\int _V(f\ast g)(x)K_\delta (-x)\, dx \overset {\delta \to 0}\to (f\ast g)(0)=\int _V \langle f(x),f(x)\rangle \, dx=\| f\| _2^2 \]

by Theorem 2.8. On the other hand, by Lemma 2.5 the left hand side simplifies to

\[ \int _V|\widehat f(x)|^2e^{-\delta \pi |x|^2}\, dx\xrightarrow {\delta \to 0}\| \widehat f\| _2^2 \]

by dominated convergence.

Since \(\check f(x)=\widehat f(-x)\), the corresponding statements for \(\check f\) follow immediately from the ones for \(\widehat f\).

We now want to extend the Fourier transform to \(L^2(V,E)\). For this, take a sequence of functions \((f_n)_n\subset L^1(V,E)\cap L^2(V,E)\) such that \(f_n\xrightarrow [L^2]{}f\). Such sequences exist:

Lemma 2.14
#

\(L^1(V,E)\cap L^2(V,E)\) is dense in \(L^2(V,E)\).

Proof

It is well-known that the space of compactly supported continuous functions is dense in every \(L^p(V,E)\). Since those are contained in \(L^1(V,E)\cap L^2(V,E)\), the claim follows.

Let \(f\in L^2(V,E)\). Plancherel’s theorem lets us now approximate a potential \(\widehat f\):

Lemma 2.15
#

Let \(f\in L^2(V,E)\) and \((f_n)_n\subset L^1(V,E)\cap L^2(V,E)\) a sequence with \(f_n\xrightarrow [L^2]{}f\). Then \((\widehat f_n)_n\) is a Cauchy sequence, hence converges in \(L^2(V,E)\).

Proof
\[ \| \widehat f_n-\widehat f_m\| _2=\| \widehat{f_n-f_m}\| _2\overset {\text{Plancherel}}=\| f_n-f_m\| _2 \]

goes to \(0\) for \(n,m\) large, as \((f_n)_n\) is convergent, hence Cauchy. Since \(L^2(V,E)\) is complete, \((\widehat f_n)_n\) converges.

Definition 2.16
#

Let \(f\in L^2(V,E)\) and take a sequence \((f_n)_n\subset L^1(V,E)\cap L^2(V,E)\) with \(f_n\xrightarrow [L^2]{}f\). Set

\[ \mathcal Ff:=\widehat f:=\lim _{n\to \infty }\widehat{f_n}, \]

the limit taken in the \(L^2\)-sense.

Lemma 2.17
#

This is well-defined: By Lemma 2.15, the limit exists. Further it does not depend on the choice of sequence \((f_n)_n\). If \(f\in L^1(V,E)\cap L^2(V,E)\), this definition agrees with the Fourier transform on \(L^1(V,E)\).

Proof

Let \((g_n)_n\) be another sequence approximating \(f\). Then

\[ \| \widehat f_n-\widehat g_n\| _2=\| f_n-g_n\| \leq \| f_n-f\| +\| g_n-g\| \to 0. \]

If \(f\in L^1(V,E)\cap L^2(V,E)\), we can choose the constant sequence \((f_n)_n=(f)_n\).

Definition 2.18
#

Define analogously \(\mathcal F^{-1}f:=\check f:=\lim _{n\to \infty }\check f_n\), if \(f_n\xrightarrow [L^2]{}f\in L^2(V,E)\) with \((f_n)_n\subset L^1(V,E)\cap L^2(V,E)\). By the same arguments as above, this is well-defined.

Corollary 2.19

Plancherel’s Theorem, the inversion formula, and the properties of Lemma 2.5 hold for the Fourier transform on \(L^2(V,E)\) as well.

Proof

All of these follow immediately from the definition and the observation, that all operations (norms, sums, conjugation, \(\ldots \)) are continuous. For example, let \(f\in L^2(V,E)\) and take an approximating sequence \((f_n)_n\) as before. Then

\[ \| \widehat f\| _2=\| \lim _{n\to \infty }\widehat f_n\| _2=\| \lim _{n\to \infty }\| \widehat f_n\| _2=\lim _{n\to \infty }\| f_n\| _2 =\| \lim _{n\to \infty }f_n\| _2=\| f\| _2. \]
Corollary 2.20

The Fourier transform induces a continuous linear map \(L^2(V,E) \to L^2(V,E)\).

Proof

This follows immediately from Corollary 2.19: Linearity from the \(L^2\)-version of Lemma 2.5, and continuity and well-definedness from the \(L^2\)-version of Plancherel’s theorem.