completedCosZeta₀_one_sub — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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