2.2. Poisson summation🔗

Theorem2.2.1

Statement uses 2

Statement dependency previews

Preview

Definition 1.1.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Let \Lambda \subseteq \mathbb{R}^d be a lattice with polar lattice \Lambda^* (Definition 2.1.5), let f be a complex Schwartz function on \mathbb{R}^d, and let v \in \mathbb{R}^d. Then, with the Fourier transform of Definition 1.1.2, \displaystyle\sum_{\lambda \in \Lambda} f(v + \lambda) = \frac{1}{\operatorname{covol}(\Lambda)}\sum_{m \in \Lambda^*}\widehat f(m)\,\mathbf{e}_m(v), \mathbf{e}_m(v) = e^{2\pi i\langle v, m\rangle},, both series converging absolutely.

Lean code for Theorem2.2.1●1 theorem

theoremdefined in CohnElkiesForMathlib/Analysis/Fourier/PoissonSummation.lean

complete

theorem SchwartzMap.latticePoissonSummationFormula {d : ℕ}
  (Λ : Submodule ℤ (EuclideanSpace ℝ (Fin d))) [DiscreteTopology ↥Λ]
  [IsZLattice ℝ Λ] (f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ)
  (v : EuclideanSpace ℝ (Fin d)) :
  ∑' (ℓ : ↥Λ), f (v + ↑ℓ) =
    1 / ↑(ZLattice.covolume Λ MeasureTheory.volume) *
      ∑' (m : ↥(SchwartzMap.polarIntegerLattice Λ)),
        FourierTransform.fourier ⇑f ↑m *
          Complex.exp
            (2 * ↑Real.pi * Complex.I * ↑⟪v.ofLp, (↑m).ofLp⟫_[ℝ])

theorem SchwartzMap.latticePoissonSummationFormula
  {d : ℕ}
  (Λ :
    Submodule ℤ
      (EuclideanSpace ℝ (Fin d)))
  [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ]
  (f :
    SchwartzMap (EuclideanSpace ℝ (Fin d))
      ℂ)
  (v : EuclideanSpace ℝ (Fin d)) :
  ∑' (ℓ : ↥Λ), f (v + ↑ℓ) =
    1 /
        ↑(ZLattice.covolume Λ
            MeasureTheory.volume) *
      ∑' (m :
        ↥(SchwartzMap.polarIntegerLattice
            Λ)),
        FourierTransform.fourier ⇑f ↑m *
          Complex.exp
            (2 * ↑Real.pi * Complex.I *
              ↑⟪v.ofLp, (↑m).ofLp⟫_[ℝ])

**Poisson summation** over a lattice `Λ ⊆ ℝ^d`: the sum of a Schwartz function over the
translated lattice `v + Λ` equals `(covolume Λ)⁻¹` times the sum of `𝓕 f` twisted by
`exp (2πi⟪v, ·⟫)` over the polar lattice of `Λ`.

Proof for Theorem 2.2.1

uses 1

Standard lattice. The periodization v \mapsto \sum_{n\in\mathbb{Z}^d} f(v+n) (SchwartzMap.PoissonSummation.Standard.periodization) converges locally uniformly by the Schwartz decay of f (summable_norm_restrict_translate) and descends to a continuous function on the torus (\mathbb{R}/\mathbb{Z})^d (torusPeriodization). Its Fourier coefficient at n \in \mathbb{Z}^d is \widehat f(n): unfold the sum over the lattice into an integral over \mathbb{R}^d of f(x)e^{-2\pi i\langle x,n\rangle} (mFourierCoeff_torusPeriodization). These coefficients are absolutely summable (summable_mFourierCoeff_torusPeriodization), because \widehat f is again Schwartz, so the Fourier series of the periodization converges uniformly and, the periodization being continuous, converges to it (Mathlib's Fourier inversion on the torus). Evaluating at v gives the formula for \mathbb{Z}^d, which is self-polar.

General lattice. Let A be the coordinate automorphism of Lemma 2.1.6 and put g = f \circ A (SchwartzMap.latticePullback), a Schwartz function. Then \sum_{\lambda\in\Lambda} f(v+\lambda) = \sum_{n\in\mathbb{Z}^d} g(A^{-1}v + n), and the change of variables \widehat{g}(w) = |\det A|^{-1}\widehat f((A^{-1})^*w) ( Real.fourier_comp_linearEquiv', SchwartzMap.fourier_latticePullback) together with (A^{-1})^*\mathbb{Z}^d = \Lambda^*, |\det A| = \operatorname{covol}(\Lambda) and \langle A^{-1}v, n\rangle = \langle v, (A^{-1})^*n\rangle (wInner_latticeCoordinateEquiv_symm) turns the \mathbb{Z}^d-formula for g into the formula for f.