English
For s not a nonpositive integer, sinZeta(a, 1 − s) is a fixed multiple of sinZeta and hurwitzZetaOdd(a, s) as given by the formula in the preceding theorem.
Русский
Для s, не принадлежащего −ℕ, sinZeta(a,1−s) выражается через множитель, умножающий sinZeta и hurwitzZetaOdd(a,s) согласно формуле.
LaTeX
$$$$ \sinZeta(a,1-s) = 2 (2\pi)^{-s} \Gamma(s) \sin(\pi s/2) \mathrm{hurwitzZetaOdd}(a,s). $$$$
Lean4
/-- If `s` is not in `-ℕ`, then `sinZeta a (1 - s)` is an explicit multiple of
`hurwitzZetaOdd s`. -/
theorem sinZeta_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -n) :
sinZeta a (1 - s) = 2 * (2 * π) ^ (-s) * Gamma s * sin (π * s / 2) * hurwitzZetaOdd a s := by
rw [← Gammaℂ, sinZeta, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv, inv_Gammaℝ_two_sub hs, completedSinZeta_one_sub,
hurwitzZetaOdd, ← div_eq_mul_inv, ← mul_div_assoc, ← mul_div_assoc, mul_comm]
