English
The odd Hurwitz zeta kernel is defined as the 1-periodic lift of the function a ↦ re(jacobiTheta₂''(a, i x)).
Русский
Необходимое ядро для разложения по нечётной части zeta-функции Хурвица образуется как периодический «вылет» функции a ↦ Re(jacobiTheta₂''(a, i x)).
LaTeX
$$$$\\text{oddKernel}(a,x) = \\big(\\mathrm{Re}(\\mathrm{jacobiTheta_2''}(a, i x))\\big)^{\\text{periodic lift to }a\\text{ with period }1}. $$$$
Lean4
/-- Odd Hurwitz zeta kernel (function whose Mellin transform will be the odd part of the completed
Hurwitz zeta function). See `oddKernel_def` for the defining formula, and `hasSum_int_oddKernel`
for an expression as a sum over `ℤ`.
-/
@[irreducible]
def oddKernel (a : UnitAddCircle) (x : ℝ) : ℝ :=
(show Function.Periodic (fun a : ℝ ↦ re (jacobiTheta₂'' a (I * x))) 1 by simp [jacobiTheta₂''_add_left]).lift a
