Exponential lattice series

For a positive decay rate a, the two-sided exponential is summable over the integers, and its sum equals (1 + exp (-a)) / (1 - exp (-a)). The analogous one-sided positive tail is an ordinary geometric series.

Provenance

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

theorem TauCeti.tsum_nat_exp_neg_mul_add_one {a : ℝ} (ha : 0 < a) : ∑' (n : ℕ), Real.exp (-(a * ↑(n + 1))) = Real.exp (-a) / (1 - Real.exp (-a))

The positive tail of a geometric exponential series.

theorem TauCeti.summable_exp_neg_mul_abs_int {a : ℝ} (ha : 0 < a) : Summable fun (n : ℤ) => Real.exp (-(a * |↑n|))

The two-sided exponential with positive rate is summable on the integer lattice.

theorem TauCeti.tsum_int_exp_neg_mul_abs {a : ℝ} (ha : 0 < a) : ∑' (n : ℤ), Real.exp (-(a * |↑n|)) = (1 + Real.exp (-a)) / (1 - Real.exp (-a))

The two-sided geometric lattice sum of a decaying exponential.