English
For real a and x > 0, the series ∑_{n∈ℤ} (n+a) e^{-π (n+a)^2 x} converges to oddKernel(a) x.
Русский
Для действительного a и x > 0 сумма по целым n: (n+a) e^{-π (n+a)^2 x} сходится к oddKernel(a) x.
LaTeX
$$$$ \text{If } x>0:\quad \sum_{n\in \mathbb{Z}} (n+a) e^{-\pi (n+a)^2 x} = \operatorname{oddKernel}(a) \; x. $$$$
Lean4
theorem hasSum_int_oddKernel (a : ℝ) {x : ℝ} (hx : 0 < x) :
HasSum (fun n : ℤ ↦ (n + a) * rexp (-π * (n + a) ^ 2 * x)) (oddKernel (↑a) x) :=
by
rw [← hasSum_ofReal, oddKernel_def' a x]
have h1 := hasSum_jacobiTheta₂_term (a * I * x) (by rwa [I_mul_im, ofReal_re])
have h2 := hasSum_jacobiTheta₂'_term (a * I * x) (by rwa [I_mul_im, ofReal_re])
refine (((h2.div_const (2 * π * I)).add (h1.mul_left ↑a)).mul_left (cexp (-π * a ^ 2 * x))).congr_fun (fun n ↦ ?_)
rw [jacobiTheta₂'_term, mul_assoc (2 * π * I), mul_div_cancel_left₀ _ two_pi_I_ne_zero, ← add_mul, mul_left_comm,
jacobiTheta₂_term, ← Complex.exp_add]
push_cast
simp only [← mul_assoc, ← add_mul]
congrm _ * cexp (?_ * x)
simp only [mul_right_comm _ I, add_mul, mul_assoc _ I, I_mul_I]
ring_nf
