English
For any a ∈ UnitAddCircle, the function x ↦ cosKernel(a) is continuous on (0, ∞).
Русский
Для любого a ∈ UnitAddCircle функция x ↦ cosKernel(a, x) непрерывна на (0, ∞).
LaTeX
$$$$\\text{ContinuousOn}(\\lambda x. \\cosKernel(a,x), (0,\\infty)).$$$$
Lean4
/-- Even Hurwitz zeta kernel (function whose Mellin transform will be the even part of the
completed Hurwitz zeta function). See `evenKernel_def` for the defining formula, and
`hasSum_int_evenKernel` for an expression as a sum over `ℤ`. -/
@[irreducible]
def evenKernel (a : UnitAddCircle) (x : ℝ) : ℝ :=
(show Function.Periodic (fun ξ : ℝ ↦ rexp (-π * ξ ^ 2 * x) * re (jacobiTheta₂ (ξ * I * x) (I * x))) 1
by
intro ξ
simp only [ofReal_add, ofReal_one, add_mul, one_mul, jacobiTheta₂_add_left']
have : cexp (-↑π * I * ((I * ↑x) + 2 * (↑ξ * I * ↑x))) = rexp (π * (x + 2 * ξ * x)) :=
by
ring_nf
simp [I_sq]
rw [this, re_ofReal_mul, ← mul_assoc, ← Real.exp_add]
congr
ring).lift
a
