English
For t > 0 and a ∈ ℝ, the sum over n ≠ 0 of e^{2π i a n} e^{-π n^2 t} equals cosKernel(a,t) − 1.
Русский
Пусть t > 0 и a ∈ ℝ. Ряд по целым n, исключая n = 0: e^{2π i a n} e^{-π n^2 t} равен cosKernel(a,t) − 1.
LaTeX
$$$$ \\sum_{n \\in \\mathbb{Z}, \\; n \\neq 0} e^{2\\\\pi i a n} \\\\; e^{-\\\\pi n^2 t} \\\\;=\; \\cosKernel(a,t) - 1 \\\\quad (t>0).$$$$
Lean4
/-- Modified version of `hasSum_int_evenKernel` omitting the constant term at `∞`. -/
theorem hasSum_int_evenKernel₀ (a : ℝ) {t : ℝ} (ht : 0 < t) :
HasSum (fun n : ℤ ↦ if n + a = 0 then 0 else rexp (-π * (n + a) ^ 2 * t))
(evenKernel a t - if (a : UnitAddCircle) = 0 then 1 else 0) :=
by
haveI := Classical.propDecidable
simp_rw [AddCircle.coe_eq_zero_iff, zsmul_one]
split_ifs with h
· obtain ⟨k, rfl⟩ := h
simpa [← Int.cast_add, add_eq_zero_iff_eq_neg] using hasSum_ite_sub_hasSum (hasSum_int_evenKernel (k : ℝ) ht) (-k)
· suffices ∀ (n : ℤ), n + a ≠ 0 by simpa [this] using hasSum_int_evenKernel a ht
contrapose! h
let ⟨n, hn⟩ := h
exact ⟨-n, by simpa [neg_eq_iff_add_eq_zero]⟩
