English
The Dirichlet series representation of sinZeta(a, s) can be written as an absolutely convergent sum over n ∈ ℤ: sinZeta(a, s) = ∑_{n∈ℤ} (-i) sign(n) e^{2π i a n} / (|n|^s) / 2, valid for Re(s) > 1.
Русский
Дирихле-ряд для sinZeta(a, s) может быть записан как абсолютно сходящийся сумминг по n∈ℤ: sinZeta(a,s) = ∑_{n∈ℤ} (-i) sign(n) e^{2π i a n} / |n|^s / 2, при Re(s) > 1.
LaTeX
$$$$ \sinZeta(a,s) = \frac{-i}{2} \sum_{n\in\mathbb{Z}} \frac{\operatorname{sign}(n) e^{2\pi i a n}}{|n|^{s}}, \quad \Re(s)>1. $$$$
Lean4
/-- Formula for `sinZeta` as a Dirichlet series in the convergence range, with sum over `ℤ`. -/
theorem hasSum_int_sinZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℤ ↦ -I * n.sign * cexp (2 * π * I * a * n) / ↑|n| ^ s / 2) (sinZeta a s) :=
by
rw [sinZeta]
refine ((hasSum_int_completedSinZeta a hs).div_const (Gammaℝ (s + 1))).congr_fun fun n ↦ ?_
have : 0 < re (s + 1) := by rw [add_re, one_re]; positivity
simp only [mul_assoc, div_right_comm _ _ (Gammaℝ _), mul_div_cancel_left₀ _ (Gammaℝ_ne_zero_of_re_pos this)]
