English
For any a ∈ ℝ and t > 0, the series over integers n of e^{2π i a n} e^{-π n^2 t} equals cosKernel a t (as a real number, viewed in ℂ).
Русский
Пусть a ∈ ℝ и t > 0. Ряд по целым n: e^{2π i a n} e^{-π n^2 t} сходится к cosKernel(a,t) (как действительное число, рассматриваемое в ℂ).
LaTeX
$$$$ \\sum_{n \\in \\mathbb{Z}} e^{2\\\\pi i a n} \\, e^{-\\\\pi n^2 t} \\\\;=\; \\cosKernel(a,t) \\\\quad (t>0).$$$$
Lean4
theorem hasSum_int_cosKernel (a : ℝ) {t : ℝ} (ht : 0 < t) :
HasSum (fun n : ℤ ↦ cexp (2 * π * I * a * n) * rexp (-π * n ^ 2 * t)) ↑(cosKernel a t) :=
by
rw [cosKernel_def a t]
have (n : ℤ) : cexp (2 * π * I * a * n) * cexp (-(π * n ^ 2 * t)) = jacobiTheta₂_term n a (I * ↑t) :=
by
rw [jacobiTheta₂_term, ← Complex.exp_add]
ring_nf
simp [sub_eq_add_neg]
simpa [this] using hasSum_jacobiTheta₂_term _ (by simpa)
