English
For a ∈ ℝ and s with Re(s) > 1, sinZeta(a, s) = ∑_{n=1}^∞ sin(2π a n) / n^s, i.e. sinZeta is given by the Dirichlet series with coefficients sin(2π a n).
Русский
Для a∈ℝ и Re(s)>1, sinZeta(a,s) равна ∑_{n=1}^∞ sin(2π a n)/n^s; синус-зета задаётся как Дирихле-ряд с коэффициентами sin(2π a n).
LaTeX
$$$$ \sinZeta(a,s) = \sum_{n=1}^{\infty} \frac{\sin(2\pi a n)}{n^{s}}. $$$$
Lean4
/-- Formula for `sinZeta` as a Dirichlet series in the convergence range, with sum over `ℕ`. -/
theorem hasSum_nat_sinZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℕ ↦ Real.sin (2 * π * a * n) / (n : ℂ) ^ s) (sinZeta a s) :=
by
have := (hasSum_int_sinZeta a hs).nat_add_neg
simp_rw [abs_neg, Int.sign_neg, Int.cast_neg, Nat.abs_cast, Int.cast_natCast, mul_neg, abs_zero, Int.cast_zero,
zero_cpow (ne_zero_of_one_lt_re hs), div_zero, zero_div, add_zero] at this
simp_rw [push_cast, Complex.sin]
refine this.congr_fun fun n ↦ ?_
rcases ne_or_eq n 0 with h | rfl
· simp only [neg_mul, sub_mul, div_right_comm _ (2 : ℂ), Int.sign_natCast_of_ne_zero h, Int.cast_one, mul_one,
mul_comm I, neg_neg, ← add_div, ← sub_eq_neg_add]
congr 5 <;> ring
· simp
