completedCosZeta_one_sub — Mathlib

English

Alternative form of the functional equation: completedCosZeta(a, 1 - s) equals completedHurwitzZetaEven(a, s).

Русский

Альтернативная форма функционального уравнения: completedCosZeta(a, 1 - s) = completedHurwitzZetaEven(a, s).

LaTeX

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

Lean4

/-- Functional equation for the even Hurwitz zeta function (alternative form). -/
theorem completedCosZeta_one_sub (a : UnitAddCircle) (s : ℂ) :
    completedCosZeta a (1 - s) = completedHurwitzZetaEven a s := by
  rw [← completedHurwitzZetaEven_one_sub, sub_sub_cancel]

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