Gaussian and power sums over lattices converge

Let E be a finite-dimensional real normed space and L a discrete ℤ-submodule of E. For 0 < c and any x : E, the Gaussian v ↦ exp (-c ‖x + v‖²) is summable over L (ZLattice.summable_exp_neg_mul_norm_add_sq).

The proof compares the Gaussian with the power ‖x + v‖ ^ r for r < -rank L, whose sum over L converges by Mathlib's ZLattice.summable_norm_sub_rpow: the Gaussian decays faster than every power, and ‖x + v‖ → ∞ along the cofinite filter of L because L is discrete and closed.

This is the majorant behind the convergence of the theta series of a lattice, a sum of exp (π i ‖x + v‖² τ) over L whose terms have norm exp (-π ‖x + v‖² im τ).

For the standard lattice ℤ^d, read with the sup norm on d → ℤ, the power sum ∑ n, ‖n‖ ^ r converges for r < -card d (TauCeti.summable_pi_int_norm_rpow). This is the majorant used to sum Fourier coefficients on the torus (ℝ / ℤ)^d.

Main statements

• ZLattice.summable_exp_neg_mul_norm_add_sq: ∑ v ∈ L, exp (-c ‖x + v‖²) converges for 0 < c.
• ZLattice.discreteTopology_of_summable_exp_neg_mul_norm_add_sq: the converse, a subgroup L of a normed group over which some Gaussian v ↦ exp (-c ‖x + v‖²), 0 < c, is summable is discrete.
• ZLattice.summable_one_add_norm_pow_inv: ∑ ℓ ∈ L, (1 + ‖ℓ‖) ^ (-r) converges once the natural number r exceeds the rank of L.
• TauCeti.summable_pi_int_norm_rpow: ∑ n : d → ℤ, ‖n‖ ^ r converges for r < -card d.
• TauCeti.summable_pi_int_inv_one_add_norm_pow: ∑ n : d → ℤ, (1 + ‖n‖) ^ (-(card d + 1)) converges.

theorem ZLattice.discreteTopology_of_summable_exp_neg_mul_norm_add_sq {E : Type u_1} [NormedAddCommGroup E] (L : Submodule ℤ E) (γ : E) {c : ℝ} (hc : 0 < c) (h : Summable fun (v : ↥L) => Real.exp (-c * ‖γ + ↑v‖ ^ 2)) : DiscreteTopology ↥L

If the Gaussian exp (-c ‖γ + v‖²), c > 0, is summable over a subgroup L of a normed group, then L is discrete: only finitely many v ∈ L have ‖γ + v‖ bounded.

theorem ZLattice.summable_exp_neg_mul_norm_add_sq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {c : ℝ} (hc : 0 < c) (x : E) : Summable fun (v : ↥L) => Real.exp (-c * ‖x + ↑v‖ ^ 2)

For 0 < c, the Gaussian v ↦ exp (-c ‖x + v‖²) is summable over a discrete subgroup L of a finite-dimensional real normed space, for every centre -x.

theorem ZLattice.summable_one_add_norm_pow_inv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {r : ℕ} (hr : Module.finrank ℤ ↥L < r) : Summable fun (ℓ : ↥L) => ((1 + ‖↑ℓ‖) ^ r)⁻¹

On a discrete subgroup L of a finite-dimensional real normed space, (1 + ‖ℓ‖) ^ (-r) is summable as soon as r exceeds the rank of L.

theorem TauCeti.summable_pi_int_norm_rpow {d : Type u_1} [Fintype d] (r : ℝ) (hr : r < -↑(Fintype.card d)) : Summable fun (n : d → ℤ) => ‖n‖ ^ r

The sup norms of the integer vectors n : d → ℤ satisfy ∑ n, ‖n‖ ^ r < ∞ when r < -card d. Here ‖0‖ ^ r = 0.

theorem TauCeti.summable_pi_int_inv_one_add_norm_pow {d : Type u_1} [Fintype d] : Summable fun (n : d → ℤ) => ((1 + ‖n‖) ^ (Fintype.card d + 1))⁻¹

The series ∑ n, (1 + ‖n‖) ^ (-(card d + 1)) over the integer vectors n : d → ℤ, with the sup norm, converges.