English
For s not of the form 1−n, cosZeta(a)(1−s) equals 2 (2π)^{−s} Γ(s) cos(π s/2) cosZeta(a)(s).
Русский
Если s не имеет вида 1−n, то cosZeta(a)(1−s) = 2 (2π)^{−s} Γ(s) cos(π s/2) cosZeta(a)(s).
LaTeX
$$$$\\cosZeta(a)(1-s) = 2\\cdot (2\\pi)^{-s} \\Gamma(s) \\cos\\left(\\frac{\\pi s}{2}\\right) \\cosZeta(a)(s), \\quad \\forall s\\ \\text{not of form } 1-n.$$$$
Lean4
/-- Auxiliary function appearing in the functional equation for the odd Hurwitz zeta kernel, equal
to `∑ (n : ℕ), 2 * n * sin (2 * π * n * a) * exp (-π * n ^ 2 * x)`. See `hasSum_nat_sinKernel`
for the defining sum. -/
@[irreducible]
def sinKernel (a : UnitAddCircle) (x : ℝ) : ℝ :=
(show Function.Periodic (fun ξ : ℝ ↦ re (jacobiTheta₂' ξ (I * x) / (-2 * π))) 1 by simp [jacobiTheta₂'_add_left]).lift
a
