English
The odd part of the Hurwitz zeta function is defined as the quotient of the completed odd part by Gamma(s+1).
Русский
Нечетную часть Хёрвитц ζ-функции определяют как отношение завершенной нечетной части к Γ(s+1).
LaTeX
$$$$ \text{hurwitzZetaOdd}(a,s) = \frac{\operatorname{completedHurwitzZetaOdd}(a,s)}{\Gamma(s+1)}. $$$$
Lean4
/-- Formula for `completedSinZeta` as a Dirichlet series in the convergence range
(second version, with sum over `ℕ`). -/
theorem hasSum_nat_completedSinZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) :
HasSum (fun n : ℕ ↦ Gammaℝ (s + 1) * Real.sin (2 * π * a * n) / (n : ℂ) ^ s) (completedSinZeta a s) :=
by
have := (hasSum_int_completedSinZeta a hs).nat_add_neg
simp_rw [Int.sign_zero, Int.cast_zero, mul_zero, zero_mul, zero_div, add_zero, abs_neg, Int.sign_neg, Nat.abs_cast,
Int.cast_neg, Int.cast_natCast, ← add_div] at this
refine this.congr_fun fun n ↦ ?_
rw [div_right_comm]
rcases eq_or_ne n 0 with rfl | h
· simp
simp_rw [Int.sign_natCast_of_ne_zero h, Int.cast_one, ofReal_sin, Complex.sin]
simp only [← mul_div_assoc, push_cast, mul_assoc (Gammaℝ _), ← mul_add]
congr 3
rw [mul_one, mul_neg_one, neg_neg, neg_mul I, ← sub_eq_neg_add, ← mul_sub, mul_comm, mul_neg, neg_mul]
congr 3 <;> ring
