English
Negating a leaves completedHurwitzZetaEven₀ invariant: completedHurwitzZetaEven₀(−a, s) = completedHurwitzZetaEven₀(a, s).
Русский
Отрицание a не изменяет CompletedHurwitzZetaEven₀: completedHurwitzZetaEven₀(−a, s) = completedHurwitzZetaEven₀(a, s).
LaTeX
$$$$ \\operatorname{completedHurwitzZetaEven}_0(-a, s) = \\operatorname{completedHurwitzZetaEven}_0(a, s). $$$$
Lean4
theorem completedCosZeta_eq (a : UnitAddCircle) (s : ℂ) :
completedCosZeta a s = completedCosZeta₀ a s - 1 / s - (if a = 0 then 1 else 0) / (1 - s) :=
by
rw [completedCosZeta, WeakFEPair.Λ, sub_div, sub_div]
congr 1
·
rw [completedCosZeta₀, WeakFEPair.symm, hurwitzEvenFEPair, smul_eq_mul, mul_one, div_div,
div_mul_cancel₀ _ (two_ne_zero' ℂ)]
·
simp_rw [WeakFEPair.symm, hurwitzEvenFEPair, push_cast, inv_one, smul_eq_mul, mul_comm _ (if _ then _ else _),
mul_div_assoc, div_div, ← sub_div, div_mul_cancel₀ _ (two_ne_zero' ℂ), mul_one_div]
