completedSinZeta_neg — Mathlib

English

For a real a and t>0, sinKernel(a,t) equals the sum ∑_{n∈ℤ} (-i n) e^{2π i a n} e^{-π n^2 t}.

Русский

Для действительного a и t>0 sinKernel(a,t) равно сумме ∑_{n∈ℤ} (-i n) e^{2π i a n} e^{-π n^2 t}.

LaTeX

$$$$ \sinKernel(a,t) = \sum_{n\in \mathbb{Z}} (-i\,n) e^{2\pi i a n} e^{-\pi n^{2} t}, \quad t>0. $$$$

Lean4

theorem completedSinZeta_neg (a : UnitAddCircle) (s : ℂ) : completedSinZeta (-a) s = -completedSinZeta a s := by
  simp [completedSinZeta, StrongFEPair.Λ, mellin, StrongFEPair.symm, WeakFEPair.symm, hurwitzOddFEPair, sinKernel_neg,
    integral_neg, neg_div]

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