English
For a ∈ ℝ and s with Re(s) > 1, the Dirichlet series over n ∈ ℕ without absolute values represents sinZeta(a,s): HasSum (fun n : ℕ ↦ (sign(n+a)/|n+a|^s − sign(n+1−a)/|n+1−a|^s)/2) (hurwitzZetaOdd a s).
Русский
Для a∈ℝ и Re(s)>1 ряд над n∈ℕ без модуля задаёт sinZeta(a,s) через hurwitzZetaOdd.
LaTeX
$$$$ \text{HasSum}_{n\ge 0} \frac{1}{2}\left( \frac{\operatorname{sign}(n+a)}{|n+a|^{s}} - \frac{\operatorname{sign}(n+1-a)}{|n+1-a|^{s}} \right) = \mathrm{hurwitzZetaOdd}(a,s), \Re(s)>1.$$$$
Lean4
/-- Formula for `hurwitzZetaOdd` as a Dirichlet series in the convergence range, with sum over `ℕ`
(version without absolute values, assuming `a ∈ Icc 0 1`) -/
theorem hasSum_nat_hurwitzZetaOdd_of_mem_Icc {a : ℝ} (ha : a ∈ Icc 0 1) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℕ ↦ (1 / (n + a : ℂ) ^ s - 1 / (n + 1 - a : ℂ) ^ s) / 2) (hurwitzZetaOdd a s) :=
by
refine (hasSum_nat_hurwitzZetaOdd a hs).congr_fun fun n ↦ ?_
suffices ∀ b : ℝ, 0 ≤ b → SignType.sign (n + b) / (↑|n + b| : ℂ) ^ s = 1 / (n + b) ^ s by
simp only [add_sub_assoc, this a ha.1, this (1 - a) (sub_nonneg.mpr ha.2), push_cast]
intro b hb
rw [abs_of_nonneg (by positivity), (by simp : (n : ℂ) + b = ↑(n + b))]
rcases lt_or_eq_of_le (by positivity : 0 ≤ n + b) with hb | hb
· simp [sign_pos hb]
· rw [← hb, ofReal_zero, zero_cpow ((not_lt.mpr zero_le_one) ∘ (zero_re ▸ · ▸ hs)), div_zero, div_zero]
