English
For a ∈ ℝ and s with Re(s) > 1, the Dirichlet series ∑_{n∈ℤ} sign(n+a) / |n+a|^s divided by 2 converges to hurwitzZetaOdd(a,s); i.e., HasSum (fun n:ℤ => sign(n+a)/|n+a|^s / 2) (hurwitzZetaOdd a s).
Русский
Для a ∈ ℝ и s с Re(s) > 1 ряд ∑_{n∈ℤ} sign(n+a)/|n+a|^s, взятый с коэффициентом 1/2, сходится к hurwitzZetaOdd(a,s).
LaTeX
$$$$ \text{HasSum}_{n\in\mathbb{Z}} \frac{\operatorname{sign}(n+a)}{|n+a|^{s}} \cdot \frac{1}{2} = \mathrm{hurwitzZetaOdd}(a,s), \quad \Re(s)>1.$$$$
Lean4
/-- Formula for `hurwitzZetaOdd` as a Dirichlet series in the convergence range (sum over `ℤ`). -/
theorem hasSum_int_hurwitzZetaOdd (a : ℝ) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℤ ↦ SignType.sign (n + a) / (↑|n + a| : ℂ) ^ s / 2) (hurwitzZetaOdd a s) :=
by
refine ((hasSum_int_completedHurwitzZetaOdd a hs).div_const (Gammaℝ _)).congr_fun fun n ↦ ?_
have : 0 < re (s + 1) := by rw [add_re, one_re]; positivity
simp [div_right_comm _ _ (Gammaℝ _), mul_div_cancel_left₀ _ (Gammaℝ_ne_zero_of_re_pos this)]
