5. Fourier Analysis
Recall the definition of a Fourier transform.
-
VectorFourier.fourierIntegral[complete]
The Fourier transform of an L^1-function f:\R^d\to\C is defined as
\mathcal{F}(f)(y) = \widehat{f}(y) := \int_{\R^d} f(x)e^{-2\pi i \langle x, y \rangle} \,\mathrm{d}x, \quad y \in \R^d
where
\langle x, y \rangle = \frac12\|x\|^2 + \frac12\|y\|^2 - \frac12\|x - y\|^2
is the standard scalar product in \R^d.
Lean code for Definition5.1●1 definition
Associated Lean declarations
-
VectorFourier.fourierIntegral[complete]
-
VectorFourier.fourierIntegral[complete]
-
defdefined in Mathlib/Analysis/Fourier/FourierTransform.leancomplete
def VectorFourier.fourierIntegral.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (w : W) : E
def VectorFourier.fourierIntegral.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} [CommRing 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [MeasurableSpace V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (w : W) : E
The Fourier transform integral for `f : V → E`, with respect to a bilinear form `L : V × W → 𝕜` and an additive character `e`.
The following computational result will be of use later on.
- No associated Lean code or declarations.
\mathcal{F}(e^{\pi i \|x\|^2 z})(y) = z^{-4}\,e^{\pi i \|y\|^2 \,(\frac{-1}{z}) }.
Fill in proof.
Of great interest to us is 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.
-
BlueprintDocAliases.SchwartzMap[complete]
A C^\infty function f:\R^d\to\C is called a Schwartz function if it
decays to zero as \|x\|\to\infty faster than any inverse power of
\|x\|, and the same holds for all partial derivatives of f. That is,
for all k, n \in \N, there exists a constant C \in \R such that for
all x \in \R^d,
\norm{x}^k \cdot \norm{f^{(n)}(x)} \leq C,
where f^{(n)} denotes the n-th derivative of f together with the
appropriate operator norm. The set of all Schwartz functions from \R^d to
\C is called the Schwartz space. It is an \R-vector space.
Lean code for Definition5.3●1 definition
Associated Lean declarations
-
BlueprintDocAliases.SchwartzMap[complete]
-
BlueprintDocAliases.SchwartzMap[complete]
-
abbrevdefined in SpherePackingBlueprint/Formalization.leancomplete
abbrev BlueprintDocAliases.SchwartzMap.{u_1, u_2} (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : Type (max u_1 u_2)
abbrev BlueprintDocAliases.SchwartzMap.{u_1, u_2} (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : Type (max u_1 u_2)
The space of Schwartz functions.
-
SchwartzMap.fourierTransformCLM[complete]
The Fourier transform is a continuous linear automorphism of the space of Schwartz functions.
Lean code for Lemma5.4●1 definition
Associated Lean declarations
-
SchwartzMap.fourierTransformCLM[complete]
-
SchwartzMap.fourierTransformCLM[complete]
-
defdefined in Mathlib/Analysis/Distribution/SchwartzSpace/Fourier.leancomplete
def SchwartzMap.fourierTransformCLM.{u_1, u_2, u_3} (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : SchwartzMap V E →L[𝕜] SchwartzMap V E
def SchwartzMap.fourierTransformCLM.{u_1, u_2, u_3} (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : SchwartzMap V E →L[𝕜] SchwartzMap V E
The Fourier transform on a real inner product space, as a continuous linear map on the Schwartz space. This definition is only to define the Fourier transform, use `FourierTransform.fourierCLM` instead.
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. The proof that
for any Schwartz function f, its Fourier transform and its image under this
continuous linear equivalence are the same \R^d \to \R function is stated
in Mathlib solely for the purpose of rw and simp, and is proved simply by
rfl.
Another reason we are interested in Schwartz functions is that they behave well under infinite sums. This will be useful when proving the Cohn-Elkies linear programming bound.
We begin by stating a general summability result over specific subsets of
\R^d.
- No associated Lean code or declarations.
Let X \subset \R^d be a set of sphere-packing centers of separation 1
that is periodic with some lattice \Lambda \subset \R^d. Then there exists
k \in \N sufficiently large such that
\sum_{x \in X} \frac{1}{\norm{x}^{k}} < \infty.
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 is to bound the
sequence of partial sums by considering the volumes of concentric d-spheres
of the appropriate radii, or scaled versions of a zero-centered fundamental
domain.
/- source paragraph break -/
Finish.
The decaying property of Schwartz functions means that they can be compared with the absolutely convergent power series above.
Let f : \R^d \to \C be a Schwartz function and let
X \subset \R^d be periodic with respect to some lattice
\Lambda \subset \R^d. Then
\sum_{x \in X} |f(x)| < \infty.
Without loss of generality, assume that 0 \notin X: if 0 \in X, we
can add the f(0) term to the sum over nonzero elements of X. We know
that for all k \in \N there exists some constant C such that
|f(x)| \leq C\norm{x}^{-k} for all x \in \R^d.
Choosing k to be sufficiently large, we obtain
\sum_{x \in X} |f(x)| \leq \sum_{x \in X} \frac{C}{\norm{x}^{k}} = C \sum_{x \in X} \frac{1}{\norm{x}^k} < \infty.
We end with a crucial result on Schwartz functions, the statement of which only makes sense because of the above result.
-
SchwartzMap.PoissonSummation_Lattices[sorry in proof]
Let \Lambda be a lattice in \R^d, and let f:\R^d\to\R be a
Schwartz function. Then, for all v \in \R^d,
\sum_{\ell\in\Lambda}f(\ell + v) = \frac{1}{\Vol{\R^d/\Lambda}} \sum_{m\in\Lambda^*}\widehat{f}(m) e^{-2\pi i \ang{v, m}}.
Lean code for Theorem5.7●1 theorem, incomplete
Associated Lean declarations
-
SchwartzMap.PoissonSummation_Lattices[sorry in proof]
-
SchwartzMap.PoissonSummation_Lattices[sorry in proof]
-
theoremdefined in SpherePacking/CohnElkies/Prereqs.leancontains sorry
theorem SchwartzMap.PoissonSummation_Lattices {d : ℕ} [Fact (0 < d)] (Λ : Submodule ℤ (EuclideanSpace ℝ (Fin d))) [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] (f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) (v : EuclideanSpace ℝ (Fin d)) : ∑' (ℓ : ↥Λ), f (v + ↑ℓ) = 1 / ↑(ZLattice.covolume Λ MeasureTheory.volume) * ∑' (m : ↥(LinearMap.BilinForm.dualSubmodule (innerₗ (EuclideanSpace ℝ (Fin d))) Λ)), FourierTransform.fourier ⇑f ↑m * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(RCLike.wInner 1 v.ofLp (↑m).ofLp))
theorem SchwartzMap.PoissonSummation_Lattices {d : ℕ} [Fact (0 < d)] (Λ : Submodule ℤ (EuclideanSpace ℝ (Fin d))) [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] (f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) (v : EuclideanSpace ℝ (Fin d)) : ∑' (ℓ : ↥Λ), f (v + ↑ℓ) = 1 / ↑(ZLattice.covolume Λ MeasureTheory.volume) * ∑' (m : ↥(LinearMap.BilinForm.dualSubmodule (innerₗ (EuclideanSpace ℝ (Fin d))) Λ)), FourierTransform.fourier ⇑f ↑m * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(RCLike.wInner 1 v.ofLp (↑m).ofLp))
One possible proof would be by induction on d. However, there are numerous
nuances involved, particularly in manipulating nested infinite sums. Ideas
would be appreciated.
While the Poisson summation formula over lattices can be stated in greater generality and probably should be formalised as such in Mathlib due to its many applications, we stick with Schwartz functions because that should be sufficient for our purposes.
- No associated Lean code or declarations.
Assume f : \R \to \C is smooth on [0, \infty) and for all
k, n \in \N there exists C \in \R such that
x^{\frac{k}{2}} \cdot |f^{(n)}(x)| \leq C.
Then, for all d \in \N, the function
f_d : \R^d \to \C, \quad f_d(x) := f(\|x\|^2)
is a Schwartz function.