Poisson summation for the Cauchy kernel

For y > 0, Poisson summation identifies the two-sided exponential lattice sum with the lattice sum of its Cauchy Fourier transform. Combined with the geometric lattice series, this evaluates the full Cauchy lattice sum.

Main results

• TauCeti.tsum_exp_neg_mul_abs_int_eq_tsum_div: the real-valued Poisson identity.
• TauCeti.tsum_int_inv_sq_add_sq: the Cauchy lattice sum in exponential form.

Provenance

Adapted from ForTauCeti/Analysis/Fourier/Poisson/CauchyLattice.lean in AIQ-Kitware/aiq-dkps-formalization (Apache-2.0; Jon Crall and GPT 5.6 High).

theorem TauCeti.tsum_exp_neg_mul_abs_int_eq_tsum_div {y : ℝ} (hy : 0 < y) : ∑' (n : ℤ), Real.exp (-(2 * Real.pi * y * |↑n|)) = ∑' (n : ℤ), y / (Real.pi * (y ^ 2 + ↑n ^ 2))

Real Cauchy Poisson identity. For y > 0, the sum over integers of exp (-2π y |n|) equals the sum of y / (π (y² + n²)).

theorem TauCeti.tsum_int_inv_sq_add_sq {y : ℝ} (hy : 0 < y) : ∑' (n : ℤ), (y ^ 2 + ↑n ^ 2)⁻¹ = Real.pi / y * ((1 + Real.exp (-(2 * Real.pi * y))) / (1 - Real.exp (-(2 * Real.pi * y))))

Cauchy lattice sum. For y > 0, the sum over integers of 1 / (y² + n²) equals (π / y) * (1 + exp (-2πy)) / (1 - exp (-2πy)).