Gaussian lattice sums

This file defines the Gaussian lattice sum Z(c, s) = ∑ n : ℤ, exp (-(n - c) ^ 2 / (2 * s ^ 2)) and develops its elementary theory for a centre c : ℝ and a nonzero width s : ℝ.

The sum Z(c, s) is the normalizing constant of the discrete Gaussian law on ℤ with centre c and width s, whose masses are exp (-(n - c) ^ 2 / (2 * s ^ 2)) / Z(c, s). The moments of that law are polynomially weighted lattice sums, and are obtained by differentiating Z(c, s) in the centre c.

Main declarations

• Real.gaussianLatticeSum — the Gaussian lattice sum Z(c, s).
• Real.hasSum_gaussianLatticeSum and Real.gaussianLatticeSum_pos — convergence and positivity for s ≠ 0; Real.gaussianLatticeSum_zero_right records the totalized value 0 at s = 0.
• Real.summable_pow_mul_exp_neg_sub_sq — convergence of the lattice sums with polynomial weights; Real.summable_abs_pow_mul_exp_neg_sub_sq_div is the absolute version for any positive denominator, as used for domination arguments.
• Real.gaussianLatticeSum_add_intCast, Real.gaussianLatticeSum_periodic, Real.gaussianLatticeSum_neg_left and Real.gaussianLatticeSum_intCast_sub — invariance under integer translations and reflections of the centre.
• Real.gaussianLatticeSum_eq_jacobiTheta₂ — the expression Z(c, s) = exp (-c ^ 2 / (2 * s ^ 2)) * Re (θ(-i c / (2π s ^ 2), i / (2π s ^ 2))) through Mathlib's two-variable Jacobi theta function jacobiTheta₂.
• Real.hasDerivAt_tsum_pow_mul_exp_neg_sub_sq and Real.hasDerivAt_gaussianLatticeSum — termwise differentiation in the centre of the lattice sums with weight n ^ k.
• Real.contDiff_gaussianLatticeSum, Real.continuousAt_gaussianLatticeSum and Real.measurable_gaussianLatticeSum — analyticity in the centre, joint continuity on s ≠ 0, and joint measurability.

References

• C. L. Canonne, G. Kamath and T. Steinke, The Discrete Gaussian for Differential Privacy, 2020, arXiv:2004.00010.

noncomputable def Real.gaussianLatticeSum (c s : ℝ) : ℝ

The Gaussian lattice sum Z(c, s) = ∑ n : ℤ, exp (-(n - c) ^ 2 / (2 * s ^ 2)) with centre c and width s.

The series converges exactly when s ≠ 0; at s = 0 every term is 1, so the totalized sum is 0 (see Real.gaussianLatticeSum_zero_right).

theorem Real.gaussianLatticeSum_def (c s : ℝ) : c.gaussianLatticeSum s = ∑' (n : ℤ), exp (-(↑n - c) ^ 2 / (2 * s ^ 2))

theorem Real.summable_abs_pow_mul_exp_neg_sub_sq_div (k : ℕ) (c : ℝ) {b : ℝ} (hb : 0 < b) : Summable fun (n : ℤ) => |↑n| ^ k * exp (-(↑n - c) ^ 2 / b)

Gaussian lattice sums with absolute polynomial weights converge, by comparison with the bound used for the terms of jacobiTheta₂.

theorem Real.summable_pow_mul_exp_neg_sub_sq (k : ℕ) (c : ℝ) {s : ℝ} (hs : s ≠ 0) : Summable fun (n : ℤ) => ↑n ^ k * exp (-(↑n - c) ^ 2 / (2 * s ^ 2))

Gaussian lattice sums with polynomial weights n ^ k converge for every nonzero width.

theorem Real.hasSum_gaussianLatticeSum (c : ℝ) {s : ℝ} (hs : s ≠ 0) : HasSum (fun (n : ℤ) => exp (-(↑n - c) ^ 2 / (2 * s ^ 2))) (c.gaussianLatticeSum s)

For a nonzero width, the Gaussian lattice series converges to gaussianLatticeSum c s.

@[simp]

theorem Real.gaussianLatticeSum_zero_right (c : ℝ) : c.gaussianLatticeSum 0 = 0

At width zero every term of the Gaussian lattice series is 1, so the totalized sum is 0.

