hasSum_int_evenKernel — Mathlib

English

For any real a and t > 0, the series over all integers n of exp(-π (n + a)^2 t) equals the evenKernel a t.

Русский

Пусть a ∈ ℝ и t > 0. Ряд по целым n: e^{-π (n + a)^2 t} сходится к значению evenKernel(a, t).

LaTeX

$$$$ \\sum_{n \\in \\mathbb{Z}} e^{-\\\\pi (n + a)^2 t} \\\\;=\; \\operatorname{evenKernel}(a,t) \\\\quad (t>0).$$$$

Lean4

theorem hasSum_int_evenKernel (a : ℝ) {t : ℝ} (ht : 0 < t) :
    HasSum (fun n : ℤ ↦ rexp (-π * (n + a) ^ 2 * t)) (evenKernel a t) :=
  by
  rw [← hasSum_ofReal, evenKernel_def]
  have (n : ℤ) : cexp (-(π * (n + a) ^ 2 * t)) = cexp (-(π * a ^ 2 * t)) * jacobiTheta₂_term n (a * I * t) (I * t) :=
    by
    rw [jacobiTheta₂_term, ← Complex.exp_add]
    ring_nf
    simp
  simpa [this] using (hasSum_jacobiTheta₂_term _ (by simpa)).mul_left _

Похожие утверждения