oddKernel_def — Mathlib

English

The complex value of the odd kernel equals jacobiTheta₂'' with the real part and appropriate combination of gamma and exponent factors, i.e., Complex.ofReal(oddKernel(a) x) equals a product involving jacobiTheta₂'' and cosZeta.

Русский

Комплексное значение нечетного ядра равно jacobiTheta₂'' с необходимыми множителями гамма-функции и экспоненциальной части; эквивалентно произведению, связывающему jacobiTheta₂'' и cosZeta.

LaTeX

$$$$\\text{oddKernel}(a,x) = i\\cdot\\text{(сложное выражение через jacobiTheta₂'' и cosZeta)}.$$$$

Lean4

theorem oddKernel_def (a x : ℝ) : ↑(oddKernel a x) = jacobiTheta₂'' a (I * x) := by
  simp [oddKernel, ← conj_eq_iff_re, jacobiTheta₂''_conj]

Похожие утверждения