completedHurwitzZetaOdd_one_sub — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Functional equation for the odd Hurwitz zeta function. -/
theorem completedHurwitzZetaOdd_one_sub (a : UnitAddCircle) (s : ℂ) :
    completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s := by
  rw [completedHurwitzZetaOdd, completedSinZeta,
    (by { push_cast; ring
    } : (1 - s + 1) / 2 = ↑(3 / 2 : ℝ) - (s + 1) / 2),
    ← hurwitzOddFEPair_k, (hurwitzOddFEPair a).functional_equation ((s + 1) / 2), hurwitzOddFEPair_ε, one_smul]

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