completedHurwitzZetaEven_one_sub — Mathlib

English

Functional equation in the 1−s form: completedHurwitzZetaEven(a, 1−s) equals completedCosZeta(a, s).

Русский

Функциональное уравнение в форме 1−s: completedHurwitzZetaEven(a, 1−s) = completedCosZeta(a, s).

LaTeX

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

Lean4

/-- Functional equation for the even Hurwitz zeta function. -/
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]

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