completedHurwitzZetaEven₀_one_sub

English

Pole-removed form: completedHurwitzZetaEven₀(a, 1 − s) equals completedCosZeta₀(a, s).

Русский

Форма без полюсов: completedHurwitzZetaEven₀(a, 1 − s) = completedCosZeta₀(a, s).

LaTeX

$$$$ \\operatorname{completedHurwitzZetaEven}_0(a, 1-s) = \\operatorname{completedCosZeta}_0(a,s). $$$$

Lean4

/-- Functional equation for the even Hurwitz zeta function with poles removed. -/
theorem completedHurwitzZetaEven₀_one_sub (a : UnitAddCircle) (s : ℂ) :
    completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s := by
  rw [completedHurwitzZetaEven₀, completedCosZeta₀, sub_div, (by simp : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
    (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k), (hurwitzEvenFEPair a).functional_equation₀ (s / 2),
    (by rfl : (hurwitzEvenFEPair a).ε = 1), one_smul]

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