English
For a ∈ ℝ and s with Re(s) > 1, the Dirichlet series over n ∈ ℕ given by (sign(n+a)/|n+a|^s − sign(n+1−a)/|n+1−a|^s)/2 sums to hurwitzZetaOdd(a,s).
Русский
Для a ∈ ℝ и Re(s) > 1 ряд над n∈ℕ: (sign(n+a)/|n+a|^s − sign(n+1−a)/|n+1−a|^s)/2 сходится к hurwitzZetaOdd(a,s).
LaTeX
$$$$ \text{HasSum}_{n\ge 0} \frac{\operatorname{sign}(n+a)}{|n+a|^{s}} - \frac{\operatorname{sign}(n+1-a)}{|n+1-a|^{s}}}{2} = \mathrm{hurwitzZetaOdd}(a,s), \quad \Re(s)>1.$$$$
Lean4
/-- Formula for `hurwitzZetaOdd` as a Dirichlet series in the convergence range, with sum over `ℕ`
(version with absolute values) -/
theorem hasSum_nat_hurwitzZetaOdd (a : ℝ) {s : ℂ} (hs : 1 < re s) :
HasSum
(fun n : ℕ ↦
(SignType.sign (n + a) / (↑|n + a| : ℂ) ^ s - SignType.sign (n + 1 - a) / (↑|n + 1 - a| : ℂ) ^ s) / 2)
(hurwitzZetaOdd a s) :=
by
refine (hasSum_int_hurwitzZetaOdd a hs).nat_add_neg_add_one.congr_fun fun n ↦ ?_
rw [Int.cast_neg, Int.cast_add, Int.cast_one, sub_div, sub_eq_add_neg, Int.cast_natCast]
have : -(n + 1) + a = -(n + 1 - a) := by ring_nf
rw [this, Left.sign_neg, abs_neg, SignType.coe_neg, neg_div, neg_div]
