English
For a real a and t > 0, sinKernel(a, t) equals the sum ∑_{n∈ℤ} (-i n) e^{2π i a n} e^{-π n^2 t}.
Русский
Для действительного a и t > 0 синKernel(a, t) равен сумме ∑_{n∈ℤ} (-i n) e^{2π i a n} e^{-π n^2 t}.
LaTeX
$$$$ \sinKernel(a,t) = \sum_{n\in \mathbb{Z}} (-i\,n)\, e^{2\pi i a n}\, e^{-\pi n^2 t}, \quad t>0. $$$$
Lean4
theorem hasSum_int_sinKernel (a : ℝ) {t : ℝ} (ht : 0 < t) :
HasSum (fun n : ℤ ↦ -I * n * cexp (2 * π * I * a * n) * rexp (-π * n ^ 2 * t)) ↑(sinKernel a t) :=
by
have h : -2 * (π : ℂ) ≠ (0 : ℂ) := by
simp only [neg_mul, ne_eq, neg_eq_zero, mul_eq_zero, OfNat.ofNat_ne_zero, ofReal_eq_zero, pi_ne_zero, or_self,
not_false_eq_true]
rw [sinKernel_def]
refine ((hasSum_jacobiTheta₂'_term a (by rwa [I_mul_im, ofReal_re])).div_const _).congr_fun fun n ↦ ?_
rw [jacobiTheta₂'_term, jacobiTheta₂_term, ofReal_exp, mul_assoc (-I * n), ← Complex.exp_add, eq_div_iff h,
ofReal_mul, ofReal_mul, ofReal_pow, ofReal_neg, ofReal_intCast, mul_comm _ (-2 * π : ℂ), ← mul_assoc]
congrm ?_ * cexp (?_ + ?_)
· simp [mul_assoc]
· exact mul_right_comm (2 * π * I) a n
· simp [← mul_assoc, mul_comm _ I]
