English
CompletedHurwitzZetaEven equals CompletedHurwitzZetaEven₀ minus a linear combination of 1/s and 1/(1-s); the two representations are related by simple algebraic identities.
Русский
CompletedHurwitzZetaEven равна CompletedHurwitzZetaEven₀ минус линейная комбинация 1/s и 1/(1-s); две формы эквивалентны через простые алгебраические преобразования.
LaTeX
$$$$ \\operatorname{completedHurwitzZetaEven}(a,s) = \\operatorname{completedHurwitzZetaEven}_0(a,s) - \\frac{(a=0)}{s} - \\frac{1}{1-s}. $$$$
Lean4
theorem completedHurwitzZetaEven_eq (a : UnitAddCircle) (s : ℂ) :
completedHurwitzZetaEven a s = completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s) :=
by
rw [completedHurwitzZetaEven, WeakFEPair.Λ, sub_div, sub_div]
congr 1
· change
completedHurwitzZetaEven₀ a s - (1 / (s / 2)) • (if a = 0 then 1 else 0) / 2 =
completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
rw [smul_eq_mul, mul_comm, mul_div_assoc, div_div, div_mul_cancel₀ _ two_ne_zero, mul_one_div]
· change (1 / (↑(1 / 2 : ℝ) - s / 2)) • 1 / 2 = 1 / (1 - s)
push_cast
rw [smul_eq_mul, mul_one, ← sub_div, div_div, div_mul_cancel₀ _ two_ne_zero]
