Poisson summation over a lattice

Let L be a full lattice in a finite-dimensional real inner product space E, with dual lattice L^∨. For a Schwartz function f : 𝓢(E, ℂ) and v : E, Poisson's summation formula reads

∑' ℓ : L, f (v + ℓ) = (covolume L)⁻¹ * ∑' m : L^∨, 𝓕 f m * exp (2πi ⟪v, m⟫)

(SchwartzMap.tsum_eq_tsum_dual_fourier), with Mathlib's Fourier transform 𝓕 f w = ∫ x, exp (-2πi ⟪x, w⟫) f x. Both sides are summable (ZLattice.summable_poisson_left, ZLattice.summable_poisson_right).

The sign of the phase is fixed by this convention for 𝓕. Reindexing the dual side by m ↦ -m reflects the transform as well as the phase, which gives the reflected form ∑' m : L^∨, 𝓕 f (-m) * exp (-2πi ⟪v, m⟫) of the right-hand side for every f. The form ∑' m : L^∨, 𝓕 f m * exp (-2πi ⟪v, m⟫) used in sources with the opposite sign convention for the Fourier transform holds when f is even, such as a Gaussian. Evenness is sufficient, not necessary: the periodization can be even although f is not. For a general f the expression is the formula at -v, so it need not equal the periodization at v.

The base case is the lattice Λ = span ℤ (range o) spanned by an orthonormal basis o, indexed by a finite type ι; for E = EuclideanSpace ℝ ι and the standard basis this is ℤ^ι. It is its own dual (ZLattice.dual_span_orthonormalBasis) and has covolume one, so the formula reads ∑' ℓ : Λ, f (v + ℓ) = ∑' m : Λ, 𝓕 f m * exp (2πi ⟪v, m⟫) (SchwartzMap.tsum_eq_tsum_fourier_span_orthonormalBasis). Its proof is the classical one, in all dimensions at once rather than one coordinate at a time. The periodization P x = ∑' ℓ : Λ, f (x + ℓ) is continuous and Λ-periodic, so it descends to a continuous function on the torus UnitAddTorus ι = (ℝ/ℤ)^ι through the coordinates of o. Its n-th Fourier coefficient is an integral over the fundamental domain D of Λ; unfolding the periodization and reassembling the translates ℓ + D into E (MeasureTheory.IsAddFundamentalDomain.integral_eq_tsum'') shows that this coefficient is the value of 𝓕 f at the lattice point with coordinates n. These coefficients are summable, since 𝓕 f is again a Schwartz function, so the multivariate Fourier series of the periodization converges to it pointwise (UnitAddTorus.hasSum_mFourier_series_apply_of_summable). The one-dimensional case of this argument is Mathlib's Real.tsum_eq_tsum_fourier.

A general full lattice is reduced to the base case by a linear change of variables rather than by induction on the dimension. Every full lattice is the image A Λ of Λ under a linear automorphism A with |det A| = covolume L, and its dual is carried onto Λ by the adjoint of A (ZLattice.exists_comap_span_orthonormalBasis_eq). Applying the base case to f ∘ A and the Fourier change of variables ContinuousLinearEquiv.fourier_comp, which introduces the factor |det A|⁻¹, gives the formula for L.

Main statements

• SchwartzMap.tsum_eq_tsum_fourier_span_orthonormalBasis: Poisson summation over the lattice spanned by an orthonormal basis.
• SchwartzMap.tsum_eq_tsum_dual_fourier: Poisson summation over a full lattice.
• SchwartzMap.tsum_eq_tsum_dual_fourier_neg: its reflected form, for every f.
• SchwartzMap.tsum_eq_tsum_dual_fourier_of_even: the form with phase exp (-2πi ⟪v, m⟫), for even f.

References

• E. M. Stein and G. Weiss, Introduction to Fourier Analysis on Euclidean Spaces, Ch. VII, Corollary 2.6.

The torus of the lattice spanned by o

Measure theory of the coordinates

The periodization of a Schwartz function

The Fourier coefficients of the periodization

Poisson summation

theorem SchwartzMap.tsum_eq_tsum_fourier_span_orthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_2} [Fintype ι] (f : SchwartzMap E ℂ) (o : OrthonormalBasis ι ℝ E) [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (v : E) : ∑' (ℓ : ↥(Submodule.span ℤ (Set.range ⇑o))), f (v + ↑ℓ) = ∑' (m : ↥(Submodule.span ℤ (Set.range ⇑o))), FourierTransform.fourier ⇑f ↑m * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ v ↑m))

Poisson's summation formula over the lattice L spanned by an orthonormal basis o of a finite-dimensional real inner product space: for a Schwartz function f and v : E, ∑' ℓ : L, f (v + ℓ) = ∑' m : L, 𝓕 f m * exp (2πi ⟪v, m⟫). For the standard basis of EuclideanSpace ℝ ι this is Poisson summation over ℤ^ι.

Poisson summation over a full lattice

theorem SchwartzMap.tsum_eq_tsum_dual_fourier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : SchwartzMap E ℂ) (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (v : E) : ∑' (ℓ : ↥L), f (v + ↑ℓ) = (↑(ZLattice.covolume L MeasureTheory.volume))⁻¹ * ∑' (m : ↥(ZLattice.dual L)), FourierTransform.fourier ⇑f ↑m * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ v ↑m))

Poisson's summation formula over a full lattice L of a finite-dimensional real inner product space: for a Schwartz function f and v : E, ∑' ℓ : L, f (v + ℓ) = (covolume L)⁻¹ * ∑' m : L^∨, 𝓕 f m * exp (2πi ⟪v, m⟫). The sign of the phase is the one forced by Mathlib's 𝓕 f w = ∫ x, exp (-2πi ⟪x, w⟫) f x.

theorem SchwartzMap.tsum_eq_tsum_dual_fourier_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : SchwartzMap E ℂ) (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (v : E) : ∑' (ℓ : ↥L), f (v + ↑ℓ) = (↑(ZLattice.covolume L MeasureTheory.volume))⁻¹ * ∑' (m : ↥(ZLattice.dual L)), FourierTransform.fourier (⇑f) (-↑m) * Complex.exp (-(2 * ↑Real.pi * Complex.I * ↑(inner ℝ v ↑m)))

Poisson's summation formula in reflected form: reindexing the dual side by m ↦ -m reflects both the Fourier transform and the phase, ∑' ℓ : L, f (v + ℓ) = (covolume L)⁻¹ * ∑' m : L^∨, 𝓕 f (-m) * exp (-2πi ⟪v, m⟫).

theorem SchwartzMap.tsum_eq_tsum_dual_fourier_of_even {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : SchwartzMap E ℂ) (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (hf : ∀ (x : E), f (-x) = f x) (v : E) : ∑' (ℓ : ↥L), f (v + ↑ℓ) = (↑(ZLattice.covolume L MeasureTheory.volume))⁻¹ * ∑' (m : ↥(ZLattice.dual L)), FourierTransform.fourier ⇑f ↑m * Complex.exp (-(2 * ↑Real.pi * Complex.I * ↑(inner ℝ v ↑m)))

Poisson's summation formula with the phase exp (-2πi ⟪v, m⟫), for an even Schwartz function f: ∑' ℓ : L, f (v + ℓ) = (covolume L)⁻¹ * ∑' m : L^∨, 𝓕 f m * exp (-2πi ⟪v, m⟫). Evenness is a sufficient hypothesis. In general the right-hand side is ∑' ℓ : L, f (-v + ℓ), by SchwartzMap.tsum_eq_tsum_dual_fourier at -v, so equality holds whenever the periodization is even and need not hold for an arbitrary f.