English
Let a be an element of the unit circle modulo 1 and s be a complex variable. The sine zeta function sinZeta(a, s) is defined by sinZeta(a, s) = completedSinZeta(a, s) / Gamma(s + 1). It is a meromorphic function of s which, in the half-plane Re(s) > 1, coincides with the Dirichlet series sum over n ≥ 1 of sin(2π a n) / n^s.
Русский
Пусть a принадлежит единичному кругу по модулю и s — комплексная переменная. Векторная функция синуса-дзета sinZeta(a, s) задаётся формулой sinZeta(a, s) = completedSinZeta(a, s) / Γ(s + 1). Это мероморфная функция по переменной s, которая в полуплоскости Re(s) > 1 совпадает с Дирихле-серией ∑_{n≥1} sin(2π a n) / n^s.
LaTeX
$$$$ \sinZeta(a,s) = \frac{\mathrm{completedSinZeta}(a,s)}{\Gamma(s+1)} $$$$
Lean4
/-- The sine zeta function, i.e. the meromorphic function of `s` which agrees
with `∑' (n : ℕ), sin (2 * π * a * n) / n ^ s` for `1 < re s`. -/
noncomputable def sinZeta (a : UnitAddCircle) (s : ℂ) :=
completedSinZeta a s / Gammaℝ (s + 1)
