English
An explicit form of the odd kernel in terms of exp, pi, and Jacobi theta functions: The complex value of oddKernel equals exp(-π a^2 x) times a bracket containing Jacobi theta prime and theta functions times gamma and cos terms.
Русский
Явное выражение для нечетного ядра через экспоненту, π и функции JacobiTheta: комплексное значение oddKernel содержит exp(-π a^2 x) и скобку сJacobi theta-ами, гаммой и косинусами.
LaTeX
$$$$\\text{oddKernel}(a,x) = e^{-\\pi a^2 x}\\left( \\frac{\\mathrm{jacobiTheta_2'}(a i x)}{2\\pi i} + a\\mathrm{jacobiTheta_2}(a i x) \\right) \\mathrm{jacobiTheta_2''}(a i x).$$$$
Lean4
theorem oddKernel_def' (a x : ℝ) :
↑(oddKernel (↑a) x) =
cexp (-π * a ^ 2 * x) *
(jacobiTheta₂' (a * I * x) (I * x) / (2 * π * I) + a * jacobiTheta₂ (a * I * x) (I * x)) :=
by
rw [oddKernel_def, jacobiTheta₂'', ← mul_assoc (↑a) I x,
(by ring : ↑π * I * ↑a ^ 2 * (I * ↑x) = I ^ 2 * ↑π * ↑a ^ 2 * x), I_sq, neg_one_mul]