theorem Real.gaussianLatticeSum_pos (c : ℝ) {s : ℝ} (hs : s ≠ 0) : 0 < c.gaussianLatticeSum s

For a nonzero width the Gaussian lattice sum is positive.

@[simp]

theorem Real.gaussianLatticeSum_neg_right (c s : ℝ) : c.gaussianLatticeSum (-s) = c.gaussianLatticeSum s

The Gaussian lattice sum depends on the width only through its square.

@[simp]

theorem Real.gaussianLatticeSum_add_intCast (c : ℝ) (k : ℤ) (s : ℝ) : (c + ↑k).gaussianLatticeSum s = c.gaussianLatticeSum s

The Gaussian lattice sum is invariant under integer translations of the centre.

theorem Real.gaussianLatticeSum_periodic (s : ℝ) : Function.Periodic (fun (c : ℝ) => c.gaussianLatticeSum s) 1

The Gaussian lattice sum is 1-periodic in the centre.

@[simp]

theorem Real.gaussianLatticeSum_neg_left (c s : ℝ) : (-c).gaussianLatticeSum s = c.gaussianLatticeSum s

The Gaussian lattice sum is even in the centre.

@[simp]

theorem Real.gaussianLatticeSum_intCast_sub (k : ℤ) (c s : ℝ) : (↑k - c).gaussianLatticeSum s = c.gaussianLatticeSum s

The Gaussian lattice sum is invariant under the reflection c ↦ k - c for every integer k.

theorem Real.gaussianLatticeSum_eq_jacobiTheta₂ (c s : ℝ) : c.gaussianLatticeSum s = exp (-c ^ 2 / (2 * s ^ 2)) * (jacobiTheta₂ (-Complex.I * ↑c / (2 * ↑Real.pi * ↑s ^ 2)) (Complex.I / (2 * ↑Real.pi * ↑s ^ 2))).re

Theta-function expression of the Gaussian lattice sum: Z(c, s) = exp (-c ^ 2 / (2 * s ^ 2)) * Re (θ(-i c / (2π s ^ 2), i / (2π s ^ 2))), where θ is Mathlib's two-variable Jacobi theta function jacobiTheta₂.

At s = 0 both sides vanish.

theorem Real.hasDerivAt_tsum_pow_mul_exp_neg_sub_sq (k : ℕ) (c s : ℝ) : HasDerivAt (fun (x : ℝ) => ∑' (n : ℤ), ↑n ^ k * exp (-(↑n - x) ^ 2 / (2 * s ^ 2))) (∑' (n : ℤ), ↑n ^ k * ((↑n - c) / s ^ 2 * exp (-(↑n - c) ^ 2 / (2 * s ^ 2)))) c

Termwise differentiation of weighted Gaussian lattice sums: for every natural weight exponent k and every width s, the derivative in the centre of x ↦ ∑ n : ℤ, n ^ k * exp (-(n - x) ^ 2 / (2 * s ^ 2)) is the sum of the termwise derivatives. At width zero the function is constant and every termwise derivative is 0.

theorem Real.hasDerivAt_gaussianLatticeSum (c s : ℝ) : HasDerivAt (fun (x : ℝ) => x.gaussianLatticeSum s) (∑' (n : ℤ), (↑n - c) / s ^ 2 * exp (-(↑n - c) ^ 2 / (2 * s ^ 2))) c

The derivative of the Gaussian lattice sum in the centre, computed termwise.

theorem Real.contDiff_gaussianLatticeSum (s : ℝ) {n : WithTop ℕ∞} : ContDiff ℝ n fun (c : ℝ) => c.gaussianLatticeSum s

The Gaussian lattice sum is analytic, in particular smooth, in the centre.

theorem Real.continuousAt_gaussianLatticeSum (c : ℝ) {s : ℝ} (hs : s ≠ 0) : ContinuousAt (fun (p : ℝ × ℝ) => p.1.gaussianLatticeSum p.2) (c, s)

The Gaussian lattice sum is jointly continuous in the centre and the width at every nonzero width.

theorem Real.measurable_gaussianLatticeSum : Measurable fun (p : ℝ × ℝ) => p.1.gaussianLatticeSum p.2

The Gaussian lattice sum is jointly measurable in the centre and the width.