Poisson summation for Gaussian lattice sums

This file rewrites the shifted Gaussian lattice sum as its Fourier series. The identity is the Poisson summation formula for a translated Gaussian and is the analytic bridge from Real.gaussianLatticeSum to periodized Gaussian densities.

For every width s,

Z(c, s) = sqrt (2 * pi) * |s| * sum n, exp (-2 * pi^2 * s^2 * n^2) * cos (2 * pi * n * c).

The Fourier series converges absolutely, and uniformly in the centre c. Splitting the integer sum into its zero term and paired positive and negative terms gives the corresponding one-sided cosine series used for wrapped normal densities. The proof specializes Mathlib's Complex.tsum_exp_neg_quadratic.

References

• K. V. Mardia and P. E. Jupp, Directional Statistics, Wiley, 2000, section 3.5.

theorem Real.summable_gaussianLatticeFourier (c : ℝ) {s : ℝ} (hs : s ≠ 0) : Summable fun (n : ℤ) => exp (-2 * Real.pi ^ 2 * s ^ 2 * ↑n ^ 2) * cos (2 * Real.pi * ↑n * c)

The real cosine series in the Gaussian Poisson summation formula is absolutely summable for every nonzero width.

theorem Real.gaussianLatticeSum_eq_fourier (c s : ℝ) : c.gaussianLatticeSum s = √(2 * Real.pi) * |s| * ∑' (n : ℤ), exp (-2 * Real.pi ^ 2 * s ^ 2 * ↑n ^ 2) * cos (2 * Real.pi * ↑n * c)

Poisson summation for the Gaussian lattice sum. Z(c, s) is the absolutely convergent Fourier series with coefficients sqrt (2π) |s| exp (-2π²s²n²).

theorem Real.hasSum_gaussianLatticeFourier (c s : ℝ) : HasSum (fun (n : ℤ) => √(2 * Real.pi) * |s| * exp (-2 * Real.pi ^ 2 * s ^ 2 * ↑n ^ 2) * cos (2 * Real.pi * ↑n * c)) (c.gaussianLatticeSum s)

The Gaussian Poisson formula as a HasSum statement: the Fourier series with coefficients sqrt (2π) |s| exp (-2π²s²n²) sums to Z(c, s).

theorem Real.hasSumUniformly_gaussianLatticeFourier (s : ℝ) : HasSumUniformly (fun (n : ℤ) (c : ℝ) => √(2 * Real.pi) * |s| * exp (-2 * Real.pi ^ 2 * s ^ 2 * ↑n ^ 2) * cos (2 * Real.pi * ↑n * c)) fun (c : ℝ) => c.gaussianLatticeSum s

The Fourier series of the Gaussian lattice sum converges to Z(c, s) uniformly in the centre c.

theorem Real.gaussianLatticeSum_eq_cosineSeries (c s : ℝ) : c.gaussianLatticeSum s = √(2 * Real.pi) * |s| * (1 + 2 * ∑' (n : ℕ), exp (-2 * Real.pi ^ 2 * s ^ 2 * (↑n + 1) ^ 2) * cos (2 * Real.pi * (↑n + 1) * c))

The Gaussian Poisson formula with the zero mode separated and the positive and negative frequencies paired. This is the usual one-sided cosine-series form.

theorem Real.hasSum_gaussianLatticeCosineSeries (c s : ℝ) : HasSum (fun (n : ℕ) => 2 * √(2 * Real.pi) * |s| * exp (-2 * Real.pi ^ 2 * s ^ 2 * (↑n + 1) ^ 2) * cos (2 * Real.pi * (↑n + 1) * c)) (c.gaussianLatticeSum s - √(2 * Real.pi) * |s|)

The one-sided cosine series of the Gaussian lattice sum: its positive frequencies, doubled and scaled by sqrt (2π) |s|, sum to Z(c, s) minus the zero mode.

theorem Real.hasSumUniformly_gaussianLatticeCosineSeries (s : ℝ) : HasSumUniformly (fun (n : ℕ) (c : ℝ) => 2 * √(2 * Real.pi) * |s| * exp (-2 * Real.pi ^ 2 * s ^ 2 * (↑n + 1) ^ 2) * cos (2 * Real.pi * (↑n + 1) * c)) fun (c : ℝ) => c.gaussianLatticeSum s - √(2 * Real.pi) * |s|

The one-sided cosine series of the Gaussian lattice sum converges uniformly in the centre.