English
For a real a and t>0, sinKernel(a, t) equals the sum ∑_{n∈ℕ} 2 n sin(2π a n) e^{-π n^2 t}.
Русский
Для действительного a и t>0 sinKernel(a, t) равно сумме ∑_{n≥0} 2 n sin(2π a n) e^{-π n^2 t}.
LaTeX
$$$$ \sinKernel(a,t) = \sum_{n\in \mathbb{N}} 2 n \sin(2\pi a n) e^{-\pi n^{2} t}, \quad t>0. $$$$
Lean4
theorem hasSum_nat_sinKernel (a : ℝ) {t : ℝ} (ht : 0 < t) :
HasSum (fun n : ℕ ↦ 2 * n * Real.sin (2 * π * a * n) * rexp (-π * n ^ 2 * t)) (sinKernel (↑a) t) :=
by
rw [← hasSum_ofReal]
have := (hasSum_int_sinKernel a ht).nat_add_neg
simp only [Int.cast_zero, zero_mul, mul_zero, add_zero] at this
refine this.congr_fun fun n ↦ ?_
simp_rw [Int.cast_neg, neg_sq, mul_neg, ofReal_mul, Int.cast_natCast, ofReal_natCast, ofReal_ofNat, ← add_mul,
ofReal_sin, Complex.sin]
push_cast
congr 1
rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self two_ne_zero, one_mul, neg_mul, neg_mul,
neg_neg, mul_comm _ I, ← mul_assoc, mul_comm _ I, neg_mul, ← sub_eq_neg_add, mul_sub]
congr 3 <;> ring
