English
If s is not a nonpositive integer, then hurwitzZetaOdd(a, 1 − s) equals 2 (2π)^(−s) Γ(s) sin(π s/2) sinZeta(a,s).
Русский
Если s не принадлежит −ℕ, то hurwitzZetaOdd(a,1−s) = 2 (2π)^(−s) Γ(s) sin(π s/2) sinZeta(a,s).
LaTeX
$$$$ \mathrm{hurwitzZetaOdd}(a,1-s) = 2 \,(2\pi)^{-s} \Gamma(s) \sin\left(\frac{\pi s}{2}\right) \sinZeta(a,s). $$$$
Lean4
/-- If `s` is not in `-ℕ`, then `hurwitzZetaOdd a (1 - s)` is an explicit multiple of
`sinZeta s`. -/
theorem hurwitzZetaOdd_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -n) :
hurwitzZetaOdd a (1 - s) = 2 * (2 * π) ^ (-s) * Gamma s * sin (π * s / 2) * sinZeta a s := by
rw [← Gammaℂ, hurwitzZetaOdd, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv, inv_Gammaℝ_two_sub hs,
completedHurwitzZetaOdd_one_sub, sinZeta, ← div_eq_mul_inv, ← mul_div_assoc, ← mul_div_assoc, mul_comm]
